Algebra, Meaning, and Computation: Essays dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday (Lecture Notes in Computer Science, 4060)

Joseph Goguen is one of the most prominent computer scientists worldwide. His numerous research contributions span many topics and have changed the way we think about many concepts. Our views about data types, programming languages, software specification and verification, computational behavior, logics in computer science, semiotics, interface design, multimedia, and consciousness, to mention just some of the areas, have all been enriched in fundamental ways by his ideas. This Festschrift volume - published to honor Joseph Goguen on his 65th Birthday on June 28, 2006 - includes 32 refereed papers by leading researchers in the different areas spanned by Joseph Goguen's work. The papers address a broad variety of topics from meaning, meta-logic, specification and composition, behavior and formal languages, as well as models, deduction, and computation. The papers were presented at a Symposium in San Diego, California, USA in June 2006. Both the Festschrift volume and the Symposium allow the articulation of a retrospective and prospective view of a range of related research topics by key members of the research community in computer science and other fields connected with Joseph Goguen's work. Algebra, Meaning and Computation 1 36 1 Introduction 36 2 Insect Music 38 3 A Web Without a Spider 45 4 Harnessing Complexity 51 5 Final Thoughts 55 References 58 2 60 3 66 1 Introduction 66 2 Metalogic, Qualia, and Identity 70 3 Discussion 76 4 Conclusions 81 Acknowledgments 83 References 83 4 85 Introduction 85 Institutional Preliminaries 86 Global Institution 88 Probability Institution 89 Quantum Institution 91 Conclusion 97 5 100 Introduction 100 Basic Concepts 104 Internal Logic 109 Model Ultraproducts 113 Saturated Models 115 Preservation and Axiomatizability 117 Interpolation 121 Definability 124 Other Topics 128 Philosophical Roots 129 6 134 Introduction 134 Preliminaries 136 RDF and RDF Schema Logics 142 Semantic Web Logics 145 RDF Serialization of Semantic Web Logics 151 Conclusion 156 7 159 Introduction 159 Institutions 160 Institution (Co)Morphism Modifications 163 Colimits in Hom-Categories 165 Comorphism-Based Grothendieck Institutions 166 Amalgamation and Exactness 168 From Specifications to Programs 175 Proofs of the Theorems 177 8 185 9 192 Introduction 192 Preliminaries 194 Factorization Systems 194 Equations as Epimorphisms 195 Sound Deduction 197 Finiteness 200 Completeness 203 Conclusion and Future Work 205 10 208 Introduction 208 The Architecture Design Language CommUnity 210 Component Extension in CommUnity 216 An Example Using Extension 224 Related Work 224 Conclusion 226 11 229 Introduction 229 Formal Islands 231 {sf TOM} 232 Strategic Rewriting for a Chemical Reactor 235 A Formal Island Implementation of the Primary Mechanism 238 Conclusion 247 12 251 Introduction 251 The Three Languages 253 Example 256 Priority Queues in OBJ 257 Priority Queues in ML 260 Priority Queues in Coq 263 Conclusion 266 13 270 Introduction 270 Review of Adhesive and Adhesive HLR Categories 272 Weak Adhesive HLR Categories and Systems 275 Petri Net Transformation Systems 278 Conclusion 284 14 287 Introduction 287 From Order-Sorted to Membership Equational Logic 291 Rewriting Logic: From OBJ to Maude 293 Beyond Maude 299 Conclusions 306 15 316 Introduction 316 Algebraic Semantics in OBJ 318 Action Semantics in OBJ 321 Constructive Semantics in OBJ 326 Conclusion 329 16 331 Introduction 331 CAT 332 Specifications and Programs 335 Implementations and Vertical Composition 340 Horizontal Composition 342 Conclusions 348 17 352 Introduction 352 Preliminaries 353 Composing and Refining Specifications 355 Design by Classification 356 Policy Enforcement 359 Concluding Remarks 365 18 368 1 Introduction 368 2 BasicConcepts 370 3 Behavioral Refinements 375 4 Proof Rules for Behavioral Refinements: Part I 378 5 Proof Rules for Behavioral Refinements: Part II 380 6 Example: Implementation of Sets by Non-redundantLists 384 7 Conclusion 388 19 390 1 Regular Morphology 390 2 Modular Aums 395 3 Modular Aum Transducers 398 4 Dispatch Synthesis from Regular Expressions 402 5 Conclusion 408 20 410 Introduction 410 Deterministic Automata as Coalgebras 412 Structured Output Sets and Distributive Laws 414 Regular Expressions 421 Regular Expressions with Equations 430 Conclusions 438 21 440 Introduction 440 Transition Systems and Sheaves 441 Hierarchical Systems 446 Conclusion 453 22 455 Introduction 455 Background 457 Standard Functors and Monads 465 The Class $TV$ and the Map $chi $ 467 Uniformity 469 Consequences of Uniformity 477 A Variation: $lambda $-Uniformity 478 Concluding Remarks 481 23 484 Introduction 484 Algebraic Operations with Structured Domains 485 Regular Subsets of Initial Extended Algebras 487 Regular Expressions Based on Colimits 489 Conclusions 492 24 494 Introduction 494 Elementary Algebraic Specifications 496 Specifications for Rational Complex Numbers 500 Proof of Main Theorem 503 Concluding Remarks 507 25 511 1 Introduction 511 2 Simple Running Example: Division 516 3 Inductive Definitions, Total Functions 517 4 Recursive Equations in CPOs and Metric Spaces 519 5 Lattice of Predicate Logics 524 6 Sets of Models 525 7 The Herbrand Universe 527 8 Conclusion 528 Appendix 528 References 530 26 532 Introduction 532 Presentation 534 Proof Representations 538 Standard Completion Is an Instance of Abstract Canonical System 544 Conclusion 546 Proofs for Section 3 and 4 549 27 556 Introduction 556 Dependent Pattern Matching 557 Type Theory and Pattern Matching 562 Translating Pattern Matching 569 Conclusions 574 28 576 Introduction 576 The Iterative Lexicographic Path Order 577 Examples of ILPO-terminating TRSs 580 ILPO-termination Implies Termination 582 Equivalence of ILPO with the Recursive Lexicographic Path Order 585 Conclusion 588 29 590 Introduction 590 Preliminaries 592 Domain Constraints for Constraint Normal Logic Programs 595 Semantic Constructions for Constraint Normal Logic Programs 597 Functorial Semantics 602 Equivalence of Semantics 605 Appendix 606 30 613 Introduction 613 Logical Foundations of Functional Black-Box Testing 614 A Stochastic Calculus for Program Correctness 617 Test Coverage and Software Reliability 622 Test Case Generation (TCG) 625 Conclusions 628 31 631 Introduction 631 The OTS/CafeOBJ Method 632 Tips 641 Soundness of Proof Scores 646 Conclusion 649 32 651 Introduction 651 Preliminaries to Drug Interaction Ontology (DIO) Modeling 654 Preliminaries to Linear Logical Inference Systems for Process Descriptions 659 A Linear Logical Formulation of Basic Relations in DIO 663 Discussion and Conclusion 670 back-matter 678 Front Matter....Pages - Sync or Swarm: Musical Improvisation and the Complex Dynamics of Group Creativity....Pages 1-24 My Friend Joseph Goguen....Pages 25-30 Metalogic, Qualia, and Identity on Neptune’s Great Moon: Meaning and Mathematics in the Works of Joseph A. Goguen and Samuel R. Delany....Pages 31-49 Quantum Institutions....Pages 50-64 Jewels of Institution-Independent Model Theory....Pages 65-98 Semantic Web Languages – Towards an Institutional Perspective....Pages 99-123 Institutional 2-cells and Grothendieck Institutions....Pages 124-149 Some Varieties of Equational Logic....Pages 150-156 Complete Categorical Deduction for Satisfaction as Injectivity....Pages 157-172 Extension Morphisms for CommUnity....Pages 173-193 Non-intrusive Formal Methods and Strategic Rewriting for a Chemical Application....Pages 194-215 From OBJ to ML to Coq....Pages 216-234 Weak Adhesive High-Level Replacement Categories and Systems: A Unifying Framework for Graph and Petri Net Transformations....Pages 235-251 From OBJ to Maude and Beyond....Pages 252-280 Constructive Action Semantics in OBJ....Pages 281-295 Horizontal Composability Revisited....Pages 296-316 Composition by Colimit and Formal Software Development....Pages 317-332 Proving Behavioral Refinements of COL-specifications....Pages 333-354 The Reactive Engine for Modular Transducers....Pages 355-374 A Bialgebraic Review of Deterministic Automata, Regular Expressions and Languages....Pages 375-404 Sheaves and Structures of Transition Systems....Pages 405-419 Uniform Functors on Sets....Pages 420-448 An Algebraic Approach to Regular Sets....Pages 449-458 Elementary Algebraic Specifications of the Rational Complex Numbers....Pages 459-475 From Chaos to Undefinedness....Pages 476-496 Completion Is an Instance of Abstract Canonical System Inference....Pages 497-520 Eliminating Dependent Pattern Matching....Pages 521-540 Iterative Lexicographic Path Orders....Pages 541-554 A Functorial Framework for Constraint Normal Logic Programming....Pages 555-577 A Stochastic Theory of Black-Box Software Testing....Pages 578-595 Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method....Pages 596-615 Drug Interaction Ontology (DIO) and the Resource-Sensitive Logical Inferences....Pages 616-642 Back Matter....Pages - This Volume - Honoring The Computer Science Pioneer Joseph Goguen On His 65th Birthday - Includes 32 Refereed Papers By Leading Researchers In Areas Spanned By Goguen's Work. The Papers Address A Variety Of Topics From Meaning, Meta-logic, Specification And Composition, Behavior And Formal Languages, As Well As Models, Deduction, And Computation, By Key Members Of The Research Community In Computer Science And Other Fields Connected With Joseph Goguen's Work. Kokichi Futatsugi, Jean-pierre Jouannaud, José Meseguer (eds.). Papers Presented At A Symposium In San Diego, Calif., June 27-29, 2006. Includes Bibliographical References And Index.