Reduction semantics for a Calculus of Closures
_Reduction semantics for a Calculus of Closures_
David Van Horn
This is a PLT Redex formulation of the applicative order reduction
strategy for the _lambda-rho-hat_ calculus, an extension of Curien's
calculus of _closures_, lambda rho, that allows for one-step reduction
to be expressed.
The reference for this work is Section 2.2 and 2.4 of A Concrete
Framework for Environment Machines, Magorzata Biernacka and Olivier
(Note that this uses de Bruijn indices-- variables are represented by
natural numbers and a substitution (an environment) is a list of values.
A variable's number gives the index into the list for value to which it
is bound. Environment extension is just cons.)
See examples.ss to trace a few example expressions in the language.