LARA

Operational Semantics of Lambda Calculus with Letrec

We describe evaluation rules for our lambda calculus with letrec

We need such description to make rigorous proofs about compilers, including type systems

This is a mathematical description of an interpreter for this language

It is also analogous to relations that transform configurations in

  • finite state machines
  • push-down machines

Configuration in this case is simply an expression of lambda calculus with letrec

  • for programming languages with state, configuration would also need to include (global and local) state, and stack

We define one-step relation on configurations, here denoted $\leadsto$

We write $e_1 \leadsto e_2$ to denote $(e_1,e_2) \in {\leadsto}$

  • meaning: one step of evaluating $e_1$ leads to $e_2$

Evaluation Rules for Operational Semantics

Evaluate Primitive Operation

Example $(+\ 5\ 4) \leadsto 9$

Depends on the set of primitive operators in the language

Beta Reduce

$(\lambda x:T.e_1)e_2 \leadsto e_1[x:=e_2]$

Letrec Base

\begin{equation*}\begin{array}{l} (\textbf{letrec}\ {(f_1:T_1)} = e_1\, \textbf{and}\, \ldots \textbf{and}\, {(f_n:T_n)} = e_n\ \textbf{in}\ e) \leadsto e \end{array} \end{equation*}

if $e$ does not contain any of the variables $f_1,\ldots,f_n$

Letrec Unfold

\begin{equation*}\begin{array}{l} (\textbf{letrec}\ {(f_1:T_1)} = e_1\, \textbf{and}\, \ldots \textbf{and}\, {(f_n:T_n)} = e_n\ \textbf{in}\ e) \leadsto \\ (\textbf{letrec}\ {(f_1:T_1)} = e_1[f_1:=e_1,\ldots,f_n:=e_n]\, \textbf{and}\, \ldots \textbf{and}\, {(f_n:T_n)} = e_n[f_1:=e_1,\ldots,f_n:=e_n]\,\ \textbf{in}\ e[f_1:=e_1,\ldots,f_n:=e_n]) \end{array} \end{equation*}

Context Rule

\begin{equation*} \frac{e \leadsto e'} {C[e] \leadsto C[e'] \end{equation*}

Here $C[e]$ denotes expression containing one occurrence of $e$ and $C[e']$ results from $C[e]$ by replacing this ocurrence of $e$ by $e'$

Note: sometimes we pick a particular evaluation strategy

  • eager: evaluate arguments of function application before unfolding function
  • outermost: pick outermost expressions to evaluate

Example

Example of (outermost) evaluation: 

  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in (twice 1)
 
-unfold->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in ((% x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))) 1)
 
-beta->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in (ite (<= 1 0) 0 (+ 2 (twice (- 1 1))))
 
-primitive(<=)-->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in (ite false 0 (+ 2 (twice (- 1 1))))
 
-primitive(ite)-->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in (+ 2 (twice (- 1 1)))
 
-primitive(-)-->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in (+ 2 (twice 0))
 
-unfold-->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in (+ 2 ((% x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))) 0))
 
-beta->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in (+ 2 (ite (<= 0 0) 0 (+ 2 (twice (- 0 1)))))
 
-primitive(<=)->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in (+ 2 (ite true 0 (+ 2 (twice (- 0 1)))))
 
-primitive(ite)->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in (+ 2 0)
 
-primitive(+)->
  letrec (twice:int->int) = % x.(ite (<= x 0) 0 (+ 2 (twice (- x 1))))
  in 2
 
-base->
  2