Looking at the striking parallels between combinatory logic and concatenative languages makes me wonder how many theorems of the former hold in the latter. The Church-Rosser theorem is particularly interesting because it would justify the use of transparent quotations. Is there any concatenative programming language proven to be Church-Rosser?

  • $\begingroup$ Note that usually programing languages involve a deterministic operational semantics (in the absence of threads), which makes the CR property trivial. $\endgroup$
    – cody
    Nov 17, 2014 at 16:36
  • $\begingroup$ Also: what do you mean by "transparent quotations"? $\endgroup$
    – cody
    Nov 17, 2014 at 16:37
  • $\begingroup$ By "transparent quotations" I meant quotations that allow internal rewriting (without being unquoted and applied to other quotations on the stack) in a concatenative programming language. It's also briefly discussed in the linked article. I do not quite understand your first comment. Could you point me to some further readings? $\endgroup$
    – user287393
    Nov 19, 2014 at 2:36
  • $\begingroup$ In my first comment, I was just mentioning that the operational semantics of programming languages are usually defined to allow only a single possible reduction at each step, e.g. rightmost-innermost weak-head reduction for the $\lambda$-calculus. In this situation, confluence is trivial since there is only one possible reduction at each step. $\endgroup$
    – cody
    Nov 19, 2014 at 15:29
  • $\begingroup$ I see. I was thinking of programming languages that allow more than one reduction paths. (e.g. Joy or Factor with transparent quotations.) But now that I think about it, Church-Rosser property in such languages might not make much practical difference. Reduction order-dependent procedures like I/O will contrict possible reductions, even if code evaluation is confluent. Lazy K might be an exception though. $\endgroup$
    – user287393
    Nov 22, 2014 at 8:44

1 Answer 1


SK combinators are Church-Rosser.

However, the usual $\lambda$-calculus method of proving local confluence and then appealing to Newman's lemma doesn't work. You need a slightly fancier argument, and the SEP entry on combinatory logic gives a sketch of a proof that does work.

  • 1
    $\begingroup$ Just a remark: I would not call Newman's lemma "the usual $\lambda$-calculus method". It doesn't work in the untyped case, which is where one usually proves confluence of the $\lambda$-calculus. It would work for the SK combinators if they were typed (with the usual types corrsponding to Hilbert's axiomatization of intuitionistic propositional logic). So the need for a "fancier" argument (e.g. the one given in the SEP, which is originally due to Tait and works in the untyped $\lambda$-calculus) does not come from being in the SK combinators but from being non-normalizing. $\endgroup$ Nov 17, 2014 at 17:35
  • $\begingroup$ Another (related technique) that proves confluence of SK is the very elegant parallel moves lemma (by Tait and per Martin-Löf, though there seems to be a small priority dispute). It's explained here: citeseerx.ist.psu.edu/viewdoc/summary?doi= $\endgroup$
    – cody
    Nov 18, 2014 at 15:39
  • $\begingroup$ I guess SK combinators could be considered a language in a theoretical sense, but I was wondering if there is an actual programming language (like, say, Unlambda) whose Church-Rosser property was proven. $\endgroup$
    – user287393
    Nov 19, 2014 at 2:42
  • $\begingroup$ @DamianoMazza: You're right! I have to admit that the only confluence proofs I've actually done are for typed systems using a logical relations argument. (I don't dispute the overkill involved -- it's just that it was a convenient way to get everything I wanted in one go, since I also wanted SN.) $\endgroup$ Nov 19, 2014 at 9:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.