Go to the first, previous, next, last section, table of contents.

16 History

While the underlying type theory has not changed, the Twelf implementation differs from older Elf implementation in a few ways. Mostly, these are simplifications and improvements. The main feature which has not yet been ported is the Elf server interface to Emacs. Also, while the type checker is more efficient now, the operational semantics does not yet incorporate some of the optimizations of the older Elf implementations and is therefore slower. The principal differences of Twelf 1.2 and the obsolete Elf 1.5 are given below, followed by the new features of Twelf 1.3. New features in Twelf 1.4 are given in section 1.1 New Features.

Syntax (see section 3 Syntax)
The quote `'' character is no longer a special character in the lexer, and `=' (equality) is now a reserved identifier. The syntax of %name declarations has changed by allowing only one preferred name to be specified. Also, %name, %infix, %prefix and %postfix declarations must be terminated by a period `.' which previously was optional. Further, single lines comments now must start with `%whitespace' or `%%' in order to avoid misspelled keywords of the form `%keyword' to be ignored.
Type theory
Elf 1.5 had two experimental features which are not available in Twelf: polymorphism and the classification of type as a type.
Definitions (see section 3.3 Definitions)
Twelf offers definitions which were not available in Elf.
Searching for definitions (see section 5.2 Solve Declaration)
Elf had a special top-level query form sigma [x:A] B which searched for a solution M : A and then solved the result of substituting M for x in B. In Twelf this mechanism has been replaced by a declaration %solve c : A which searches for a solution M : A and then defines c = M : A, where the remaining free variables are implicitly universally quantified.
Query declarations (see section 5.1 Query Declaration)
Twelf allows queries in ordinary Elf files as `%query' declarations. Queries are specified with an expected number of solutions, and the number of solutions to search for, which can be used to test implementations.
Operational semantics (see section 5.5 Operational Semantics)
Twelf eliminates the distinction between static and dynamic signatures. Instead, dependent function types {x:A} B where x occurs in the normal form of B are treated statically, while non-dependent function type A -> B or B <- A or {x:A} B where x does not occur in B are treated dynamically.
Modes (see section 7 Modes)
Twelf offers a mode checker which was only partially supported in Elf.
Termination (see section 8 Termination)
Twelf offers a termination checker which can verify that certain programs represent decision procedures.
Theorem prover (see section 10 Theorem Prover)
Although very limited at present, an experimental prover for theorems and meta-theorems (that is, properties of signatures) is now available. It does not yet support lemmas or meta-hypothetical reasoning, which are currently under development.
Emacs interface (see section 13 Emacs Interface)
The Elf mode has remained basically unchanged, but the Elf server interface has not yet been ported.

The version 1.3 from September 13, 2000 incorporated the following major changes from Twelf 1.2 from August 27, 1998.

Constraints (see section 6 Constraint Domains).
Type reconstruction and the logic programming engine (but not yet the theorem prover) allow various constraint domains in the style of constraint logic programming languages. The main ones are equalities and inequalities over rationals and integers.
Tracing and Breakpoints (see section 11.5 Tracing and Breakpoints)
The logic programming engine now support tracing and setting of breakpoints for illustration and debugging purposes.
Theorem Prover (see section 10 Theorem Prover)
The theorem prover now allows quantification over regular context. The theorem prover will also use previously proved theorems with %prove) and ignore those with %establish, which is otherwise equivalent. In unsafe mode, %assert can be used to claim theorems. However, at present no longer generates proof terms.
Reduction Checking (see section 8.2 Reduction Declaration)
The termination checker has been extended to verify if output arguments to a predicate are smaller than some inputs with the %reduces declaration.
Signature Printing (see section 11.4 Signature Printing)
Signatures can now be printed, also in TeX format.
Abbreviations (see section 3.3 Definitions)
Added abbreviations (%abbrev) which, unlike definition, do not need to be strict.
Name Preferences (see section 3.5 Name Preferences)
Name preference declarations (%name) now allow an optional second argument for naming of parameters.

Go to the first, previous, next, last section, table of contents.