%{

{{Summer school 2008
   |prev=Arithmetic expressions with call-by-value let-binding
   |prevname=Call-by-value let-binding syntax
   |next=Typed arithmetic expressions
   |nextname=Typed arithmetic expressions}}

Numbers and addition are 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.

%% addition is a total function on closed terms of type nat

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

%{

== Evaluation using a hypothetical judgement ==

We use the call-by-value syntax for expressions here.

Values, expressions, answers, and the first two cases of evaluation are as before:

}%

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

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

%%% evaluation, using hypothetical judgements

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)) A2
      <- eval E1 A1
      <- ({x:val} eval (ret x) A1 -> eval (E2 x) A2).

%{

<tt>eval/let</tt> deserves some explanation: the second recursive call says that we evaluate <tt>(E2 x)</tt> in an extended LF context.  In particular, we extend the context with <tt>x:val</tt>, a variable ranging over values, and a derivation of <tt>eval (ret x) A1</tt>.  In the scope of these assumptions, the expression <tt>ret x</tt> therefore evaluates to <tt>A1</tt>.  In the terminology of [http://www.cs.cmu.edu/~rwh/plbook/book.pdf Practical Foundations for Programming Languages], <tt>eval</tt> is a [[hypothetical judgement|hypothetical]] (because we add <tt>eval</tt> assumptions to the context) and general (because we add variables to the context) judgement. The context of <tt>eval</tt> is represented by the LF context, a technique called [[higher-order judgements]].  

=== Totality in non-empty worlds ===

Because evaluation recurs in an extend context, we must prove it total not just for the empty context, as we have done above, but for a [[world]] of a particular form.  

If we tried to prove it total in the empty context, Twelf would complain:

<twelf check="decl">
%worlds () (eval _ _).
</twelf> 

This error means "you said <tt>eval</tt> stays in the empty context, but it doesn't!".

In what contexts in <tt>eval</tt> total?  Not in every context: if we ever assumed a variable <tt>x:val</tt> without also assuming <tt>eval (ret x) A</tt> for some <tt>A</tt>, then <tt>ret x</tt> would be an expression without a value.  So we want to describe the invariant that the context looks like

<tt>x1:val, d1:eval (ret x) A1, ...... , xn:val, dn:eval (ret x) An</tt>

for some <tt>A1, ... , An</tt>.  

We do this by 
# defining a block <tt>eval_block</tt> describing that pattern
# stating <tt>eval</tt> for a world containing contexts made up of <tt>eval_block</tt>s
}%

%block eval_block : some {A:ans} block {x:val} {_:eval (ret x) A}.
%worlds (eval_block) (eval _ _).

%{

Now Twelf can verify the totality of <tt>eval</tt>:

}%

%total E (eval E _).

%{

{{Summer school 2008
   |prev=Arithmetic expressions with call-by-value let-binding
   |prevname=Call-by-value let-binding syntax
   |next=Typed arithmetic expressions
   |nextname=Typed arithmetic expressions}}
}%