exp : type.which reads "exp is a type". "type" here is really the kind (*) symbol in disguise. Then we declare how lambda calculus expressions look syntactically:
z : exp. s : exp -> exp. app : exp -> exp -> exp. lam : (exp -> exp) -> exp.Thats it! The symbol 'z' plays the role of zero. It is an expression. The symbol 's' is the successor operator, so when it is used one types 's E' for some expression E which we want the successor of. Hence it will have type 'exp -> exp'. Lambda application is 'app E1 E2'; our encoding of the classical '(E1 E2)' application. So when fed with 2 expressions, E1 and E2 , app will itself be an expression. Finally, the lambda abstraction. It is written as 'lam E' where E is of type 'exp -> exp'. One may wonder where the variables are hidden. The answer, curiously, is that we are using variables in Twelf to represent variables in our lambda calculus. A Lambda Calculus variable 'x' is just 'x' as a Twelf variable. This is clever since we don't have to define a set of variables and then use them in the language as one would have done in Coq. Further, it will become clear that we can get substitution for free by "borrowing" it from the Twelf host language. Again a case where we would had described it directly in Coq. We really do not need it right now, but it may be beneficial to declare what values are in our language. Values are computations which are finished and in due time, we don't want every possible stuck computation to be values. So let us be explicit and define values:
value : exp -> type. value_z : value z. value_s : value (s S) <- value S. value_lam : value (lam [x] E x).We are declaring that 'value' is of type 'exp -> type'. This means that value is a type family, indexed by expressions. We can then go on and define the members of the type family. The 'value_z' symbol defines that 'z' is a value. The next rule uses an inductive argument: '(s S)' is a value under the assumption that 'S' is a value. Since we are using a capital S, Twelf's type checker will do its magic and infer the type of S. In Twelf variables in uppercase is free in the LF-term and is then treated universially by the system. The rules 'value_z' and 'value_s' together defines a system making all natural numbers into values. We finally address that lambda expressions are values. The notation '[x] E x' is a Twelf-lambda abstraction. in Haskell one would have written something like '\x -> E x' in SML it would have been 'fn x => E x'. This leaves us with the last leg of the journey, namely the semantics of the lambda calculus. The rules are defined as:
eval : exp -> exp -> type. %mode eval +E -V. eval_z : eval z z. eval_s : eval (s S) (s S') <- eval S S'. eval_app : eval (app E1 E2) V <- eval E1 (lam E1') <- eval E2 V' <- eval (E1' V') V. eval_lam : eval (lam [x] E x) (lam [x] E x).We define a relation on evaluations 'eval E V' where the pair (E, V) is in the relation if the expression E evaluates to V. The '%mode' line is mode information known from logic programming. We define that the first argument is an input and the second argument is an output. This restricts the way the relation is allowed to be used. Twelf will carry out a mode check, ensuring that our use of 'eval' is in accordance with this mode definition. While this is mostly used to ensure certain relations are total, we use it here as an extra check of sanity. If your rules doesn't even pass the mode check, something is definitely wrong. I had a typo originally and the mode check found that immediately since some capitalized free variables were not ground. The symbol 'z' evaluates to itself. In 'eval_s' we call inductively -- if we have '(s S)' and S evaluates to S', then we have (s S'). Lambda abstractions in the last line evaluate to themselves as well. This leaves us with the 'app' case. If E1 evaluates to a lambda abstraction '(lam E1')', E2 evaluates to V', and (E1' V') evaluates to V, then (app E1 E2) evaluates to V. NOTE: The cool thing here is that E1' is of type 'exp -> exp' so we can just apply V'. This is substitution for free! There is no need to define a separate substitution rule because we just borrow it from Twelf. At this point we can begin to play with our toy:
add1 : exp = lam [x:exp] (s x). one = s z. two = s one. three = s two.These are straightforward definitions. One can then run queries prolog-style to find solutions to problems. In effect, we have a free interpreter for our language:
%query 1 5 eval (app add1 one) V.Twelf outputs 'V = s (s z).' as expected. We have a lot of rough edges in the toy interpreter however, and we may even have bugs in it. But we will weed them out over the coming postings, when we begin to add proofs on top of the system. At the Twelf Website is a lot of tutorials written by the Masters. If this is interesting to you, it is recommended reading!