4 found
  1.  73
    Martin Hofmann (1997). An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras. Bulletin of Symbolic Logic 3 (4):469-486.
    We use the category of presheaves over PTIME-functions in order to show that Cook and Urquhart's higher-order function algebra PV ω defines exactly the PTIME-functions. As a byproduct we obtain a syntax-free generalisation of PTIME-computability to higher types. By restricting to sheaves for a suitable topology we obtain a model for intuitionistic predicate logic with ∑ 1 b -induction over PV ω and use this to re-establish that the provably total functions in this system are polynomial time computable. Finally, we (...)
    Direct download (7 more)  
    Export citation  
    My bibliography   1 citation  
  2.  2
    Martin Hofmann, Emanuel Kitzelmann & Ute Schmid (2009). A Unifying Framework for Analysis and Evaluation of Inductive Programming Systems. In B. Goertzel, P. Hitzler & M. Hutter (eds.), Proceedings of the Second Conference on Artificial General Intelligence. Atlantis Press
    No categories
    Direct download  
    Export citation  
    My bibliography  
  3.  6
    Stephen Bellantoni & Martin Hofmann (2002). A New "Feasible" Arithmetic. 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 (...)
    Direct download (6 more)  
    Export citation  
    My bibliography   1 citation  
  4.  1
    Martin Hofmann (2000). Safe Recursion with Higher Types and BCK-Algebra. Annals of Pure and Applied Logic 104 (1-3):113-166.
    In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni–Cook's function algebra BC to higher types. It is a step towards a functional programming language in which all programs run in polynomial time. In this paper we develop a semantics of SLR using BCK -algebras consisting of certain polynomial-time algorithms. It will follow from this semantics that safe recursion with arbitrary result type built up from N and (...)
    Direct download (3 more)  
    Export citation  
    My bibliography   1 citation