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