All traditional implementation techniques for functional languages fail to avoid useless repetition of work. They are not optimal in their implementation of sharing, often causing a catastrophic, exponential explosion in reduction time. Optimal reduction is an innovative graph reduction technique for functional expressions, introduced by Lamping in 1990, that solves the sharing problem. This work, the first on the subject, is a comprehensive account by two of its leading exponents. Practical implementation aspects are fully covered as are the mathematical underpinnings of the subject. The relationship to the pioneering work of L�vy and to Girard's more recent Geometry of Interaction are explored; optimal reduction is thereby revealed as a prime example of how a beautiful mathematical theory can lead to practical benefit. The book is essentially self-contained, requiring no more than basic familiarity with functional languages. It will be welcomed by graduate students and research workers in lambda calculus, functional programming or linear logic.
Author(s): Andrea Asperti; Stefano Guerrini
Publisher: Cambridge University Press
Year: 1998
Language: English
Pages: 408
1 Introduction
1.0.1 How to read this book
2 Optimal Reduction
2.1 Some Sharing mechanisms
2.1.1 Wadsworth's technique
2.1.2 Combinators
2.1.3 Environment Machines
2.2 Sharing graphs
2.2.1 Graph rewriting
2.2.2 Read-back and Semantics
3 The full algorithm
3.1 Pairing fans
3.2 Sharing Graphs
3.3 The initial encoding of λ-terms
3.4 Lamping's paths
3.4.1 Contexts and proper paths
3.5 Correctness of the algorithm
3.5.1 Properties of sharing graphs
3.5.2 Correspondence between sharing graphs and λ-terms
3.5.3 Expanded proper paths
3.5.4 Proof of Theorem 3.5.15 (correctness)
3.5.5 Proof of Lemma 3.5.17 (properties of expanded proper paths)
3.5.6 Proof of the sharing graph properties
4 Optimal Reductions and Linear Logic
4.1 Intuitionistic Linear Logic
4.2 The "!" modality
4.2.1 Boxes
4.2.2 A Remark for Categoricians
4.3 The duplication problem
5 Redex Families and Optimality
5.1 Zig-Zag
5.1.1 Permutation equivalence
5.1.2 Families of redexes
5.2 Extraction
5.2.1 Extraction and families
5.3 Labeling
5.3.1 Confluence and Standardization
5.3.2 Labeled and unlabeled λ-calculus
5.3.3 Labeling and families
5.4 Reduction by families
5.4.1 Complete derivations
5.5 Completeness of Lamping's algorithm
5.6 Optimal derivations
6 Paths
6.1 Several definitions of paths
6.2 Legal Paths
6.2.1 Reminder on labeled λ-calculus
6.2.2 Labels and paths
6.2.3 The equivalence between extraction and labeling
6.2.4 Well balanced paths and legal paths
6.2.5 Legal paths and redex families
6.2.6 Legal paths and optimal reductions
6.3 Consistent Paths
6.3.1 Reminder on proper paths
6.3.2 Consistency
6.4 Regular Paths
6.4.1 The Dynamic Algebra ℒ?
6.4.2 A model
6.4.3 Virtual Reduction
6.5 Relating Paths
6.5.1 Discriminants
6.5.2 Legal paths are regular and vice-versa
6.5.3 Consistent paths are regular and vice-versa
6.6 Virtual interactions
6.6.1 Residuals and ancestors of consistent paths
6.6.2 Fan annihilations and cycles
7 Read-back
7.1 Static and dynamic sharing
7.1.1 Grouping sequences of brackets
7.1.2 Indexed λ-trees
7.1.3 Beta rule
7.1.4 Multiplexer
7.2 The propagation rules
7.2.1 Mux interactions
7.2.2 Mux propagation rules
7.2.3 The absorption rule
7.2.4 Redexes
7.3 Deadlocked redexes
7.3.1 Critical pairs
7.3.2 Mux permutation equivalence
7.4 Sharing morphisms
7.4.1 Simulation lemma
7.5 Unshared beta reduction
7.6 Paths
7.7 Algebraic semantics
7.7.1 Left inverses of lifting operators
7.7.2 The inverse semigroup LSeq*
7.8 Proper paths
7.8.1 Deadlock-freeness and properness
7.9 Soundness and adequateness
7.10 Read-back and optimality
8 Other translations in Sharing Graphs
8.1 Introduction
8.2 The bus notation
8.3 The bus notation of the translation ℱ
8.4 The correspondence of ℱ and ?
8.5 Concluding remarks
9 Safe Nodes
9.1 Accumulation of control operators
9.2 Eliminating redundant information
9.3 Safe rules
9.4 Safe Operators
9.5 Examples and Benchmarks
10 Complexity
10.1 The simply typed case
10.1.1 Typing Lamping's rules
10.1.2 The η-expansion method
10.1.3 Simulating generic elementary-time bounded computation
10.2 Superposition and higher-order sharing
10.2.1 Superposition
10.2.2 Higher-order sharing
10.3 Conclusions
11 Functional Programming
11.1 Interaction Systems
11.1.1 The Intuitionistic Nature of Interaction Systems
11.2 Sharing Graphs Implementation
11.2.1 The encoding of IS-expressions
11.2.2 The translation of rewriting rules
12 The Bologna Optimal Higher-order Machine
12.1 Source Language
12.2 Reduction
12.2.1 Graph Encoding
12.2.2 Graph Reduction
12.3 Garbage Collection
12.3.1 Implementation Issues
12.3.2 Examples and Benchmarks
12.4 Problems
12.4.1 The case of "append"
Bibliography
