Translation from basic While-language to $\lambda$-calculus

Question

Is there a simple way to translate programs written in a basic "While" language (such as Winskels Imp)?

I know about Church numerals and booleans, and I can see how if and while statements can be translated as

$$\mbox{if}~t_c~\mbox{then}~t_t~\mbox{else}~t_f\qquad\rightarrow\qquad(t_c t_t)t_f$$ and $$\mbox{while}~t_c~\mbox{do}~t_l \qquad\rightarrow\qquad \omega(\lambda r.(t_c (t_l; \omega r) I))$$ (with suitable definitions for $\omega$ and $I$).

Assignment however puzzles me.

One example translation of the following program

x := foo;
if x then t_1 else t_2

would be

$$(\lambda x.(x t_1)t_2)~foo$$

But I can't seem to find a general rule for it. How would for instance this program translate:

x := true;
y := false;
while x do
    x := y

Answer 1

Here is the toy language I am going to use. Note that locations are numbered.

$$ A := n \quad | \quad x_k \quad | \quad A_1 + A_2 \quad | \quad ... \text{ (where $n,k ∈ \mathbb{N})$ } $$ $$ B := A_1 = A_2 \quad | \quad ... $$ $$ C := \quad C_1 ; C_2 \quad |\quad x_k := A\quad | \quad skip \quad |\quad \mathop{if}~B~\mathop{then}~C_1~\mathop{else}~C_2 \quad | \quad ... $$

First, you have to encode states. What's a state ? It's map from your set $L$ of locations to your set $V$ of values. Here I choose to implement them by a function $σ : \mathbb{N} → \mathbb{N}$. We'll call $Σ$ the set of states.

There are two common operation over states : $$\mathop{get} : Σ → L → V$$ $$\mathop{get} = λs.λx.(s~x)$$

$$\mathop{set} : Σ → L → V → Σ$$ $$\mathop{set} = λs.λx.λv.\left(λk.\mathop{equal}~k~x~v~(s~k)\right)$$ where $equal$ is a λ-term representing equality between Church numerals.

Then we have to encode arithmetical expressions as function from $Σ$ to $V$ $$⟦n⟧ = λs.\lceil n \rceil$$ $$⟦x_k⟧ = λs.get~s~\lceil k \rceil$$ $$⟦A_1 + A_2⟧ = λs.\mathop{plus}~(⟦A₁⟧~s)~(⟦A₂⟧~s)$$ $$\vdots$$ where $\mathop{plus}$ is a λ-term representing addition over Church numerals and $\lceil n \rceil$ is the $n$-th Church numeral.

And boolean expressions as functions from $Σ$ to booleans: $$⟦A₁ = A₂⟧ = λs.\mathop{equal}~(⟦A₁⟧~s)~(⟦A₂⟧~s)$$ $$\vdots$$

Finally you encode your commands as "state transformers" from $Σ$ to $Σ$. $$ ⟦skip⟧ = λs.s $$ $$ ⟦x_k := A⟧ = λs.\mathop{set}~s~\lceil k \rceil~(⟦A⟧~s) $$ $$ ⟦C₁;C₂⟧ = ⟦C_2⟧ ∘ ⟦C_1⟧ = λs.⟦C_2⟧~(⟦C_1⟧~s)$$ $$ ⟦\mathop{if}~B~\mathop{then}~C_1~\mathop{else}~C_2⟧ = λs.⟦B⟧~s~(⟦C₁⟧~s)~(⟦C₂⟧~s) $$ $$\vdots$$

• Exercise 1: Prove the correctness of this compilation wrt to a standard operational semantics.

• Exercise 2: Check that everything works in a typed context (you will however need some kind of fixpoint operator to translate the while construction).

Answer 2

I would encode these side effects in a state monad [1] (or even an environment monad to be more precise). I cannot see how to do it without adding an equality predicate on binders.

[1] http://en.wikipedia.org/wiki/Monad_(functional_programming)#State_monads