%{

{{Summer school 2008
   |prev=Arithmetic expressions with let-binding
   |prevname=Arithmetic expressions with let-binding
   |next=Arithmetic expressions with let-binding (hypothetical evaluation)
   |nextname=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.

|hidden="true"}%

nat : type.             %name nat M.
z : nat.
s : nat -> nat.

add : nat -> nat -> nat -> type.
%mode add +M +N -P.

add/z : add z N N.
add/s : add (s M) N (s P) <- add M N P.

%worlds () (add _ _ _).
%total M (add M _ _).

%{

== Call-by-value arithmetic expressions ==

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

}%

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

%{
Next, we define expressions, with a constant <tt>ret</tt> including
values into expressions.
}%

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

%{

Note that the <tt>let</tt>-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 [[Summer school 2008:Arithmetic expressions with let-binding|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 <tt>eval/let</tt>, 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 <tt>E2</tt> as having the same size as
<tt>E2</tt>.  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
   |prev=Arithmetic expressions with let-binding
   |prevname=Arithmetic expressions with let-binding
   |next=Arithmetic expressions with let-binding (hypothetical evaluation)
   |nextname=Defining evaluation with a hypothetical judgement}}

}%