Summer school 2008:Arithmetic expressions

Rudimentary arithmetic

In on-paper notation, the syntax of the natural numbers is given as follows:

$n ::= \mathsf{z} \, | \, \mathsf{s}(n)$

That is, $\mathsf{z}$ is a natural number, and if $n$ is a natural number, then $\mathsf{s}(n)$ is as well.

We represent natural numbers as an LF type nat with two constants generating LF terms of that type:

%sort nat %.
%name nat %.
%term z nat %.
%term s %pi nat %-> nat %.

The constant z constructs a nat; the constant s constructs a nat from a nat.

Addition

Next, we define addition as a judgement relating two natural numbers to their sum:

${\qquad} \over {\mathsf{add}(\mathsf{z},n,n)}$

${\mathsf{add}(m,n,p)} \over {\mathsf{add}(\mathsf{s}(m), n, \mathsf{s}(p))}$

This judgement is represented in LF as follows:

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

The first line says that the type family add relates three natural numbers. The second line says that the first two (the addends) determine the third (the sum). The constants add/z and add/s correspond to the inference rules above.

Totality

STELF verifies that addition is a total function on closed terms of type nat:

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

The declarations should be read as follows:

• %mode: The two addends are inputs; the sum is an output.
• %worlds: add is defined on closed LF terms
• %total: For all M and N, there exists a P such that add M N P is derivable.

This proves a totality assertion for add.

Simple arithmetic expressions

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

Evaluation

First, we define a syntactic category of answers, which in this case is just natural numbers:

%sort ans %.
%name ans %.
%term anum %pi nat %-> ans %.

Next, we define the evaluation judgement relating an expression to an answer.

%sort eval {_ exp} {_ ans} %.
%name eval %.
%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) %.
%worlds () (eval _ _) %.
%total E (eval E _) %.

STELF verifies that evaluation is total:

• the mode declaration says that the expression is an input, and the answer is an output.
• the worlds declaration says that we’re only considering closed expressions
• the total declaration asks STELF to verify that eval defines a total relation from closed expressions to closed answers.

Solving for derivations

We can use logic programming to solve for derivations.

%define two nat s (s z) %.
%solve _ : add two two N %.
%define two_exp exp num two %.
%solve _ : eval (plus two_exp two_exp) E %.