Types of lexical semantics

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.