Term rewriting theory for the primitive recursive functions

DOI10.1016/S0168-0072(96)00015-2zbMATH Open0871.03033OpenAlexW1996792588MaRDI QIDQ674412FDOQ674412

Authors: E. A. Cichon, Andreas Weiermann 

Publication date: 29 September 1997

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(96)00015-2

Recommendations

• An ordinal calculus for proving termination in term rewriting
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Predicative lexicographic path orders. An application of term rewriting to the region of primitive recursive functions
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Strictly orthogonal left linear rewrite systems and primitive recursion

zbMATH Keywords

terminationrewriting systemsprimitive recursive functionsderivation lengthsparameter recursionsimple nested recursionunnested multiple recursion

Mathematics Subject Classification ID

Recursive functions and relations, subrecursive hierarchies (03D20)

Cites Work

• The realm of primitive recursion
• Title not available (Why is that?)
• Title not available (Why is that?)
• The slow-growing and the Graegorczyk hierarchies
• Title not available (Why is that?)
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• Title not available (Why is that?)
• Herbrand analyses
• Bounding derivation lengths with functions from the slow growing hierarchy
• Computability. Recursive and programmable functions
• Equational derivation vs. computation
• A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity
• Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones
• Title not available (Why is that?)
• Slow growing versus fast growing
• Π12-logic, Part 1: Dilators
• Title not available (Why is that?)
• Title not available (Why is that?)
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (19)

• Invariants, patterns and weights for ordering terms
• Proving consistency of equational theories in bounded arithmetic
• On some slowly terminating term rewriting systems
• Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones
• An ordinal calculus for proving termination in term rewriting
• How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study
• Walther recursion
• Primitive recursion for higher-order abstract syntax
• Title not available (Why is that?)
• A proof-theoretic account of primitive recursion and primitive iteration
• On the Computational Content of Termination Proofs
• Strictly orthogonal left linear rewrite systems and primitive recursion
• Predicative lexicographic path orders. An application of term rewriting to the region of primitive recursive functions
• Title not available (Why is that?)
• Complexity analysis of precedence terminating infinite graph rewrite systems
• On sharing, memoization, and polynomial time
• Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion
• Divergence phenomena during completion
• Some results on cut-elimination, provable well-orderings, induction and reflection

This page was built for publication: Term rewriting theory for the primitive recursive functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q674412)