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?
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.