Type Polymorphism, Natural Language Semantics, and TIL

Abstract

Transparent intensional logic (TIL) is a well-explored type-theoretical framework for semantics of natural language. However, its treatment of polymorphic functions, which are essential for the analysis of various natural language phenomena, is still underdeveloped. In this paper, we address this issue and propose an extension of TIL that introduces polymorphism via type variables ranging over types and generalized variables ranging over constructions and types. Furthermore, we offer an analysis of sentences involving non-specific notional attitudes of the general form ‘A considers (believes, desires, wants, seeks, ...) something’.

1 Introduction

Analysis of notional attitudes exemplified by the following cases¹:

• I am thinking of Pegasus.

• Ponce de Leon searched for the fountain of youth.

• Schliemann sought the site of Troy.

• Ctesias is hunting unicorns.

has a long tradition in the semantic analysis of natural language. In this paper, we will be interested in a more general class of these sentences that can be obtained by replacing the concrete objects² of the respective attitudes (thinking, searching, hunting, etc.) with non-specific ones:

• I am thinking of something.

• Ponce de Leon searched for something.

• Schliemann sought the site of something.

• Ctesias is hunting something.

This represents a specific challenge to type-theoretic approaches to natural language semantics for obvious reasons: since we cannot know in advance what type of object is being referred to by ‘something’ (e.g., I can be thinking of people, trees, houses, places, ..., numbers, sets, types, functions, etc.) we have to adopt polymorphic properties that can be applied to an unspecified range of objects. In other words, we have to introduce polymorphism into the system. There are two general approaches to how to treat polymorphism which we might call syntactic polymorphism and semantic polymorphism.³

The first approach treats polymorphism just as a meta-language tool for referring to a wide range of similar functions. Usually a meta-language symbol is introduced, e.g., ‘$\alpha$’, that ranges over all the possible variations. For example, we might encounter a function isEqual of the type $(\alpha \rightarrow \alpha \rightarrow Bool)$ which takes two objects of type $\alpha$ as arguments and returns True if they are equal and False otherwise. This approach entails, among other things, that we have similar yet different functions specific for each type. For example, if we are dealing with the equality of individuals, we get the function $isEqual\_Ind$ of the type $(Ind \rightarrow Ind \rightarrow Bool)$, if we are dealing with natural numbers, we get the function $isEqual\_Nat$ of the type $(Nat \rightarrow Nat\rightarrow Bool)$, etc. But, generally speaking, there is no ‘the’ equality function, only its multiple instances tailored for each type. Hence, $(\alpha \rightarrow \alpha \rightarrow Bool)$ is not a type, just a notation shorthand for various types.

The second approach treats polymorphism as a semantic feature of the system itself. In practice, this means extending the definition of types and allowing the type variables to appear on the object level of the framework. For example, using this approach the type $(\alpha \rightarrow \alpha \rightarrow Bool)$ is a proper type of the system (or more specifically, type constructor/type-valued function) and the general properly polymorphic function isEqual can thus be entertained and applied to objects of any type. For instance, if we apply the type constructor $(\alpha \rightarrow \alpha \rightarrow Bool)$ to the type Ind, we get the type $(Ind \rightarrow Ind \rightarrow Bool)$, etc.

In this paper, we investigate the issue of non-specific notional attitudes from the perspective of transparent intensional logic (TIL; Tichỳ, 1988). TIL is a well-explored type-theoretic framework for the semantics of natural language, however, it relies on the syntactic approach to polymorphism where the type variables are treated just as placeholders. This puts them outside of the semantic framework of TIL and thus provides much less interesting analyses in return. In this paper, we propose an extension of TIL that handles polymorphism semantically via type variables ranging over types and generalized variables ranging over constructions and types. Furthermore, we offer the analysis of sentences involving non-specific notional attitudes of the general form ‘A considers (believes, desires, wants, seeks, ...) something’.

This paper is structured as follows: in Sect. 2 we present the basics of TIL, in Sect. 3 we examine closely the treatment of polymorphism and variables in TIL, in Sect. 4 we introduce type variables and in the final section, Sect. 5, we introduce generalized variables, offer an extension to the ramified type theory of TIL, and propose a semantic analysis of non-specific notional attitudes.

Remark 1

The problem of polymorphism is closely related to the problem of ‘nominalization’, i.e., the process of the transformation of non-noun phrases (verb phrases, common nouns, ...) into noun phrases and the problem of flexible predicates such as ‘good’, ‘fun’, ‘interesting’, ‘boring’, etc. that are predicable over a variety of types of objects (‘Sleep is good’, ‘Sleeping is good’, ‘To sleep is good’, ‘That they sleep is good’, etc.). Also, as was already observed by Chierchia (1982), type theory in general enforces constraints on the structure of natural language that is not directly observable. In natural language it seems to be the case that we are using ‘one size fits all’ predicates, e.g., ‘is interesting’ can be applied to cakes just as to mathematical results. As Chierchia put it:

A theory [of types] imposes various limitations on the categorial structure of English syntax. As we will see, in type theory properties (like, say, to be fun) have to be ranked differently in the type hierarchy according to whether they are attributed to individuals (as in ‘John is fun’) or to properties (as in, say, ‘to dance is fun’). Such ranking doesn’t seem to have any overt correlate in the syntactic behavior of predicate nominals like fun in natural languages. So, those limitations that type theory imposes on English syntax are likely to turn out to be artificial (Chierchia, 1982, p. 305).

On the other hand, it seems certainly true that in both cases we are encountering different kinds of ‘interestingness’ with various applicability criteria (an interesting cake is probably interesting in a different sense than a mathematical theorem) and many-sorted type-theoretical approaches are well-equipped to handle these differences. Briefly put, although type-theoretical approaches to natural language semantics without a doubt come with their own set of challenges, the benefits of utilizing them (e.g., blocking paradoxical behavior due to violations of the vicious circle principle, avoiding categorical mistakes, etc.) seem to generally outweigh their potential drawbacks.

2 Brief Introduction to TIL

Transparent intensional logic (TIL; Tichý, 1988; Duží et al., 2010; Raclavský et al., 2015) is a theory of abstract constructions that utilizes the extended language of typed lambda calculus with partial functions and focuses on the semantics of natural language.⁴ In spirit, it shares many similarities with Montague semantics but the meanings of natural language expressions are understood rather in terms of algorithms (hyperintensions) than in terms of functions from possible worlds (intensions), which takes it closer to the systems with an interpreted formal syntax such as Martin-Löf constructive type theory (see, e.g., Pezlar, 2017).

Syntactically, TIL’s theory of constructions can be captured using the following four construction terms, namely variables, compositions, closures, and n-executions, respectively:

$$\begin{aligned} \textit{constructions} \; := \; x \quad \vert \quad [C \, C_1 \ldots C_m] \quad \vert \quad [\lambda x_1 \ldots x_m C] \quad \vert \quad {^nX} \end{aligned}$$

where $C_i$ is any construction, X is either a construction or a non-construction (e.g., a truth value, an individual, a number, etc.).⁵

The first three constructions roughly correspond to variables, function applications, and function abstractions as known from $\lambda$-calculus. Construction n-execution allows us to either execute constructions to determine what object they construct, if any (if $n > 0$),⁶ or not execute them, i.e., leave them as they are (if $n = 0$).⁷ What constructions construct might depend on a valuation v, i.e., an assignment of values to free variables. In that case, we say that they v-construct. If a construction C v-constructs nothing at all, we will say that it is a v-improper construction. Otherwise, we say that C is a v-proper construction. If we have two constructions $C_1$ and $C_2$ that v-construct the same object X, or they are both v-improper, we will say that $C_1$ and $C_2$ are v-congruent constructions, denoted as $C_1 \cong C_2$. If they are v-congruent for all valuations v, we will say that $C_1$ and $C_2$ are equivalent constructions, denoted as $C_1 = C_2$.

In standard TIL, there are four atomic types forming the type base B: truth values, individuals, real numbers/time moments, and possible worlds, denoted as $o , \iota , \tau , \omega$, respectively.⁸ These basic types are then expanded with types of n-th order constructions, denoted as $*_n$. If $\alpha$ and $\beta 1 , \ldots , \beta _m$ are types, then we can form a function type $(\alpha \beta _1 \ldots \beta _m)$. Specifically, it is a type of function from the elements of type $\beta 1 , \ldots , \beta _m$ to the elements of type $\alpha$.⁹

Since constructions can v-construct other objects or be v-constructed by other constructions they receive two-dimensional typing: the first dimension is the type of the construction itself, denoted as C/type, the second dimension is the type of the object the construction is supposed to construct, denoted as C : type. We can also chain these notations to get $C / type_1 : type_2$. For example, $[^0+ \; ^05\; ^07] / *_1 : \nu$ which can be read as ‘$[^0+ \; ^05\; ^07]$ is a first-order construction typed to construct natural numbers’.¹⁰

To simplify notation, we denote 0-execution by ${\textbf {boldface}}$ font, with the exception of standard logical and mathematical symbols such as ‘$+$’, ‘$=$’, ‘$\forall$’, ‘$\supset$’, etc. which we keep in normal font with 0-execution implicitly assumed. Also, we will use infix notation whenever expected. For example, instead of ‘$[^0+ \; ^05\; ^07]$’ we will write ‘$[{\mathbf {5}} + {\mathbf {7}}]$’ and instead of ‘$[^0\supset A \; B]$’ we will write ‘$[A \supset B]$’. Furthermore, we extend the standard notation of closure construction by including explicit typing of variables and omit the outer most brackets whenever possible. Thus, we will write $\lambda x_1 : \alpha _1 \, \ldots \, x_m : \alpha _m \, Y$ instead of $[ \lambda x_1 \ldots x_m \, Y]$.¹¹

Example 1

(Sample analysis) The sentence:

(s):

Alice believes there is a natural number greater than four but smaller than five.

can be analysed as follows (see Fig. 1 for the corresponding type-checking tree):

$$\begin{aligned} \lambda w : \omega \; \lambda t : \tau \; [{\textbf {Believe}}^*_{wt} \; {\textbf {Alice}} \; ^0[\exists x : \nu [[x > {{\textbf {4}}}] \wedge [x < {{\textbf {5}}}] ] ]] \end{aligned}$$

Reading this construction from left to right (with some minor simplifications):

• ‘$\lambda w : \omega \; \lambda t : \tau$’ binds the world and time parameters w and t—which receives the function $Believe^*$ as two of its four arguments (see below)—and displays their type annotations, i.e., the variable w ranges over objects of type $\omega$ (possible worlds) and the variable t ranges over objects of type $\tau$ (time moments captured as real numbers),

• ${\textbf {Believe}}^*$ is a construction (specifically a trivialization also known as 0-execution) that constructs the function $Believe^*$ of type $(((o \iota *_n) \tau ) \omega )$, usually shortened as $(o \iota *_n)_{\tau \omega }$. The superscript $^*$ indicates that this is a constructional/hyperintensional belief (i.e., a belief that a given construction v-constructs a proposition that is true in a given world and time of evaluation, or that a given construction v-constructs a truth value true, in the case of mathematics and logic), which is different from other types of belief (e.g., a sentential belief, i.e., a belief that a given proposition is true in a given world and time, which would have type $(o \iota (o_{\tau \omega }))_{\tau \omega }$). Informally, $Believe^*$ is a function that takes a possible world, a specific time moment in that world, an individual, and a construction of a proposition/truth value, and returns true if that individual believes that the construction produces (a proposition that takes) the truth value true, otherwise false.

• ‘$_{wt}$’ is used as a shorthand for consecutive applications of world and time parameters to the function $Believe^*$. In full, it should be written as: $[[{\textbf {Believe}}^* \; w ] \; t]$,

• ${\textbf {Alice}}$ is a construction (a trivialization, see above) that constructs the individual Alice of type $\iota$.

• $^0[\exists x : \nu \, [[x > {{\textbf {4}}}] \wedge [x < {{\textbf {5}}}] ] ]$ is a higher-order construction (due to trivialization) that constructs a first-order construction, namely the composition construction $[\exists x : \nu \, [[x > {{\textbf {4}}}] \wedge [x < {{\textbf {5}}}] ] ]$. ‘$\exists x : \nu \ldots$’ is an abbreviation for ‘$[\exists \; \lambda x : \nu \, [\ldots ] ]$’ where $\exists$ is the existential quantifier of type $(o(o\nu ))$ applied to the class of numbers $\lambda x : \nu \, [\ldots ]$ and returns true if the class is non-empty, otherwise false.

Fig. 1

Type-checking tree

3 Polymorphism in TIL

3.1 The Problem

Let us try to analyse our initial examples involving notional attitudes. Since all of the sentences share an analogous form ‘[subject] + [notional attitude] + [object]’, we will focus only on the first sentence ‘I am thinking of something’. Furthermore, to slightly simplify it, we replace the personal pronoun ‘I’ with a proper noun ‘Alice’ and obtain:

• (1’) Alice is thinking of something.

In TIL, we can analyze it, e.g., in the following manner:

$$\begin{aligned} \lambda w : \omega \; \lambda t : \tau \; \exists x : \,?\, {[}{} {\textbf {Think}}_{wt} \; {\textbf {Alice}} \; x] \end{aligned}$$

which constructs the proposition (a function from possible worlds w and time moments t to truth values) that is true if there is something Alice is thinking of, otherwise it is false. However, we encounter problems once we start checking types of the involved objects. Namely, it is unclear over what type of objects should the variable x range and, consequently, what the type of the function Think should be.

For specific instances this is straightforward. For example, assuming Alice is thinking of some individual (e.g., ‘Bob’), we can simply restrict the variable x to the type $\iota$, i.e., $x : \iota$, and the type of the function Think would become $(o\iota \iota )_{\tau \omega }$, i.e., $Think / (o\iota \iota )_{\tau \omega }$. If she is thinking of some property of natural numbers (e.g., ‘being prime’), we would have $x : (o\nu )$ and $Think / (o \iota (o \nu ) )_{\tau \omega }$, etc. But in more general cases, such as ‘Alice is thinking of something’, where no specific type of object of Alice’s contemplation is known or can be known, difficulties arise. In particular, we have no appropriate type to assign to the variable x, which we symbolized by ‘?’ in the corresponding analysis above. Thus, we need variables that range over objects of any type, not just over objects of some specific type.¹²

3.2 TIL: Current State

In TIL, we can encounter many type-theoretically polymorphic functions (see Table 1), but what exactly are they? Duží et al. (2010) we are given the following informal explanation in a footnote:

By ‘type-theoretically polymorphous functions’ we mean a set of functions that are defined and thus behave in the same way, independently of their type. For instance, any member of the set of functions Cardinality associates a finite class with the number of its elements. Hence this definition is polymorphous; there are actually infinitely many cardinality functions, one for each type: $Card1/(\tau (o\iota ))$ – the number of a set of individuals, $Card2/(\tau (o\tau ))$ – the number of a set of numbers, etc., which we indicate by using a type variable $\alpha$ in the type of $Cardinality/(\tau (o\alpha ))$. (Duží et al., 2010, p. 86)

From the above description it is clear that the symbol ‘$\alpha$’ plays the role of type variable. Thus, we can view type-theoretically polymorphic functions as functions whose types involve at least one occurrence of a type variable. This seems straightforward, unfortunately, it is not obvious what exactly a type variable from the TIL perspective is. The only available variables in standard TIL are variables understood as construction and these do not range over types themselves, only over objects of specific types.

Table 1 Examples of polymorphic functions of TIL

So how should we understand type variables? As already discussed above, there are essentially only two options how to approach them:

• 1. Type variables as metavariables: this is the easier, but also the less interesting answer. Type variables become just syntactic placeholders, which means that they are beyond the semantic framework of TIL.

• 2. Type variables as variables: this is the more attractive answer, yet also the more demanding. Since ‘standard’ variables are considered as constructions, it seems reasonable to consider type variables as some kind of constructions as well. This way, type variables would enrich the semantic framework of TIL. However, a new kind of construction v-constructing types would have to be introduced.

Regarding type variables as metavariables seems to be the implicit approach taken in Duží et al. (2010).¹³ Type variable ‘$\alpha$’ is not considered as a part of TIL’s ramified type theory, rather as a metalanguage device. See, e.g.,:

Remark. $\alpha$-sets of elements of type $\alpha$ are modelled by their characteristic functions. Thus they are $(o \alpha )$-objects. For instance, a set of individuals is an object of type $(o\iota )$, a set of real numbers is an object of type $(o\tau )$, a set of couples of real numbers (i.e., a binary relation over reals) is an object of type $(o \tau \tau )$. (Duží et al., 2010, p. 44).

It gets the job done, however, it is somewhat undesirable given the fact that one of the basic credos of TIL is that it has no use for metalanguage: “TIL does not need a metalanguage, since [it has] a ramified type hierarchy instead” (see Duží et al., 2010, p. 55).

Understanding type variables as constructions seems to be the approach most in line with TIL semantic doctrine. After all, type variables are variables, and variables are treated as constructions in TIL, thus type variables should be treated as constructions as well.¹⁴ Furthermore, this would allow us to regard type variables as proper entities of the semantic framework of TIL (with appropriately extended ramified type theory). First, however, we explore TIL’s standard notion of variables as constructions developed by Tichý (1988, pp. 60–62) and then we propose how to extend it to cover even type variables and generalized variables.

3.3 Variables

As discussed above, variables are basic constructions of TIL and they construct objects dependently on a valuation function v. This means, among other things, that variables are taken as extra-linguistic entities, whose procedural content consists in retrieving values, i.e., variables are not just symbolic placeholders. To better understand this approach to variables, we will examine Tichý’s original definition from Tichý (1988).¹⁵

Definition 1

(Variable) (Tichý, 1988, p. 60) Let R be an arbitrary non-empty collection. By an R-sequence we shall understand any infinite sequence:

(s):

$X_1, X_2, X_3, X_4, \ldots$

(with or without repetitions) of members of R.

For any natural number n let $\vert R \vert _n$ be the (incomplete) [i.e., depending on external sequence] construction which consists in retrieving the n-th member of an R-sequence. Constructions of this form will be called variables.

Definition 2

(Valuation) (Tichý, 1988, p. 61) In [a] more general case [where various logical types are needed] we shall need whole arrays of sequences containing an $R^i$-sequence for each type $R^i$. We shall call such arrays valuations. Thus, where $R^1, R^2, R^3, R^4, \ldots$ is an enumeration (without repetitions) of all the types, a valuation is an array of the form

(v):

$\begin{matrix} X_1^1, X_2^1, X_3^1, X_4^1, \ldots \\ X_1^2, X_2^2, X_3^2, X_4^2, \ldots \\ X_1^3, X_2^3, X_3^3, X_4^3, \ldots \\ X_1^4, X_2^4, X_3^4, X_4^4, \ldots \\ \vdots \\ \end{matrix}$

where $X_1^i, X_2^i, X_3^i, X_4^i, \ldots$ is an $R^i$-sequence. Let v be this valuation. Relative to v, the variable $\vert R^i \vert _n$ constructs $X^i_n$, i.e., the n-th term of the $R^i$-sequence occurring in v.

Thus, a valuation array is, simply put, a sequence of sequences—to make this more apparent, we will utilize the following list notation:

$$\begin{aligned} \small v = \left[ \begin{array}{lcccc} \left[ X^1_1 \; , \; X^1_2 \; , \; X^1_3 \; , \; X^1_4 \; , \; \ldots \right] , &{} \\ \left[ X^2_1 \; , \; X^2_2 \; , \; X^2_3 \; , \; X^2_4 \; , \; \ldots \right] , &{} \\ \left[ X^3_1 \; , \; X^3_2 \; , \; X^3_3 \; , \; X^3_4 \; , \; \ldots \right] , &{} \\ \left[ X^4_1 \; , \; X^4_2 \; , \; X^4_3 \; , \; X^4_4 \; , \; \ldots \right] , &{} \\ \vdots \\ \end{array} \right] \end{aligned}$$

For example, let us have the following toy valuation array (or valuation for short) $v_1$:

$$\begin{aligned} \small v_1 = \left[ \begin{array}{lcccc} \left[ true^1_1 \; , \; false^1_2 \right] , &{} \\ \left[ 1^2_1 \; , \; 2^2_2 \; , \; 3^2_2 \; , \; \ldots \right] , &{} \\ \left[ Alice^3_1 \; , \; Bob^3_2 \; , \; Cecil^3_3 \; , \; Dana^3_4 \; , \; \ldots \right] , &{} \\ \vdots \\ \end{array} \right] \end{aligned}$$

In this case, the variable $\vert R^1 \vert _2$ receives through $v_1$ the value false, $\vert R^3 \vert _1$ retrieves Alice, etc. So what is a variable from Tichý’s point of view? It is essentially a search and retrieve mechanism that takes the coordinates $\langle i, n \rangle$ and some valuation array $v_m$ as input and returns the object located at that position as output.

From a type-theoretical perspective, the valuation array $v_1$ looks as follows:

$$\begin{aligned} \small v_1{_t} = \left[ \begin{array}{lcccc} \left[ o \; , \; o \right] , &{} \\ \left[ \nu \; , \; \nu \; , \; \nu \; , \; \ldots \right] , &{} \\ \left[ \iota \; , \; \iota \; , \; \iota \; , \; \iota \; , \; \ldots \right] , &{} \\ \vdots \\ \end{array} \right] \end{aligned}$$

where o, $\nu$, $\iota$ represent types of truth values, natural numbers, and individuals, respectively.¹⁶ But what about the variables $\vert R^i \vert _n$ themselves? What type do they belong to? Tichý gives the following answer:

($\hbox {c}_n$i) Let $\tau$ be any type of order n over B. Every variable ranging over $\tau$ is a construction of order n over B. If $\mathrm {X}$ is of (i.e., belongs to) type $\tau$ then $^0 \mathrm {X}$, $^1 \mathrm {X}$, and $^2 \mathrm {X}$ are constructions of order n over B.

Let $*_n$ be the collection of constructions of order n over B. (Tichý, 1988, p. 61)

Let types o, $\nu$, $\iota$ from our example above constitute the type base $\hbox {B}_1$. Then, by definition 16.1.– 1.($\hbox {t}_1$i) (see Tichý, 1988, p. 66) o, $\nu$, $\iota$ are types of order 1. Further, let us have variables $\vert R^1 \vert _1$, $\vert R^2 \vert _1$, $\vert R^3 \vert _1$ that range over types o, $\nu$, $\iota$, respectively. By definition 16.1.–2.($\hbox {c}_n$i) above, they are constructions of order 1 and hence they all belong to the same type $*_1$.

Due to the dependency of variables on valuation arrays, Tichý describes them as incomplete (or heteronomous) constructions (Tichý, 1988, p. 60). In other words, variables need some ‘external’ building material, in this case valuation arrays, to be able to construct anything. This might sound odd at first, but remember that in TIL, variables are not placeholders for values but general procedures for fetching them, so it makes sense that they need some independent database to get their values from.

Also note that if we want to learn what type of objects variables are v-constructing, we have to check not the type of the variables themselves, but the type of objects they are typed to construct within the ramified type hierarchy (see Appendix 7). For example, from the information given above, we can infer that variable $\vert R^2 \vert _1$ is typed to v-construct objects of type $\nu$ (the superscript ‘$^2$’ points our attention to the second row (R-sequence) of $v_1$, which is the type of natural numbers), i.e., $\vert R^2 \vert _1 / *_1 : \nu$, which can be read as “$\vert R^2 \vert _1$ is a first-order construction (a variable) that is typed to v-construct an object of type $\nu$”. In other words, it is the parameter i in conjunction with some specific valuation v that sets the range of the variable $\vert R^i \vert _n$ by pointing it to a specific row of v, which represents some type.

In the rest of the paper, we will write variables $\vert R^i \vert _n$, $\vert R^i \vert _{n+1}$, $\ldots$ simply as $x, y, \ldots$ to use a less cluttered notation.¹⁷

4 Type Variables

Recall that standard variables are restricted to objects of a certain type. For example, a variable x : o is restricted to the type of truth values. In other words, standard variables are locked to a single row in our valuation arrays and they v-construct only the objects of this specific row. However, we want them to range not over objects but over types. Thus, type variables should, in a way, range over columns of $v{_t}$ as opposed to standard variables that range over rows of v.

The definitions of variables and valuations presented above lead naturally to the following definition of type variables:

Definition 3

(Type variable) Let T be a collection of base types together with types of constructions and function types generated inductively from them (see Definition 16.1. in Tichý, 1988). By a T-sequence we shall understand any infinite sequence

(s’):

$t_1, t_2, t_3, t_4, \ldots$

(with or without repetitions) of members of T.

For any natural number n let $\vert T \vert _n$ be the (incomplete) construction which consists in retrieving the n-th member of an T-sequence. Constructions of this form will be called type variables.

Each valuation array v determines a T-sequence. It consists of the collection of types to which the objects of v belong and these types are linearly ordered in the same way as the rows of v to which they correspond are. For example, in the case of $v_1{_t}$ the T-sequence would be $[o, \nu , \iota , \ldots ]$, since the first three rows of v correspond to types of truth values, natural numbers, and individuals, respectively.¹⁸

Thus, the range of a type variable is the collection of all types of ramified type theory of TIL (see Appendix 7) ordered in a T-sequence. For example, the type variable $\vert T^1 \vert$ will v-construct the type o (i.e., the type represented by the first row of the valuation-array $v_1t$), $\vert T^2 \vert$ will v-construct $\nu$, etc.

It is worth emphasizing that we can keep the original structure of valuation arrays from Definition 1, we just need to adjust the ‘crawl’ mechanism accordingly to the above explanation. We can do this as follows: first, we will search $v_{1t}$ that can be obtained from the corresponding valuation array $v_{1}$, then: type variable $\vert T \vert _n$ v-constructs $t_n$, i.e., the n-th type of the T-sequence occurring in $v_t$.¹⁹ Hereinafter, we will write type variables $\vert T \vert _n, \vert T \vert _{n+1}, \ldots$ simply as $\alpha , \beta , \ldots$.

Once we start treating types as objects, we introduce a new type denoted $\textsf {Type}$ which is essentially the collection of all types. Thus, e.g., $o / \textsf {Type}$, $\nu / \textsf {Type}$, ..., $*_1 / \textsf {Type}$, etc. Furthermore, note that this type of types is not part of our valuation arrays, hence, we cannot have type variables ranging over it (it is not the case that $\textsf {Type} / \textsf {Type}$).²⁰

Now, let us return to our initial example, specifically to the analysis of the sentence ‘Alice is thinking of something’, which we already attempted unsuccessfully earlier. With type variables adopted, we could analyze it as follows:

$$\begin{aligned} \lambda w : \omega \; \lambda t : \tau \; \exists \alpha : \textsf {Type} \,[{\textbf {Thinks}}_{wt} \; {\textbf {Alice}} \; \alpha ] \end{aligned}$$

Note, however, that this analysis is not general enough. It can be interpreted as ‘Alice is thinking of some type’, since $\alpha$ is a type variable only. But the original sentence was ‘Alice is thinking of something’, which means she might be considering objects of various types, not just various types. Hence, a more general analysis will be necessary. Specifically, note that so far we have treated variables (ranging over constructions and non-constructions) and type variables (ranging over types) separately. Considering two different sorts of variables (valuations, etc.) can be, however, restricting sometimes, as we have just seen above. Thus, in the next section, we introduce a generalized notion of a variable that can range over objects belonging to any type (including the construction types $*_n$) and types as well.

5 Generalized Variables

So far, we have introduced i) standard variables ranging over constructions (and non-constructions) and operating with valuation arrays v and ii) type variables ranging over types and operating with type valuation arrays $v_t$. It follows that if we want to introduce variables that range over both constructions (and non-constructions) and types, the associated valuation arrays will have to contain the information from both arrays v and $v_t$. This can be simply done by taking v and enriching it with the corresponding type information contained in $v_t$. Note that since the types are constant throughout the whole rows of $v_t$ (recall, e.g., $v_1{_t}$ with the second row $[\nu \; , \; \nu \; , \; \nu \; , \; \ldots ]$), we do not need to incorporate the whole rows of $v_t$ into v, we just need to incorporate their first elements, since they already carry all the type information we need. Thus, valuation arrays for generalized variables will still be two-dimensional, but their first element will now be the type of all the subsequent elements.

Definition 4

(Generalized Variable) Let W be an arbitrary non-empty collection. By a W-array we shall understand any infinite sequence:

$$\begin{aligned}{}[X_0, X_1 , X_2 , X_3 , X_4 , \ldots ] \end{aligned}$$

such that the first member $X_0$ of the sequence is a type, while the other members $X_n$, $n > 0$, are the entities belonging to the type $X_0$.

   Then, for any natural number n, let $\vert W \vert _n$ be the (incomplete) construction that consists in retrieving the member $X_n$ of the given $W^i$-array, i.e., the element on the coordinates $\langle i, n \rangle$. The construction $\vert W \vert _n$ is a generalised variable.²¹

Definition 5

(Generalized valuation) In a more general case we will need a two-dimensional array containing a $W^i$-array $[X_0^i, X_1^i , X_2^i , X_3^i , X_4^i , \ldots ]$ for each type. We shall call such arrays generalized valuations. Thus, where $W^1, W^2, W^3, W^4, \ldots$ is an enumeration of all the types, a generalized valuation is a two-dimensional array of the form:

$$\begin{aligned} \small V = \left[ \begin{array}{lcccc} \left[ X^1_0 \; , \; X^1_1 \; , \; X^1_2 \; , \; X^1_3 \; , \; \ldots \right] , &{} \\ \left[ X^2_0 \; , \; X^2_1 \; , \; X^2_2 \; , \; X^2_3 \; , \; \ldots \right] , &{} \\ \left[ X^3_0 \; , \; X^3_1 \; , \; X^3_2 \; , \; X^3_3 \; , \; \ldots \right] , &{} \\ \left[ X^4_0 \; , \; X^4_1 \; , \; X^4_2 \; , \; X^4_3 \; , \; \ldots \right] , &{} \\ \vdots \\ \end{array} \right] \end{aligned}$$

Let V be this valuation. Relative to V, variable $\vert W^i \vert _n$ constructs $X^i_n$, i.e., the n-th member of the $W^i$-array occurring in V.

   For example, let us have the following generalized toy valuation array $V_1$:

$$\begin{aligned} \small V1 = \left[ \begin{array}{lcccc} \left[ o_0^1 \; , \; true_1^1 \; , \; false^1_2 \right] , &{} \\ \left[ \nu _0^2 \; , \; 1_1^2 \; , \; 2^2_2 \; , \; 3^2_3 \; , \; \ldots \right] , &{} \\ \left[ \iota _0^3 \; , \; Alice^3_1 \; , \; Bob^3_2 \; , \; Cecil^3_3 \; , \; Dana^3_4 \; , \; \ldots \right] , &{} \\ \vdots \\ \end{array} \right] \end{aligned}$$

Then, e.g., the variable $\vert W^1 \vert _2$ constructs through $V_1$ as value false, but through $\vert W^1 \vert _0$ it constructs o, $\vert W^3 \vert _1$ constructs Alice, $\vert W^3 \vert _0$ constructs $\iota$, etc.

To keep the notation simple, we will use the letters ‘x’, ‘y’, ...for generalized variables as well and it should always be clear from the context whether a standard or generalized variable is used.

5.1 Extending Ramified Type Theory

We have already described the mechanism of generalized variables that v-construct an object or a type to which the object belongs and their relation to expanded valuations, which closely mirrors the rationale behind standard variables. Next, we extend the definition of ramified type theory (see Appendix 7) to accommodate them accordingly.

The extension of ramified type theory will involve an introduction of an additional dimension to the ramification that will subsume the standard ramified type theory.²² This will allow us to have (generalized) variables that range over constructions (and non-constructions) as well as over all the types of the ‘lower’ dimensions.

First, we briefly introduce the ramified type theory of TIL. The core of the ramified type theory of TIL is its step-wise stratification of types by orders (for a proper specification, see Appendix 7). We start with first-order types (types inhabited by objects involving no constructions), then we define second-order types which are inhabited by constructions, including variables ranging over first-order types. Naturally, we can go further and introduce third-order types with constructions including variables that v-construct objects belonging to second or first-order types, and so on.

For example, assume our first-order types are natural numbers $\nu$ and truth values o. With these types, we can, e.g., form a new function type $(o \nu )$ which is the type of properties of natural numbers. As an example of a function of this type, consider the function Prime that takes a natural number and returns true if it is a prime number and false otherwise. Thus, e.g., the construction $[{\textbf {Prime}} \; {{\textbf {3}}}]$ constructs true and $[{\textbf {Prime}} \; {{\textbf {4}}}]$ constructs false. Note that Prime is still an object of the first-order type.

Next, assume we introduce a variable x ranging over natural numbers, i.e., $x : \nu$. Now, we can form a construction $[{\textbf {Prime}} \; x]$ which constructs true if the variable x gets assigned a prime number, otherwise it constructs false. Since this object contains a variable ranging over objects of the first-order type, it is an object of the second-order type.²³ Furthermore, we can introduce a variable y ranging over objects of the second-order type. For example, assume a higher-order predicate HasVariable that takes a construction of the second-order type and constructs true if it contains at least one occurrence of a variable (free or bound) and false otherwise. Thus, $[{\textbf {HasVariable}} \; y]$ constructs false, if the variable y gets assigned the construction $[{\textbf {Prime}} \; {{\textbf {3}}}]$ and it returns true if it gets assigned the construction $[{\textbf {Prime}} \; x]$. Note that in this case, the variable y ranges over objects of the second-order type, hence it itself is an object of the third-order types. Analogously, we could introduce even fourth-, fifth-, sixth-order variables and so on.

Now, the limitation of ramified type theory in its current form is that it does not regard types as proper objects, and, consequently, does not allow variables ranging over types. However, this is exactly what we need to adequately analyze sentences containing semantic polymorphism. As mentioned above, we extend the current ramified type theory with a new dimension that will allow us to introduce generalized variables that can range over both constructions (and non-constructions) and types. We start with basic ramified type theory, whose objects (including types) will be assigned a new common type called kind, then we introduce variables ranging over all objects of this supertype. Note that this modification mirrors the definition of ramified type theory where we begin with simple type theory and then expand it. Now, we start with ramified type theory and extend it.

Definition 6

Let $\textsf {Type}$ be a base, i.e., a set of types defined by ramified type theory (RTT).

($\hbox {k}_1$i):

Every member of $\textsf {Type}$ or an entity belonging to that member is a kind of order 1 over $\textsf {Type}$, denoted as $\square _1$.

($\hbox {C}_k$i):

Let ${\mathsf {A}}$ be any kind of order k over $\textsf {Type}$. Every generalized variable ranging over ${\mathsf {A}}$ is a construction of kind of order k over $\textsf {Type}$. If X is of (i.e., belongs to) kind ${\mathsf {A}}$ but is not itself a member of $\textsf {Type}$, i.e., it is an entity belonging to some member of $\textsf {Type}$, then $^0 X$, $^1 X$, and $^2 X$ are constructions of kind of order k over $\textsf {Type}$.

($\hbox {C}_k$ii):

If $0<m$ and $X_0, X_1, \ldots , X_m$ are constructions of kind of order k, then $[X_0 \; X_1 \ldots \, X_m]$ is a construction of kind of order k over $\textsf {Type}$. If $0<m$, ${\mathsf {A}}$ is a kind of order k over $\textsf {Type}$, and Y as well as the distinct variables $x_1, \ldots , x_m$ are constructions of kind of order k over $\textsf {Type}$, then $[\lambda _{\mathsf {A}} \, x_1 \ldots x_m \; Y]$ is a construction of kind of order k over $\textsf {Type}$.

($\hbox {C}_k$iii):

Nothing is a construction of kind of order k over $\textsf {Type}$ unless it follows from ($\hbox {C}_k$i) and ($\hbox {C}_k$ii).

Let $\square _k$ ($k > 1$) be the collection of generalized constructions of kind order k over $\textsf {Type}$. The collection of kinds of order $k+1$ over $\textsf {Type}$ is defined as follows:

($\hbox {K}_{k+1}$i):

Every kind of order k, denoted $\square _k$ ($k \ge 1$), is a kind of order $k+1$.

($\hbox {K}_{k+1}$ii):

If $0<m$ and ${\mathsf {A}}, {\mathsf {B}}_1 , \ldots , {\mathsf {B}}_m$ are kinds of order $k+1$ over $\textsf {Type}$, then the collection $({\mathsf {A}} {\mathsf {B}}_1 \ldots {\mathsf {B}}_m)$ of all m-ary (total and partial) mappings from ${\mathsf {B}}_1 , \ldots , {\mathsf {B}}_m$ to ${\mathsf {A}}$ is also a kind of order $k+1$ over $\textsf {Type}$.

($\hbox {K}_{k+1}$iii):

Nothing is a kind of order $k+1$ over $\textsf {Type}$ unless it follows from ($\hbox {K}_{k+1}$i) and ($\hbox {K}_{k+1}$ii).

So, simply put, first-order kinds are types of objects involving no generalized variables or constructions containing them. In other words, a kind of first-order is the type of all members of $\textsf {Type}$ or entities belonging to those members.²⁴ For example, $Alice / \iota$, ${\textbf {Alice}} / *_1$, $^0{\textbf {Alice}} / *_2$, $\iota / \mathsf {Type}$ are all first-order kinds, i.e., $Alice, {\textbf {Alice}}, {^0{\textbf {Alice}}}, \iota / \square _1$. But, e.g., a generalized variable x ranging over objects of first-order kind has type $\square _2$, i.e., $x / \square _2 : \square _1$.

Second-order kinds are types of objects containing generalized variables ranging over first-order kinds and constructions containing such variables. Analogously, we can have third-order kinds with variables ranging over objects of second-order kind and so on. Furthermore, analogously to RTT’s cumulativity of types, we have cumulativity of kinds, i.e., objects of kind $\square _n$ are also objects of kind $\square _{n+1}$.

Extended ramified type theory gives us tools to properly analyze our motivating examples containing instances of semantic polymorphism. As an example, let us try to offer a more appropriate analysis of the simplified variant of (1):

• (1’) Alice is thinking of something.

Fig. 2

Type-checking tree

All we need to do to properly analyze (1’) is to use a generalized variable and adjust the type of the involved function accordingly. The analysis we obtain is as follows:

$$\begin{aligned} \lambda w : \omega \; \lambda t : \tau \; \exists x : \square _1 {[}{} {\textbf {Think}}_{wt} \; {\textbf {Alice}} \; x] \end{aligned}$$

where ${\textbf {Think}}$ constructs a function of type $(o \iota \square _1)_{\tau \omega }$, Alice constructs an individual of type $\iota$ and variable x ranges over first-order kinds. Within eRTT, the whole construction will receive the type $\square _2$ (i.e., second-order kind) because it contains a generalized variable. For the corresponding type checking tree, see Fig. 2.²⁵ Analyses of (1), (2), (3), and (4) would proceed analogously.²⁶

Remark 2

Note that we can now properly type even the inadequate analysis of (1’) from earlier which corresponded rather to the sentence ‘Alice is thinking of some type’. If we consider type variables only (no generalized variables), then we will have the following types: $Think^T : (o \iota \textsf {Type})_{\tau \omega }$ and $\alpha / \square _2 : \textsf {Type}$. The analysis would then be: $\lambda w : \omega \; \lambda t : \tau \; \exists \alpha : \textsf {Type} \,[{\textbf {Think}}_{wt} \; {\textbf {Alice}} \; \alpha ]$.

Of course, even this analysis is potentially insufficient. Since Alice can be thinking of anything, she might be thinking, e.g., of the type of all types, kinds, or eRTT itself, etc., which our current analysis cannot cover since we have no variables that could range over these types of objects, so we would have to introduce yet another expansion of eRTT. In other words, it might always turn out that we need some larger type or kind than we currently have. However, for the analysis of everyday natural language phenomena the level of generality provided by eRTT seems to be more than sufficient.

Remark 3

Some might argue that the role of generalized variables is too overloaded and that we are trying to do too much with them.²⁷ Wouldn’t it be better to keep standard variables and type variables separate as is, e.g., common in polymorphic lambda calculus? Of course, we could do that. We do not need to go all the way towards generalized variables. We can just stop with the introduction of type variables from the previous section and be satisfied with that (assuming we appropriately extend the definition of ramified type theory). However, recall that our goal was to adequately analyze the sentence (1’). And for that purpose, considering separately standard variables and type variables seem insufficient. In practice, it might turn out that an implementation of generalized variables is indeed an overkill and thus their adoption should be carefully considered, however, semantically speaking, they allow us analyses otherwise unattainable.

6 Conclusion

In this paper, we have investigated the treatment of polymorphic functions in TIL, which relies on type variables understood as syntactic placeholders. This approach, however, carries certain disadvantages, most importantly it puts type variables outside of semantic theory of TIL. In practice, this leads, e.g., to our inability to properly analyse sentences involving non-specific notional attitudes such as ‘Alice is thinking of something’, etc.

To alleviate these issues, we have proposed an alternative approach that treats type variables as proper variables in the sense of TIL, i.e., as semantic objects that can v-construct other objects. To address the issue of analysis of non-specific notional attitudes we furthermore introduced generalized variables that act as both standard variables as well as type variables by ranging over both constructions (and non-constructions) and types. This led to the introduction of generalized valuations arrays and to the extended definition of ramified type theory which introduces new ‘large’ types called kinds.

Appendix

1.1 Constructions

The original definition of TIL constructions was given by Tichý (1988), here we follow Duží et al. (2010) (an alternative formulation can be found in Raclavský et al., 2015):

Definition 7

(Constructions)

• 1. The variable x is a construction that constructs an object O of the respective type dependently on a valuation. We say that it v-constructs O.

• 2. Where X is any object, $^0 X$ is the construction trivialization. It constructs X without any change.

• 3. The composition $[X_0 \, X_1 \ldots X_m]$ is the following construction. If X v-constructs a function f of type $(\alpha \beta _1 \ldots \beta _m)$ and $X_1 \ldots X_m$ v-construct objects $b_1 , \ldots , b_m$ of types $\beta _1 , \ldots , \beta _m$, respectively, then the composition $[X_0 \, X_1 \ldots X_m]$ v-constructs the value (an object of type $\alpha$, if any) of f on the tuple-argument $\langle b_1 , \ldots ,b_m \rangle$. Otherwise, it is a v-improper construction, i.e., construction that does not construct anything.

• 4. The closure $[\lambda x_1 \ldots x_m \, Y]$ is the following construction. Let $x_1 , \ldots x_m$ be pairwise distinct variables v-constructing objects of types $\beta _1 , \ldots , \beta _m$ and Y a construction v-constructing an object of type $\alpha$. Then $[\lambda x_1 \ldots x_m \, Y]$ is the construction closure. It v-constructs the following function f of type $(\alpha \beta _1 \ldots \beta _m)$: let $\langle b_1, \ldots , b_m \rangle$ be a tuple of objects of types $\beta _1 \ldots \beta _m$, respectively, and $v'$ be a valuation that associates $x_i$ with $b_i$ and is identical to v otherwise. Then the value of function f on argument tuple $\langle b_1, \ldots , b_m \rangle$ is the object of type $\alpha$ $v'$-constructed by Y. If Y is $v'$-improper, then f is undefined on $\langle b_1, \ldots , b_m \rangle$.

• 5. The single execution $^1 X$ is the construction that either v-constructs the object v-constructed by X or, if X v-constructs nothing, is v-improper.

• 6. The double execution $^2 X$ is the following construction: let X be any object, the double execution $^2 X$ is v-improper if X is a non-construction or if X does not v-construct a construction or if X v-constructs a v-improper construction. Otherwise, let X v-construct a construction $X'$ and let $X'$ v-construct and object $X''$, then $^2 K$ v-constructs $X''$.

• 7. Nothing other is a construction, unless it follows from 1 to 6.

1.2 Ramified Type Theory

We follow the specification from Tichý (1988):

Definition 8

(Ramified type theory of TIL)

Let B be a base, i.e., a set of atomic types.

• 1.

  ($\hbox {t}_1$i):

  Every member of B is a type of order 1 over B.

  ($\hbox {t}_1$ii):

  If $0<m$ and $\alpha , \beta _1 , \ldots , \beta _m$ are types of order 1 over B, then the collection $(\alpha \beta _1 \ldots \beta _m)$ of all m-ary (total and partial) mappings from $\beta _1 ,\ldots , \beta _m$ to $\alpha$ is also a type of order 1 over B.

  ($\hbox {t}_1$iii):

  Nothing is a type of order 1 over B unless it follows from ($\hbox {t}_1$i) and ($\hbox {t}_1$ii).

• 2.

  ($\hbox {c}_k$i):

  Let $\alpha$ be any type of order k over B. Every variable ranging over $\alpha$ is a construction of order k over B. If X is of (i.e., belongs to) type $\alpha$, then $^0 X$, $^1 X$, and $^2 X$ are constructions of order k over B.

  ($\hbox {c}_k$ii):

  If $0<m$ and $X_0, X_1, \ldots , X_m$ are constructions of order k, then $[X_0 \; X_1 \ldots \, X_m]$ is a construction of order k over B. If $0<m$, $\alpha$ is a type of order k over B, and Y as well as the distinct variables $x_1, \ldots , x_m$ are constructions of order k over B, then $[\lambda _\alpha \, x_1 \ldots x_m \; Y]$ is a construction of order k over B.

  ($\hbox {c}_k$iii):

  Nothing is a construction of order k over B unless it follows from ($\hbox {c}_k$i) and ($\hbox {c}_k$ii).

Let $*_k$ be the collection of constructions of order k over B. The collection of types of order $k+1$ over B is defined as follows:

($\hbox {t}_{k+1}$i):

$*_k$ and every type of order k is a type of order $k+1$.

($\hbox {t}_{k+1}$ii):

If $0<m$ and $\alpha , \beta _1 , \ldots , \beta _m$ are types of order $k+1$ over B, then the collection $(\alpha \beta _1 \ldots \beta _m)$ of all m-ary (total and partial) mappings from $\beta _1 , \ldots , \beta _m$ to $\alpha$ is also a type of order $k+1$ over B.

($\hbox {t}_{k+1}$iii):

Nothing is a type of order $k+1$ over B unless it follows from ($\hbox {t}_{k+1}$i) and ($\hbox {t}_{k+1}$ii).

1.3 Types and Rules

In this paper, we have explored a semantic treatment of type variables in TIL. Alternatively, we could attempt a syntactic rule-based analysis as well. However, since this topic is outside the scope of the present paper, we sketch only the basics of this approach. The key observation is that type variables generally appear in two kinds of judgments in TIL literature:

$$\begin{aligned}&C : *_n \rightarrow \sigma (\alpha )\\&X : \sigma (\alpha ) \end{aligned}$$

which can be read as ‘a construction C belonging to a type $*_n$ is typed to v-construct an object of type $\sigma$’ and ‘a non-construction X belongs to a type $\alpha$’, respectively, where $\sigma$ may contain $\alpha$ as a free type variable. For example²⁸:

$Cardinality_\tau : (\tau (o \tau ))$

$Cardinality_\alpha : (\tau (o \alpha ))$

$Tr_\alpha : (*_n \alpha )$

$X : *_n \rightarrow ((\alpha \tau ) \omega )$

$z : *_1 \rightarrow \alpha$

Furthermore, note that these judgments are composed of three parts: a typed object (i.e., either a construction C or a non-construction X), a typing relation ‘ : ’ and a type term (i.e., either $*_n \rightarrow \sigma (\alpha )$ in case of constructions or $\sigma (\alpha )$ in case of non-constructions).

Now, as we mentioned above, type terms might depend on some variable $\alpha$ of type $\textsf {Type}$ (the type of all types). We can explicitly capture this dependency by abstracting type terms from $\alpha$ via ${\uplambda }$ abstractor and get ${\uplambda }$$\alpha : \textsf {Type} . *_n \rightarrow \sigma (\alpha )$ and ${\uplambda }$$\alpha : \textsf {Type} . \sigma (\alpha )$. Consequently, every free occurrence of $\alpha$ in $\sigma$ becomes bound in ${\uplambda }$$\alpha : \textsf {Type} . *_n \rightarrow \sigma (\alpha )$ and ${\uplambda }$$\alpha : \textsf {Type} . \sigma (\alpha )$. The obvious complement to abstraction is, of course, application. Thus, the rules we obtain are as follows:²⁹

where $\sigma [\kappa /\alpha ]$ is the result of substituting $\kappa$ for all occurrences of $\alpha$ in $\sigma$.

Note that the premises of abs-C and abs-X rules are hypothetical judgments, i.e., judgments made in a certain context. Thus, we can read $\alpha : \mathsf {Type} \vdash C : *_n \rightarrow \sigma (\alpha )$ as ‘a judgment $C : *_n \rightarrow \sigma (\alpha )$ is assertable given that we have some type term $\alpha$ of type $\textsf {Type}$’. Analogously for the hypothetical judgment $\alpha : \mathsf {Type} \vdash X : \sigma (\alpha )$.

These rules can help us to explain syntactically the general process of instantiation of type terms containing type variables to some specific type, a process which was investigated semantically in this paper via the use of expanded valuation arrays.