| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 New Features.
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.
Elf 1.5 had two experimental features which are not available in Twelf: polymorphism and the classification of type as a type.
Twelf offers definitions which were not available in Elf.
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.
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.
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.
Twelf offers a mode checker which was only partially supported in Elf.
Twelf offers a termination checker which can verify that certain programs represent decision procedures.
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.
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.
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.
The logic programming engine now support tracing and setting of breakpoints for illustration and debugging purposes.
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.
The termination checker has been extended to verify if output
arguments to a predicate are smaller than some inputs with
the %reduces declaration.
Signatures can now be printed, also in TeX format.
Added abbreviations (%abbrev) which, unlike definition, do not
need to be strict.
Name preference declarations (%name) now allow an optional
second argument for naming of parameters.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by Florian Rabe on April, 3 2009 using texi2html 1.76.