Summer school 2008:Arithmetic expressions with call-by-value let-binding

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.
Summer school 2008
Previous: Arithmetic expressions with let-binding
Next: Defining evaluation with a hypothetical judgement


We define a simple expression language with let-bindings, making explicit the invariant that variables stand for values into the syntax. This allows Twelf to prove termination of evaluation.

Natural numbers and addition are defined as before.

Call-by-value arithmetic expressions

First, we define a type of open values, which are either a numeral or a variable. Numerals are represented by a constant num; variables are represented by LF variables.

val : type.		%name val V.
num : nat -> val.

Next, we define expressions, with a constant ret including values into expressions.

exp : type.             %name exp E.
ret : val -> exp.
plus : exp -> exp -> exp.
let : exp -> (val -> exp) -> exp.

Note that the let-bound variable stands for a value.

Evaluation, using substitution

As before, the type of answers includes only numerals. The code for evaluation is exactly the same as before.

ans : type.				%name ans A.
anum : nat -> ans.

eval : exp -> ans -> type.
%mode eval +E1 -E2.

eval/val
   : eval (ret (num N)) (anum N).

eval/plus
   : eval (plus E1 E2) (anum N)
      <- eval E1 (anum N1)
      <- eval E2 (anum N2)
      <- add N1 N2 N.

eval/let
   : eval (let E1 ([x] E2 x)) A
      <- eval E1 (anum N)
      <- eval (E2 (num N)) A.

But now, Twelf can prove evaluation total:

%worlds () (eval _ _).
%total E (eval E _).

Why does this work? When termination-checking eval/let, Twelf observes that no expressions can appear in variables (this observation is based on subordination), so it's possible to view all substitution instances of E2 as having the same size as E2. This justifies the recursive call. If Twelf didn't build in this reasoning, one could justify it explcitly by using a numeric termination metric where the size of any value = the size of a variable = 1.


Summer school 2008
Previous: Arithmetic expressions with let-binding
Next: Defining evaluation with a hypothetical judgement