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

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.

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)
```%worlds () (eval _ _).