This paper recounts the origins of the λx family of calculi of explicit substitution with proper variable names, including the original result of preservation of strong β-normalization based on the use of special reductions for garbage collection. We then discuss the properties of a variant of the calculus which is also confluent for “open” terms (with meta-variables), and verify that a version with garbage collection preserves strong β-normalization (as is the state of the art). Finally, we summarize the relationship with other efforts on using names and garbage collection rules in explicit substitution.
This paper is an expanded version of the journal paper.
By: Kristoffer H. Rose; Roel Bloo; Frédéric Lang
Published in: RC24909 in 2009
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .