ErgoTree Evaluation

Evaluation of $\mathrm{ErgoTree}$ is specified by its translation to $\mathrm{Core\text{-}\lambda}$, whose terms form a subset of $\mathrm{ErgoTree}$ terms. Thus, typing rules of $\mathrm{Core\text{-}\lambda}$form a subset of typing rules of $\mathrm{ErgoTree}$.

Here we specify evaluation semantics of $\mathrm{Core\text{-}\lambda}$, which is based on call-by-value (CBV) lambda calculus. Evaluation of $\mathrm{Core\text{-}\lambda}$ is specified using denotational semantics. To do that, we first specify denotations of types, then typed terms and then equations of denotational semantics.

We now describe and explain a denotational semantics for the $\mathrm{Core\text{-}\lambda}$ language. The key principle is that each type $A$ denotes a set $[\![A]\!]$ whose elements are the denotations of values of the type $A$.

Thus the type $\mathrm{Boolean}$ denotes the 2-element set $\{\mathrm{true},\mathrm{false}\}$, because there are two values of type $\mathrm{Boolean}$. Likewise the type $(T_1,\dots,T_n)$denotes $([\![T_1]\!],\dots,[\![T_n]\!])$ because a value of type $(T_1,\dots,T_n)$must be of the form $(V_1,\dots,V_n)$, where each $V_i$ is value of type $T_i$.

Given a value $V$ of type $A$, we write $[\![V]\!]$ for the element of $A$ that it denotes. Given a close term $M$ of type $A$, we recall that it produces a value $V$ of type $A$. So $M$ will denote an element $[\![M]\!]$ of $[\![A]\!]$.

A value of type $A \to B$ is of the form $\lambda x.M$. This, when applied to a value of type $A$ gives a value of type $B$. So $A \to B$ denotes$[\![A]\!] \to [\![B]\!]$. It is true that the syntax appears to allow us to apply $\lambda x.M$to any term $N$ of type $A$. But $N$ will be evaluated before it interracts with $\lambda x.M$, so $\lambda x.M$ is really only applied to the value that $N$ produces.

• Given a context $\Gamma = x_1:A_1,\dots,x_n:A_n$, an environment (list of bindings for identifiers) associates to each $x_i$ as value of type $A_i$. So the environment denotes an element of $([\![A_1]\!],\dots,[\![A_n]\!])$, and we write $[\![\Gamma]\!]$ for this set.
• Given a $\mathrm{Core\text{-}\lambda}$ term $\Gamma \vdash M: B$, we see that $M$, together with environment, gives a closed term of type $B$. So $M$ denotes a function $[\![M]\!]$ from $[\![\Gamma]\!]$ to $[\![B]\!]$.

In summary, the denotational semantics is organized as follows.

• A type $A$ denotes a set $[\![A]\!]$
• A context $x_1:A_1,\dots,x_n:A_n$ denotes the set $([\![A_1]\!],\dots,[\![A_n]\!])$
• A term $\Gamma \vdash M: B$ denotes a function $[\![M]\!]$: $[\![\Gamma]\!] \to [\![B]\!]$