3. Introduction to functional semantics

For the context of the next few chapters, we will be considering a small, first-order, functional programming language working on integers and Booleans, called SFUN.

Evaluation strategies

We can classify functional languages according to the evaluation strategy they implement:

• Call-by-value: argument expressions are evaluated before applying function definitions
• Call-by-name: function definitions are applied before evaluating argument expressions

Syntax of SFUN

Let $\mathcal{V}$ be a set of variables $\{x,y,z,\dots \}$ and left $\mathcal{F}$ be a set of function names $\{f_1,f_2,\dots ,f_i\}$ each with a fixed arity $⟨f_i⟩$.

The terms of the language SFUN are defined by the grammar:

$$\begin{array}{rl}\text{op}& ::=+|-|\ast |/\\ \text{bop}& ::=>|<|=|\le |\ge \\ t& ::=n|b|x|t_1\text{ op }{t}_2|t_1\text{ bop }{t}_2|\neg t_1|t_1\wedge t_2|\text{if }{t}_0\text{ then }{t}_1\text{ else }{t}_2|f(t_1,\dots ,t_n)\end{array}$$

• Where $n$ represents an integer value, $n\in \mathbb{Z}$.
• Where $b$ represents a Boolean value, $b\in \{\text{True},\text{False}\}$.

The notation $\text{vars}(t)$ is used to denote the variables that occur in the term $t$.

• $\text{vars}(x)=\{x\}$
• $\text{vars}(f(y,z))=\{y,z\}$
• A closed term is a term such that $\text{vars}(t)=\varnothing$, that is, a term that contains no variables.

A program in SFUN is a set of recursive equations:

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

• Where $d_1,\dots ,d_k$ are terms.
• Where $\text{vars}(d_i)\subseteq \{x_1,\dots ,x_{\{}{f}_i\}\},\forall i.1\le i\le k$.
• Such that there is only one equation for each function name $f_i$.

Equations may be recursive, hence the terms $d_i$ may contain occurrences of $f_1,\dots ,f_k$.

-- Example SFUN programs
max(x, y) = if x >= y then x else y
fact(x)   = if x <= 0 then 1 else x * fact(x - 1)
 
square(x)             = x * x
quadratic(x, a, b, c) = a * square(x) + b * c + c
 
mod(x, y)  = if x - y < 0 then x else mod(x - y, y)
even(x)    = mod(x, 2) = 0
collatz(x) = if x = 1 then 1 else if even(x) then x / 2 else 3 * x + 1

Operational Semantics of SFUN

In this section, the semantics of SFUN are provided in structural operation semantics style.

We assume that programs are well-typed.

• We define the evaluation relation (a big-step semantics) for terms in the context of the program $P$ using a transition system where configurations are just terms.
• The values of the system are integer and Boolean values.
• The evaluation relation relates closed SFUN terms to values in the context of $P$, and is denoted by ${\Downarrow }_P$.
• The evaluation strategy we model is call-by-value.

The evaluation relation ${\Downarrow }_P$ is defined inductively as:

Example: call-by-value evaluation

Let $P$ be the program:

infinity = infinity + 1
fortytwo(x) = 42
square(x) = x * x

The term $\text{fortytwo}(0)$ has the value $42$, that is, $\text{fortytwo}(0){\Downarrow }_{P}42$.

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

The term $\text{fortytwo}(\text{infinity})$ does not have a value, because the evaluation of the argument $\text{infinity}$ gives no value. A derivation for $\text{infinity}$ cannot be constructed because it recurses infinitely on the rule $(f{n}_{\text{val}})$. The term $\text{square}(2+1)$ has the value $9$, $\text{square}(2+1){\Downarrow }_{P}9$.

$$\frac{\frac{\frac{}{2{\Downarrow }_{P}2}(n)\frac{}{1{\Downarrow }_{P}1}(n)}{2+1{\Downarrow }_{P}3}(op)\frac{\frac{}{3{\Downarrow }_{P}3}(n)\frac{}{3{\Downarrow }_{P}3}(n)}{(x\ast x)\{x\mapsto 3\}{\Downarrow }_{P}9}(op)}{\text{square}(2+1){\Downarrow }_{P}9}(f{n}_{\text{val}})$$

Example: call-by-value derivation for the evaluation of the term $\text{max}(3,\text{square}(2))$.

$$\frac{\frac{}{3{\Downarrow }_{P}3}(n)\frac{\frac{}{2{\Downarrow }_{P}2}(n)\frac{\frac{}{2{\Downarrow }_{P}2}(n)\frac{}{2{\Downarrow }_{P}2}(n)}{(x\ast x)\{x\mapsto 2\}{\Downarrow }_{P}4}(f{n}_{\text{val}})}{\text{square}(2){\Downarrow }_{P}4}(f{n}_{\text{val}})\frac{\frac{\frac{}{3{\Downarrow }_{p}3}(n)\frac{}{4{\Downarrow }_{p}4}(n)}{3\ge 4{\Downarrow }_p\text{False}}(bop)\frac{}{4{\Downarrow }_{P}4}(n)}{\text{if }x\ge y\text{ then }x\text{ else }y\{x\to 3,y\to 4\}{\Downarrow }_{P}4}(i{f}_f)}{\text{max}(3,\text{square}(2))}(f{n}_{\text{val}})$$

Unicity of Normal Forms

The evaluation strategy defined by the axioms and rules is deterministic, that is: Theorem: for any closed term $t$, $t{\Downarrow }_P{v}_1$ and $t{\Downarrow }_P{v}_2$ implies $v_1=v_2$. Proof: by rule induction.

Details of proof of determinism

We distinguish cases according to the rule that applies to $t$. For any term, there is only one rule that can be applied.

Base cases (axioms):

• If $t$ is an integer $n$ then $n{\Downarrow }_{P}n$ using the axiom ($n$)
• If $t$ is a Boolean $b$ then $b{\Downarrow }_{P}b$ using the axiom ($b$)

Therefore, there is only one value in both cases. There are no more base cases, because $t$ is closed and thus cannot contain variables.

Inductive cases (rules):

• Assume $t$ is the term $f(t_1,\dots ,t_{⟨f⟩})$.
• Then, using the rule $(f{n}_{\text{val}})$, $f_i(t_1,\dots ,t_{⟨f_i⟩}){\Downarrow }_{P}v$ if and only if $t_1{\Downarrow }_P{v}_1,\dots ,t_{⟨f_i⟩}{\Downarrow }_P{v}_{⟨f_i⟩}$, and $d_i\{x\mapsto v_1,\dots ,x_{⟨f_i⟩}\mapsto v_{⟨f_i⟩}\}{\Downarrow }_{P}v$.
• By the induction hypothesis, there is at most one value for each term $t_1,\dots ,t_n$ and $d_i\{x\mapsto v_1,\dots ,x_{⟨f_i⟩}\mapsto v_{⟨f_i⟩}$.
• Therefore $v$ is uniquely determined.

The cases corresponding to the other rules are similar.