Glossary

  
20.0.0.0.1 Alpha-equivalence

Two expressions are alpha-equivalent if one can be obtained from the other by renaming bound variables.

  
20.0.0.0.2 Application

An expression whose lead constructor is named apply. Applications must have at least two components. The first component of an application is called the operator and the remaining components are called arguments. Applications are usually denoted by prefixing the operator to the arguments enclosed in parentheses as $f(x_1, \ldots, x_n).$ However, other forms (such as infix for algebraic operations) are also used.

  
20.0.0.0.3 Beta-reduction

An inference rule which plugs in the values of lambda-applications. For example, beta-reduction transforms the expression

$$\lambda(x,y \mbox{:}{bf Z}, x^3+6*y)(1,2)$$

to 13.

  
20.0.0.0.4 Buffer

An Emacs data structure for representing portions of text, for example, text files which are being edited. To the user, a buffer has the appearance of a scrollable page. More than one buffer may exist at a given time in an Emacs session. Users will also use buffers to build, edit and evaluate def-forms.

  
20.0.0.0.5 Command form

An s-expression

$$\mbox{\tt (} \mbox{\it command-name} \ \mbox{\it arg}_1 \dots\ \mbox{\it arg}_n\mbox{\tt ) }$$

used in proof scripts. The number and type of arguments is command-dependent. If the command takes no arguments, then the form command-name is also valid.

  
20.0.0.0.6 Compound expression

An expression with a constructor and a (possibly empty) list of components. 1+2is a compound expression whose constructor is named apply and whose components are +,1,2.

  
20.0.0.0.7 Constant

A kind of IMPS expression. For example, in the theory named h-o-real-arithmetic, the expressions 1,2,+ are constants.

  
20.0.0.0.8 Constructor

One of the 19 logical constants of LUTINS. Constructors are used to build compound expressions.

  
20.0.0.0.9 Context

An IMPS data structure representing a set of of formulas to be used as assumptions. Contexts contain various kinds of cached information (for example, about definedness of terms), used by the IMPS simplification machinery.

  
20.0.0.0.10 Core

All the basic logical and deductive machinery of IMPS on which the soundness of the system depends.

  
20.0.0.0.11 Deduction graph

An IMPS data structure representing a proof. Deduction graphs contain two kinds of nodes: inference nodes and sequent nodes.

  
20.0.0.0.12 Def-form

An s-expression whose evaluation has some effect on the IMPS environment, such as building a theory, adding a theorem to a theory, making a definition in a theory or building a translation between theories. There are about 30 such def-forms.

  
20.0.0.0.13 Emacs

A text editor. Although various implementations of Emacs exist, in this manual we mean exclusively GNU Emacs, which is the extensible display editor developed by the Free Software Foundation. Because of the many extension facilities it provides (including a programming language with many string-processing functions), GNU Emacs is well-suited for developing interfaces.

  
20.0.0.0.14 Expression

An IMPS data structure representing an element of a language. Expressions are used to describe mathematical entities or to make logical assertions. Two examples (printed in TEX) are 2²ⁿ-1 and

$$\forall k,m : { \bf Z }, (1 \leq k \wedge k \leq m) \supset {... ... { k } } = { { m } \choose { k-1 } } + { { m } \choose { k } }.$$

An expression is either a formal symbol or a compound expression.

  
20.0.0.0.15 Evaluate

To cause an s-expression to be read by the T process, thereby creating an internal representation of a program, which is then executed by T. This sequence of events usually has a number of side-effects on the IMPS environment. For example, to define a constant named square in the theory h-o-real-arithmetic, evaluate the s-expression:

 
   (def-constant SQUARE
     "lambda(x:rr, x^2)"
     (theory h-o-real-arithmetic))

  
20.0.0.0.16 Formal symbol

A primitive IMPS expression. A formal symbol has no components, although it is possible for an expression with no components to be a compound expression. A formal symbol can be a variable or a constant. Every formal symbol has a name which is used for display. The name is a Lisp object such as a symbol or a number.

  
20.0.0.0.17 Formula

Intuitively, an expression having a truth value, for example,

$$\forall x,y,z:{\bf R}, x<y \wedge y<z \supset x<z.$$

In IMPS a formula is an expression whose sort is $\ast$.

  
20.0.0.0.18 IMPS

A formal reasoning system and theorem prover developed at The MITRE Corporation.

  
20.0.0.0.19 Inference node

A node in a deduction graph, connecting a conclusion sequent node with zero or more hypothesis sequent nodes, that represents an instance of a rule of inference.

  
20.0.0.0.20 Iota-expression

A compound expression whose lead constructor is named iota, denoted in the mathematical syntax by $\iota.$ An iota-expression has the form $\iota x\mbox{:}\sigma, \varphi.$ It denotes the unique object in the sort $\sigma$ which satisfies the condition $\varphi,$ if such an object exists. Otherwise, the iota-expression is undefined.

  
20.0.0.0.21 Kind

Each sort and expression is of kind $\iota$ (also written as iota) or $\ast$ (prop). Expressions of kind $\iota$ are used to refer to mathematical objects; they may be undefined. Expressions of kind $\ast$ are primarily used in making assertions about mathematical objects; they are always defined.

  
20.0.0.0.22 Lambda-application

An application whose operator is a lambda-expression. For example $\lambda(x,y \mbox{:}{\bf R}, x^2+3*y)(1,z).$

  
20.0.0.0.23 Lambda-expression

A compound expression whose lead constructor is named lambda, denoted in the mathematical syntax by $\lambda.$ A lambda-expression has the form $\lambda x_1\mbox{:}\sigma_1, \ldots , x_n\mbox{:}\sigma_n, \varphi.$ It denotes the function of n arguments whose value at $x_1,\ldots,x_n$ is given by the value of term $\varphi,$ provided the x_i are of sort $\sigma_i.$

  
20.0.0.0.24 Language

Mathematically, a language in IMPS consists of expressions, sorts, and user-supplied information about sort inclusions. At the implementation level, a language is a Lisp data structure having additional structure which procedurally encodes this information. This is meant to facilitate various kinds of lower level reasoning, such as reasoning about membership of an expression in a sort.

  
20.0.0.0.25 Little theories

A version of the axiomatic method in which mathematical reasoning is distributed over a network of theories linked to one another by theory interpretations, in contrast to the ``big theory'' approach in which all reasoning is performed within a single, usually very expressive theory.

  
20.0.0.0.26 Local context

The set of assumptions relevant to a particular location in an expression.

  
20.0.0.0.27 LUTINS

A version of type theory with partial functions and subtypes; the logic of IMPS.

  
20.0.0.0.28 Macete

A user-defined extension of the simplifier. When a theorem is installed, it is also automatically installed as a macete. The way the corresponding macete works depends on the syntactic form of the theorem. In the simplest case in which the theorem is a universally quantified equality, the theorem is used as a rewrite rule. Macetes can be composed using the def-form named def-compound-macete. The word ``macete'' comes from Brazilian Portuguese, where it means ``clever trick.'' Theorem macetes can also be made into transportable macetes.

  
20.0.0.0.29 Mode Line

The line at the bottom of each buffer window. It provides information about the displayed buffer such as its name and mode.

  
20.0.0.0.30 Parser

A program which takes user input, usually represented as text, and builds a data structure suitable for computer processing.

  
20.0.0.0.31 Primitive inference procedure

An IMPS procedure that implements one of the primitive rules of inference of the IMPS proof system. IMPS has about 30 primitive inference procedures.

  
20.0.0.0.32 Proof

Conclusive mathematical evidence of the validity of some assertion. The rules for admissible evidence are given by a proof system.

  
20.0.0.0.33 Quasi-constructor

A user-defined macro/abbreviation for building expressions. Quasi-constructors are used much like constructors.

  
20.0.0.0.34 Quasi-equality

A quasi-constructor, written as infix $\simeq$ in the mathematical syntax. $t \simeq s$ means that either t and s are both undefined or they are equal.

  
20.0.0.0.35 S-expression

The external representation of the basic data structure of Lisp-like languages including T. S-expressions are usually represented as nested lists such as (fuba (abacaxi farofa) alface).

  
20.0.0.0.36 Sequent node

A node in a deduction graph that represents a sequent, a formula composed of a set of assumptions and an assertion.

  
20.0.0.0.37 Sort

A sort denotes a nonempty set of mathematical entities. Every expression has a sort which restricts the value of that expression.

  
20.0.0.0.38 Syntax

Rules for parsing and printing expressions. The syntaxes that are currently used in IMPS are the string syntax which allows for infix and postfix notation, the s-expression syntax which provides a uniform prefix syntax for all constructors and operators, and the tex syntax for displaying (but not parsing) in TEX.

  
20.0.0.0.39 T

A dialect of Lisp developed at the Yale University Computer Science Department in which the core machinery of IMPS is implemented. T is very similar to the Scheme programming language, familiar to readers of Abelson and Sussman's book [1].

  
20.0.0.0.40 Tea

An alias for the T programming language.

  
20.0.0.0.41 Theory

The term ``theory'' as used in this manual, consists of a language and a set of closed formulas in the language called axioms. A theory is implemented as a record structure having slots for the language, the list of axioms, and other relevant information. There is also a slot for a table of procedures which the simplifier uses to apply the axioms. This is meant to facilitate various kinds of lower-level reasoning, such as algebraic or order simplification. In a different sense, theory is also commonly used to refer to a collection of related facts about a given mathematical structure, such as the theory of rings or the theory of ordinary differential equations.

  
20.0.0.0.42 Theory ensemble

A data structure which bundles together theories which are unions of copies of a single base theory. Theory ensembles are mainly used to treat multiple instances of structures, such as triples of metric spaces or pairs of vector spaces.

  
20.0.0.0.43 Theory interpretation

A translation that maps theorems to theorems.

  
20.0.0.0.44 Translation

An IMPS data structure, created with the def-form named def-translation, that is used to translate expressions from one theory to another.

  
20.0.0.0.45 Transportable macete

A theorem macete that can be used in a theory different from the one in which it was installed. Transportable macetes are named by the system by prefixing tr% to the name of the theorem.

  
20.0.0.0.46 Type

A sort that is maximal with respect to the subsort relation.

  
20.0.0.0.47 Variable

A kind of IMPS expression. An occurrence of a variable v within an expression is bound if it occurs with the body of a binding constructor which includes v as a binding variable. Otherwise, the occurrence of v is free.

  
20.0.0.0.48 Xview

An IMPS procedure for printing expressions in TEX and then displaying them in an X window TEX previewer.