5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.