Home » forums » LtU Forum

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.

By Anton Salikhmetov at 2018-06-19 08:56 | LtU Forum | previous forum topic | next forum topic | other blogs | 3135 reads

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?

By John Shutt at Tue, 2018-07-03 01:31 | login or register to post comments

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.

By Anton Salikhmetov at Tue, 2018-07-03 10:36 | login or register to post comments