============ 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)