<p>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.</p>

<p>[1] <a href="http://en.wikipedia.org/wiki/Monad_(functional_programming)#State_monads" rel="nofollow">http://en.wikipedia.org/wiki/Monad_(functional_programming)#State_monads</a></p>

CC BY-SA 3.0
2011-05-19T09:32:48.243Z
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)
aioobe
CC BY-SA 3.0
2011-05-19T11:22:56.700Z
@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.
Charles Stewart
CC BY-SA 3.0
2011-05-19T11:25:13.720Z
gallais: Since we only have global state in this language, you can interpret variables as Church numerals, making the definition of environment lookup trivial.
Charles Stewart
CC BY-SA 3.0
2011-05-19T11:37:58.870Z
@Charls Stewart, if you care to elaborate this into an answer, I'd really appreciate it. I'm quite new to this and I'm having troubles wrapping my head around monads. (What you you mean by "environment lookup" being trivial for instance?)
aioobe
CC BY-SA 3.0
2011-05-19T12:52:45.017Z
@Aioobe: Marc's answer explains all of my points.
Charles Stewart
CC BY-SA 3.0
2012-02-27T20:29:05.033Z
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!
Uday Reddy
CC BY-SA 3.0
2011-05-19T08:45:51.080Z
2011-05-19T08:45:51.080Z
gallais
<p>Here is the toy language I am going to use. Note that locations are numbered. </p>

<p>$$    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  ...  $$</p>

<p>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. </p>

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

<p>$$\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. </p>

<p>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. </p>

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

<p>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$$</p>

<ul>
<li><p>Exercise 1: Prove the correctness of this compilation wrt to a standard operational semantics.  </p></li>
<li><p>Exercise 2: Check that everything works in a typed context (you will however need some kind of fixpoint operator to translate the while construction). </p></li>
</ul>

CC BY-SA 3.0
2011-05-19T17:58:50.480Z
Nice answer, thanks! Shouldn't $\mathit{get}$ be of type Σ → L → V ?
aioobe
CC BY-SA 3.0
2011-05-20T12:38:50.143Z
@aiobe. You are right.
Marc
CC BY-SA 3.0
2011-05-23T12:49:12.737Z
Also I think $C_1; C_2$ should be translated as $⟦C_2⟧ ∘ ⟦C_1⟧$, no?
aioobe
CC BY-SA 3.0
2011-06-13T14:42:51.473Z
$(⟦A⟧~s)$ for the assignment rule?
aioobe
CC BY-SA 3.0
2012-02-27T20:23:45.390Z
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.
Uday Reddy
CC BY-SA 3.0
2011-05-19T11:51:14.640Z
2011-06-22T17:38:13.053Z
2011-06-22T17:38:13.053Z
Marc
<p>Is there a simple way to translate programs written in a basic "While" language (such as Winskels Imp)?</p>

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

<p>$$\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$).</p>

<p>Assignment however puzzles me.</p>

<p>One example translation of the following program</p>

<pre><code>x := foo;
if x then t_1 else t_2
</code></pre>

<p>would be</p>

<p>$$(\lambda x.(x t_1)t_2)~foo$$</p>

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

<pre><code>x := true;
y := false;
while x do
    x := y
</code></pre>

CC BY-SA 3.0
2011-05-23T16:25:32.820Z
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.
Christopher Monsanto
CC BY-SA 3.0
2011-05-23T16:32:45.047Z
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.
aioobe
CC BY-SA 3.0
2011-05-23T21:04:12.323Z
@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: http://meta.cstheory.stackexchange.com/questions/1066/we-should-stop-claiming-that-this-website-is-research-level/1115#1115.
Charles Stewart
CC BY-SA 3.0
2011-05-24T02:07:47.243Z
@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.)
Kaveh
<pl.programming-languages><lambda-calculus>
Translation from basic While-language to $\lambda$-calculus
aioobe
# Translation from basic While-language to $\lambda$-calculus

(Asked by: username_0 on 2011-05-19)

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

**Tags:** pl.programming-languages, lambda-calculus

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  
> **username_2**: @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 username_0 is coming from in this case, at least.  I said a bit more on meta: http://meta.cstheory.stackexchange.com/questions/1066/we-should-stop-claiming-that-this-website-is-research-level/1115#1115.  
> **username_3**: @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.)  

---

## 2 answers

### Answer by username_6 on 2011-05-19. Score: 12 | Accepted answer

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

> **Comments:**
> **username_0**: Nice answer, thanks! Shouldn't $\mathit{get}$ be of type Σ → L → V ?  
> **username_6**: @aiobe. You are right.  
> **username_0**: Also I think $C_1; C_2$ should be translated as $⟦C_2⟧ ∘ ⟦C_1⟧$, no?  
> **username_0**: $(⟦A⟧~s)$ for the assignment rule?  
> **username_5**: I would like to say that there a couple of problems with this translation.  First of all username_6 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.  

---

### Answer by username_4 on 2011-05-19. Score: 5

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>

> **Comments:**
> **username_0**: 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)  
> **username_2**: @username_0: 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.  
> **username_2**: username_4: Since we only have global state in this language, you can interpret variables as Church numerals, making the definition of environment lookup trivial.  
> **username_0**: @Charls Stewart, if you care to elaborate this into an answer, I'd really appreciate it. I'm quite new to this and I'm having troubles wrapping my head around monads. (What you you mean by "environment lookup" being trivial for instance?)  
> **username_2**: @Aioobe: username_6's answer explains all of my points.  
> **username_5**: I am sorry.  I fail to see how "monads" improve anything on what username_6 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!  

---

