Summer school 2008:Arithmetic expressions with let-binding

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

%sort nat %.
%name nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort add {_ nat} {_ nat} {_ nat} %.
%mode add %in %in %out %.
%term add/z add z N N %.
%term add/s %pi (add (s M) N (s P)) %<- (add M N P) %.
%% addition is a total function on closed terms of type nat
%worlds () (add _ _ _) %.
%total M (add M _ _) %.

Arithmetic expressions with let-binding

Syntax

First, the syntax:

%sort exp %.
%name exp %.
%term num %pi nat %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term let %pi exp %-> (%pi exp %-> exp) %-> exp %.

Let-binding is represented using higher-order abstract syntax: $\mathsf{let} \, x \, = e_1 \, \mathsf{in} \, e_2$ 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

%sort ans %.
%name ans %.
%term anum %pi nat %-> ans %.
%sort eval {_ exp} {_ ans} %.
%mode eval %in %out %.
%term eval/num eval (num N) (anum N) %.
%term eval/plus
  %pi (eval (plus E1 E2) (anum N))
  %<- (eval E1 (anum N1))
  %<- (eval E2 (anum N2))
  %<- (add N1 N2 N) %.
%term eval/let %pi (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

STELF 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 _ _) %.

%total E (eval E _) %.

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

• 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 STELF in two ways: -# We can prove termination ourselves as a metatheorem. We’ll learn about this in class 3. -# We can make the invariant that variables stand for values explicit in the syntax of the language, in which case STELF can prove termination itself. See Variation: Call-by-value let-binding syntax
• 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.