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)

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)