Nondeterminism in Algebraic Specifications and Algebraic Programs

0: Introduction.- 0.1 Preview.- 0.2 Historical Background.- 0.3 Basic Notions.- 1: Nondeterministic Algebraic Specifications.- 1.1 Nondeterministic Algebras.- 1.1.1 A Discussion of Alternative Approaches.- 1.1.2 The Principle of Extensionality.- 1.1.3 The Notion of an Algebra.- 1.2 Inclusion Rules as a Specification Language.- 1.2.1 Axioms and their Semantics.- 1.2.2 The Calculus of Term Rewriting.- 1.2.3 Soundness: A Negative Result.- 1.2.4 Right-Linearity: A Special Case.- 2: Specifications with a Deterministic Basis.- 2.1 Deterministic Basis.- 2.1.1 Soundness and Deterministic Basis.- 2.1.2 Determinacy Predicate.- 2.1.3 Completeness: A Negative Result.- 2.2 Additive Specifications.- 2.2.1 DET-Completeness and DET-Additivity.- 2.2.2 Term Models and Completeness.- 2.3 Junk-Free Models.- 2.3.1 "Junk" in Nondeterministic Models.- 2.3.2 Breadth Induction.- 2.3.4 DET-Generated Models.- 2.3.5 Term-Generated Models.- 2.4 Hierarchical Specifications.- 3: Structure of the Model Classes.- 3.1 Homomorphisms and Extremal Algebras.- 3.2 Initial Models.- 3.3 Initial Models with Deterministic Basis.- 4: Nondeterministic Specifications as a General Framework.- 4.1 Equational Logic.- 4.2 Term Rewriting.- 4.3 Conditional Axioms.- 4.4 Algebraic Programming.- 4.4.1 Constructor-Based Specifications.- 4.4.2. Narrowing without Confluence.- 4.5 Logic Programming.- 4.5.1. Narrowing Simulates Logic Programming.- 4.5.2. Logic Programming Simulates Narrowing.- 5: Implementation and Examples.- 5.1 Term Rewriting.- 5.1.1 Innermost Rewriting.- 5.1.2 Search Strategies.- 5.1.3 Optimizations.- 5.2 Graph Rewriting.- 5.2.1 Representation of Terms by Graphs.- 5.2.2 Rewriting of Term Graphs.- 5.2.3 Soundness and Completeness.- 5.3 Examples.- 5.3.1 Nondeterministic Finite State Automata.- 5.3.2 Petri Nets.- 5.3.3 The Eight Queens Problem.- 5.3.4 The Monkey-Banana Problem.- 5.3.5 Printer Scheduling.- 6: Partial Nondeterministic Specifications.- 6.1 Partial Operations.- 6.1.1 Undefined "Values".- 6.1.2 Partial Multi-Algebras.- 6.2 Partiality and Term Rewriting.- 6.2.1 A Calculus for Partial Specifications.- 6.2.2 Partial DET-Completeness and DET-Additivity.- 6.3 Partial Specifications with Constructor Basis.- 6.4 Structure of the Model Classes.- 6.4.1 Homomorphisms.- 6.4.2 Initial Algebras.- 6.4.3 Terminal Algebras.- 7: Communicating Processes: An Example.- 7.1. Communicating Processes (CP).- 7.2. Semantics of CP.- 7.2.1. Transition Semantics.- 7.2.2. Trace Semantics.- 7.2.3. Refusal Semantics.- 7.3. Improvements and Applications.- 8: Concluding Remarks.- 8.1. Summary and Evaluation.- 8.2. Future Work.- References.- Appendix A: Proofs.- Appendix B: Experiments with RAP.