Talk:S and K Turing-completeness proof
This article aims to show that S and K combinators are Turing-complete but only shows a way to convert a lambda expression into combinators. Can someone explain why this is already enough? Why is there no need for prooving the equivalence of the reduction rules and that the reduced expression can be translated back into lambda calculus resulting in an equally simple expression as direct reduction in lambda calculus would give? --(this comment by 109.192.148.158 at 20:09, 27 March 2013 UTC; please sign your comments with ~~~~)
- You have a point there. For now, I added a short note about it. --Ørjan (talk) 23:24, 27 March 2013 (UTC)
- Ugh, yes this isn't sufficient at all. To make the translation work, we need to relate computations by a simulation lemma: if M ->* N in the lambda calculus, then [M] ->* [N] in combinatory logic, or at least the two terms need to be equivalent (allowing some backward steps). The question whether [.] is bijective is mostly a red herring. The only important bit is that [.] isn't constant. For example, it distinguishes [λt f.t] = K from [λt f.f] = KI. --Int-e (talk) 20:04, 6 February 2026 (UTC)
I've augmented the relevant section of combinatory logic to inline the bracket expansion; it's fairly short and doesn't require the ceremony of a standalone article. The Turing-completeness there is wholly syntactic; given the set of SKI terms, the subset of terms which don't normalize is undecidable. This page could be replaced with a more complete exploration of evaluation ordering, perhaps. Corbin (talk) 18:06, 2 April 2025 (UTC)
This is not actually a bijection. In particular, the λx.fx → f & f → λx.fx rules mean we can, by applying the transformation and its inverse, end up with distinct terms (though they may be η-equivalent). It's possible this is a bijection given a precise definition of `constant function f`, but as it stands I'm not personally convinced. Also, I believe this transformation is not well-defined, since it's only defined for λ-abstractions. For example, it seems to me that [λxy.yx] (which is shorthand for [λx.(λy.yx)]) is not well-defined, unless we consider [λy.yx] a `constant` or `constant function`.
--Iacgm (talk) 19:12, 6 February 2026 (UTC)
- This is good food for thought. I'll have to think about your first objection for a bit. For the second part, the given bracket is missing a case. It's not clear how to fix this, though. We should probably replace it with a proven bracket from a reputable paper instead. Corbin (talk) 19:21, 6 February 2026 (UTC)
- I see no reason to consider λy.yx a constant function since the expression inside lambda (yx) depends on lambda argument (y). --Blashyrkh (talk) 19:25, 6 February 2026 (UTC)