The purpose of this chapter is fourfold:
The constructors of LUTINS are fixed, but you can define quasiconstructors which effectively serve as additional constructors. Quasiconstructors are desirable for several reasons:
Quasiconstructors are implemented as ``macro/abbreviations.'' For
example, the quasiconstructor quasiequals^{10.1} is defined by the following
biconditional:
When the preparsed string representation of an expression (``preparsed string'' for short) of the form is parsed, is treated as a macro with the list of arguments E_{1},E_{2}: an internal representation of the expression (``internal expression'') is built from the preparsed string as if it had the form . When an internal expression of the form is printed, is used as an abbreviation: the printed string representation of the expression (``printed string'') is generated from the internal expression as if the latter had the form . In other words, in string representation of the expression looks like , an operator applied to a list of two arguments, but it is actually represented internally as .
Abstractly, a quasiconstructor definition consists of three components: a name, a list of schema variables, and a schema. In our example above, quasiequals is the name, E_{1},E_{2} is the list of schema variables, and the righthand side of the biconditional above is the schema. A quasiconstructor is defined by a user with the defquasiconstructor form. The list of schema variables and the schema are represented together by a lambdaexpression which is specified by a string and a name of a language or theory. The variables of the lambdaexpression represent the list of schema variables, and the body of the lambdaexpression represents the schema.
For instance, quasiequals could be defined by:
(defquasiconstructor QEQUALS "lambda(e1,e2:ind, #(e1) or #(e2) implies e1 = e2)" (language thekerneltheory))The name of the quasiconstructor is qequals, and the lambdaexpression is the expression specified by the string in thekerneltheory. After this form has been evaluated, an expression of the form is wellformed in any language containing the language of thekerneltheory, provided A and B are wellformed expressions of the same type of kind . Separate from the definition, special syntax may be defined for parsing and printing qequals (e.g., as the infix symbol ).
The quasiconstructor quasiequals is not actually defined using a defquasiconstructor form in IMPS. It is one of a small number of ``system quasiconstructors'' which have been directly defined by the IMPS implementors. A system quasiconstructor cannot be defined using the defquasiconstructor form because the schema of the quasiconstructor cannot be fully represented as a LUTINS lambdaexpression. This is usually because one or more variables of the schema variables ranges over function expressions of variable arity or over expressions of both kind and . For example, is not welldefined if A and B are of kind , but is welldefined as long as A and B have the same type (regardless of its kind). The major system quasiconstructors are listed in Table 10.1.

There are two modes for reasoning with a quasiconstructor Q. In the enabled mode the internal structure of Q is ignored. For example, in this mode, when an expression Q(E_{1},..,E_{n}) is simplified, only the parts of the internal expression corresponding to the arguments E_{1},..,E_{n} are simplified, and the part corresponding to Q is ``skipped.'' Similarly, when a macete is applied to an expression Q(E_{1},..,E_{n}), subexpressions located in the part of the internal expression corresponding to Q are ignored. In this mode, quasiconstructors are intended to behave as if they were ordinary constructors.
In the disabled mode, the internal structure of Q has no special status. That is, deduction is performed on internal expressions as if Q was never defined. (However, in this mode expressions involving Q will still be printed using Q as an abbreviation.) The mode is activated by ``disabling Q,'' and it inactivated by ``enabling Q.'' The disabled mode is used for proving basic properties about Q. Once a good set of basic properties are proven and formalized as theorems, there is usually little need for the disabled mode. Most quasiconstructors are intended to be employed in multiple theories. Hence, you will usually want to install a theorem about a quasiconstructor with the usage transportablemacete.
For a few of the interactive proof commands, there is a dual command with the word ``insistent'' put somewhere into the command's name. For example, the dual of simplify is the simplifyinsistently. Calling the dual of a command C is equivalent to disabling all quasiconstructors and then calling Citself. In other words, the dual commands behave as if there were no quasiconstructors at all. These ``insistent'' commands are intended to be used sparingly because they can disturb the internal structure corresponding to a quasiconstructor, creating a new internal expression that can no longer be abbreviated by the quasiconstructor. In visual terms, the quasiconstructor ``explodes.''
One of the advantages of working in a logic like LUTINS, with a rich structure of functions, is that generic objects like sets and sequences can be represented directly in the logic as certain kinds of functions. For instance, sets are represented in IMPS as indicators, which are similar to characteristic functions, except that x is a ``member'' of an indicator f iff f(x) is defined. Operators on indicators and other functions representing generic objects are formalized in IMPS as quasiconstructors, and theorems about these operators are proved in ``generic theories'' that contain neither constants nor axioms (except for possibly the axioms of the theory horealarithmetic). Consequently, reasoning is performed in generic theories using only the purely logical apparatus of LUTINS (and possibly horealarithmetic). Moreover, theorems about generic objects are easy to apply in other theories since the operators, as quasiconstructors, are polymorphic and since the theory interpretations involved usually have no obligations to check.
(viewexpr "1/0==?zz" (languagename horealarithmetic) noquasiconstructors)is evaluated, the expression is printed as
(#(1/0) or #(?zz)) implies 1/0=?zz.
q{e1,...,en}
, where q is
a quasiconstructor, is parsed exactly like q(e1,...,en)
. In
addition, the internal expression is always printed like
q{e1,...,en}
, unless you have defined a special print syntax
for q.
with(f:[ind,ind], forall(x:ind, #(f(x))))It parses into an internal expression E_{1} which is printed as the string S_{2}
with(f:[ind,ind],total_q{f,[ind,ind]})with quasiconstructor abbreviations and is printed as S_{1} without quasiconstructor abbreviations. However, S_{2} parses into an internal expression E_{2} which is printed as S_{2} with quasiconstructor abbreviations and is printed as the string S_{3}
with(f:[ind,ind],forall(x_0:ind,#(f(x_0))))without quasiconstructor abbreviations. That is, the two internal expressions are the same except for the name of the single bound variable.