Twelf
Encyclopedia
Twelf is an implementation of the logical framework LF
. It is used for logic programming and for the formalization of programming language theory.
nat : type.
z : nat.
s : nat -> nat.
Here
system, types can be indexed by terms, which allows the definition of more interesting type families (relations). Here is a definition of addition:
plus : nat -> nat -> nat -> type.
plus_zero : {M:nat} plus M z M.
plus_succ : {M:nat} {N:nat} {P:nat}
plus M (s N) (s P)
<- plus M N P.
The type family
The constant
). The result is the successor of
call is made via the subgoal
Twelf features type reconstruction and supports implicit parameters, so in practice one usually does not need to explicitly write
These simple examples do not display LF's higher-order features, nor any of its theorem checking capabilities. See the Twelf distribution for its included examples.
language. Its core is more sophisticated than Prolog
, since it is higher-order and dependently typed, but it is restricted to pure operators: there is no cut or other extralogical operators (such as ones for performing I/O
) as are often found in Prolog implementations, which may make it less well-suited for practical logic programming applications. Some of the use of cut rule as used in Prolog is obtained through the ability to declare that certain operators belong to deterministic type families, which avoids recalculation.
s). Used this way it is closely related to Coq
and Isabelle
/HOL
/HOL Light. However, unlike those systems, Twelf proofs are typically developed by hand. Despite this, for the problem domains at which it excels, Twelf proofs are often shorter and easier to develop than in the automated, general-purpose systems.
Twelf is particularly well suited to the encoding of programming languages and logics, because it has a built-in notion of binding and substitution. Most logics and programming languages of interest make use of binding and substitution. When implemented in Twelf, binders can often be directly encoded using the technique of higher-order abstract syntax
(HOAS), in which the meta-language (Twelf) binders are used to represent the object-level binders. As a consequence, standard theorems such as type-preserving substitution and alpha conversion come "for free".
Twelf has been used to formalize many different logics and programming languages (examples are included with the distribution). Among the larger projects are a proof of safety for the Standard ML
programming language, a foundational typed assembly language
system from CMU, and a foundational proof carrying code system from Princeton.
and binaries are available for Linux
and Microsoft Windows
. it is under active development (mostly at Carnegie Mellon University
).
LF (logical framework)
In logic, a logical framework provides a means to define a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for ...
. It is used for logic programming and for the formalization of programming language theory.
Introduction
At its simplest, a Twelf program (called a "signature") is a collection of declarations of type families and constants that inhabit those type families. For example, the following is the standard definition of the natural numbers, withz standing for zero and s the successor operator.nat : type.
z : nat.
s : nat -> nat.
Here
nat is a type, and z and s are constant terms. As a dependently-typedDependent type
In computer science and logic, a dependent type is a type that depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like ATS, Agda and Epigram....
system, types can be indexed by terms, which allows the definition of more interesting type families (relations). Here is a definition of addition:
plus : nat -> nat -> nat -> type.
plus_zero : {M:nat} plus M z M.
plus_succ : {M:nat} {N:nat} {P:nat}
plus M (s N) (s P)
<- plus M N P.
The type family
plus is read as a relation between three natural numbers M, N and P, such that M + N = P. We then give the constants that define the relation: plus_zero indicates that any natural number M plus zero is still M. The quantifier {M:nat} can be read as "for all M of type nat".The constant
plus_succ defines the case for when the second argument is the successor of some other number N (see pattern matchingPattern matching
In computer science, pattern matching is the act of checking some sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually has to be exact. The patterns generally have the form of either sequences or tree structures...
). The result is the successor of
P, where P is the sum of M and N. This recursiveRecursion
Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
call is made via the subgoal
plus M N P, introduced with <-. The arrow can be understood operationally as Prolog's :-, or as logical implication ("if M + N = P, then M + (s N) = (s P)"), or most faithfully to the type theory, as the type of the constant plus_succ ("when given a term of type plus M N P, return a term of type plus M (s N) (s P)").Twelf features type reconstruction and supports implicit parameters, so in practice one usually does not need to explicitly write
{M:nat} (etc.) above.These simple examples do not display LF's higher-order features, nor any of its theorem checking capabilities. See the Twelf distribution for its included examples.
Logic programming
Twelf signatures can be executed via a search procedure, so Twelf can be used as a logic programmingLogic programming
Logic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...
language. Its core is more sophisticated than Prolog
Prolog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
, since it is higher-order and dependently typed, but it is restricted to pure operators: there is no cut or other extralogical operators (such as ones for performing I/O
Input/output
In computing, input/output, or I/O, refers to the communication between an information processing system , and the outside world, possibly a human, or another information processing system. Inputs are the signals or data received by the system, and outputs are the signals or data sent from it...
) as are often found in Prolog implementations, which may make it less well-suited for practical logic programming applications. Some of the use of cut rule as used in Prolog is obtained through the ability to declare that certain operators belong to deterministic type families, which avoids recalculation.
Formalizing mathematics
Twelf's main use today is as a system for formalizing mathematics (especially the metatheory of programming languageProgramming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
s). Used this way it is closely related to Coq
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
and Isabelle
Isabelle theorem prover
The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic theorem prover. It is an LCF-style theorem prover , so it is based on a small logical core guaranteeing logical correctness...
/HOL
HOL theorem prover
HOL denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies....
/HOL Light. However, unlike those systems, Twelf proofs are typically developed by hand. Despite this, for the problem domains at which it excels, Twelf proofs are often shorter and easier to develop than in the automated, general-purpose systems.
Twelf is particularly well suited to the encoding of programming languages and logics, because it has a built-in notion of binding and substitution. Most logics and programming languages of interest make use of binding and substitution. When implemented in Twelf, binders can often be directly encoded using the technique of higher-order abstract syntax
Higher-order abstract syntax
In computer science, higher-order abstract syntax is a technique for the representation of abstract syntax trees for languages with variable binders.-Relation to first-order abstract syntax:...
(HOAS), in which the meta-language (Twelf) binders are used to represent the object-level binders. As a consequence, standard theorems such as type-preserving substitution and alpha conversion come "for free".
Twelf has been used to formalize many different logics and programming languages (examples are included with the distribution). Among the larger projects are a proof of safety for the Standard ML
Standard ML
Standard ML is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.SML is a modern descendant of the ML...
programming language, a foundational typed assembly language
Typed Assembly Language
In computer science, a typed assembly language is an assembly language that is extended to include a method of annotating the datatype of each value that is manipulated by the code. These annotations can then be used by a program that processes the assembly language code in order to analyse how...
system from CMU, and a foundational proof carrying code system from Princeton.
Implementation
Twelf is written in Standard MLStandard ML
Standard ML is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.SML is a modern descendant of the ML...
and binaries are available for Linux
Linux
Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...
and Microsoft Windows
Microsoft Windows
Microsoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an add-on to MS-DOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal...
. it is under active development (mostly at Carnegie Mellon University
Carnegie Mellon University
Carnegie Mellon University is a private research university in Pittsburgh, Pennsylvania, United States....
).