A syntactical analysis of non-size-increasing polynomial time computation

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A syntactical analysis of non-size-increasing polynomial time computation

Full text

Pdf (201 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 3 , Issue 3 (July 2002) table of contents

Pages: 383 - 401

Year of Publication: 2002

ISSN:1529-3785

Authors

Klaus Aehlig	Universität München, Munich, Germany
Helmut Schwichtenberg	Universität München, Munich, Germany

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 25, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/507382.507386 What is a DOI?

ABSTRACT

A syntactical proof is given that all functions definable in a certain affine linear typed λ-calculus with iteration in all types are polynomial time computable. The proof provides explicit polynomial bounds that can easily be calculated.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Klaus Aehlig , Helmut Schwichtenberg, A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.84, June 26-29, 2000
	2	Beckmann, A. and Weiermann, A. 2000. Characterizing the elementary recursive functions by a fragment of Gödel's T. Arch. Math. Logic 39, 7 (Oct.), 475--492.
	3	Stephen Bellantoni , Stephen Cook, A new recursion-theoretic characterization of the polytime functions, Computational Complexity, v.2 n.2, p.97-110, 1992 [doi>10.1007/BF01201998]
	4	Bellantoni, S., Niggl, K.-H., and Schwichtenberg, H. 2000. Higher type recursion, ramification and polynomial time. Ann. Pure Appl. Logic 104, 17--30.
	5	Caseiro, V.-H. 1997. Equations for defining poly-time functions. Ph.D. thesis, Department of Computer Science, University of Oslo, Oslon, Norway. Available at www.ifi.uio.no/~ftp/publications/research-reports/.
	6	Stephen A. Cook, Characterizations of Pushdown Machines in Terms of Time-Bounded Computers, Journal of the ACM (JACM), v.18 n.1, p.4-18, Jan. 1971 [doi>10.1145/321623.321625]
	7	Gödel, K. 1958. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunkts. Dialectica 12, 280--287.
	8	Hofmann, M. 1998. Typed lambda calculi for polynomial-time computation. Habilitation thesis, Mathematisches Institut, TU Darmstadt, Germany. Available under www.dcs.ed.ac.uk/home/mxh/habil.ps.gz.
	9	Martin Hofmann, Linear Types and Non Size-Increasing Polynomial Time Computation, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.464, July 02-05, 1999
	10	Hofmann, M. 2000a. Linear types and non-size-increasing polynomial time computation. Theoret. Comput. Sci. To appear.
	11	Martin Hofmann, A type system for bounded space and functional in-place update, Nordic Journal of Computing, v.7 n.4, p.258-289, Winter 2000
	12	Hofmann, M. 2001. The strength of non size-increasing computation. In Proceedings of the 3rd International Workshop on Implicit Computational Complexity (ICC '01) Aarhus, Denmark, May 20--21, 2001), M. Hofmann, Ed. Number NS-01-3 in Notes Series. BRICS, Department of Computer Science, University of Aarhus, Aarhus, Denmark, 19--35.
	13	Joachimski, F. and Matthes, R. 1999. Short proofs of normalisation for the simply-typed λ-calculus, permutative conversions and Gödel's T. Arch. Math. Logic, To appear.
	14	Neil D. Jones, Computability and complexity: from a programming perspective, MIT Press, Cambridge, MA, 1997
	15	Neil D. Jones, LOGSPACE and PTIME characterized by programming languages, Theoretical Computer Science, v.228 n.1-2, p.151-174, Oct. 1999 [doi>10.1016/S0304-3975(98)00357-0]
	16	Neil D. Jones, The expressive power of higher-order types or, life without CONS, Journal of Functional Programming, v.11 n.1, p.55-94, January 2001 [doi>10.1017/S0956796800003889]
	17	Daniel Leivant, A foundational delineation of poly-time, Papers presented at the IEEE symposium on Logic in computer science, p.391-420, May 1994, Amsterdam, The Netherlands
	18	Daniel Leivant, Applicative Control and Computational Complexity, Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, p.82-95, September 20-25, 1999
	19	Daniel Leivant , Jean-Yves Marion, Lambda calculus characterizations of poly-time, Fundamenta Informaticae, v.19 n.1-2, p.167-184, Sept./Oct. 1993
	20	Simmons, H. 1988. The realm of primitive recursion. Arch. Math. Logic 27, 2 (Oct.), 177--188.