4
$\begingroup$

Consider combinatory calculi that don't have tail reduction. So there may be combinators $x$, $y$ and $z$ such that $y\to z$ but $xy\nrightarrow xz$. We can still write every combinator as a combination of the following four: $\mathbf bxyz\to x(yz)$, $\mathbf cxyz\to (xz)y$, $\mathbf kxy\to x$, $\mathbf wxy \to (xy)y$. The usual $\mathbf{bckw}$-calculus in other words.

Let $\mathbf sxyz \to xz(yz)$. Now $\mathbf b = \mathbf s(\mathbf{ks})\mathbf k$, but I can't find combinations for $\mathbf c$ and $\mathbf w$. It appears that without tail reduction, the $\mathbf{ks}$-basis is no longer complete (no longer a basis). Do you know a proof for this, or are $\mathbf c$ and $\mathbf w$ definable in terms of $\mathbf k$ and $\mathbf s$?

  • 0
    You might be interested in JW Klop's "Reduction Cycles in Combinatory Logic" (http://web.mac.com/janwillemklop/Site/Bibliography_files/10.RCCL.PDF). He doesn't deal directly with head-only-reduction, but I think some of the proof techniques might help you.2012-05-25

1 Answers 1

1

For $\bf W$, for example, the usual construction gives something like $\begin{align} {\bf W} =& \lambda x.\lambda y.(x y) y \\ =& \lambda x. {\bf S}\, x\, {\bf I} \\ =& {\bf S\, S\, (K\, I)} \\ =& {\bf S\, S\, (K\, (S\, K\, K))} \end{align}$ The only question, I think, is whether this simulates $\bf W$ well enough for your purpose. We have at least $\tag{*} {\bf S\, S\, (K\, (S\, K\, K))}\,M\, N \to^* (M\,N)\, ({\bf K\, (S\, K\, K)}\, M\, N)$ It is true that with a strict head-only reduction strategy, you don't immediately get to reduce ${\bf K\, (S\, K\, K)}\, M\, N \to^* M$ But is that actually a problem? If we're working in a pure combinator calculus, $M$ will always be some concrete term, which is now ready to reduce. Eventually ${\bf K\, (S\, K\, K)}\, M\, N$ will either end up in a head position and get reduced, or disappear, in which case it doesn't matter anyway.

For every concrete $M$ and $N$ it holds that ${\bf S\, S\, (K\, (S\, K\, K))}\,M\, N$ has the same normal form (if any) as $(M\,N)\,N$. That will be sufficient for most purposes I can imagine -- unless you're insisting on a bisimulation between $\bf \{BCKW\}$ and $\bf \{SK\}$ (but why would you? Bisimilarity is a tool for showing observational equivalence; if you can get that by other means, what have you lost?)

Edit: Hmm, that doesn't quite hold. It might be that $M$ is just $\bf S$, and then it still has too few arguments to reduce on the right-hand side of (*). We may have to settle for observational equivalence, where ${\bf W}\,M\,N\,P_1\ldots P_n$ has a normal form exactly when $M\,N\,N\, P_1\ldots P_n$ has, for all $n\ge 1$.

  • 0
    How do we know that there is no better construction for $\mathbf w$?2012-03-22