A List of Papers on

Computational Complexity at Higher Types
and Related Topics

Version 2.0 – 29 July 1999
with sporadic updates since then
(Version 3 will be out one of these days.)

The following was originally built from the list of papers for my Spring 97 course Computation and Complexity at Higher Types. It is incomplete, out of date, biased towards my interests, and the categories & categorization are rather arbitary, but the list may still be of use.

• Papers
  • Surveys
  • Papers before 1989
  • Studies of the BFFs and related classes
  • Characterizing complexity classes via categorical constructs, lambda-calculi, logics, and types
  • Using types to build higher-type functionals over polynomial time
  • Other papers of interest
• Supplementary books
• Meetings of interest
• Illustrations by Gustave Dore
  (Since this is the web, of course there must be pictures.)

Surveys

• R. Gandy and J. Hyland, Computable and recursively countable functions of higher type, in Logic Colloquium 76, North-Holland (1977) 407-438.
  • This covers higher-type computability.
  
  
• S. Cook, Computability and complexity of higher type functions, in Logic from Computer Science (Y.N. Moschovakis, ed.), Springer-Verlag (1991) 51-72.
  • This covers higher-type computing and complexity and contains some interesting original results, e.g., the quasi-linear ordering functional.
    A reasonable starting point for learning about higher types and complexity.
  
  
• J. Longley, Notions of computability at higher types, I, to appear in Logic Colloquium 2000
  • A very nice historical survey. See John Longley's home page for the current drafts of Parts II and III.
    A very good starting point for learning about higher types.
  
  
• R. Irwin, B. Kapron, and J. Royer, On Characterizations of the Basic Feasible Functionals, Part I Journal of Functional Programming 11 (2001) 117-153.
  • Roughly the first half of this is a survey of complexity at higher types mainly focusing on type level 2.
  
  
• R. Irwin, B. Kapron, and J. Royer, On Characterizations of the Basic Feasible Functionals, Part II
  • The beginning of this paper has a brief survey of complexity at higher types at type levels 3 and above.
  
  

Papers before 1989

• S. Buss, The Polynomial Hierarchy and Intuitionistic Bounded Arithmetic, In Structure in Complexity Theory, Springer-Verlag (1986) 77-103.
  • Buss introduces a class of ``polynomial-time'' functionals at all simple types as realizers for IS₂¹, his intuitionistic theory of bounded arithmetic. This roughly parallels Gödel's use of primitive recursive functionals in the Dialectica paper.
  
  
• R. Constable, Type two computational complexity, in Proc. of the Fifth Ann. ACM Symp. on Theory of Computing (1973) 108-121.
  • As far as I can tell this is the first paper to consider the question of the computational complexity of functionals and operators (as opposed to using functionals and operators as tools).
  
  
• R. Daley and C. Smith, On the Complexity of Inductive Inference, Information and Control 69 (1986) 12-40.
  • This concerns the computational complexity of limiting functionals as used in learning theory.
  
  
• K. Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten, in Dialectica (1958) 280-287. Available in English as: K. Gödel, On a hitherto unutilized extension of the finitary standpoint, in Kurt Gödel: Collected Works, Volume II, S. Feferman, J. Dawson, S. Kleene, G. Moore, R. Solovay, and J. van Heijenoort (eds.), Oxford University Press (1990) 241-251.
  • Gödel Uses higher-type primitive recursive functionals to give a relative consistency proof for Heyting Arithmetic.
  
  
• D. Hilbert, Über das unendliche, Mathematische Annalen 95 (1925) 161-190. Available in English as: D. Hilbert, On the infinite, in From Frege to Gödel: A source book in mathematical logic, 1879-1931, (J. van Heijenoort, ed.), Harvard University Press (1967) 367-392.
  • In the course of his work on proof theory, Hilbert uses a higher-type primitive recursive functional to define a variant of Ackerman's function. This is one of the earliest uses of subrecursive higher-type recursion. I have been told that C.S. Peirce's work on his Calculus of Relations (the first version of which was published in 1870) may well contain other examples.
  
  
• K. Mehlhorn, Polynomial and Abstract Subrecursive Classes, Journal of Computer and Systems Sciences 12 (1976) 147-178.
  • This was a follow up of some of the questions posed by the 1973 Constable paper.
  
  
• H. Schwichtenberg, Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976) 113-114.
  • This paper shows that the functions definable over the Church numerals in the simply typed lambda calculus are precisely the extended polynomial functions; these are roughly the polynomials closed up under a conditional operator.
  
  
  

Studies of the Basic Feasible Functionals and Related Classes

• P. Clote, A note on the relation between polynomial time functionals and Constable's class K, in Proceedings of the Conference for Computer Science Logic '95, LNCS 1092, Springer-Verlag (1996).
  
  
• S. Cook and B. Kapron, Characterizations of the basic feasible functions of finite type, in Feasible Mathematics: A Mathematical Sciences Institute Workshop, (S. Buss and P. Scott, eds.), Birkhäuser (1990) 71-95.
  • Contains several programming formalism characterizations of the type-2 BFFs and shows that the type-2 class studied by Mehlhorn corresponds to the type-2 BFFs.
  
  
• S. Cook and A. Urquhart, Functional Interpretations of Feasibly Constructive Arithmetic, Annals of Pure and Applied Logic 63 (1993) 103-200.
  • The first place the BFFs at all simple types appear. The paper follows up some problems raised by Buss's paper. Cook and Urquhart set out to develop an alternative class of realizers for IS₂¹ than the ones used by Buss. The goal was to present the result as a feasible variant of Gödel's Dialectica interpretation of Heyting Arithmetic. They introduced a formal system PV^omega in which the terms consist of simply typed lambda-expressions built from numeric constants, function constants for each polynomial-time computable function, variables of all finite types, and a type-2 recursor that corresponds to Cobham's limited recursion on notation.
  
  
• R. Irwin, B. Kapron, and J. Royer, On Characterizations of the Basic Feasible Functionals, Part I (draft), 1999, to appear in the Journal of Functional Programming.
  • This paper builds on the Bellantoni-Cook and Leivant characterizations of Ptime to obtain a kind of type-theoretic characterization the type-2 basic feasible functionals. The first part contains a brief, but chatty, survey of the prior work on the BFFs.
  
  
• R. Irwin, B. Kapron, and J. Royer, On Characterizations of the Basic Feasible Functionals, Part II
  • This concerns characterizations of the basic feasible functionals as type-level three and above. In contrast to Part I, in which the focus was on types, the focus here is on semantics. Be warned that this is a big, complex paper that clarifies some mysteries and raises some others.
  
  
• B. Kapron and S. Cook, A new characterization of type 2 feasibility, SIAM Journal on Computing 25 (1996) 117-132.
  • This contains the machine characterization of the type-2 Basic Feasible Functionals - a very pretty result, but a not so pretty proof.
  
  
• B. Kapron, Feasible Computation in Higher Types, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1991.
  
  
• B. Kapron, Feasibly continuous type-two functionals (1998), to appear in Computational Complexity.
  
  
• C.-C. Li and J. Royer On Type-2 Complexity Classes (Preliminary version) (draft), presented at ICC'00.
  • There is currently no satisfactory general notion of what a higher-type complexity class should be. In this paper we propose one such notion for type-2 functionals and begin an investigation of its properties.
  
  
• E. Pezzoli, On the computational complexity of type two functionals, Proceedings of the Conference for Computer Science Logic '97, LNCS 1414, Springer-Verlag (1998) 373-388.
  • This is a continuation of Seth's work ``natural properties'' (my bad terminology, not theirs) that may characterize the intuitively feasible type-2 functionals. She shows that the set of properties considered in Seth (1993) fail to characterize the type-2 BFFs and proposes a set of her own that do indeed yield the characterization.
  
  
• J. Royer, Semantics vs. syntax vs. computations: Machine models for type-2 polynomial-time bounded functionals, J. Comput. and Syst. Science 54 (1997) 424-436.
  • A fairly natural direct analogue of Kreisel-Lacombe-Schoenfield Theorem for type-2 feasible functionals is shown to involve complexity-theoretic conundrums. E.g., if this direct analogue holds, then P differs from NP. A weaker ``feasible'' analogue of KLS -- in which "computing over syntax" is replaced by "computing over computations (of programs)" -- is shown to hold.
  
  
• J. Royer, On the Computational Complexity of Longley's H Functional, to appear in Theoretical Computer Science, presented at ICC'00.
  • The sequentially realizable functionals (denoted SR) is a class of ``sequentially computable'' higher-type functionals that include the PCF-computable functionals along with elements that are not Scott-continuous. SR has very strong and natural mathematical properties.

    Longley exhibited a functional H in SR with the property that if one adds H to the language PCF, then the resulting language, PCF+H, computes exactly SR. Longley hesitated to recommend PCF+H as the basis of a practical programming language as the only known ways of computing H seemed to involve high computational complexity.

    This paper shows that if P is different from NP, then the computational complexity of H (and of similar SR-functionals) is inherently infeasible.

  
  
• A. Seth, There is No Recursive Axiomatization for Feasible Functionals of Type 2, Seventh Annual IEEE Symposium on Logic in Computer Science (1992) 286-295.
  
  
• A. Seth, Some Desirable Conditions for Feasible Functions of Type 2, Eighth Annual IEEE Symposium on Logic in Computer Science (1993) 320-331.
  
  
• A. Seth, Turing Machine Characterizations of Feasible Functionals of All Finite Types, in Feasible Mathematics II, Birkhäuser (1995) 407-428.
  • This contains an extension of the Kapron-Cook type-2 machine characterization to all simple types.
  
  
• A. Seth, Complexity Theory of Higher Type Functionals, Ph.D. Thesis, University of Bombay, 1994.
  • This contains the matterial of the previous three papers and more.
  
  

Characterizing Complexity Classes via Categorical Constructs, Lambda-Calculi, Logics, and, most especially, Types

There is too much recent work here for a comprehensive list. So, just some of the earlier papers are listed below. See

• Martin Hoffman, Programming languages capturing complexity classes SIGACT News Logic Column 9 (2000).

for a recent survey. Also see the home page of the International Workshop on Implicit Computational Complexity, a continuing series of workshops on this and related topics.

• Andrea Asperti, Light Affine Logic, Proceedings of LICS '98, IEEE-CS (1998).
  
  
• S. Bellantoni, Predicative recursion and computational complexity, Ph.D. Thesis, University of Toronto, published as University of Toronto, Computer Science Department Technical Report 264/92 (1992).
  
  
• S. Bellantoni and S. Cook, A new recursion-theoretic characterization of the polytime functions, Computational Complexity 2 (1992) 97-110.
  
  
• V.-H. Caeserio, Equations for Defining Poly-time Functions, Ph.D. Thesis, Univ. of Oslo, 1997.
  
  
• P. Clote, A safe recursion scheme for exponential time, Boston College Computer Science Department Technical Report.
  
  
• J.-Y. Girard and A. Scedrov and P.J. Scott, Bounded Linear Logic: A Modular Approach to Polynomial Time Computability, Theoretical Computer Science 97 (1992) 1-66.
  
  
• J.-Y. Girard, Light Linear Logic, Information and Computation 143 (1998) 175-204.
  
  
• A. Goerdt, Characterizing Complexity Classes by Higher-Type Primitive Recursive Definitions, Theoretical Computer Science 100 (1992) 45-66.
  
  
• A. Goerdt and H. Seidl, Characterizing Complexity Classes by Higher-Type Primitive Recursive Definitions, Part II, in Aspects and Prospects of Theoretical Computer Science, LNCS 464, J. Dassow and J. Kelemen (Eds.), Springer-Verlag (1990) 148-158.
  
  
• A. Goerdt, Characterizing Complexity Classes by General Recursive Definitions in Higher Types, Information and Computation 101 (1992) 202-218.
  
  
• D. Leivant, Ramified Recurrence and Computational Complexity I: Word Recurrence and Poly-time, in Feasible Mathematics II, (P. Clote and J. Remmel, eds.) Birkhäuser (1995) 320-343.
  
  
• D. Leivant, Predicative Recurrence in Finite Types, in Logical Foundations of Computer Science, Third International Symposium, (A. Nerode, Yu. Matiyasevich, eds.), Lecture Notes in Computer Science 813, Springer-Verlag (1994) 227-240.
  
  
• J. Otto, Complexity Doctrines, Ph.D. thesis, McGill University, 1995.
  
  

Using Types to Build Higher-Type Functionals over Polynomial-Time

• S. Bellantoni, K.-H. Niggl, and H. Schwichtenberg, Higher Type Recursion, Ramification and Polynomial Time, to appear in Annals of Pure and Applied Logic.
  
  
• M. Hofmann, An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras, Bulletin of Symbolic Logic 3 (1997) 469-486.
  
  
• M. Hofmann, Type systems for polynomial-time computation, Habilitation thesis. Darmstadt, 1999. Appears as LFCS Technical Report ECS-LFCS-99-406.
  
  
• M. Hofmann, Linear types and non-size-increasing polynomial time computation, in the Proceedings of the 1999 IEEE Conference on Logic in Computer Science (1999).
  
  
• J.C. Mitchell, M. Mitchell, and A. Scedrov, A linguistic characterization of bounded oracle computation and probabilistic polynomial time, in the Proceedings of the 1998 IEEE Symposium on the Foundations of Computer Science (1998) 725-733.
  
  
• E. Rose, Linear Time Hierarchies for a Functional Language Machine Model, to appear in Science of Computer Programming.
  
  

Other Papers of Interest

• D. Gurr, Semantic Frameworks for Complexity, Ph.D. Thesis, University of Edinburgh, 1990.
  
  
• H. Mairson, A Simple Proof of a Theorem of Statman, Theoretical Computer Science 103 (1992) 387-394.
  • This result is a nice contrast to the one of Schwichtenberg's 1976 paper listed above.
  
  
• H. Schwichtenberg, Density and choice for total continuous functionals, in Kreiseliana (P. Odifreddi, ed.), A.K. Peters (1996) 335-362.
  
  
• H. Schwichtenberg, Type Theory, lecture notes from a course given at Universität München, 1994.
  
  
• D. Scott, A type-theoretical alternative to ISWIM, CUCH, and OWHY, Theoretical Computer Science 121 (1993) 411-440, Originally written in 1969.
  
  
• M. Townsend, Complexity for Type-2 Relations, Nortre Dame Journal of Formal Logic 31 (1990) 241-262.
  
  
• T. Yamakami, Feasible Computability and Resource Bounded Topology, Information and Computation 116 (1995) 214-230.
  • This is a follow up to Townsend's paper.
  
  

Supplementary Books

• R. Hindley, Basic Simple Type Theory, Cambridge, 1997.
• N. Jones, Computability and Complexity from a Programming Perspective, MIT Press, 1997.
• P. Odifreddi, Classical Recursion Theory, Vol. I North Holland, 1989.
• P. Odifreddi, Classical Recursion Theory, Vol. II North Holland, 1999.
• C. Okasaki, Purely Functional Data Structures, Cambridge, 1998.
• C. Papadimitriou, Computational Complexity, Addison-Wesley, 1994.
• H. Rogers, Theory of Recursive Functions and Effective Computability, McGraw-Hill, 1969.
• J. Royer and J. Case, Subrecursive Programming Systems: Complexity & Succinctness, Birkhäuser, 1994.

Meetings of Interest

• DIMACS Workshop on Computational Complexity and Programming Languages, Rutgers University, 1996. See the Workshop Report.
• Programs: Improvements, Complexity, and Meanings; Schloß Dagstuhl; Wadern, Germany, 8-12 June 1998.
• The Implicit Computational Complexity in Programming Language Design and Methodology Workshop, Baltimore, Maryland, USA, 26 September 1998.
• Implicit Computational Complexity Workshop Trento, Italy, 30 June - 1 July, 1999.
• Implicit Computational Complexity-2000 29-30 June 2000, UC/Santa-Barbara.

Illustrations

Dante and Beatrice contemplate higher types
and computational complexity
(notice all the big-Os)

An example of downward tier coercion
(see the Irwin, Kapron, and Royer papers)

More Dore Illustrations for Dante's Comedy

Acknowledgement and Disclaimer

This material is based in part upon work supported by the National Science Foundation under Grants CCR-9522987 and CCR-0098198.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.

http://www.cis.syr.edu/~royer/
Last systematic modification: August 1999