## 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

1 hour 41 min ago

2 hours 27 min ago

2 hours 27 min ago

8 hours 40 min ago

9 hours 3 min ago

9 hours 22 min ago

11 hours 50 min ago

22 hours 12 min ago

1 day 9 min ago

1 day 7 hours ago