Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of his 60th Birthday

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