Summer school 2008:Arithmetic expressions with let-binding

This is Literate Twelf Code: here Status: %% OK %% Output: here.

Summer school 2008

Previous: Arithmetic expressions

Next: Arithmetic expressions with call-by-value let-binding

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)
      <- add N1 N2 N.

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:
   1. We can prove termination ourselves as a metatheorem. We'll learn about this in class 3.
   2. We can make the invariant that variables stand for values explicit in the syntax of the language, in which case Twelf can prove termination itself. See Variation: Call-by-value let-binding syntax
2. Rather than recursively evaluating the substitution instance, we can give an environment semantics where the values of variables are tracked off to the side. To evaluate a let, we recursively evaluate body (so evaluation is structurally inductive on the expression) in an extended environment. See Variation: Defining evaluation with a hypothetical judgement

At this point, you should explore one or both of these variations, and then proceed to see how we represent typed arithmetic expressions.

Summer school 2008

Previous: Arithmetic expressions

Next: Arithmetic expressions with call-by-value let-binding