2
$\begingroup$

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)?

$\endgroup$
2
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.