Term rewriting theory for the primitive recursive functions

DOI10.1016/S0168-0072(96)00015-2zbMath0871.03033OpenAlexW1996792588MaRDI QIDQ674412

Andreas Weiermann, E. A. Cichon

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

zbMATH Keywords

rewriting systemsterminationprimitive recursive functionsderivation lengthsparameter recursionsimple nested recursionunnested multiple recursion

Mathematics Subject Classification ID

Recursive functions and relations, subrecursive hierarchies (03D20)

Related Items (7)

How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study ⋮ Proving consistency of equational theories in bounded arithmetic ⋮ On sharing, memoization, and polynomial time ⋮ Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones ⋮ On the Computational Content of Termination Proofs ⋮ Invariants, patterns and weights for ordering terms ⋮ Some results on cut-elimination, provable well-orderings, induction and reflection

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• The realm of primitive recursion
• 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
• Herbrand analyses
• Slow growing versus fast growing
• The slow-growing and the Graegorczyk hierarchies
• Π12-logic, Part 1: Dilators
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths

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