|
Twelf is an implementation of the logical framework LF. 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, with z 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 typed 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 : plus M z M. plus_succ : 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 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 matching). The result is the successor of P, where P is the sum of M and N. This recursive 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 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. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Twelf」の詳細全文を読む スポンサード リンク
|