Evaluation

Inductive Definition

The terms of Nuprl denote data, programs and types; but programs and types can be data too. So we must say how to evaluate every term. There are many ways to approach this mathematically. We can give a denotational semantics, or a reduction (rewrite) semantics, or a structural operational semantics or something else. We choose to base the account on inductively defined relations and partial functions in the style of [13,35,39,43], sometimes called ``natural semantics''. We use a lazy evaluator [1,13,35].

We define first a relation ``evaluates to,'' $t evals\_to t'$.Then we define val as a map

$$val:\{x:term \vert \exists t:term x evals\_to t\}\rightarrow term.$$

We give some cases of the evaluation relation to illustrate the method.

• $\frac{\textstyle f evals\_to \mbox{\boldmath $\lambda${\sf (x.b)}} b[a/x] evals\_to c}{\textstyle \mbox{\sf ap(f;a)} evals\_to c}$
• $\frac{\textstyle ~~~}{\textstyle \mbox{\sf {\boldmath$\lambda$}(x.b)} \ evals\_to \mbox{\sf {\boldmath$\lambda$}(x.b)}}$
• $\frac{\textstyle ~~~}{\textstyle \mbox{\sf inl(a)} evals\_to \ \mbox{\sf inl(a)}}$
• $\frac{\textstyle d evals\_to \mbox{\sf inl(a)} \ t_1[a/u] evals\_to c}{\textstyle \mbox{\sf decide(d; u.{\boldmath $t_1$}; v.{\boldmath$t_2$})} evals\_to c}$
• $\frac{\textstyle d evals\_to \mbox{\sf inr(b)} \ t_2[b/v] evals\_to c}{\textstyle \mbox{\sf decide(d; u.{\boldmath $t_1$}; v.{\boldmath$t_2$})} evals\_to c}$

Properties of Evaluation

We can prove rather easily these properties of evaluation.

Theorem:

1.

$t evals\_to t' \& t evals\_to t''$ implies t'=t''. (deterministic)

2.

$t evals\_to t'$ implies t' is a value. (value producing)

3.

If t is a value then $t evals\_to t$. (idempotent)

Evaluation fragments

In order to allow for the addition of new operators in a systematic way, we index the evaluation process by the operator name. So the actual evaluation relation has the form $t evals\_to_{op}(f) \, t'$ where f is a parameter. We just gave these fragments for some of the operators. The evaluation relation is then defined as

Definition: $t evals\_to t'$ iff $t \ evals\_to_{opname(t)} (evals\_to) t'$