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

9 hours 25 min ago

11 hours 25 min ago

17 hours 19 min ago

1 day 10 hours ago

1 day 19 hours ago

2 days 5 hours ago

2 days 7 hours ago

2 days 7 hours ago

2 days 8 hours ago

2 days 8 hours ago