Natural language semantics uses many different kinds of objects, incl. individuals, prop- ositions, properties, situations, events, and kinds. Simple type theories tame this ‘zoo’ [1] by assuming only a small number of primitive objects (e.g. individuals, situations), and obtaining all other objects via constructions out of these primitives. By distinguishing subtypes (or sorts), these theories straightforwardly obtain more finely-grained types (e.g. concrete vs. abstract individuals), allowing them to explain selectional restrictions (e.g. eat \(\{^{\checkmark}\) an apple, \(^{\#}\)an opinion\(\}\)) (i). However, this strategy blocks an easy account of selectional flexibility (i.e. why some predicates accept different-type arguments; e.g. remember \(\{\)the girl, that she was dancing\(\}\)) (ii) and of semantic relations bet- ween such arguments (e.g. why remember that she \(\ldots\) entails remember the girl) (iii).

My talk answers this challenge by unifying intuitively distinct types in a single higher-rank type, whose objects code the lower-type objects (see [2-4]). This unification allows the same-type interpretation of expressions from different grammatical categories, immediately explaining (ii) and – through the internal structure of the new objects – (iii). Selectional restrictions (see (i)) are explained through the particular lexical semantics of the embedding predicate and its interaction with the new, higher-type object.

Bibliography

1. Emmon Bach, Natural language metaphysics, Logic, Methodology and Philosophy of Science VII (Ruth Barcan Marcus, editor), Elsevier, 1986, pp. 573–593.
2. Kristina Liefke, Modelling selectional super-flexibility, Semantics and Linguistic Theory, vol. 31 (2021), pp. 324–344.
3. Kristina Liefke and Markus Werning, Evidence for single-type semantics, Journal of Semantics, vol. 35 (2018), no. 4, pp. 639–685.
4. Nadine Theiler, Floris Roelofsen, and Maria Aloni, A uniform semantics for declarative and interrogative complements, Journal of Semantics, vol. 35 (2018), no. 3, pp. 409–466.

As pointed out by Geach and others, common nouns (CNs) are special in that they have their own criteria of identity (ICs) [3]. In type-theoretical semantics, this provides a justification for the idea of interpreting CNs as types and the ICs as equivalence relations over the types, i.e., the pairs called setoids [6]. However, there is a discrepancy here in the CNs-as-types paradigm: setoids are pairs, not types. Although in most cases ICs are ‘commonly understood’ and can hence be ignored, they cannot be so ignored in sophisticated cases where it is only adequate to interpret CNs as setoids [1,7]. Furthermore, it is known that in practice working with setoids is inconvenient and direct treatments of quotient types are called for. The recent study of Higher Inductive Types [4,5,2], as a development in the research on Homotopy Type Theory as a foundational language of mathematics, has opened up a new avenue and, in particular, it enables the study of quotient types from a fresh angle with much needed computational justification of the resulting type theory. If time permits, I’ll also discuss some related ongoing research topics, albeit only briefly.

Bibliography

1. S. Chatzikyriakidis and Z. Luo. Formal Semantics in Modern Type Theories. Wiley/ISTE, 2020.
2. T. Coquand, S. Huber, and P. Mortberg. On higher inductive types in cubical type theory. Proceedings of the 33rd Symposium on Logic in Computer Science (LICS’18), 2018.
3. P. Geach. Reference and Generality. Cornell University Press, 1962. (Third edition in 1980).
4. HoTT. Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013.
5. P. Lumsdaine and M. Shulman. Semantics of higher inductive types. Math. Proc. Camb. Phil. Soc., 169:159–208, 2020.
6. Z. Luo. Common nouns as types. In D. Bechet and A. Dikovsky, editors, Logical Aspects of Computational Linguistics (LACL’2012). LNCS 7351, pages 173–185, 2012.
7. Z. Luo. Modern Type Theories: Their Development and Applications. Tsinghua University Press, 2024. (In Chinese).

Polysemous nouns have closely related senses that denote different types of entities. For instance lunch can denote an eventuality (eating lunch) or a physical entity (the food eaten). Furthermore, polysemous nouns can be felicitous in copredication constructions such as (1) that arguably elicit both of these senses simultaneously.

(1) Lunch was delicious and lasted for two hours.

Data such as (1) have been claimed to pose a problem for canonical approaches to formal semantics in the Frege-Church-Montague tradition (see e.g., Chomsky 2000). For instance, given an assumption that lunch eating events and food are members of the domains of different semantic types, it can be shown that there is no set characterisable in simply typed lambda calculus that has as members entities that are lunch-eating eventualities and/or food.

This talk looks at two responses to the challenge of polysemy. A large number of analyses of polysemy go for an enrichment of the type theory, and so add structure. A lesser known option, I suggest, is to impoverish the type theory. This can be implemented within a mono-typed semantics as developed in e.g., Liefke 2014, Liefke & Werning 2018. However, I suggest there are reasons for why the latter approach still needs to make use of the kind of extra structure utilised by the former, even if this is not introduced in the type theory. I then discuss how distinct these two approaches may turn out to be.