adbmal

We make the notion of scope in the -calculus explicit. To that end, the syntax of the -calculus is extended with an end-of-scope operator , matching the usual opening of a scope due to . Accordingly, -reduction is extended to the set of scoped -terms by performing minimal scope extrusion before performing replication as usual. We show confluence of the resulting scoped -reduction. Confluence of -reduction for the ordinary -calculus is obtained as a corollary, by extruding scopes maximally before forgetting them altogether. Only in this final forgetful step, -equivalence is needed. All our proofs have been verified in Coq.

• Type: Conference
• Year: 2003
• Where: CADE
• Authors: Dimitri Hendriks, Vincent van Oostrom
• Keywords: Automated Reasoning, CADE 2003, End-of-scope Operator, Final Forgetful Step, Minimal Scope Extrusion