Terms to be manipulated by the prover as representing objects in mathematical theories are entered by the user and displayed by the prover in the MARK2 ``input language''.
The syntax of the input language is very simple. There are two types of tokens. Identifiers are strings of letters, numbers, question marks and underscores. Identifiers which begin with question marks are used as variables; all others are used as constants (when so declared by the user). Operators (used as either infixes or prefixes) are strings of special characters (not including brackets, braces, or parentheses). Those which begin with carets (shift-6) are operator variables; operators which begin with colons are the product of an operator construction to be described below. Operators which a user declares will not begin with colons or carets.
A term is either of the form <identifier>, the form [<term>] (such terms are called ``constant function terms'', for reasons which will become evident), the form (<operator> <term>) (such terms are called ``prefix terms'') or the form (<term> <operator> <term>) (such terms are called ``infix terms'').
It is not necessary to enter all parentheses in the above term forms. The rule followed is the old APL rule; all operators associate to the right as far as possible. Spaces are not significant, except where they are required to separate adjacent operators (only occurs when an infix is followed immediately by a prefix). The prover automatically displays terms with the least possible use of parentheses. Variables do not need to be declared.
The best way to get to know the input language is to enter into dialogue with MARK2. It is first necessary to be aware that all constant identifiers and operators used must be declared. It is also necessary to use declarations to tell the prover that an operator can be used as a prefix.
You should get an error message telling you that an undeclared constant has been used. You should also see two slightly reformatted copies of the term you have entered. The ``start'' command always displays two copies of the term entered, for reasons which will become evident below.
and repeat the ``start'' command from above. MARK2 should no longer complain.
Now try the following three commands:
start "(?x+?y)+?z"; start "?x+(?y+?z)"; start "?x+?y+?z";
Feel free to try more complex terms; explore what is meant by ``associating to the right''. Try including a constant like ``a'' (not beginning with a question mark) and see what MARK2 says. Try putting in numerals like ``0'' or ``12''; you will find that MARK2 will not give us trouble with declarations in this case.
Now we look into prefixes. Enter the command
You will discover that this makes possible the use of ``-'' as both an infix and a prefix operator. Explore this using the ``start'' command. Especially notice the difference between
start "?x+-?y"; (* There is no infix +- *) start "?x+ -?y"; (* The space is necessary *)
The form of the command for declaring constants like ``a'' is
Declare some literal constants and mix them into expressions introduced with the ``start'' command. Try declaring some new infixes and prefixes.
Try outraging the declaration system by declaring constants or operators which have already been declared, or by declaring constant identifiers with special characters, ``constant'' identifiers beginning with question marks, operators with letters in them, and so forth. MARK2 has a large library of error messages :-)
Just for the sake of completeness, we explain the mechanics behind prefixes. A prefix expression is always understood by the system as an abbreviation for an infix expression. Each operator which can be used as a prefix has associated with it a ``default value'' in such a way that the infix term (<default-value1> <infix1> <term1>) (where the appropriate default value depends on the infix) is the intended meaning of the prefix term (<infix1> <term1>) If the former term is entered, the latter term will be displayed. The default value associated with an operator is an error value which will cause MARK2 to complain; the default value associated with infixes declared using ``declareunary'' is defaultprefix (all operators without exception can legally be used as infixes; there is no way to declare an operator which can only be used as a prefix).
The command which associates a given default value with an operator is
declareprefix "<operator>" "<default-value>";
To test out this system, try the following commands:
declareconstant "true"; declareinfix "~"; start "true~?x"; start "~?x''; declareprefix "~" "true"; start "true~?x"; start "~?x";
Try entering terms like ``0-?x'' or complex terms with embedded subterms of that sort.
Save your theory using the command
To start again, use
load "tutorial"; (* in the same directory you were in when you stored it! *)
and it can be saved then using