Summer school 2008:Arithmetic expressions with call-by-value let-binding

We define a simple expression language with let-bindings, making explicit the invariant that variables stand for values into the syntax. This allows STELF to prove termination of evaluation.

Natural numbers and addition are defined 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) %.
%worlds () (add _ _ _) %.
%total M (add M _ _) %.

Call-by-value arithmetic expressions

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

%sort val %.
%name val %.
%term num %pi nat %-> val %.

Next, we define expressions, with a constant ret including values into expressions.

%sort exp %.
%name exp %.
%term ret %pi val %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term let %pi exp %-> (%pi val %-> exp) %-> exp %.

Note that the let-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 before.

%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)) A) %<- (eval E1 (anum N)) %<- (eval (E2 (num N)) A) %.

But now, STELF can prove evaluation total:

%worlds () (eval _ _) %.
%total E (eval E _) %.

Why does this work? When termination-checking eval/let, STELF observes that no expressions can appear in variables (this observation is based on subordination), so it’s possible to view all substitution instances of E2 as having the same size as E2. This justifies the recursive call. If STELF 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.