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