Algorithmic term rewriting systems

Contents......Page 7 0. Introduction......Page 9 0.1 The concept of productivity......Page 10 0.2 The concept of properness......Page 13 0.3 The concept of algorithmicity......Page 14 0.4.1 The subject of productivity......Page 15 0.4.2 The subject of tree ordinals......Page 16 0.5 Contribution and overview......Page 17 0.6 Notations......Page 18 1. Algorithmic term rewriting systems......Page 21 1.1.1 Sorts, symbols and terms......Page 22 1.1.2 Operations on terms......Page 23 1.1.3 Rules and reductions......Page 24 1.1.5 Sorted systems......Page 25 1.2.1 Inductive and coinductive sorts......Page 26 1.2.2 Semantically sorted term rewriting systems......Page 27 1.3 Algorithmicity......Page 33 1.4 Orthogonality......Page 36 2.1.1 Sorts and constructors......Page 43 2.1.2 Some algorithmic systems......Page 45 2.2 Quasiorders......Page 48 2.3 Computability......Page 50 2.4 Inductive height......Page 51 2.5 Algebraic interpretation......Page 53 2.6 Semantics......Page 59 2.6.1 Formalization......Page 60 2.6.2 Adequacy......Page 64 2.6.3 Examples......Page 65 3. Ensuring productivity......Page 67 3.1.1 Characterization via path generation......Page 68 3.1.2 Inductive height estimation......Page 70 3.2.1 Characterization by quasiorder......Page 74 3.2.2 Root activity estimation......Page 75 3.3 Constructor normalization......Page 78 3.3.1 Strong constructor normalization......Page 79 3.3.2 Characterization by observation......Page 80 3.3.3 Gauge......Page 86 3.3.4 Pre-requirement and κ-requirements......Page 88 3.3.5 Dependency......Page 91 3.4 Conclusion......Page 97 4.1 Representation limit......Page 101 4.2.1 The binary Veblen function......Page 103 4.2.2 Implementation......Page 107 4.2.3 Productivity and representation limit......Page 109 4.3.1 The Veblen meta-hierarchy......Page 112 4.3.3 Productivity and representation limit......Page 116 4.3.2 Implementation......Page 114 4.4 Hydra games......Page 120 Bibliography......Page 123 List of notations......Page 127 Index......Page 129