The Optimal Implementation of Functional Programming Languages Andrea Asperti Stefano Guerrini Contents 1 Introduction page 7 1.0.1 How to read this book 10 2 OptimalReduction 14 2.1 Some Sharing mechanisms 20 2.1.1 Wadsworth’s technique 20 2.1.2 Combinators 22 2.1.3 Environment Machines 25 2.2 Sharing graphs 26 2.2.1 Graph rewriting 27 2.2.2 Read-back and Semantics 35 3 The fullalgorithm 40 3.1 Pairing fans 42 3.2 Sharing Graphs 46 3.3 The initialencoding of (cid:21)-terms 48 3.4 Lamping’spaths 50 3.4.1 Contexts and proper paths 53 3.5 Correctness of the algorithm 58 3.5.1 Properties of sharing graphs 60 3.5.2 Correspondence between sharing graphs and (cid:21)-terms 68 3.5.3 Expanded proper paths 71 3.5.4 Proof of Theorem 3.5.15(correctness) 74 3.5.5 Proof of Lemma3.5.17 (properties of expanded proper paths) 79 3.5.6 Proof of the sharing graph properties 81 4 OptimalReductions and Linear Logic 82 4.1 Intuitionistic Linear Logic 83 4.2 The \!" modality 87 4.2.1 Boxes 89 3 4 Contents 4.2.2 A Remark for Categoricians 90 4.3 The duplication problem 93 5 Redex Familiesand Optimality 96 5.1 Zig-Zag 97 5.1.1 Permutation equivalence 99 5.1.2 Familiesof redexes 104 5.2 Extraction 106 5.2.1 Extraction and families 109 5.3 Labeling 113 5.3.1 Con(cid:13)uence and Standardization 116 5.3.2 Labeled and unlabeled (cid:21)-calculus 127 5.3.3 Labeling and families 130 5.4 Reduction by families 132 5.4.1 Complete derivations 135 5.5 Completeness of Lamping’salgorithm 137 5.6 Optimalderivations 146 6 Paths 149 6.1 Several de(cid:12)nitions of paths 150 6.2 Legal Paths 152 6.2.1 Reminder on labeled (cid:21)-calculus 156 6.2.2 Labels and paths 158 6.2.3 The equivalence between extraction and labeling 162 6.2.4 Well balanced paths and legal paths 167 6.2.5 Legal paths and redex families 175 6.2.6 Legal paths and optimalreductions 186 6.3 Consistent Paths 186 6.3.1 Reminder on proper paths 187 6.3.2 Consistency 189 6.4 Regular Paths 192 6.4.1 The DynamicAlgebra LS 193 6.4.2 A model 197 6.4.3 Virtual Reduction 199 6.5 Relating Paths 204 6.5.1 Discriminants 208 6.5.2 Legal paths are regular and vice-versa 208 6.5.3 Consistent paths are regular and vice-versa 214 6.6 Virtual interactions 216 6.6.1 Residuals and ancestors of consistent paths 217 6.6.2 Fan annihilationsand cycles 220 Contents 5 7 Read-back 223 7.1 Static and dynamicsharing 225 7.1.1 Grouping sequences of brackets 225 7.1.2 Indexed (cid:21)-trees 229 7.1.3 Beta rule 229 7.1.4 Multiplexer 231 7.2 The propagation rules 232 7.2.1 Mux interactions 232 7.2.2 Mux propagation rules 233 7.2.3 The absorption rule 235 7.2.4 Redexes 238 7.3 Deadlocked redexes 240 7.3.1 Critical pairs 241 7.3.2 Mux permutation equivalence 242 7.4 Sharing morphisms 243 7.4.1 Simulationlemma 247 7.5 Unshared beta reduction 249 7.6 Paths 251 7.7 Algebraic semantics 253 7.7.1 Left inverses of liftingoperators 255 (cid:3) 7.7.2 The inverse semigroup LSeq 256 7.8 Proper paths 259 7.8.1 Deadlock-freeness and properness 265 7.9 Soundness and adequateness 271 7.10 Read-back and optimality 273 8 Other translations in Sharing Graphs 276 8.1 Introduction 277 8.2 The bus notation 281 8.3 The bus notation of the translation F 281 8.4 The correspondence of F and G 285 8.5 Concluding remarks 288 9 Safe Nodes 289 9.1 Accumulation of control operators 289 9.2 Eliminatingredundant information 292 9.3 Safe rules 297 9.4 Safe Operators 299 9.5 Examples and Benchmarks 304 10 Complexity 310 10.1 The simplytyped case 310 10.1.1Typing Lamping’srules 311 6 Contents 10.1.2The (cid:17)-expansion method 313 10.1.3Simulatinggeneric elementary-timebounded computation 320 10.2 Superposition and higher-order sharing 323 10.2.1Superposition 324 10.2.2Higher-order sharing 327 10.3 Conclusions 339 11 Functional Programming 340 11.1 Interaction Systems 342 11.1.1The Intuitionistic Nature of Interaction Systems 345 11.2 Sharing Graphs Implementation 353 11.2.1The encoding of IS-expressions 354 11.2.2The translation of rewriting rules 355 12 The Bologna OptimalHigher-order Machine 362 12.1 Source Language 363 12.2 Reduction 363 12.2.1Graph Encoding 366 12.2.2Graph Reduction 372 12.3 Garbage Collection 377 12.3.1ImplementationIssues 382 12.3.2Examples and Benchmarks 383 12.4 Problems 387 12.4.1The case of \append" 388 Bibliography 395 1 Introduction This book is about optimal sharing in functional programming lan- guages. The formalnotion ofsharingwe shalldealwith wasformalizedin the seventies by L(cid:19)evy interms of\families"of redexes with asameorigin| moretechnically,intermsofsetsofredexesthatareresidualsofaunique (virtual)redex. Thegoalofhisfoundationalresearchwastocharacterize formallywhatanoptimallye(cid:14)cientreductionstrategyforthe(cid:21)-calculus wouldlooklike(evenifthe technologyforitsimplementationwasatthe time lacking). L(cid:19)evy’s dual goals were correctness, so that such a reduc- tion strategy does not diverge when another could produce a normal form,and optimality,so that redexes are not duplicated bya reduction, causing a redundancy in later calculation [L(cid:19)ev78, L(cid:19)ev80]. The relevant functional programminganalogies are that call-by-nameevaluation is a correctbutnotoptimalstrategy,whilecall-by-valueevaluationisa(very rough) approximationof an incorrect but \optimal"strategy. L(cid:19)evyclearlyevincedthatnosharingbasedimplementationof(cid:21)-calculus could reduce in a single step two redexes belonging to distinct families. So,accordingtohisde(cid:12)nition,areductiontechniqueisoptimalwhen(i) a whole family of redexes is contracted in a single computational step and (ii) no unneeded work is ever done (i.e., the reduction does never contract aredex thatwouldbeerased byadi(cid:11)erent reductionstrategy). Such optimal and correct implementations were known for recursion schemas [Vui74], but not for ones where higher-order functions could be passed as (cid:12)rst-class values. Actually, all the naive algorithms sug- gestedbyL(cid:19)evy’stheorylookedquitearti(cid:12)cialandrequiredanunfeasible overhead to decide whether two redexes belong to a same family. Recent research by Lamping has shown that there indeed exist (cid:21)- calculus evaluators satisfyingL(cid:19)evy’s speci(cid:12)cation [Lam89,Lam90]. The 7 8 Introduction fact that more than ten years elapsed between L(cid:19)evy’s de(cid:12)nition of op- timality and Lamping’s reduction algorithm should already give a gist of the complexityof the problem. As a matter of fact, having a unique representation for all the redexes in a same family entails the use of a very sophisticated sharing technique, where all the computational and expressive power of higher-order languages really shines. Note in par- ticular that two redexes of a same family can nest one into the other (for instance, given R = ((cid:21)x:MN), its subterms M and N may contain redexes in the family of R). Therefore, all the traditional implementa- tiontechniquesforfunctionallanguages(mostlybasedonsupercombina- tors, environments or continuations) fail in avoiding useless repetitions of work: no machinery in which the sharing is exploited at the ((cid:12)rst order) level of subterms can be L(cid:19)evy’s optimal. Lamping’s breakthrough was a technique to share contexts, that is, to share terms with an unspeci(cid:12)ed part, say a hole. Each instance of a context may (cid:12)ll its holes in a distinct way. Hence, for any shared con- text, there are several access pointers to it and, for each hole, a set of possible choices for how to (cid:12)ll it|a choice for each instance of the con- text. Lamping’ssolutionmovedfromtheideathatsomecontroloperator shouldmanagethematchingbetween the instances ofacontext andthe ways in which its holes may be (cid:12)lled. As a result, Lamping extended (cid:21)-graphs by two sharing nodes called fans: a \fan-in" node collecting the pointers to a context; a \fan-out"node collecting the ways inwhich a hole can be (cid:12)lled (the exit pointers fromthe context). Assumingthat each pointer collected by a fan-in or fan-out is associated to a named port, the correspondence between entering and exiting pointers is kept provided to have a way to pair fan-in’s and fan-out’s: the instance of thecontext correspondingtothepointerconnected toafan-inportwith namea(cid:12)llsitsholeswiththesubgraphsaccessed throughtheportswith name a of the matchingfan-out’s. Let us try to explain in more detail the last point by a simpli(cid:12)edex- x ample. Let us take the language of named angles L ::=ixj h, where x is x a symbolchosen over a given alphabet. In a string aixb hc, the pair of angles with the same label x is matching when the corresponding pair 0 0 0 of parentheses matches (by the usual rules) in the expression a (b )c obtained byerasing the angleslabeled byy6=x andreplacing \("forix x and \)" for h. According to this de(cid:12)nition of matching,two substrings xy enclosed between matchinganglesmayevenoverlap,asinixiy h h. The string between two matching angles is the idealization of a shared con- text: aleftangleix denotes theaccess pointtoashared context, aright