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$
$\endgroup$
-
$\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 '14 at 16:36
-
$\begingroup$ Also: what do you mean by "transparent quotations"? $\endgroup$ – cody Nov 17 '14 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 '14 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 '14 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 '14 at 8:44
$\begingroup$
$\endgroup$
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.
answered Nov 17 '14 at 9:29
-
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$ – Damiano Mazza Nov 17 '14 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=10.1.1.42.7565 $\endgroup$ – cody Nov 18 '14 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 '14 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$ – Neel Krishnaswami Nov 19 '14 at 9:26
