doc.txt

Reduction semantics for a Calculus of Closures

_Reduction semantics for a Calculus of Closures_
_closure-calculus_

David Van Horn
<dvanhorn@cs.brandeis.edu>

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 
Danvy.

   http://www.brics.dk/RS/06/3/

(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.