# Church-Rosser equivalent for concatenative languages?

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?

• Note that usually programing languages involve a deterministic operational semantics (in the absence of threads), which makes the CR property trivial.
– cody
Nov 17, 2014 at 16:36
• Also: what do you mean by "transparent quotations"?
– cody
Nov 17, 2014 at 16:37
• 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? Nov 19, 2014 at 2:36
• 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.
– cody
Nov 19, 2014 at 15:29
• 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. Nov 22, 2014 at 8:44

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.
• 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. Nov 17, 2014 at 17:35