Upward confluence in the interaction calculus
Anton Salikhmetov
TL;DR
This paper explores upward confluence in the interaction calculus, establishing conditions for it and demonstrating that certain systems, like the linear lambda calculus, are upward confluent.
Contribution
It provides a necessary and sufficient condition for one-step upward confluence and shows that the linear lambda calculus system is upward confluent.
Findings
Interaction systems can be upward confluent.
The condition for one-step upward confluence is very restrictive.
Linear lambda calculus is upward confluent.
Abstract
The lambda calculus is not upward confluent, one of counterexamples known thanks to Plotkin. This paper investigates upward confluence in the interaction calculus. Can an interaction system have this property? We positively answer this question and also provide a necessary and sufficient condition for stronger one-step upward confluence which happens to be very restrictive. However, the provided condition is not necessary for upward confluence as we prove that the interaction system of the linear lambda calculus is upward confluent.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge