## User login## Navigation |
## adbmaL
... or how is the title of this paper pronounced?
We make the notion of scope in the lambda-calculus explicit. To that end, the syntax of the lambda-calculus is extended with an end-of-scope operator [adbmal], matching the usual opening of a scope due to lambda. Accordingly, beta-reduction is extended to the set of scoped lambda-terms by performing minimal scope extrusion before performing replication as usual. We show confluence of the resulting scoped beta-reduction. Confluence of beta-reduction for the ordinary lambda-calculus is obtained as a corollary, by extruding scopes maximally before forgetting them altogether. Only in this final forgetful step, alpha-equivalence is needed. All our proofs have been verified in Coq.While playing with my own lambda-machine (derivative of CEK in Java) I decided that I would like to control scope better - so I found this paper. See also Lambdascope previously mentioned on LtU. |
## Browse archives## Active forum topics |

## Recent comments

3 hours 49 min ago

7 hours 3 min ago

9 hours 6 min ago

1 day 1 hour ago

1 day 2 hours ago

1 day 2 hours ago

1 day 2 hours ago

1 day 4 hours ago

1 day 7 hours ago

1 day 9 hours ago