$\lambda$-calculus, is there encoding of for or while?

Question

In $\lambda$-calculus, we can encode arithmetic, numbers, booleans, and even compute factorials of numbers, as shown here.

Is there encoding of "for" or "while"?

Answer 1

Sure! Let me show how to encode FOR using an example.

Suppose we want to translate a simple factorial FOR program

x := 1
for i := 1 to N do
   x := x * i

We rewrite it as

x := 1
i := 1
repeat N times
   x := x*i
   i := i+1

then we put all the variables we use in a tuple (a pair suffices, here)

(x,i) := (1,1)
repeat N times
   (x,i) := (x*i, i+1)

This effectively applies the function $\lambda\langle x,i \rangle. \langle x*i , i+1 \rangle$ to the initial pair $\langle 1,1 \rangle$ for $N$ times.

Since $N$ can be represented as a Church numeral, we get

$$ N (\lambda\langle x,i \rangle. \langle x*i , i+1 \rangle) \langle 1,1 \rangle $$

The above syntax uses a few things beyond the plain lambda calculus. Numbers and arithmetic can be made precise using Church numerals. Pairs also have their own Church encoding:

$$ \langle x,y \rangle \equiv \lambda k.kxy \qquad \lambda \langle x,y \rangle . M \equiv \lambda z. M\{zT/x, zF/y\} $$ where $z$ is a fresh variable, $T = \lambda ab.a$ and $F = \lambda ab.b$.

If you have more than two variables, you can generalize the above encoding to tuples, or simply represent tuples as nested pairs.

---

WHILE is best dealt with using recursion: instead of

while p(x,i) do
   (x,i) := f(x,i)

where p is a predicate and f is some (partial) function, we can use something like

def recFun(x,i):
   if p(x,i):
      return recFun(f(x,i))
   else:
      return (x,i)

In the lambda calculus, recursion is obtained using a fixed point combinator, e.g. Church's $Y$ or Turing's $\Theta$. We get something like

$$ Y (\lambda r . \lambda \langle x,i \rangle . {\sf if}\ p x i\ {\sf then }\ r(f \langle x,i \rangle)\ {\sf else}\ \langle x,i \rangle) $$

where ${\sf if}\ b\ {\sf then }\ t\ {\sf else}\ e \equiv b t e$ assuming booleans are Church encoded.

Also note that WHILE is (strictly) more powerful than FOR. Every FOR can be encoded as a WHILE, so this encoding technique can also be used for FOR.

Answer 2

There are encodings of loops, but they don't work exactly like the loops that you're used to, because the lambda calculus is not an imperative language. The lambda calculus has no side effects (it's a purely functional language), so the exact equivalent of a loop would be useless.

Explicit state

An imperative program can be translated to a purely functional language by passing all state around explicitly as a variable in the program. I'll use Python syntax for imperative pseudocode; it should be mostly transparent, with the indication that (a, b) = f(…) means that the call to the function f returns a pair and a and b are assigned the first and second component of the pair respectively. Consider a loop

while test_condition():
    do_stuff()

Let's make the state explicit.

state = initial_state
(state, cond) = test_condition(state)
while cond:
    (state, cond) = test_condition(do_stuff(state))

We can translate this to a recursive call. def loop(state): defines a function called loop.

def loop(state):
    (state, cond) = test_condition(state)
    if cond: return loop(do_stuff(state))
    else: return state
state = loop(initial_state)

This only uses the following concepts, all of which can be expressed easily in the lambda calculus:

• Function calls: native concept
• Local variable assignments without reassignment: pass the value to an auxiliary function
• Pairs: Church pairs
• Booleans: Church booleans
• Recursion: fixed point combinators

And thus we can define a while function for a condition $C$ (test_condition) and a body $B$ (do_stuff): $$ \mathsf{while} := \lambda C. \lambda B. \mathsf{fix} (\lambda f. \lambda s. (\lambda p. \text{BODY} (\mathsf{first}\, p) (\mathsf{second}\, p)) (C \, s)) \\ \text{where BODY} = \lambda s'. \lambda c. \mathsf{if} \, c \, (f \, (B \, s')) \, s' $$

For loops vary depending on the programming language, but they're always a special case of while loops, so they can be encoded in the same way. If the source language limits the expressiveness of for loops, there may be simpler encodings. For example, “repeat $n$ times” is simply function composition $n$ times, where the function is the state transformation that constitutes the body of the loop, and if $n$ is a Church numeral then that's simply applying $n$ itself to the loop body function.

Adding state to the language

An alternative approach to state is to extend the lambda calculus with state manipulation primitives. If you do that, the order of evaluation becomes important. In that case, a while loop can be expressed directly with recursion. $$ \mathsf{while}_{\text{imperative}} := \lambda C. \lambda B. \mathsf{fix} (\lambda f. \mathsf{if} \, C \, (B; f) \, ()) $$