Submitted by Roger Hindley
Date: Known since 1958!
Statement. Is there a direct proof of the conﬂuence of -strong reduction?
Problem Origin. First posed by Haskell Curry and Roger Hindley.
The -strong reduction is the combinatory analogue of -reduction in -calculus. It is conﬂuent. Its only known conﬂuence-proof is very easy, [Curry and Feys, 1958, 6F, p. 221 Theorem 3], but it depends on the having already proved the conﬂuence of -reduction. Thus the theory of combinators is not self-contained at present. Is there a conﬂuence proof independent of -calculus?
Warning: Like a bog, the theory of strong reduction is messier than it looks at ﬁrst; see [Curry and Feys, 1958, 6F], [Curry et al., 1972, 11E], [Hindley and Seldin, 1986, Ch. 9], and sources cited therein.
Solution: Two independent conﬂuence proofs have been proposed in June 2008: one by René David [David, 2009], the other by Pierluigi Minari [Minari, 2009].