# Summer school 2008:Arithmetic expressions with let-binding

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

Next, we add let-binding to our expression language. Natural numbers and addition are the same as before.

## Arithmetic expressions with let-binding

### Syntax

First, the syntax:

```exp : type.				%name exp E.
num : nat -> exp.
plus : exp -> exp -> exp.
let : exp -> (exp -> exp) -> exp.```

Let-binding is represented using higher-order abstract syntax: is represented by let e_1 ([x] e_2); an LF variable is used to represent the bound-variable. So the body of the let has LF type (exp -> exp).

### Evaluation, using substitution

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

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

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

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

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

That is, to evaluate a let, we

• evaluate the let-bound term E1 to an answer anum N
• substitute its value into the body. Substitution is represented by the LF application of E2 to (num N).
• evaluate the result

Twelf cannot prove this total without some help, because it's not obvious that the substitution instance (E2 (num N)) is smaller than the input expression.

`%worlds () (eval _ _).`
ERROR: option 'ignore' deprecated or invalid
`%total E (eval E _).`
```Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)
Error:
Termination violation:
---> (E2 (num N)) < (let E1 ([x:exp] E2 x))

%% ABORT %%```

However, evaluation does terminate. There are two different ways to see this:

1. Observe that we only substitute values for variables. Consequently, it is possible to give a size metric on terms where all the substitution instances of E2 are the same size as E2, by taking the size of a variable = the size of a value = one. We can formalize this reasoning in Twelf in two ways: