# 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

We write to denote

- meaning: one step of evaluating leads to

## Evaluation Rules for Operational Semantics

#### Evaluate Primitive Operation

Example

Depends on the set of primitive operators in the language

#### Beta Reduce

#### Letrec Base

if does not contain any of the variables

#### Letrec Unfold

#### Context Rule

Here denotes expression containing one occurrence of and results from by replacing this ocurrence of by

**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