## 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 day 17 hours ago

1 day 21 hours ago

2 days 14 hours ago

1 week 1 day ago

1 week 1 day ago

1 week 3 days ago

1 week 5 days ago

3 weeks 14 hours ago

3 weeks 23 hours ago

3 weeks 1 day ago