Switch to: References

Add citations

You must login to add citations.
  1. Term rewriting theory for the primitive recursive functions.E. A. Cichon & Andreas Weiermann - 1997 - Annals of Pure and Applied Logic 83 (3):199-223.
    The termination of rewrite systems for parameter recursion, simple nested recursion and unnested multiple recursion is shown by using monotone interpretations both on the ordinals below the first primitive recursively closed ordinal and on the natural numbers. We show that the resulting derivation lengths are primitive recursive. As a corollary we obtain transparent and illuminating proofs of the facts that the schemata of parameter recursion, simple nested recursion and unnested multiple recursion lead from primitive recursive functions to primitive recursive functions.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • A new "feasible" arithmetic.Stephen Bellantoni & Martin Hofmann - 2002 - Journal of Symbolic Logic 67 (1):104-116.
    A classical quantified modal logic is used to define a "feasible" arithmetic A 1 2 whose provably total functions are exactly the polynomial-time computable functions. Informally, one understands $\Box\alpha$ as "α is feasibly demonstrable". A 1 2 differs from a system A 2 that is as powerful as Peano Arithmetic only by the restriction of induction to ontic (i.e., $\Box$ -free) formulas. Thus, A 1 2 is defined without any reference to bounding terms, and admitting induction over formulas having arbitrarily (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Implicit recursion-theoretic characterizations of counting classes.Ugo Dal Lago, Reinhard Kahle & Isabel Oitavem - 2022 - Archive for Mathematical Logic 61 (7):1129-1144.
    We give recursion-theoretic characterizations of the counting class \(\textsf {\#P} \), the class of those functions which count the number of accepting computations of non-deterministic Turing machines working in polynomial time. Moreover, we characterize in a recursion-theoretic manner all the levels \(\{\textsf {\#P} _k\}_{k\in {\mathbb {N}}}\) of the counting hierarchy of functions \(\textsf {FCH} \), which result from allowing queries to functions of the previous level, and \(\textsf {FCH} \) itself as a whole. This is done in the style of (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Ramified recurrence and computational complexity III: Higher type recurrence and elementary complexity.Daniel Leivant - 1999 - Annals of Pure and Applied Logic 96 (1-3):209-229.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Tiering as a recursion technique.Harold Simmons - 2005 - Bulletin of Symbolic Logic 11 (3):321-350.
    I survey the syntactic technique of tiering which can be used to restrict the power of a recursion scheme. I show how various results can be obtained entirely proof theoretically without the use of a model of computation.
    Download  
     
    Export citation  
     
    Bookmark  
  • A term rewriting characterization of the polytime functions and related complexity classes.Arnold Beckmann & Andreas Weiermann - 1996 - Archive for Mathematical Logic 36 (1):11-30.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • (2 other versions)Higher type recursion, ramification and polynomial time.Stephen J. Bellantoni, Karl-Heinz Niggl & Helmut Schwichtenberg - 2000 - Annals of Pure and Applied Logic 104 (1-3):17-30.
    It is shown how to restrict recursion on notation in all finite types so as to characterize the polynomial-time computable functions. The restrictions are obtained by using a ramified type structure, and by adding linear concepts to the lambda calculus.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • (2 other versions)Characterising polytime through higher type recursion.Stephen J. Bellantoni, Karl-Heinz Niggl & Helmut Schwichtenberg - 2000 - Annals of Pure and Applied Logic 104 (1-3):17-30.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Characterizing the elementary recursive functions by a fragment of Gödel's T.Arnold Beckmann & Andreas Weiermann - 2000 - Archive for Mathematical Logic 39 (7):475-491.
    Let T be Gödel's system of primitive recursive functionals of finite type in a combinatory logic formulation. Let $T^{\star}$ be the subsystem of T in which the iterator and recursor constants are permitted only when immediately applied to type 0 arguments. By a Howard-Schütte-style argument the $T^{\star}$ -derivation lengths are classified in terms of an iterated exponential function. As a consequence a constructive strong normalization proof for $T^{\star}$ is obtained. Another consequence is that every $T^{\star}$ -representable number-theoretic function is elementary (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations