Upward confluence in the interaction calculus

The lambda calculus is not upward confluent, counterexamples being known for a long time. Now, what about the interaction calculus? Specifically, I am looking for configurations c1 and c2 that have the same normal form with no such c that c →* c1 and c →* c2.

Update: a necessary and sufficient condition for strong upward confluence discussed in arXiv:1806.07275v3 which also shows that the condition is not necessary for upward confluence by showing upward confluence for the interaction system of the linear lambda calculus.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Upward confluence

The property, I see, is that the reverse of the rewrite relation is Church-Rosser. Seems an interesting property, mathematically. Perhaps I'm being thick, but... Is it of practical significance?

Yes, it is indeed

Yes, it is indeed Church-Rosser "upside down". I am interested in that property for quite speculative reasons, but depending on the particular implications from (not) having it, I think that may turn out to be of some practical significance.