<p>SK combinators are Church-Rosser. </p>

<p>However, the usual  $\lambda$-calculus method of proving local confluence and then appealing to <a href="http://en.wikipedia.org/wiki/Newman%27s_lemma">Newman's lemma</a> doesn't work. You need a slightly fancier argument, and the <a href="http://plato.stanford.edu/entries/logic-combinatory/#2.2">SEP entry on combinatory logic</a> gives a sketch of a proof that does work. </p>

CC BY-SA 3.0
2014-11-17T17:35:22.873Z
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.
Damiano Mazza
CC BY-SA 3.0
2014-11-18T15:39:27.387Z
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: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.7565
cody
CC BY-SA 3.0
2014-11-19T02:42:36.243Z
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.
user287393
CC BY-SA 3.0
2014-11-19T09:26:02.467Z
@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.)
Neel Krishnaswami
CC BY-SA 3.0
2014-11-17T09:29:18.930Z
2014-11-17T09:29:18.930Z
Neel Krishnaswami
<p>Looking at the <a href="http://tunes.org/~iepos/joy.html">striking parallels between combinatory logic and concatenative languages</a> 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? </p>

CC BY-SA 3.0
2014-11-17T16:36:28.273Z
Note that usually *programing languages* involve a deterministic operational semantics (in the absence of threads), which makes the CR property trivial.
cody
CC BY-SA 3.0
2014-11-17T16:37:14.690Z
Also: what do you mean by "transparent quotations"?
cody
CC BY-SA 3.0
2014-11-19T02:36:31.953Z
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?
user287393
CC BY-SA 3.0
2014-11-19T15:29:11.760Z
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
CC BY-SA 3.0
2014-11-22T08:44:20.327Z
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](http://homepages.cwi.nl/~tromp/cl/lazy-k.html) might be an exception though.
user287393
<lambda-calculus><combinatory-logic>
Church-Rosser equivalent for concatenative languages?
user287393
# Church-Rosser equivalent for concatenative languages?

(Asked by: username_0 on 2014-11-17)

Looking at the [striking parallels between combinatory logic and concatenative languages](http://tunes.org/~iepos/joy.html) 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?

**Tags:** lambda-calculus, combinatory-logic

> **Comments:**
> **username_1**: Note that usually *programing languages* involve a deterministic operational semantics (in the absence of threads), which makes the CR property trivial.  
> **username_1**: Also: what do you mean by "transparent quotations"?  
> **username_0**: 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?  
> **username_1**: 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.  
> **username_0**: 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](http://homepages.cwi.nl/~tromp/cl/lazy-k.html) might be an exception though.  

---

## 1 answers

### Answer by username_2 on 2014-11-17. Score: 6

SK combinators are Church-Rosser.

However, the usual $\lambda$-calculus method of proving local confluence and then appealing to [Newman's lemma](http://en.wikipedia.org/wiki/Newman%27s_lemma) doesn't work. You need a slightly fancier argument, and the [SEP entry on combinatory logic](http://plato.stanford.edu/entries/logic-combinatory/#2.2) gives a sketch of a proof that does work.

> **Comments:**
> **username_3**: 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.  
> **username_1**: 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: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.7565  
> **username_0**: 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.  
> **username_2**: @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.)  

---

