Lambda calculus: composition of SKI

Question

I am doing some exercises on writing a lambda term as a composition of the terms: S=$\lambda$xyz.xz(yz), K=$\lambda$xy.y, I=$\lambda$x.x. I know that all lambda terms can be written using S K and I with the following rules: 0) $\lambda$x.Fx=F 1)$\lambda$x.x=I 2)$\lambda$x.F=KF if x is not in F, 3)$\lambda$x.FL=S($\lambda$x.F)($\lambda$x.L) if x is in F and in L. I did some exercises with simple $\lambda$-terms, but when it comes up with more complicated ones I have difficulties. For example, what if the $\lambda$-term is of the kind $\lambda$xyz. LF and in L or in F there is abstraction? For example $\lambda$xyz.x(zy($\lambda$x.xz)). Shall I first write the inner abstraction ($\lambda$x.xz) as a combination of SKI and then go on? Is it correct that since in this abstraction x comes before z I can't apply rule 0)?

Answer 1

If you want to write a $\lambda$-term as a product in the $SKI$-combinators (up to $\alpha\beta\eta$-equivalence), you can think of realizing, in an arbitrary context of finitely many unbound variables, an arbitrary function in a single bound variable through of the following three basic functions: the identity function $I$, the constant function $K c$ on a value $c$, and the function $S p q$ realizing the termwise product of the functions realized by $p$ and $q$.

For this, first check if the output of your function is independent on the argument, or if it is the argument itself, or if it is a product of two terms, and use $I$, $K$ or $S$ in these cases, respectively. If none of these three rules apply, the output of your function is itself a function, i.e. a $\lambda$-abstraction in some new variable. In this case, put your current variable on the stack of constant/unbound variables and first realize the function in the new, bound variable. Afterwards, when this inner function is realized as a product in the $SKI$-combinators, proceed to realize your original function using the first three rules.

Your example of the $\lambda$-term $\lambda x y z. x(zy(\lambda x.xz)))$. In the beginning, you have neither bound nor unbound variables, but your constant value is a function in the variable $x$. So make $x$ the 'active' variable and try to realize $\lambda y z. x(zy(\lambda x.xz))$. Again we meet a function abstraction in $y$, so make $y$ the active variable while considering $x$ constant. Then again, make $z$ active and consider $y$ constant, which leaves you with the problem of realizing $z\mapsto x(zy(\lambda x.xz))$. Here the $S$-rule applies several times, realizing the function as $S(Kx)(S(SI(Ky))t)$, where $t$ is the still to be found term realizing $z\mapsto \lambda x.xz$. Here again, you meet an abstraction, which you wlog rename to $\lambda w.wz$, and play the same game to realize the inner function $w\mapsto wz$ as $SI(Kz)$. Hence, $z\mapsto \lambda x.xz\sim SI(Kz)=(SI)(Kz)$ is realized by $t = S(K(SI))(S(KK)I)$, so $z\mapsto x(zy(\lambda x.xz))$ is realized by $S(Kx)(S(SI(Ky))(S(K(SI))(S(KK)I)))$ I hope it's clear now how you would, in principle, do the remaining abstraction from $x$ and $y$.

Answer 2

You should work out the inner abstractions first, as the translation from $\lambda$-terms to $SKI$ clearly specifies. For completeness sake, allow me to present the said translation more formally below.

Let $\Lambda$ be the set of $\lambda$-terms, as defined by $$ M,N ::= x\ |\ (MN)\ |\ (\lambda x M)$$ and $\mathcal{C}$ the set of $SKI$-terms, as defined by $$ F, G ::= x\ |\ (FG)\ |\ \textbf{S}\ |\ \textbf{K}\ |\ \textbf{I}$$

Define the translation $(\cdot)_{\mathcal{C}}: \Lambda\rightarrow\mathcal{C}$ recursively as:

• $x_{\mathcal{C}} = x$
• $(MN)_{\mathcal{C}} = (M_\mathcal{C}N_\mathcal{C})$
• $(\lambda xM)_{\mathcal{C}} = (\lambda^*x M_\mathcal{C})$

where, for every $F\in\mathcal{C}$ and every $x$ variable, $\lambda^*x F \in\mathcal{C}$ is the meta-term given according to the following clauses (the algorithm abcf):

• a) $\lambda^*xF = \textbf{I}$, if $F=x$
• b) $\lambda^*xF = \textbf{K}F$, if $x\not\in FV(F)$
• c) $\lambda^*xF = G$, if $F=Gx$ and $x\not\in FV(G)$
• f) $\lambda^*xF = \textbf{S}(\lambda^*x G_1)(\lambda^*x G_2)$, if $F=(G_1G_2)$ and neither (b) nor (c) applies.

Notice the equation $(\lambda xM)_{\mathcal{C}} = (\lambda^*xM_{\mathcal{C}})$: it clearly tells us to work out the inner abstractions first. By the way, you may also remove the (c) clause from the definition of $\lambda^*xF$.