============ WELCOME IN METAMORPHO ============
This file contains detailed instructions for installing and using the Metamorpho
system (currently, only the Anamorpho part of it is publicly available).
=== SUMMARY of this file
------ What the System can do
------ Installation
------ Using the System
------ Experimenting with the System
------ System functionalities in detail
------------------------------------------------------------------------------
=== WHAT THE SYSTEM CAN DO
The system is able to recognize: (1) sentences and expressions of map calculus,
(2) definitions which extend its language, (3) axioms and inference rules that form
theories based on the map calculus, and (4) schemes which represent collections of
map sentences or map expressions within which metavariables may occur in place of
map expressions. To be accepted as belonging to any of these classes, a string
is first parsed by Prolog, then subjected to a syntactic filter, and in some
cases also subjected to suitable static semantic checks.
Powerful definition mechanism for enhancing the expressive power of the basic
language of map calculus are available and are implemented in the system.
Dialects of map calculus, as well as formalisms whose general features
are akin to those of map calculus, can be treated too.
For a description see the paper metamorpho.ps
The system also has a pretty-print component which translates into LaTeX
map expressions, sentences, definitions, and axioms.
------------------------------------------------------------------------------
=== INSTALLATION
Uncompress the file metamorpho.zip, metamorpho.gz, or metamorpho.tar
Download SWI-Prolog from URL http://www.swi.psy.uva.nl/projects/SWI-Prolog/
(this is a free Prolog system).
During installation, select the extension .swi for Prolog files
(alternatively, modify the extension of the file VIA.swi to, e.g., VIA.pl or
VIA.pro)
Now the system is ready to be used.
Files in this directory:
VIA.swi Main program, for starting the system
.pro Prolog programs
.txt Text files (documentation; macros.txt which consists of LaTeX macros)
(no extension) data for Prolog programs
.tex LaTeX files. They are generated by the system: hence they can be deleted
------------------------------------------------------------------------------
=== USING THE SYSTEM
A run of the metamorpho system is started by double-clicking on the icon
VIA.swi
The system will prompt some questions. To each of them you can answer '_'
(underscore) to get the default value.
Don't forget to end your answer with '.' (a dot, which is required from Prolog i/o).
1. --- Names and number of map letters
What initial letter will you use for the map letters? (Default _=p)
Question:
How many map letters do you want? (Default _=infinitely many)
If for instance you answer 'a' and '100', you get the map letters a1..a100.
2. --- Primitive and derived constructors of map expressions
Question:
What endowment of constructs do you want? (Default _=[defAs0A])
Here the systems wants to know the notation for basic map operators.
The default provides you with some basic operators, among which the following:
id, % diagonal map
1 % top
0 % bottom:
rev(P) % converse of map P
int(P,Q) % Boolean meet
symm(P,Q) % Boolean symmetric difference
circ(P,Q) % Peircean composition
setminus(P,Q) % map difference
some of which are takes as primitive, while others are taken as derived (i.e.,
secondary), constructs. It is understood that equality, equiv(P,Q), is
always available, whether the default is adopted or an alternative choice is
made.
3. --- Logical Axioms
Question:
Which endowment of logical axioms do you choose? (Default _=[logicalA])
The default will provide you with the basic axioms for the above operators. i.e.
commutativity and associativity of int, symm and circ, trivial properties of circ,
convolutory laws and Schroeder's cycle law involving rev, int and circ.
Otherwise, you can load your set of logical axioms, say LAx, by writing "[LAx]."
There are several example files that you can try, listed and commented below.
4. --- Proper axioms
Question:
Which proper axioms do you want to install? (Default _=[])_.
Here the defult is the empty set.
Otherwise, you can load your set of proper axioms, say PAx, by writing "[PAx]."
You can also load several files of logic axioms at once, say by writing
"[Pax1,Pax2,...,Pax9]."
There are several example files that you can try, listed and commented below:
to show the flexibility of the system, such examples do not all belong to
map calculus (e.g., defStar and regular relate to regular expressions for the
specification of lexical languages).
5. At this point, a parser for map language is available that will try to
recognize formulas according to the axioms you have provided.
Precisely:
mapeq/1,2,3 -- parser of map formulas
mapxpr/1,2,3 -- parser of map expressions
Examples of use:
?- mapeq(in circ in). % this is neither an equation
no %
?- mapxpr(in circ in,[]). % nor it is acceptable in the empty context
no
?- mapxpr(in circ in,[ax_sets]). % this is an expression of set theory
yes
?- mapeq(in circ in equiv 0,[ax_sets]). % this is an equation of set theory
yes
?- mapxpr(in circ in equiv 0,[ax_sets]). % an equation is not an expression
no
?- mapeq(in circ in equiv z,[ax_sets], V). % this is an equation of set theory
V = p1 circ p1 equiv 0 % this is its translation into basic endowment
6. You can dump the axioms of the overall theory you have specified by invoking:
printlaws/0,1,2 -- writes all axioms on a given file
Invocation:
-- printlaws(ThName,OuFile)
-- printlaws(ThName) (output: file user),
-- printlaws (input: underlying calculus; output: file user)
printtheories
-- prints the list of all the theories that have been loaded
7. A LaTeX pretty-printer is available:
prettyecho/1 -- translates a file of map formulas/expression into a LaTeX file;
takes as input the name of the file.
--------------------------------------------------------------------------
=== EXPERIMENTING WITH THE SYSTEM
The package you have unzipped contains several files with different versions and sample
applications of map calculus, listed and commented below.
--- Files which define language constructs:
defAs0A -- basic map operators (choice n.1)
defAs0B -- basic map operators (choice n.2)
defAs0C -- basic map operators (choice n.3)
defStar -- basic operators for regular expressions (choice n.4)
defAs1 -- other map constructs (series n. 1):
-- non-primitive although fundamental operators
-- (some of them variadic like union, intersection, list product)
defFoAs0 -- other map constructs (series n. 2):
-- some trivial though fundamental alternative syntax forms for equalities
defFoAs1 -- other map constructs (series n. 3):
-- some propositional connectives, monadic dyadic and variadic
defProps -- characterization of some very common properties of maps
defGraphIsom -- characterization of isomorphism between two graphs
defProj -- tuples, and (quasi-)projections operating on tuples
defAttrs -- formalization of E-R model in map calculus:
characterization of entities, attributes, keys, placeholders, etc.
defInd -- definition of some basic theories, and of induction
defALL -- the union of all the above definitions
defPlH -- E-R model: a better definition of placeholder
--- Files which contain logical axioms:
logicalA -- logical axioms for map calculus to be used in combination with defAs0A
logicalB -- logical axioms for map calculus to be used in combination with defAs0B
logicalC -- Tarski-Givant logical axioms for map calculus to be used in combination with defAs0B
regular -- Salomaa's axioms on regular expressions
--- Files which contain proper axioms for various theories
ax_graphIsom -- axioms concerning a specific graph isomorphism
axGraphIsom -- variant of the axioms on graph isomorphism
ax_tenseLogic -- axioms of the logic of past and future
ax_HdTl -- axioms of conjugated projections in a universe devoid of individuals
ax_sets -- axioms of a weak theory of sets
ax_nats -- some axioms on natural numbers
ax_key -- E-R model: axioms for super-keys
ax_ER -- E-R model: representation of a simple diagram
ax_plh -- axioms on a subdiagonal placeholder within a list of other predicates
ax_nested -- example demonstrating how to include axiom files one inside another
-----------------------------------------------------------------------------
=== SYSTEM FUNCTIONALITIES IN DETAIL
Here we comment all modules composing the Metamorpho system. Some of them can be used
directly by the user (as specified in each case), others are internal utilities.
mapEqualities -- parser of map formulas and expressions
mapEqExpand -- expands well-formed map formulas and expressions
-- the main ways of using this function are:
-- mapeq/1,2 -- accepts map formulas (equalities in various forms)
--
-- mapeq/3 -- accepts and expands map formulas
-- mapeq_meta/1,2 -- accepts schemata denoting map formulas
--
-- mapeq_meta/3 -- accepts and expands schemata denoting map formulas
-- mapEq/3 -- accepts both map formulas and schemata
--
-- mapXpr/3 -- accepts both map expressions and schemata
-- letter/4 -- accepts map letters with underscript
nstallDefs -- installs one or more files of definitions after syntactic check
-- installDefs(Infiles) -- loads form one or more files
-- sameVars/2 -- checks that the two arguments are the same variable
-- varsin/2 -- extracts the list of variables from a formula
-- isDef/2 -- utility for semantic attachment
-- mkObj/2 -- reflection at the object level of a meta-level formula
with variables denoting operators
nstallAxs -- installs or more files of axioms
-- installAxs(Theory,Infiles) -- assigns to each file from the list Infiles
-- a corresponding name from the list Theory
and loads the axioms in the file,
associating each axiom to the
corresponding theory.
Default: theory name = file name
stubDefs -- internal utility managing abbreviations
priorities -- configuration file for prettyecho, defines the priorities of operators
-- and associates with the map constructors their LaTeX counterpart
letter -- utilities of lexical and syntactic analysis
-- accepts letters with underscript (letter/4)
-- computes term size (size/3)
-- finds distinct variables in a term (varsin/2)
-- renames variables in a term (rename/2)
-- checks whether two terms contain the same variables (sameVar/2)
-- generates default names when missing (matchNames/2)