Leverhulme Project Proposal
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.