Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Recognizability in the Simply Typed Lambda-Calculus

  • Conference paper
Logic, Language, Information and Computation (WoLLIC 2009)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5514))

Abstract

We define a notion of recognizable sets of simply typed λ-terms that extends the notion of recognizable sets of strings or trees. This definition is based on finite models. Using intersection types, we generalize the notions of automata for strings and trees so as to grasp recognizability for λ-terms. We then expose the closure properties of this notion and present some of its applications.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. de Groote, P.: Towards abstract categorial grammars. In: Association for Computational Linguistics, 39th Annual Meeting and 10th Conference of the European Chapter, Proceedings of the Conference, pp. 148–155 (2001)

    Google Scholar 

  2. Montague, R.: Formal Philosophy: Selected Papers of Richard Montague. Yale University Press, New Haven (1974)

    Google Scholar 

  3. Salvati, S.: On the membership problem for Non-linear Abstract Categorial Grammars. In: Muskens, R. (ed.) Proceedings of the Workshop on New Directions in Type-theoretic Grammars (NDTTG 2007), Dublin, Ireland, Foundation of Logic, Language and Information (FoLLI), August 2007, pp. 43–50 (2007)

    Google Scholar 

  4. Lambek, J.: The mathematics of sentence structure. American Mathematical Monthly 65, 154–170 (1958)

    Article  MathSciNet  MATH  Google Scholar 

  5. Moortgat, M.: Categorial Investigations: Logical & Linguistic Aspects of the Lambek Calculus. Foris Pubns USA (1988)

    Google Scholar 

  6. Urzyczyn, P.: The emptiness problem for intersection types. J. Symb. Log. 64(3), 1195–1215 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  7. Loader, R.: The undecidability of λ-definability. In: Anderson, C.A., Zeleny, M. (eds.) Logic, Meaning and Computation: Essays in memory of Alonzo Church, pp. 331–342. Kluwer, Dordrecht (2001)

    Chapter  Google Scholar 

  8. Statman, R.: Completeness, invariance and λ-definability. Journal of Symbolic Logic 47(1), 17–26 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  9. Statman, R., Dowek, G.: On statman’s finite completeness theorem. Technical Report CMU-CS-92-152, University of Carnegie Mellon (1992)

    Google Scholar 

  10. Myhill, J.: Finite automata and the representation of events. Technical Report WADC TR-57-624, Wright Patterson Air Force Base, Ohio, USA (1957)

    Google Scholar 

  11. Nerode, A.: Linear automaton transformations. In: Proceedings of the American Mathematical Society, vol. 9, pp. 541–544. American Mathematical Society (1958)

    Google Scholar 

  12. Mezei, J., Wright, J.: Algebraic automata and context-free sets. Information and Control 11, 3–29 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  13. Dezani-Ciancaglini, M., Giovannetti, E., de’ Liguoro, U.: Intersection Types, Lambda-models and Böhm Trees. In: MSJ-Memoir. Theories of Types and Proofs, vol. 2, pp. 45–97. Mathematical Society of Japan (1998)

    Google Scholar 

  14. Babaev, A.A., Soloviev, S.V.: Coherence theorem for canonical maps in cartesian closed categories. Journal of Soviet Mathematics 20 (1982)

    Google Scholar 

  15. de Groote, P., Pogodalla, S.: On the expressive power of abstract categorial grammars: Representing context-free formalisms. Journal of Logic, Language and Information 13(4), 421–438 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  16. Thatcher, J.W.: Characterizing derivation trees of context-free grammars through a generalization of finite automata theory. Journal of Computer and System Sciences 1(4), 317–322 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  17. Schmidt-Schauß, M.: Decidability of arity-bounded higher-order matching. In: Baader, F. (ed.) CADE 2003. LNCS, vol. 2741, pp. 488–502. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Comon, H., Jurski, Y.: Higher-order matching and tree automata. In: CSL, pp. 157–176 (1997)

    Google Scholar 

  19. Loader, R.: Higher order β matching is undecidable. Logic Journal of the IGPL 11(1), 51–68 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  20. Stirling, C.: A game-theoretic approach to deciding higher-order matching. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 348–359. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Robertson, N., Seymour, P.D.: Graph minors. v. excluding a planar graph. J. Comb. Theory, Ser. B 41(1), 92–114 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  22. Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81–90. IEEE Computer Society Press, Los Alamitos (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Bordeaux – Sud-Ouest, 351, cours de la Libération Bâtiment A29, 33405, Talence cedex, France

    Sylvain Salvati

Authors
  1. Sylvain Salvati
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Japan Advanced Institute of Science and Technology, 1-1 Asahidai, Nomi, 923-1292, Ishikawa, Japan

    Hiroakira Ono

  2. National Institute of Informatics, 2–1–2 Hitotsubashi, Chiyoda-ku, 101–8430, Tokyo, Japan

    Makoto Kanazawa

  3. Centro de Informática, Universidade Federal de Pernambuco, Recife, PE, Brazil

    Ruy de Queiroz

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Salvati, S. (2009). Recognizability in the Simply Typed Lambda-Calculus. In: Ono, H., Kanazawa, M., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2009. Lecture Notes in Computer Science(), vol 5514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02261-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02261-6_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02260-9

  • Online ISBN: 978-3-642-02261-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation