Lambda Calculus factorial I have a few exercises for my study subject computability theory. One of this is:
Please, write term for function $f(n) = n!$
I don't know how start doing it. Maybe someone can help with this example or maybe someone can send me where in net I can find material for this topic.
 A: If we exploit the iteration that we get for free from the Church numerals, we don't need to do our own fixpoints, so we can get through a lot easier than DanielV's solution.
If we create a function $F$ such that
$$ \underbrace{F(F(\cdots(F}_n (1,1))\cdots)) = (n+1,n!) $$
then the factorial of $k$ is the second element of the pair that results from $k\; F\; (1,1)$
The standard representation of the ordered pair $(A,B)$ is $\lambda g.g A B$,
so this means that
$$ ! = \lambda k. k\;F\;(\lambda g.g\,1\,1)\;(\lambda ab.b) $$
So we need to define $F$. It must satisfy the definition (in ordinary arithmetic notation)
$$ F(a,b) = (a+1, a\times b) $$
which we can translate directly to lambda notation using known successor and multiplication constructions for Church numerals as
$$ F = \lambda p.p (\lambda a b g. g \; (\lambda f x.f(afx))\; (\lambda f.a(bf))) $$
Now all there is left is to expand the definitions of  $F$ and $1$, and we get
$$ ! = \lambda k. k
 \; \Bigl(\lambda p.p\bigl(\lambda abg.g\;\bigl(\lambda fx.f(afx)\bigr)\;\bigl(\lambda f.a(bf)\bigr)\bigr)\Bigr)
 \; \bigl(\lambda g.g\, (\lambda h.h)\, (\lambda h.h)\bigr)
 \; \bigl(\lambda ab.b\bigr)
$$

Using this technique we can write any primitive recursive function -- or, in programming terms, every FOR program -- in a quite natural way without ever using an explicit fixpoint combinator. In contrast to the recursion schema DanielV uses, the results will be typable in System F.
A: So a factorial is:
$$n! = \text{ if } (n \leq 1) \text{ then } 1 \text{ else } n \times (n - 1)!$$
or in prefix form:
$$!n = \leq n 1 1 (\times n (! (- n 1)))$$
A lambda calculus expression satisfying
$$Fx \triangleright Jx ( F (P x) )$$
is
$$F  = \langle y, \langle G x, Jx ( G (P x) ) \rangle  y^2\rangle ^2$$
(using $a^2$ to represent $(aa)$).  Here $J$ represents your sentinal conditions, value, and wrapper around the recursive return, and $P$ represents the predecessor function.  So translating $\leq x 1 1 (\times n ! (- n 1))$ into  $Jn ( F (P n) )$ you get
$J = \langle n r, \leq n 1 1 (\times n r)\rangle $
So altogether, you get:
$$\begin{align}
! &= \langle y, \langle G n, Jn ( G (P n) ) \rangle  y^2\rangle ^2   
\\&= \langle y, \langle G n, \langle n r, \leq n 1 1 (\times n r)\rangle n ( G (P n) ) \rangle  y^2\rangle ^2
\\&= \langle y, \langle G n, \leq n 1 1 (\times n ( G (P n) )) \rangle  y^2\rangle ^2  
\end{align}$$
Now to look up the church encoding https://en.wikipedia.org/wiki/Church_encoding of $1$, $\leq$, $\times$, and $P$:
$$\begin{align}
     1 & = \langle f x, fx\rangle                                                                    \\
\times & = \langle m n f, m(nf)\rangle                                                               \\
     P & = \langle nfx, n\langle g h, h(gf)\rangle  \langle u,x\rangle \langle u,u\rangle \rangle    \\
  \leq & = \langle m n, Z (- m n)\rangle                                                             \\
     Z & = \langle n, n \langle x, \bot \rangle  \top \rangle                                         \\
 \bot  & = \langle a b, b\rangle                                                                     \\
  \top  & = \langle a  b, a\rangle                                                                    \\
     - & = \langle m n, n P m\rangle                                                                 \\
\end{align}$$
So putting it all together:
$$\begin{array} {rcl}
 ! &=& \langle y, \langle G n, \leq n 1 1 (\times n ( G (P n) )) \rangle  y^2\rangle ^2  
\\ &=& \langle y, \langle G n, \langle m n, Z (- m n)\rangle  n 1 1 (\times n ( G (P n) )) \rangle  y^2\rangle ^2  
\\ &=& \langle y, \langle G n, Z (- n 1) 1 (\times n ( G (P n) )) \rangle  y^2\rangle ^2  
\\ &=& \langle y, \langle G n, Z (Pn) 1 (\times n ( G (P n) )) \rangle  y^2\rangle ^2  
\\ &=& \langle y, \langle G n, \langle n, n \langle x, \bot \rangle  \top \rangle  (P n) 1 (\times n ( G (P n) )) \rangle  y^2\rangle ^2  
\\ &=& \langle y, \langle G n, P n \langle x, \bot \rangle  \top  1 (\times n ( G (P n) )) \rangle  y^2\rangle ^2  
\\ &=& \langle y, \langle G n, P n \langle x, \langle a b, b\rangle \rangle  \langle a  b, a\rangle  1 (\times n ( G (P n) )) \rangle  y^2\rangle ^2  
%
\\ &=& \left \langle y, \left \langle G n, \begin{array} {l}
\langle nfx, n\langle g h, h(gf)\rangle  \langle u,x\rangle \langle u,u\rangle \rangle  n \langle x, \langle a b, b\rangle \rangle  \langle a  b, a\rangle  1 \\
(\times n ( G (\langle nfx, n\langle g h, h(gf)\rangle  \langle u,x\rangle \langle u,u\rangle \rangle  n) )) 
\end{array} \right\rangle  y^2 \right\rangle ^2  
%
\\ &=& \left \langle y, \left \langle G n,  \begin{array} {l}
n\langle g h, h(g\langle x, \langle a b, b\rangle \rangle )\rangle  \langle u,\langle a  b, a\rangle \rangle \langle u,u\rangle  1 \\
(\times n ( G (\langle fx, n\langle g h, h(gf)\rangle  \langle u,x\rangle \langle u,u\rangle \rangle ) )) 
\end{array}\right\rangle  y^2\right\rangle ^2  
%
\\ &=& \left \langle y, \left \langle G n, \begin{array} {l}
n\langle g h, h(g\langle x, \langle a b, b\rangle \rangle )\rangle  \langle u,\langle a  b, a\rangle \rangle \langle u,u\rangle  1 \\
(\langle m n f, m(nf)\rangle  n ( G (\langle f x, n\langle g h, h(gf)\rangle  \langle u,x\rangle \langle u,u\rangle \rangle ) )) 
\end{array}\right \rangle  y^2\right\rangle ^2  
%
\\ &=& \left \langle y, \left \langle G n, \begin{array} {l}
n\langle g h, h(g\langle x, \langle a b, b\rangle \rangle )\rangle  \langle u,\langle a  b, a\rangle \rangle \langle u,u\rangle  1 \\
 (\langle f, n( G (\langle fx, n\langle g h, h(gf)\rangle  \langle u,x\rangle \langle u,u\rangle \rangle )       f)\rangle  ) 
\end{array}\right \rangle  y^2 \right\rangle ^2  
%
\\ &=& \left \langle y, \left \langle G n, \begin{array} {l}
n\langle g h, h(g\langle x, \langle a b, b\rangle \rangle )\rangle  \langle u,\langle a  b, a\rangle \rangle \langle u,u\rangle  \langle f x, f x\rangle \\
 (\langle f, n( G (\langle f x, n\langle g h, h(gf)\rangle  \langle u,x\rangle \langle u,u\rangle \rangle )  f)\rangle  ) 
\end{array}\right\rangle  y^2 \right \rangle ^2  
%
\\ &=& 
\left \langle y, \left \langle G n, \begin{array} {l}
n\langle g h, h(g\langle x, \langle a b, b\rangle \rangle )\rangle  \langle u,\langle a  b, a\rangle \rangle \langle u,u\rangle  \langle f x, f x\rangle \\
 (\langle f, n( G (\langle f x, n\langle g h, h(gf)\rangle  \langle u,x\rangle \langle u,u\rangle \rangle )  f)\rangle  ) 
\end{array}\right\rangle  (yy) \right \rangle  \\
%
& &\left \langle y, \left \langle G n, \begin{array} {l}
n\langle g h, h(g\langle x, \langle a b, b\rangle \rangle )\rangle  \langle u,\langle a  b, a\rangle \rangle \langle u,u\rangle  \langle f x, f x\rangle \\
 (\langle f, n( G (\langle f x, n\langle g h, h(gf)\rangle  \langle u,x\rangle \langle u,u\rangle \rangle )  f)\rangle  ) 
\end{array}\right\rangle  (yy) \right \rangle   
%
\end{array}$$
And that is the complete unabstracted lambda expression representing a factorial with church encoding.  
