[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

A construction of typed lambda models related to feasible computability

  • Contributed Papers
  • Conference paper
  • First Online:
Computational Logic and Proof Theory (KGC 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 713))

Included in the following conference series:

Abstract

In this paper we develop an approach to the notion of computable functionals in a very abstract setting not restricted to Turing or, say, polynomial computability. We assume to start from some basic class of domains and a basic class of functions defined on these domains. (An example may be natural numbers with poly time computable functions). Then we define what are “all“ corresponding functionals of higher types which add nothing new to these basic functions. We call such functionals computable or, more technically and adequately speaking, substitutable. (Similarly, in D.Scott's domains we say about continuous functionals as about far-reaching abstraction of computable ones.) Our results are applicable t o quite arbitrary (complexity) classes of functions, satisfying a very general Assumption.

Supported by Russian Foundation of Fundamental Investigations (project 93-011-16016).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S.R. Buss. The polynomial hierarchy and intuitionistic bounded arithmetic. In Structure in Complexity Theory, volume 223 of Lecture Notes in Computer Science, pages 77–103, 1986.

    Google Scholar 

  2. A. Carboni, P. Freyd, and A. Scedrov. A categorical approach to realizability and polymorphic types. In M. Main e.a., editors, Proceedings of 3rd ACM Workshop on Mathematical Foundations of Programming Languages Semantics, volume 298 of Lecture Notes in Computer Science, pages 23–42. Springer Verlag, New Orleans, 1988.

    Google Scholar 

  3. S. Cook and A. Urquhart. Functional interpretations of feasibly constructive arithmetic. In Proc. 21st ACM STOC, pages 107–112, 1989.

    Google Scholar 

  4. S.C. Kleene. Introduction to Metamathematics. Van Nostrand P.C., Amsterdam, 1952.

    Google Scholar 

  5. G.Longo and E.Moggi. The hereditary partial effective functionals and recursion theory in higher types. The Journal of Symbolic Logic, 49(4) 1319–1332, 1984.

    Google Scholar 

  6. J.C. Mitchell. Abstract realizability for intuitionistic and relevant implication (abstract). Journal of Symbolic Logic, 51(3):851–852, 1986.

    Google Scholar 

  7. J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 8, pages 367–458. Elsevier Science, 1990.

    Google Scholar 

  8. J.C. Mitchell and M.J. O'Donnel. Realizability semantics for errortolerant logics. In Theoretical Aspects of Reasoning about Knowledge. Morgan Kaufman, Los Altos, CA, 1986.

    Google Scholar 

  9. H.Jr.Rogers. Theory of recursive functions and effective computability. McGraw-Hill, New York, 1967

    Google Scholar 

  10. V.Yu. Sazonov. An equivalence between polynomial constructivity of Markov's principle and the equality P = NP. In P. Petkov, editor, Mathematical Logic, Proceedings of the Summer School and Conference on Mathematical Logic, Dedicated to the Ninetieth Anniversary of Arend Heyting, held in 1988, Varna, Bulgaria, pages 351–360. Plenum Press, NY, 1990. (A short English version.)

    Google Scholar 

  11. V.Yu. Sazonov and D.I. Sviridenko. Denotational semantics of the language of ∑-expressions (in Russian). In Logical Problems in the Theory of Data Types, volume 114 of Vychislitelnye sistemy, pages 16–34. Novosibirsk, 1986.

    Google Scholar 

  12. R. Statman. Logical relations and the typed λ-calculus. Information and Control, volume 65, pages 85–97, 1985.

    Google Scholar 

  13. A.A. Voronkov. Towards the theory of programming in constructive logic. In N. Jones, editor, Proc. of the European Symp. on Programming, volume 432 of Lecture Notes in Computer Science, pages 421–435. Springer Verlag, 1990.

    Google Scholar 

  14. A.A. Voronkov. N-realizability: one more constructive semantics. Technical Report 71, Department of Mathematics, Monash University, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Program Systems Institute, Research Center of Artificial Intelligence, 152140, Pereslavl-Zalessky, Russia

    Vladimir Sazonov

  2. Batiment Loria, CRIN-CNRS and INRIA-Lorraine, BP 239, 54506, Vandœuvre-les-Nancy Cedex, France

    Andrei Voronkov

Authors
  1. Vladimir Sazonov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Georg Gottlob Alexander Leitsch Daniele Mundici

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sazonov, V., Voronkov, A. (1993). A construction of typed lambda models related to feasible computability. In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1993. Lecture Notes in Computer Science, vol 713. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022578

Download citation

  • DOI: https://doi.org/10.1007/BFb0022578

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57184-1

  • Online ISBN: 978-3-540-47943-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation