Skip to main content
SpringerLink
Log in

On the Membership Problem for Non-Linear Abstract Categorial Grammars

  • Published:
Journal of Logic, Language and Information Aims and scope Submit manuscript

Abstract

In this paper we show that the membership problem for second order non-linear Abstract Categorial Grammars is decidable. A consequence of that result is that Montague-like semantics yield to a decidable text generation problem. Furthermore the proof we propose is based on a new tool, Higher Order Intersection Signatures, which grasps statically dynamic properties of λ-terms and presents an interest in its own.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  • Aoto T., Ono H. (1994) Non-uniqueness of normal proofs for minimal formulas in implication-conjunction fragment of BCK. Bulletin of the Section of Logic 23(3): 104–112

    Google Scholar 

  • Aoto T. (1999) Uniqueness of normal proofs in implicational intuitionistic logic. Journal of Logic, Language and Information 8(2): 217–242

    Article  Google Scholar 

  • Barendregt, H. P. (1984). The lambda calculus: Its syntax and semantics, Vol. 103. Studies in logic and the foundations of mathematics. Amsterdam: North-Holland. revised edition.

    Google Scholar 

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

  • Damm W. (1982) The IO- and OI-hierarchies. Theoretical Computer Science 20: 95–207

    Article  Google Scholar 

  • Dezani-Ciancaglini, M., Giovannetti, E., & de’ Liguoro, U. (1998). 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.

  • de Groote, P. (2001). Towards abstract categorial grammars. In Association for Computational Linguistic (Eds.), Proceedings 39th annual meeting and 10th conference of the European chapter, (pp. 148–155). Morgan Kaufmann Publishers.

  • de Groote, P. (2007). Towards a montagovian account of dynamics. In: Proceedings of semantics in linguistic theory XVI. CLC Publications.

  • Girard J. -Y., Taylor P., Lafont Y. (1989) Proofs and types. Cambridge University Press, Cambridge

    Google Scholar 

  • Hillebrand, G. G. (1994). Finite model theory in the simply typed lambda calculus. PhD thesis, Department of Computer Science, Brown University, Providence, Rhode Island 02912.

  • Hirokawa, S., & Tatsuta, M. (2000). Long D-normal form yields uniqueness of proofs. In Proceedings of logic colloqium.

  • Huet, G. (1976). Résolution d’équations dans des langages d’ordre 1,2, . . .,ω. Thèse de doctorat es sciences mathématiques, Université Paris VII.

  • Kanazawa M. (2006) Abstract families of abstract categorial languages. Electronic Notes in Theoretical Computer Science 165: 65–80

    Article  Google Scholar 

  • Kanazawa, M. (2007). Parsing and generation as datalog queries. In Proceedings of the 45th annual meeting of the association for computational linguistics (pp. 176–183). Association for Computational Linguistics.

  • Loader, R. (2001) The undecidability of λ-definability. In C. A. Anderson & M. Zeleny (Eds.), Logic, meaning and computation: Essays in memory of Alonzo church (pp. 331–342). Kluwer

  • Montague R. (1974) Formal philosophy: Selected papers of Richard Montague. Yale University Press, New Haven, CT

    Google Scholar 

  • Pogodalla, S. (2001). Réseaux de preuve et génération pour les grammaires de types logiques. PhD thesis, Institut National Polytechnique de Lorraine.

  • Pogodalla, S. (2004). Computing semantic representation: Towards ACG abstract terms as derivation trees. In Proceedings of the seventh international workshop on tree adjoining grammar and related formalisms (TAG+7) (pp. 64–71).

  • Salvati, S. (2005). Problèmes de filtrage et problèmes d’analyse pour les grammaires catégorielles abstraites. PhD thesis, Institut National Polytechnique de Lorraine.

  • Seki H., Matsumura T., Fujii M., Kasami T. (1991) On multiple context free grammars. Theoretical Computer Science 88(2): 191–229

    Article  Google Scholar 

  • Statman R. (1979) The typed lambda-calculus is not elementary recursive. Theoretical Computer Science 9: 73–81

    Article  Google Scholar 

  • Takahashi M., Joshi A. K., Levy L. S. (1975) Tree adjunct grammars. Journal of Computer and System Sciences 10(1): 136–163

    Article  Google Scholar 

  • Tatsuta, M. (1999). Uniqueness of d-normal proofs. In Proceedings of 7th Asian logic conference (pp. 41–42).

Download references

Author information

Authors and Affiliations

  1. INRIA Bordeaux Sud-Ouest, LaBRI, Université de Bordeaux, Unité Mixte de Recherche CNRS (UMR 5800), 351, cours de la Libération, 33405, Talence cedex, France

    Sylvain Salvati

Authors
  1. Sylvain Salvati
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sylvain Salvati.

Additional information

This work was done while the author was at the National Institute of Informatics as a postdoctoral fellow of the Japan Society for the Promotion of Science, and was supported by the Grant-in-Aid for Scientific Research (18-06739).

Rights and permissions

Reprints and permissions

About this article

Cite this article

Salvati, S. On the Membership Problem for Non-Linear Abstract Categorial Grammars. J of Log Lang and Inf 19, 163–183 (2010). https://doi.org/10.1007/s10849-009-9110-0

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10849-009-9110-0

Keywords

Search

Navigation