4. Call-by-name evaluation, types, and typing

Call-by-name Evaluation

We have previously seen the call-by-value rule:

$$\frac{t_1{\Downarrow }_P{v}_1\dots t_{⟨f_1⟩}{\Downarrow }_P{v}_{⟨f_i⟩}{d}_i\{x_1\mapsto v_1,\dots ,x_{⟨f_i⟩}\mapsto v_{⟨f_i⟩}{\Downarrow }_{P}v\}}{f_i(t_1,\dots ,t_{⟨f_1⟩}){\Downarrow }_{P}v}(f{n}_{\text{val}})$$

Consider the functions in the program $P$:

• $\text{infinity}=\text{infinity}+1$
• $\text{fortytwo}(x)=42$

This rule can get problematic for certain computations such as:

• $\text{fortytwo}(\text{infinity})$
• $\text{fortytwo}(2^{3542})$

In order to model call-by-name evaluations, we replace the call-by-value rule with following call-by-name rule:

$$\frac{d_i\{x_1\mapsto t_1,\dots ,x_{⟨f_i⟩}\}{\Downarrow }_{P}v}{f_i(t_1,\dots ,t_{⟨f_i⟩}){\Downarrow }_{P}v}(f{n}_{\text{name}})$$

Example: Show call-by-name evaluation of program $P$

Let program $P$ be:

$$\begin{array}{rl}\text{infinity}& =\text{infinity}+1\\ \text{fortytwo}(x)& =42\\ \text{square}(x)& =x\ast x\end{array}$$

Using call-by-name semantics the term $\text{fortytwo}(0)$ also has the value $42$, $\text{fortytwo}(0){\Downarrow }_{P}42$. However in contrast to call-by-value, $\text{fortytwo}(\text{infinity}){\Downarrow }_{P}42$ because the argument is discarded without evaluation:

$$\frac{\frac{}{42\{x\mapsto \text{infinity}{\Downarrow }_{P}42\}}(n)}{\text{fortytwo}(\text{infinity}){\Downarrow }_{P}42}(f{n}_{\text{name}})$$

Types for SFUN

The grammar defining the syntax of SFUN allows us to build terms such as $1+\text{True}$ which do not make sense. In the definition of the semantics of SFUN we only consider well-typed terms.

The base types, $\beta$, and the types $\mathcal{T}$ of SFUN are defined as follows:

$$\begin{array}{rl}\beta & ::=\text{int}|\text{bool}\\ \mathcal{T}& ::=({\beta }_1,\dots ,{\beta }_n)\to \beta \end{array}$$

In the case of a type $\mathcal{T}$ such that $n=0$ (function with no arguments), $\mathcal{T}$ may be written as $\beta$.

Well-typed terms

The set of well-typed terms can be defined using the relation:

$$\Gamma {⊢}_{ϵ}t:\mathcal{T}$$

• Where $\Gamma$ is the variable environment which maps some variables to types. It is a finite partial function assignment.
• Where $ϵ$ is the function environment which maps each fn. to a type specifying arity.
• Where $t$ is an SFUN term.
• Where $\mathcal{T}$ is a type.

“If the variable $x$ has type $\Gamma (x)$ for each $x\in \text{dom}(\Gamma )$ and the functions $f_1,\dots ,f_k$ have types $ϵ(f_1),\dots ,ϵ(f_k)$ then the term $t$ has type $\mathcal{T}$.”

Typing SFUN terms

The well-typed relation is inductively defined by the following system of axioms and rules. In case the case of the application of a function $f$ where $⟨f⟩=0$ then the rule reduces to an axiom, because there are no arguments to check.

Example: Give the derivation for the typing of term $\text{if }x\le 0\text{ then }1\text{ else }x\ast \text{fact}(x-1)$.

$$\frac{\frac{\frac{}{\Gamma {⊢}_{ϵ}x:\text{int}}\frac{}{\Gamma {⊢}_{ϵ}0:\text{int}}}{\Gamma {⊢}_{ϵ}x\le 0:\text{bool}}\frac{}{\Gamma {⊢}_{ϵ}1:\text{int}}\frac{\frac{}{\Gamma {⊢}_{ϵ}x:\text{int}}\frac{\frac{\frac{}{\Gamma {⊢}_{ϵ}x:\text{int}}\frac{}{\Gamma {⊢}_{ϵ}1:\text{int}}}{\Gamma {⊢}_{ϵ}x-1:\text{int}}}{\Gamma {⊢}_{ϵ}\text{fact}(x-1):\text{int}}}{\Gamma {⊢}_{ϵ}x\ast \text{fact}(x-1):\text{int}}}{\Gamma {⊢}_{ϵ}\text{ if }x\le 0\text{ then }1\text{ else }x\ast \text{fact}(x-1):\text{int}}$$

Example: Give derivation of typing of term $\text{max}(3,\text{square}(2))$.

Given that $ϵ(\text{max})=(\text{int},\text{int})\to \text{int}$. And that $ϵ(\text{square})=(\text{int})\to \text{int}$. We have that:

$$\frac{\frac{}{\Gamma {⊢}_{ϵ}3:\text{int}}\frac{\frac{}{\Gamma {⊢}_{ϵ}2:\text{int}}}{\Gamma {⊢}_{ϵ}\text{square}(2):\text{int}}}{\Gamma {⊢}_{ϵ}\text{max}(3,\text{square}(2)):\text{int}}$$

Typing SFUN programs

Given a program $P$ in SFUN:

$$\begin{array}{rl}{f}_1(x_1,\dots ,x_{⟨f_1⟩})& =t_1\\ & ⋮\\ f_k(x_1,\dots ,x_{⟨f_k⟩})& =t_k\end{array}$$

and a function environment $ϵ$, $P$ is typeable, if for each equation $f_i(x_1,\dots ,x_{⟨f_i⟩})=t_i$, there exists an environment ${\Gamma }_i$ and a type ${\mathcal{T}}_i$, such that:

• ${\Gamma }_i{⊢}_{ϵ}{f}_i(x_1,\dots ,x_{⟨f_i⟩}):{\mathcal{T}}_i$
• ${\Gamma }_i{⊢}_{ϵ}{t}_i:{\mathcal{T}}_i$

Example: Is program $P$ typeable?

Let program $P$ be:

$$\begin{array}{rl}\text{infinity}& =\text{infinity}+1\\ \text{fortytwo}(x)& =42\\ \text{square}(x)& =x\ast x\end{array}$$

And given a function environment $ϵ$ where:

$$\begin{array}{rl}ϵ(\text{infinity})& =\text{int}\\ ϵ(\text{fortytwo})& =(\text{int})\to \text{int}\\ ϵ(\text{square})& =(\text{int})\to \text{int}\end{array}$$

$P$ is a typeable program. All the equations are typeable with type $\text{int}$, the first in an empty environment and the latter two using an environment $\Gamma$, such that $\Gamma (x)=\text{int}$.

Proving properties of SFUN programs

We can use proof by induction on SFUN programs directly.

Example: Given that $\text{fact}(x)=\text{if }x\le 0\text{ then }1\text{ else }x\ast \text{fact}(x-1)$, prove that $\text{fact}(n)=n!$ for all natural numbers $n$.

Base Case: Show that $\text{fact}(0)=0!=1$. By definition of $\text{fact}(x)$, $0\le 0$ evalutes to $\text{True}$, and then by the left-hand side of the conditional, $\text{fact}(0)=1$, as expected. Induction Hypothesis: Assume $\text{fact}(n)=n!$. Induction Step: Show that $\text{fact}(n+1)=(n+1)!$. $n+1\le 0$ will evaluate to $\text{False}$. By the right-hand side of the conditional, $\text{fact}(n+1)=(n+1)\ast \text{fact}((n+1)-1)$ which is equal to $(n+1)\ast \text{fact}(n)$. By the inductive hypothesis, this is equal to $(n+1)\ast n!$, which is simply $(n+1)!$.