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
  • 2
    $\begingroup$ For future reference, is this considered "research level" on this site? I don't want to come across as a jerk, but this is standard material in an undergraduate course in PL theory. $\endgroup$ – Christopher Monsanto May 23 '11 at 16:25
  • $\begingroup$ Probably not a research level question. I've seen simpler questions asked on this site though. Besides, the community seems to have appreciated the question (and answer!) considering the vote counts. $\endgroup$ – aioobe May 23 '11 at 16:32
  • $\begingroup$ @Chris: It's an exercise-level question from an advanced undergrad course, but that's a course that a lot of TCS folk have never taken. I'm uncomfortable about this class of question, but bona fide research can lead to these so I think we shouldn't say they are off-topic. I do think we should insist on motivation with these questions; it's clear enough where aioobe is coming from in this case, at least. I said a bit more on meta: meta.cstheory.stackexchange.com/questions/1066/…. $\endgroup$ – Charles Stewart May 23 '11 at 21:04
  • 1
    $\begingroup$ @Charles, this was not part of the undergrad course in PL that I had when I was doing my BS, but if it is a standard topic in typical undergrad courses on PL these days then I would say it is off-topic, if you see a question which is covered in the standard undergrad textbooks on the topic let us know and we will close it as off-topic. But you may want to raise the issue by posting a question on the meta to get a better feedback from the community. (btw, I have the impression that in general European universities tend to have a stronger PL undergrad course than other places.) $\endgroup$ – Kaveh May 24 '11 at 2:07

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).

  • 1
    $\begingroup$ Nice answer, thanks! Shouldn't $\mathit{get}$ be of type Σ → L → V ? $\endgroup$ – aioobe May 19 '11 at 17:58
  • $\begingroup$ @aiobe. You are right. $\endgroup$ – Marc May 20 '11 at 12:38
  • 1
    $\begingroup$ Also I think $C_1; C_2$ should be translated as $⟦C_2⟧ ∘ ⟦C_1⟧$, no? $\endgroup$ – aioobe May 23 '11 at 12:49
  • $\begingroup$ $(⟦A⟧~s)$ for the assignment rule? $\endgroup$ – aioobe Jun 13 '11 at 14:42
  • $\begingroup$ I would like to say that there a couple of problems with this translation. First of all Marc had to bring in something called "locations" which were never there in the source language. Secondly, his toy language didn't have local variable declarations. For a full solution to the problem, see O'Hearn and Reynolds: "From Algol to Polymorphic Linear Lambda-Calculus", JACM 2000. $\endgroup$ – Uday Reddy Feb 27 '12 at 20:23

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

  • $\begingroup$ Trying to wrap my head around state monads. Could you give an example? For instance of how the last While-program in my question would be translated? (Unless it's a bad example in some sense) $\endgroup$ – aioobe May 19 '11 at 9:32
  • 2
    $\begingroup$ @aioobe: Essentially statement composition will be interpreted as function composition, where statements are functions taking state to state - here monads just give you a way of making this idea of sequentialisation algebraic. $\endgroup$ – Charles Stewart May 19 '11 at 11:22
  • 1
    $\begingroup$ gallais: Since we only have global state in this language, you can interpret variables as Church numerals, making the definition of environment lookup trivial. $\endgroup$ – Charles Stewart May 19 '11 at 11:25
  • 1
    $\begingroup$ @Aioobe: Marc's answer explains all of my points. $\endgroup$ – Charles Stewart May 19 '11 at 12:52
  • 1
    $\begingroup$ I am sorry. I fail to see how "monads" improve anything on what Marc wrote. Hope somebody can explain this clearly. I see the "monad" word being thrown around a lot, but never with any substance. It seems to me to be some form of mysticism! $\endgroup$ – Uday Reddy Feb 27 '12 at 20:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.