Go to the first, previous, next, last section, table of contents.
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.