Compiler Theory

Functions and Memory Cells

Functions

Syntax extension

e ::= … | λx.e | (e e) | x | y | … | xᵢ, where x, y, …, xᵢ (i ∈ ℕ).

The introduction rule for functions is λx.e.

Semantics

e → e Reductions

(λx.e) e’ → e[e’/x]

e[e’/x] = e Substitutions

———————————————————
 true[e'/x] = true

and so on, for all values.

——————————————
 x[e'/x] = e'

    x ≠ y
—————————————
 y[e'/x] = y

≠ here is syntactic difference.

For dynamic scoping, we only need one rule.

     e[e'/y] = e₂
——————————————————————
 (λx.e)[e'/y] = λx.e₂

For static scoping, we need two rules.

 fresh x₁    e[e'/y] = e₂   e₁[e'/y] = e₂   x ≠ y
——————————————————————————————————————————————————
              (λx.e)[e'/y] = λx₁.e₂

 e[e'/y] = e₂     x = y
————————————————————————
  (λx.e)[e'/y] = λx.e₂

Memory cells

Syntax

e ::= … | x := e | deref x | e;e

e ; e can also be modeled as begin e … e end.

Semantics

In order to write down small step operational semantics for memory cells, we need to model the heap. Thus, we add M to the rules to model the heap.

M ::= • | M,[x ↦ e]

M, e → M’, e’ Reductions

M, x := e → M,[x ↦ e], e

which means that allocations return e as a result.

M,(add1 n₁ ) + n₂ → M,n₁ + add1 n₂

and so on.

    [x ↦ e] ∈ M
———————————————————
 M, deref x → M, e

    M, e₁ → M', e₁'
———————————————————————
 M, e₁;e₂ → M', e₁';e₂

—————————————————
 M, v;e₂ → M, e₂

M, e →* M, e Conversions

——————————————
 M, e →* M, e

 M, e → M', e'     M', e' →* M'', e''
——————————————————————————————————————
         M, e →* M'', e''

 M, e₁ →* M', e₁'     M', e₂ →* M'', e₂'
—————————————————————————————————————————
    M, e₁ + e₂ →* M'', e₁' + e₂'

eval(e) = v

 ·, e →* M', v
———————————————
  eval(e) = v