Summer school 2008:Arithmetic expressions with let-binding (hypothetical evaluation)

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

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:

%sort val %.
%name val %.
%term num %pi nat %-> val %.
%sort exp %.
%name exp %.
%term ret %pi val %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term let %pi exp %-> (%pi val %-> exp) %-> exp %.
%%% evaluation, using hypothetical judgements
%sort ans %.
%name ans %.
%term anum %pi nat %-> ans %.
%sort eval {_ exp} {_ ans} %.
%mode eval %in %out %.
%term eval/val eval (ret (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)) A2)
  %<- (eval E1 A1)
  %<- ({x val} %pi (eval (ret x) A1) %-> (eval (E2 x) A2)) %.

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

%worlds () (eval _ _) %.

This error means “you said eval stays in the empty context, but it doesn’t!”.

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

x1:val, d1:eval (ret x) A1, ...... , xn:val, dn:eval (ret x) An

for some A1, ... , An.

We do this by

• defining a block eval_block describing that pattern
• stating eval for a world containing contexts made up of eval_blocks

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

Now STELF can verify the totality of eval:

%total E (eval E _) %.