Feasible Operations and Applicative Theories Based on λη

Mathematical Logic Quarterly 46 (3):291-312 (2000)
  Copy   BIBTEX

Abstract

We study a theory PTO of polynomial time computability on the type of binary strings, as embedded in full lambda calculus with total application and extensionality. We prove that the closed terms of type W → W are exactly the polynomial time operations. This answers a conjecture of Strahm [13].

Categories

Add categories

Keywords

Reprint years

DOI

10.1002/1521-3870(200008)46:3

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Review: Thomas Strahm, Polynomial Time Operations in Explicit Mathematics ; Andrea Cantini, Feasible Operations and Applicative Theories Based on $\lambda \eta $. [REVIEW]Fernando Ferreira - 2002 - Bulletin of Symbolic Logic 8 (4):534-535.
Elementary explicit types and polynomial time operations.Daria Spescha & Thomas Strahm - 2009 - Mathematical Logic Quarterly 55 (3):245-258.
Polynomial time operations in explicit mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
On the proof theory of type two functionals based on primitive recursive operations.David Steiner & Thomas Strahm - 2006 - Mathematical Logic Quarterly 52 (3):237-252.
Remarks on applicative theories.Andrea Cantini - 2005 - Annals of Pure and Applied Logic 136 (1-2):91-115.
Applicative theories for the polynomial hierarchy of time and its levels.Reinhard Kahle & Isabel Oitavem - 2013 - Annals of Pure and Applied Logic 164 (6):663-675.
Totality in applicative theories.Gerhard Jäger & Thomas Strahm - 1995 - Annals of Pure and Applied Logic 74 (2):105-120.
A feasible theory of truth over combinatory algebra.Sebastian Eberhard - 2014 - Annals of Pure and Applied Logic 165 (5):1009-1033.
The Suslin operator in applicative theories: Its proof-theoretic analysis via ordinal theories.Gerhard Jäger & Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (8):647-660.
A theory of rules for enumerated classes of functions.Andreas Schlüter - 1995 - Archive for Mathematical Logic 34 (1):47-63.
Realisability in weak systems of explicit mathematics.Daria Spescha & Thomas Strahm - 2011 - Mathematical Logic Quarterly 57 (6):551-565.
Truth in applicative theories.Reinhard Kahle - 2001 - Studia Logica 68 (1):103-128.
Asymmetric Interpretations for Bounded Theories.Andrea Cantini - 1996 - Mathematical Logic Quarterly 42 (1):270-288.
Polytime, combinatory logic and positive safe induction.Cantini Andrea - 2002 - Archive for Mathematical Logic 41 (2):169-189.
Counting as integration in feasible analysis.Fernando Ferreira & Gilda Ferreira - 2006 - Mathematical Logic Quarterly 52 (3):315-320.

Analytics

Added to PP
2013-12-01

Downloads
15 (#923,100)

6 months
4 (#790,687)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Andrea Cantini
Università degli Studi di Firenze

Citations of this work

Elementary explicit types and polynomial time operations.Daria Spescha & Thomas Strahm - 2009 - Mathematical Logic Quarterly 55 (3):245-258.
Remarks on applicative theories.Andrea Cantini - 2005 - Annals of Pure and Applied Logic 136 (1-2):91-115.

Add more citations

References found in this work

No references found.

Add more references