$\lambda$-calculus, is there encoding of for or while? 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"?
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.