Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of his 60th Birthday (Lecture Notes in Computer Science, 3838)

This Festschrift is dedicated to Jan Willem Klop on the occasion of his 60th birthday. The volume comprises a total of 23 scientific papers by close friends and colleagues, written specifically for this book. The papers are different in nature: some report on new research, others have the character of a survey, and again others are mainly expository. Every contribution has been thoroughly refereed at least twice. In many cases the first round of referee reports led to significant revision of the original paper, which was again reviewed. The articles especially focus upon the lambda calculus, term rewriting and process algebra, the fields to which Jan Willem Klop has made fundamental contributions. Front-matter ......Page 2 The Spectra of Words......Page 17 Introduction......Page 22 Proof System......Page 23 Completeness......Page 24 Undecidability......Page 25 Introduction......Page 30 The $\mu$-Calculus......Page 31 Interpretations......Page 32 Interpreting Löb's Logic in the $\mu$ -Calculus......Page 35 Fixed Points in Löb's Logic......Page 36 Interpreting the $\mu$-Calculus in Löb's Logic......Page 38 Habemus Retractionem......Page 39 A Characterisation of Weak Bisimulation Congruence......Page 42 Process Graphs......Page 43 Strong Bisimulation......Page 45 Rooted Weak Bisimulation......Page 46 The Definition of Alternative Composition......Page 47 Rooted Weak Bisimulation......Page 48 Weak Bisimulation Congruence......Page 49 The Fresh Atom Principle......Page 50 Arbitrary Many Non-bisimilar Processes......Page 51 The Left-Merge and Rooted Weak Simulations......Page 53 Concluding Remark......Page 54 Introduction......Page 56 Preliminaries......Page 61 Böhm's Theorem for V-Sets......Page 64 Discussion......Page 69 Preliminaries......Page 71 High Level......Page 72 Middle Level......Page 74 Low Level......Page 82 Conclusions......Page 83 Introduction......Page 86 The Weak $\lambda$-Calculus......Page 88 The Weak Labeled $\lambda$-Calculus......Page 91 Sharing of Subterms......Page 95 Dag Implementation......Page 99 Conclusion......Page 101 Introduction......Page 104 Aspect-Oriented Programming......Page 105 Applications of Term Rewriting......Page 106 Aspect Weaving Implemented by Term Rewriting Systems......Page 107 Implementing a Weaver for $\mu$ AspectJ......Page 108 Aspects in Term Rewriting Systems......Page 110 Introducing AspectAsf......Page 113 Applying Aspect-Oriented Term Rewriting......Page 115 Discussion and Further Research......Page 117 Introduction......Page 122 Synchronous (Finite) $\phi$-Calculus......Page 124 Graphs and Their Ranked Extension......Page 126 From Processes to Graphs......Page 128 Reductions Via Sequential Composition......Page 130 Encoding the Rules......Page 131 Observing Reductions......Page 133 Conclusions and Further Work......Page 135 Introduction......Page 143 Background......Page 144 Primitive Rewriting......Page 146 Partial Rewriting......Page 148 Computations......Page 150 Word Problems......Page 151 Halting Problems......Page 154 Conclusion......Page 156 Introduction......Page 164 Infinite Terms......Page 165 Reduction on Infinite Terms......Page 166 Reduction Sequences of Transfinite Length......Page 167 Compression of Transfinite Sequences to Length $\omega$......Page 169 Confluence......Page 170 Axiomatic Treatment of Undefinedness......Page 172 Syntactic Domain Models from Sets of Undefined Terms......Page 173 Sets of Undefined Terms......Page 174 Reduction on Infinite $\lambda$-Terms......Page 175 Undefinedness in Lambda Calculus......Page 177 Sets of Undefined Lambda Terms......Page 178 Normal form Models of the Lambda Calculus......Page 182 Another Proof of Incompleteness of the Finite Lambda Calculus......Page 184 Extensional Infinite Lambda Calculus......Page 185 Summary and Conclusions......Page 186 Reducing Right-Hand Sides for Termination......Page 189 Introduction......Page 190 Term Rewriting......Page 191 The Theory......Page 192 Implementation......Page 198 Complete Dummy Elimination......Page 201 Complete Dummy Elimination for Term Rewriting......Page 202 Complete Dummy Elimination for String Rewriting......Page 208 Conclusions......Page 210 Introduction......Page 214 Reduction Systems......Page 216 Balanced Weak Church-Rosser Property......Page 217 Term Rewriting Systems......Page 221 Externality......Page 222 Normalization of External Reduction......Page 224 Normalization of Quasi-External Reduction......Page 228 Decidable Approximations of Externality......Page 229 Left-Normal Systems......Page 235 Conclusion......Page 238 Introduction......Page 240 Examples......Page 242 Signatures......Page 248 Typing Rules......Page 249 Substitutions......Page 250 Higher-Order Rewriting Relations......Page 251 Confluence......Page 254 Termination of Plain Higher-Order Rewriting......Page 257 Termination of Normal Higher-Order Rewriting......Page 262 Conclusion......Page 264 The Untimed Past......Page 267 Timing the Untimed......Page 268 MPTdrt......Page 275 MPT^$drt*$......Page 277 BSP......Page 279 BSP^$drt*$......Page 280 TSP......Page 282 TSP^$drt*$......Page 284 TCP......Page 287 TCP^$drt*$......Page 290 Concluding Remarks......Page 293 Introduction......Page 296 Relations......Page 297 Hypergraphs......Page 298 Rules and Derivations......Page 300 Clipping and Embedding......Page 304 Rewriting Modulo Isomorphism......Page 306 The Decision Problem......Page 308 Critical Pairs......Page 312 Related Work and Conclusion......Page 319 Introduction......Page 325 Probabilistic Process Calculus......Page 328 Equivalence of Distributions......Page 330 Behavioral Equivalences......Page 331 Probabilistic ``Bisimulation up to'' Techniques......Page 332 Some Properties of Behavioral Equivalences......Page 333 Axiomatizing Strong Bisimilarity......Page 334 Axiomatizing Observational Equivalence......Page 337 Conclusion and Related Work......Page 342 Introduction......Page 354 Preliminaries......Page 358 Methods for Establishing Positive Results......Page 363 Methods for Establishing Negative Results......Page 366 The Linear Time/Branching Time Spectrum......Page 368 BCCSP......Page 369 Positive and Negative Results for BCCSP......Page 370 Overview......Page 373 Parallelism......Page 374 Left Merge......Page 376 Communication Merge......Page 377 Overview......Page 378 Sequential Composition......Page 379 Introduction......Page 384 Preliminaries......Page 387 Confluence......Page 389 Confluence Modulo......Page 390 Skew Confluence......Page 391 $\omega$-Skew-Confluence......Page 392 Abstract Böhm Semantics......Page 393 Skew Confluence......Page 395 $\omega$-Skew Confluence......Page 396 Lack of Confluence in Term Graph Rewriting......Page 399 Cyclic Lambda Calculi......Page 402 Lifting Abstract Böhm Semantics......Page 408 Finite Basis......Page 409 Extensions......Page 410 Abstract Böhm Semantics......Page 412 Conclusions......Page 417 Introduction......Page 420 An Explanatory Example: The Publisher......Page 422 The Calculus......Page 427 Soundness......Page 434 An Exemplifying Application: The Train Scenario......Page 443 Type Inference......Page 445 Conclusions and Related Work......Page 456 Introduction......Page 461 The First-Order Theory \foBPAd......Page 463 Infinitary and Second-Order Axioms......Page 468 Transition Systems and Bisimilarity......Page 471 Full Bisimulation Models of BPAfo......Page 474 External Bisimilarity......Page 478 Observational Equivalence......Page 480 SOS-Based Bisimilarity......Page 482 A Modal Fragment of \lang(\foBPAd)......Page 485 Deadlock Freedom......Page 486 Restricted Reachability......Page 490 The First-Order Theory ACPfo......Page 495 Full Bisimulation Models of ACPfo......Page 498 Interpretation of One Theory in Another......Page 501 Interpretation of \foACP\ in \foBPAdrr......Page 502 Concluding Remarks......Page 508 Introduction......Page 512 A Short History of ERSs......Page 513 ERSs with Respect to Other Higher-Order Formalisms......Page 514 Outline......Page 515 The Syntax of CCERSs......Page 516 Expressive Power of CCERSs......Page 519 Orthogonality and Confluence......Page 521 A Classification of Orthogonal CCERSs According to Redex Creation......Page 524 Relative Normalisation by Neededness in Orthogonal CCERSs......Page 525 External Redexes......Page 526 Normalisation of the Essential Strategy......Page 527 Similarity of Redexes......Page 528 A Minimal Perpetual Strategy......Page 530 Two Characterisations of Critical Redexes......Page 531 The Longest Perpetual Reductions in OERSs......Page 533 Basic Notions of the ERSP Formalism......Page 535 Rewrite Rules and Reduction Relation......Page 540 A Subclass of Confluent ERSP......Page 542 SERS as Particular ERSP......Page 545 Simplified Expression Reduction Systems with Indices......Page 546 From Names to Indices......Page 551 From Indices to Names......Page 552 Preserving Properties......Page 553 From Indices to First-Order Systems......Page 554 The $σ_⇑$ Calculus......Page 555 The Conversion Procedure......Page 556 Conclusions and Further Work......Page 562 Axiomatic Rewriting Theory I: A Diagrammatic Standardization Theorem......Page 570 Computing Leftmost Outermost is Judicious... in the $\lambda$-Calculus......Page 573 Computing Leftmost Outermost is not Necessarily Judicious... in Other Rewriting Systems......Page 575 Forget Syntax, Think Diagrammatically!......Page 576 Standardization as 2-Dimensional Rewriting ``Modulo''......Page 577 The Basic Vocabulary of Axiomatic Rewriting Theory......Page 579 Reversible and Irreversible Permutations......Page 581 The Standardization Theorem......Page 582 Illustration: The $\lambda$-Calculus and Its Three Standardization Orders......Page 583 A Concise History of the Standardization Theorem......Page 584 Axiom 1: Shape......Page 586 Axioms 2, 3, 4, 5: Ancestor, Reversibility, Irreversibility and Cube......Page 587 Axiom 6: Enclave......Page 591 Axioms 7 and 8: Stability and Reversible Stability......Page 592 Drag and Extraction......Page 594 A Direct Characterization of the Standard Paths......Page 596 The Structure of Starts and Stops......Page 597 Characterization Lemma......Page 603 The Outermost Redex......Page 608 Uniqueness......Page 610 Existence......Page 615 Standardization Theorem......Page 618 Tiling Graph, Tiling Paths, and Partial Injections......Page 619 Standard=Strong Terminal......Page 621 The 2-Category 2-cat(G,)......Page 625 An Alternative Axiomatics Based on Residuals and Nesting......Page 626 The First N-axioms: Finite, Compat, Ancestor, Self......Page 627 A Few Preliminary Definitions: Multi-redex, Development......Page 628 The Fundamental N-axioms: I, II, III, IV......Page 629 Every Axiomatic Nesting System Defines an Axiomatic Rewriting System......Page 630 Epimorphisms wrt.......Page 636 Monomorphisms wrt.......Page 637 A Simpler Structure of Starts......Page 638 Examples and Open Problems......Page 639 Conclusion......Page 652 Back-matter ......Page 655 Dedicated to Jan Willem Klop, this volume comprises a total of 23 scientific papers by his close friends and colleagues. The articles especially focus upon the lambda calculus, term rewriting and process algebra, the fields to which Jan Willem Klop has made fundamental contributions.