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 $c_1$ and $c_2$ such that $\exists c: c_1 \rightarrow^* c\ \wedge\ c_2 \rightarrow^* c$, but $\nexists c': c' \rightarrow^* c_1\ \wedge\ c' \rightarrow^* c_2$.

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.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.