Leverhulme Project

Lexical Semantics in Type Theory with Coercive Subtyping

Zhaohui Luo
Dept of Computer Science
Royal Holloway, Univ of London

Funded by the Leverhulme Trust (Grant Ref: F/07-537/AJ; 147K; June 2011 -- May 2014)

Summary of the Project Proposal

There have been very interesting developments in lexical semantics in the last fifteen years including, e.g., the Generative Lexicon Theory [6]. However, the research so far has failed to provide an adequate formal account of the lexical theories. Most of the employed formalisms are based on (extensions of) the Montague grammar and unable to capture the important linguistic phenomena satisfactorily.

The modern type theories such as [5,2] provide a promising formalism for lexical semantics: the rich type structures are capable to capture various sophisticated lexical phenomena. There is a problem, though. In a type-theoretical semantics, as studied by Ranta [7], types are used in a crucial way in place of the functional subsets as used in Montague grammar, but the operations on types are rather fewer than those on functional subsets and appear to be not enough for a formal semantics. This has become a major obstacle in obtaining a satisfactory type-theoretical semantics.

To solve this problem, we have conducted a preliminary study [3]. It shows that a theory of subtyping is not only useful but crucial in giving a natural and adequate type-theoretical semantics and that coercive subtyping [4] provides us with such a framework. The first goal of the current project is to develop this type-theoretical approach, employing modern type theory with coercive subtyping to obtain an adequate formal account of lexical semantics as studied by Pustejovsky [6], Asher [1] and others.

In the past two decades, type theory has been applied successfully to interactive theorem proving. The second goal of this project is to apply the type theory based proof technology to linguistic reasoning, by designing and implementing a natural language reasoning tool based on the type-theoretical semantics, on top of an existing proof assistant. This will also open up a new research direction to apply the proof technology to computer-assisted reasoning with natural languages.

[1] N. Asher. Lexical Meaning in Context: A Web of Words. CUP, 2010.
[2] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. OUP, 1994.
[3] Z. Luo. Type-theoretical semantics with coercive subtyping. Semantics and Linguistic Theory 20 (SALT20), Vancouver. 2010.
[4] Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9(1). 1999.
[5] P. Martin-Lof. Intuitionistic Type Theory. Bibliopolis, 1984.
[6] J. Pustejovsky. The Generative Lexicon. MIT, 1995.
[7] A. Ranta. Type-Theoretical Grammar. OUP, 1994.

Relevant publications and documents

  • S. Chatzikyriakidis and Z. Luo. Adjectives in a Modern Type-Theoretical Setting. The 18th Conf. on Formal Grammar, Dusseldorf. LNCS 8036. 2013. [pdf file of the final version available.]
  • Z. Luo. Formal Semantics in Modern Type Theories with Coercive Subtyping. Linguistics and Philosophy, 35(6). 2012. [pdf-file available]
  • N. Asher and Z. Luo. Formalisation of coercions in lexical semantics. Sinn und Bedeutung 17, Paris. 2012. [abstract and full paper available]
  • S. Chatzikyriakidis and Z. Luo. An Account of Natural Language Coordination in Type Theory with Coercive Subtyping. Constraint Solving and Language Processing 2012. 2012.
  • Z. Luo. Common nouns as types. LACL'12, LNCS 7351. 2012.
  • T. Xue and Z. Luo. Dot-types and their implementation. LACL'12, LNCS 7351. 2012.
  • Z. Luo. Notes and slides at ESSLLI 2011, Ljubljana, Slovenia (for a course on Lexical Semantics, taught together with Prof Nicholas Asher)
  • Z. Luo. Contextual analysis of word meanings in type-theoretical semantics. Logical Aspects of Computational Linguistics (LACL'2011). LNAI 6736, 2011.
  • Z. Luo. Type-theoretical semantics with coercive subtyping. Semantics and Linguistic Theory 20 (SALT20), Vancouver. 2010.
  • Z. Luo and P. Callaghan. Coercive subtyping and lexical semantics (extended abstract). Logical Aspects of Computational Linguistics (LACL'98). 1998.