Abstract
This paper introduces a simply-typed lambda calculus with both modal and linear function types. Through the use of subtyping extra term formers associated with modality and linearity are avoided. We study the basic metatheory of this system including existence and inference of principal types.
The system serves as a platform for certain higher-order generalisations of Bellantoni-Cook's function algebra capturing polynomial time using a separation of the variables into “safe” and “normal” ones.
The distinction between and the syntactic restrictions involved with the safe and normal variables in the Bellantoni-Cook framework are captured by the modal function space and the associated typing rules.
The linear function spaces on the other hand are used to enable a certain form of primitive recursion with functional result type which is conservative over polynomial time.
The proofs associated with these applications are based on an interpretation of the lambda calculus in a category-theoretic model in which all functions are polynomial time computable by construction. The details of this interpretation are not the main subject of this paper and will appear elsewhere.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
S. Bellantoni. Predicative recursion and computational complexity. PhD thesis, University of Toronto, 192. Technical Report 26492.
S. Bellantoni, K.-H. Niggl, and H. Schwichtenberg. Ramification, Modality, and Linearity in Higher Type Recursion. in preparation, 1998.
Stephen Bellantoni and Stephen Cook. New recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97–110, 1992.
Nick Benton. A mixed linear and nonlinear logic: proofs, terms, and models. In Jerzy Tiuryn and Leszek Pacholski, editors, Proc. CSL '94, Kazimierz, Poland, Springer LNCS, Vol. 933, pages 121–135, 1995.
Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of system F with subtyping. Information and Computation, 109(1/2):4–56, 15 February/March 1994.
Vuokko-Helena Caseiro. Equations for Defining Poly-time Functions. PhD thesis, University of Oslo, 1997. Available by ftp from ftp.ifi.uio.no/pub/vuokko/oadm.ps.
Iliano Cervesato and Frank Pfenning. A Linear Logical Framework. In Symposium on Logic in Computer Science (LICS'96), pages 264–275. IEEE, 1996.
Peter Clote. Computation models and function algebras. available electronically under http://thelonius.tcs.informatik.uni-muenchen.de/ clote/Survey.ps.gz, 1996.
J. Despeyroux, F. Pfennning, and C. Schürmann. Primitive Recursion for Higher-Order Abstract Syntax. Technical Report CMU-CS-96-172, Carnegie Mellon University, 1996.
Martin Hofmann. An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras. To appear in Bulletin of Symbolic Logic, 1997.
Martin Hofmann. More results on modal/linear lambda calculus. Submitted. Available under www.mathematik.tu-darmstadt.de/}mh, 1998.
Yves Lafont and Thomas Streicher. Game semantics for linear logic. In Proc. 6th Annual IEEE Symp. on Logic in Computer Science, editor, Logic in Computer Science (LICS), pages 43–49, 1991.
Daniel Leivant and Jean-Yves Marion. Lambda calculus characterisations of polytime. Fundamentae Informaticae, 19:167–184, 1993.
Daniel Leivant and Jean-Yves Marion. Ramified Recurrence and Computational Complexity II: Substitution and Poly-space. In Jerzy Tiuryn and Leszek Pacholski, editors, Proc. CSL '94, Kazimierz, Poland, Springer LNCS, Vol. 933, pages 448–6500, 1995.
Daniel Leivant and Jean-Yves Marion. Ramified Recurrence and Computational Complexity IV: Predicative functionals and Poly-space. Manuscript, 1997.
Frank Pfenning and Rowan Davies. A modal analysis of staged computation. In Proc. POPL '96, Florida. IEEE, 1996.
Gordon Plotkin. Type theory and recursion. Invited talk at the 8th Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, 1993.
V.R. Pratt. Chu spaces and their interpretation as concurrent objects. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, volume 1000 of Springer LNCS, pages 392–405. Springer-Verlag, 1995.
David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In 7th International Conference on Functional Programming and Computer Architecture, San Diego, California, June 1995.
Philip Wadler. Is there a use for linear logic? In ACM Conference on Partial Evaluation and Semantics-Based Program Manipulation, New Haven, Connecticut, June 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hofmann, M. (1998). A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion. In: Nielsen, M., Thomas, W. (eds) Computer Science Logic. CSL 1997. Lecture Notes in Computer Science, vol 1414. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028020
Download citation
DOI: https://doi.org/10.1007/BFb0028020
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64570-2
Online ISBN: 978-3-540-69353-6
eBook Packages: Springer Book Archive