Paper Info
Title
A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi
Abstract
This paper concerns the explicit treatment of substitutions in the lambda calculus. One of its contributions is the simplification and rationalization of the suspension calculus that embodies such a treatment. The earlier version of this calculus provides a cumbersome encoding of substi- tution composition, an operation that is important to the ecient realization of reduction. This encoding is simplified here, resulting in a treatment that is easy to use directly in applications. The rationalization consists of the elimination of a practically inconsequential flexibility in the unravelling of substitutions that has the inadvertent side eect of losing contextual information in terms; the modified calculus now has a structure that naturally supports logical analyses, such as ones related to the assignment of types, over lambda terms. The overall calculus is shown to have pleasing theoretical properties such as a strongly terminating sub-calculus for substitution and confluence even in the presence of term meta variables that are accorded a grafting interpre- tation. Another contribution of the paper is the identification of a broad set of properties that are desirable for explicit substitution calculi to support and a classification of a variety of proposed systems based on these. The suspension calculus is used as a tool in this study. In particular, mappings are described between it and the other calculi towards understanding the characteristics of the latter.
Year
Venue
Keywords
2007
Clinical Orthopaedics and Related Research
additional key words and phrases: lambda calculus,higher-order abstract syntax,term rewriting,metalanguages,explicit substitutions,lambda calculus
Field
DocType
Volume
Deductive lambda calculus,Discrete mathematics,Typed lambda calculus,Simply typed lambda calculus,Natural deduction,Algorithm,Explicit substitution,Director string,Pure type system,Process calculus,Mathematics,Calculus
Journal
abs/cs/070
Citations 
PageRank 
References 
0
0.34
20
Authors
2
Name
Order
Citations
PageRank
Andrew Gacek125216.87
Gopalan Nadathur21047117.85