1 Introduction

Interpretation of pronouns can be sensitive to linguistically introduced dependency relations between objects. Consider the following examples discussed in the literature (Kamp and Reyle [12], van den Berg [4, 5], Krifka [14], Nouwen [17], Brasoveanu [7]).Footnote 1

figure a

In (1a), given a reading where every boy receives wide scope over a present (henceforth, the \(\forall \)–\(\exists \) reading), the whole sentence can mean that if every boy received a present, each boy opened the present he received. Similarly, the second sentence in (1b) can be understood to mean that each boy opened the present he received. In both cases, the \(\forall \)–\(\exists \) reading induces a dependency relation between boys and presents. This quantificational dependency plays a crucial role in the interpretation of the singular pronoun it in the consequent of (1a) and the second sentence of (1b).

More generally, the reference to a dependency relation is possible when a semantic link between the restrictor of the universal quantifier and the subject of a subsequent sentence can be established.

figure b

In (2a), the subjects of the antecedent and the consequent share the same noun phrase boy. The consequent can be understood to mean that some boy will open the present he received (Hintikka and Carlson [10], Ranta [18]). In (2b), young boy is a subset of boy. Again, a similar interpretation is allowed (cf. van den Berg [5]). There is no explicit link in the case of (2c), but if we have the background information that John is a boy, i.e., the information that links John to boy, the sentence can mean that John will open the present he received. The same observation applies to the following examples.

figure c

However, if it is difficult to establish a link between the two NPs, the dependent interpretation of the pronoun in question is impossible. The following examples demonstrate this contrast.

figure d

In (4a), since it is relatively easy to find a relation between man and wife, the second sentence can be understood to mean that some man’s wife will open the present he received. This contrasts with (4b), where a dependent reading is not possible unless a strong relation between man and woman is provided by the context.

A similar observation can be made about the so-called quantificational subordination phenomenon, which was originally discussed by Karttunen [13].

figure e

Although this example is more complicated than those we have considered so far, a similar structure seems to be involved. (5a) can only mean that there is one specific girl such that Harvey courts her at every convention and she is very pretty. If we discard this reading and force ourselves to keep the \(\forall \)–\(\exists \) reading, there is no way to establish an anaphoric link between a girl and the singular pronoun she, and hence the discourse becomes infelicitous. In (5b), however, she can refer to a girl at each convention, since the subsequent discourse contains quantificational adverbs such as always and usually, which provide links to every convention.

This observation suggests that if the dependency relation between objects is used later on to interpret a pronoun, it must be tracked through discourse as an anaphoric resource. Since dependency relations are crucially involved in plural anaphora phenomena in general, constructing a formal mechanism to account for dependencies is one of the central issues in the dynamic semantics literature. The standard approach is to model dependencies as sets of assignments (van den Berg [4, 5], Nouwen [17], Brasoveanu [7]). Another approach is to model it using an extended notion of assignment functions called parametrized sum individuals (Krifka [14]). However, since integrating functional relations directly into the underlying semantics is not straightforward, both approaches require substantial changes to the central notion of context to account for dependent interpretations.

In this paper, we propose an alternative account. We account for dependency relations in terms of dependent function types (\(\varPi \)-types) in dependent type theory (Martin-Löf [16]). In contrast to the mechanisms introduced in previous model-theoretic approaches, \(\varPi \)-types are independently motivated objects that are already provided in dependent type theory. We will adopt Dependent Type Semantics (Bekki [1], Bekki and Mineshima [2]; henceforth DTS) as a semantic framework and illustrate how \(\varPi \)-types encode the dependency relations in question and are readily provided as anaphoric resources in discourse. In the following section, we will first provide an overview of DTS. In Sect. 3, we describe our approach to handling the reference to dependency relations and show how it can be applied to the examples discussed above. In Sect. 4, we compare our technique with existing approaches.

2 Dependent Type Semantics

2.1 Dependent Types and Natural Language Sentences

DTS is a proof-theoretic natural language semantics based on dependent type theory. Dependent type theory (Martin-Löf [16]) is a formal system that extends simple type theory with the notion of types depending on terms. This rich type structure provides a foundation for handling context dependence in natural language. One of the distinctive features of DTS, compared with other frameworks based on dependent type theory, is that it is augmented with underspecified terms called @-terms. DTS uses @-terms to provide a unified analysis of entailment, anaphora, and presupposition from an inferential and computational perspective. DTS also gives a compositional account of inferences involving anaphora; see Bekki [1] and Bekki and Mineshima [2] for details on compositional semantics within the framework of DTS.

Dependent type theory uses two type constructors \(\varPi \) (dependent function type) and \(\varSigma \) (dependent product type) to construct dependent types. The type constructor \(\varPi \) is a generalized form of the functional type. A term of type \((\varPi x:A)B(x)\) is a function f which takes any element a of A and returns a term f(a) of type B(a) dependent on the choice of the argument a. In other words, a dependent function is a function whose codomain is dependent on the given argument. The type constructor \(\varSigma \) is a generalized form of the product type. A term of type \((\varSigma x:A)B(x)\) is a pair \((m,\, n)\) which consist of a term m of type A and a term n of type B(m), where the type of the second element n depends on the choice of the first element m.

Dependent type theory is based on the Curry-Howard correspondence, where a type can be regarded as a proposition and a term of the type can be regarded as a proof of the proposition. Accordingly, a \(\varPi \)-type corresponds to a universal quantifier; a proof term of the universal sentence is a function. If x does not occur free in B, i.e., there is no dependencies involved, \((\varPi x:A)B\) corresponds to implication. A \(\varSigma \)-type corresponds to an existential quantifier; a proof term of the existential sentence is a pair. If x does not occur free in B, \((\varSigma x:A)B\) corresponds to conjunction. See, e.g., Martin-Löf [16] for more details, including inference rules for \(\varSigma \) and \(\varPi \) constructors. Figure 1 shows the notation of \(\varSigma \)-type and \(\varPi \)-type adopted in DTS.

Fig. 1.
figure 1

Notation of \(\varPi \)-type and \(\varSigma \)-type.

Full size image

Since \(\varPi \)-types correspond to propositions with the universal quantifier, the sentence every boy entered can be represented as follows.

figure f

Here, \( \mathbf{entity }\) is a basic type for all entities. The restrictor boy is analyzed as a \(\varSigma \)-type. A term u having this \(\varSigma \)-type would be a pair (e, b), where e is a term of type \( \mathbf{entity }\) and b is a proof term of the proposition \( \mathbf{boy }(e)\). \(\varSigma \)-types are associated with projection functions \(\pi _1\) and \(\pi _2\). These functions allow one to access the first and second elements of the pair, respectively: for any pair \((m,\, n)\), \(\pi _1 (m,\, n) = m\) and \(\pi _2 (m,\, n) = n\). Thus, the term \(\pi _1 u\) picks up from u the term e of type \( \mathbf{entity }\). Therefore, (6) corresponds to the proposition that for every entity that is a boy, that entity entered.

A sentence with an existential quantifier such as a boy entered is represented in terms of \(\varSigma \)-types. Again, \(\pi _1 u\) corresponds to an entity which is a boy, and thus, (7) corresponds to the proposition that there exists an entity which is a boy and which entered.

figure g

One advantage of using \(\varSigma \)-types is that they can capture an externally dynamic property of existential quantifier and conjunction (Groenendijk and Stokhof [9]). For instance, a discourse such as (8a) is problematic in the sense that its syntactically-corresponding formula in predicate logic, (8b), fails to represent an anaphoric link between a boy and he.

figure h

The \(\varSigma \)-type, by contrast, can straightforwardly provide the semantic representation of this discourse as follows.

figure i

Although a term u is no longer accessible from the argument position of \( \mathbf{whistle }\), one can still pick up the term via a newly introduced term v, since v is a pair and each of its parts is accessible by applying (a sequence of) the projection function. In this way, the \(\varSigma \)-type can pass a variable binding relation to a subsequent discourse.

2.2 DTS and Anaphora Resolution

The remaining question is how one can obtain the term \(\pi _1 \pi _1 v\) in (9) for the representation of the pronoun he. In DTS, anaphoric expressions are represented in terms of underspecified terms called @-terms. Anaphora resolution in DTS is therefore defined as a process that replaces the @-term with the specific term that is constructed via type checking and proof construction (Bekki and Satoh [3], Bekki and Mineshima [2]). For instance, the pronoun he is assigned the semantic representation in (10), where the type annotation of the @-term represents the requirement that he refers to some entity being male.

figure j

Dynamic conjunction between sentences is defined in terms of \(\varSigma \)-type. Thus, the semantic representation of the whole discourse in (8a) is given as follows.

figure k

This underspecified representation is required to be well formed, that is, to have type \( \mathbf{type }\). This condition (called the felicity condition of a sentence) invokes type checking and leads to the proof construction associated with the @-term. In the current example, one needs to find a proof term that satisfies the following inference.

figure l

Here, \(\varGamma \) is a global context that represents background knowledge, and v is a term accessible from the position of the @-term, which corresponds to the information provided up to this point of the mini-discourse. From these premises \(\varGamma \) and v, one needs to construct a proof term of the consequent that fills in the position marked by . Now, suppose that the global context contains the proof term in (13), which corresponds to the knowledge that every boy is male.

figure m

By using this knowledge \(k_b\) together with v, one can eventually construct a proof term of the required type that can replace the underspecified term in (11), yielding the fully-specified representation in (9).

Note that this anaphora resolution procedure in DTS can account for the following externally static property of universal quantifiers.

figure n

In these cases, the first sentences are universal sentences, so proof terms provided to the subsequent discourse are functions. Thus, neither an entity being a boy embedded in the domain of the function (i.e., an entity in the restrictor), nor an entity being a present embedded in the codomain of the function (i.e., an entity in the nuclear scope) can be picked up by the operation that is available in the case of existential sentences represented as \(\varSigma \)-types.

In this way, \(\varSigma \)-types and \(\varPi \)-types, together with the anaphora resolution process in DTS, provide a proof-theoretic account of the dynamic properties of the existential and universal quantifiers.

3 Dependency Relations and Dependent Interpretation

As we have seen so far, \(\varSigma \)-types are externally dynamic in that they introduce pairs of objects as discourse referents which can be picked up by projection functions; by contrast, \(\varPi \)-types are externally static in that they do not introduce individual discourse referents. Because of this difference, one might think that \(\varPi \)-types do not contribute to establishing any discourse referents. Ranta [18], however, describes exactly such a case in the following example.Footnote 2

figure o

In (15), the antecedent clause is analyzed as a \(\varPi \)-type, so it introduces a function as a discourse referent. The functional discourse referent introduced by this \(\varPi \)-type can be used to give the interpretation of the pronoun it in the consequent clause. Although Ranta’s brief discussion is confined to the example in (15), we will show below that the idea that proof terms of \(\varPi \)-types serve as functional discourse referents can apply to examples (2)–(4) discussed in Sect. 1, as well as to the case of plural anaphora involving the pronoun they and to quantificational subordination. In Sect. 3.1, we will first focus on the basic case of the dependent interpretation of a pronoun and show how the idea of functional discourse referents couched within the framework of DTS can capture the quantificational dependency.Footnote 3 In Sect. 3.2, we will generalize this idea to other cases including plural anaphora involving they.

3.1 Basic Example

Let us consider the simplest example in (3a), which is repeated below.

figure p

Since a universal quantifier corresponds to a \(\varPi \)-type, the first sentence can be represented as follows.

figure q

The terms \(\pi _1 u\) and \(\pi _1 v\) pick up the entity being a boy and the entity being a present, respectively. The type as a whole represents the proposition that, for every boy, there exists a present such that the boy received it. This representation corresponds to the distributive reading in question. Thus, a term of this type is a function that receives a pair consisting of an entity and a proof of that entity being a boy, and then returns a tuple that consists of an entity, a proof of that entity being a present, and a proof of the boy and the present being in the receiving relation. This means that the representation of the first sentence introduces a function that corresponds to the dependency relation between boys and presents.

The second sentence is represented by the \(\varSigma \)-type, where the pronoun it can be defined as an underspecified term of type \( \mathbf{entity }\). Thus, by combining the semantic representation of the two sentences in terms of dynamic conjunction, (3a) is represented as the following \(\varSigma \)-type.

figure r

In this way, the proof term f of the first sentence that corresponds to a dependency relation between boys and presents serves as an anaphoric resource. In the current case, anaphora resolution of the pronoun it yields the following inference.

figure s

There are two proof terms accessible from the position of the @-term: the term f, which is a proof term of the first sentence, and z, which is a term corresponding to the subject of the second sentence. The proof construction goes as follows: first, by applying z to the function f, one obtains the proof term fz that is a pair corresponding to the present received by the boy, \(\pi _\mathrm{1} z\); second, by taking the first projection of the first projection of fz, one obtains a term \(\pi _\mathrm{1} \pi _\mathrm{1} (fz)\) of type \( \mathbf{entity }\). Therefore, by replacing the @-term with the obtained term \(\pi _\mathrm{1} \pi _\mathrm{1} (fz)\), the second argument of \( \mathbf{open }\) will be filled with an entity which depends on the term z, namely, an entity which depends on the subject of the second sentence. In this way, we can account for the dependent interpretation of the pronoun it in (3a).Footnote 4

3.2 More Examples

In Sect. 1, we have observed that an anaphoric link can be established even when the subject of a subsequent discourse does not exactly match the restrictor of the universal quantifier of an earlier sentence. These examples, (3b) and (3c), are repeated below.

figure t

Both the first and the second sentences in (3b) can be represented in terms of \(\varPi \)-types. Thus, the whole sentence receives the following semantic representation.

figure u

The premises of the inference associated with the resolution of \(@_\mathrm{1}\) are terms f and t. Since the term \(\pi _\mathrm{1} t\), shown in (20), can be derived from the given t and can be applied to f, one eventually obtains a term \(\pi _\mathrm{1} \pi _\mathrm{1} f(\pi _\mathrm{1} t)\), which corresponds to the present dependent on each young boy, \(\pi _\mathrm{1} \pi _\mathrm{1} t\).

figure v

Similarly, (3c) is represented as follows.

figure w

To find a semantic link between John and boy, one needs the background knowledge that John is a boy. If the global context \(\varGamma \) supplies the knowledge \(k_j : \mathbf{boy }( \mathbf{john })\), one can construct the following term.

figure x

Again, this term can serve as an argument to the function f.

If the relation between the restrictor of the universal quantifier and the subject of the subsequent discourse is not clear, then the procedure simply fails to find a proof. For instance, in the case of (4b), repeated here as (23a), there exists neither an explicit link nor an implicit link between men and women.

figure y

In this case, one needs to apply an argument to the function f to construct a proof of the present received by some man. Thus, unless some relation which bridges men and women is available in the global context, there is no way to obtain the required proof term from z and f.

The conditional sentences in (2a–c) can be treated in parallel to the examples in (3a–c). The sentences are reproduced below.

figure z

For instance in the case of (2a), we can provide the following semantic representation.

figure aa

The whole conditional is analyzed as a \(\varPi \)-type of the form \( \left( f:A \right) \rightarrow B \). Here the antecedent clause every boy receives a present is represented as a \(\varPi \)-type and thus introduces a function f in the antecedent. This proof term f is accessible from the consequent. As a result, the proof term f, together with the proof term z introduced in the consequent, can be used for the resolution of \(@_\mathrm{1}\). This enables the dependent interpretation of the pronoun it. We can see that the resolution of \(@_\mathrm{1}\) involves essentially the same inference as that for (17). Similarly, (2b) and (2c) can be analyzed along the same lines as (3b) and (3c), whose semantic representation are given in (19) and (21), respectively.

The case of quantificational subordination repeated here can be accounted for in a similar way.

figure ab

The \(\forall \)–\(\exists \) reading of the first sentence of (5a,b) is analyzed in the following simplified representation.

figure ac

This \(\varPi \)-type introduces a function, so the anaphoric link between a girl and she is blocked in (5a). In the case of (5b), always in the second sentence introduces another \(\varPi \)-type, whose restrictor provides an adequate argument for the function introduced by the first sentence. The entire derivation is similar to the case of (19) above. Thus, she can be interpreted as a girl at each convention.

Let us now turn back to our first example (1) involving plural anaphora. Example (26) is similar, but with adjectival quantifiers (Krifka [14]).

figure ad

Although providing a comprehensive analysis of plural anaphora including an analysis of the so-called collective reading is not the main concern of this paper, we will briefly sketch how to account for the dependency relation involved in plural anaphora. In our analysis, two factors are essential to account for the reference to the dependency relation. Firstly, the initial sentence must have the \(\forall \)–\(\exists \) reading which induces a dependency relation between objects in terms of a dependent function. Secondly, a singular pronoun in the subsequent discourse can be interpreted anaphorically if it supplies an adequate argument to the dependent function introduced by the initial sentence. These two points are critical for our analysis of plural anaphora in (1) and (26).

As for the first point, we follow an analysis of generalized quantifiers and adjectival quantifiers in DTS (Tanaka et al. [20], Tanaka [19]) that provides semantic representation of those quantificational expressions by using a dependent function. According to this analysis, generalized quantifiers such as mostFootnote 5 and adjectival quantifiers such as three are uniformly represented as involving existential quantification over dependent functions whose domain is restricted by the cardinality condition.Footnote 6 Thus, this dependent function can be used for anaphora resolution as in the cases we have seen so far.

The essential role of the plural pronoun they is thus to supply terms that are adequate for the arguments of the dependent function. The semantic representation of they is also given in terms of the @-term. In contrast to the singular pronoun it, the type annotation of the @-term associated with they requires a predicate and a proof term of the cardinality condition. This is because the domain of the dependent function provided by the quantificational expression is restricted by the predicate and the cardinality condition. Therefore, the term replacing the @-term can supply an adequate argument to the function, which enables the dependent interpretation of the singular pronoun which comes after.

4 Previous Approaches

In this section, we provide a brief overview of some of the existing solutions in dynamic semantics to handle reference to a dependency relation.

In classical Discourse Representation Theory (Kamp and Reyle [12], henceforth DRT), reference to a dependency relation is handled by using a copy mechanism. First, the first sentence in (1), every boy received a present, yields the following discourse representation structure (DRS).

figure ae

The construction of this DRS triggers the operation called abstraction, which constructs a new plural discourse referent \(X'\) consisting of an object that satisfies the condition of x. The pronoun they refers to this \(X'\) and yields the DRS in Fig. 2a, where universal quantification over \(X'\) takes place. In this DRS, however, there is no discourse referent which can be associated with singular y in \( \mathbf{open }(x,y)\). In such a case, there is an option to apply a copy operation, which copies the conditions of x constituting \(X'\) to the restrictor part of the duplex condition. The corresponding DRS is given in Fig. 2b. In this way, the singular variable y in \( \mathbf{open }(x,y)\) can refer to each present associated with each boy.

Fig. 2.
figure 2

DRS associated with (1).

Full size image

Krifka [14] criticizes using a representation-based copying operation as ad hoc, and proposes an analysis based on an enriched assignment function called parametrized sum individuals. Parametrized sum individuals are sets of pairs of an individual and a variable assignment associated with that individual. A possible instance of parametrized individuals for every boy received a present may have the following representation.

$$\begin{aligned} \langle x, \{ \langle b_\mathrm{1}, \{ \langle y, p_\mathrm{1} \rangle \} \rangle , \langle b_2, \{ \langle y, p_2 \rangle \} \rangle , \langle b_3, \{ \langle y, p_3 \rangle \} \rangle , \ldots \} \rangle \end{aligned}$$

The individuals can be either singular or plural. Since individuals are followed by assignments associated with them, this structure captures dependency relations between objects. In the case of the distributive interpretation, each parametrized individual is independently evaluated against predicates. Thus, singular pronouns can be interpreted along each parametrized individual, which produces an effect of interpretation sensitive to the dependency relation.

The standard way to encode dependency relations is to adopt information states for plurals, as proposed by van den Berg [4, 5] in Dynamic Plural Logic. In this approach, formulas are interpreted relative to information states, which are sets of assignments, instead of to assignments. A possible information state for every boy received a present may have the following representation.

$$\begin{aligned} \{ \{ \langle x,\, b_\mathrm{1} \rangle , \langle y,\, p_\mathrm{1} \rangle \}, \{ \langle x,\, b_2 \rangle , \langle y,\, p_2 \rangle \}, \{ \langle x,\, b_3 \rangle , \langle y,\, p_3 \rangle \}, \ldots \} \end{aligned}$$

When distribution over x is involved, predicates are evaluated against each assignment of information states. The assignment of new values takes place independently of each assignment function; thus, the variables introduced may be dependent on x. This is the source of dependency.

Our intuition about the \(\forall \)–\(\exists \) reading of every boy received a present is that it introduces a quantificational dependency, that is, a function f such that x is a boy receiving a present f(x). However, there is no natural place in standard dynamic semantics theory to store such a function for subsequent anaphora. Therefore, each of the three approaches mentioned above need to capture dependency relations in an indirect way, which requires integrating a special mechanism or structure into the underlying framework.

There are also several empirical issues to consider. First, the copy mechanism in DRT is triggered by the resolution of the plural pronoun they. However, we have seen that there are cases such as (3a–c), where a plural pronoun does not appear but still reference to a dependency relation takes place. A stipulation or operation is needed in DRT to handle more general cases including these examples. Second, there exists no proof theory for either of the frameworks proposed by Krifka or van den Berg. Van den Berg’s [5] analysis can account for cases such as (3b), where a subset relation allows reference to a dependency relation. In general, however, a semantic link between the restrictor of the universal quantifier and the subject of the subsequent discourse is not limited to the subset relation, as we can observe in example (4a). Rather, the dependent interpretation involves a more general kind of inference, of which a semantic link in terms of subset relations is a special instance.

An advantage of the proposed DTS analysis is that \(\varPi \)-types are independently motivated objects already provided in dependent type theory, and thus, we do not need to extend our framework to account for dependency relations. By following the standard dynamic conjunction operation and anaphora resolution procedure, DTS can naturally provide a function as a discourse referent, which straightforwardly leads to the dependent interpretation of singular pronouns. In addition, because the anaphora resolution process in DTS involves a proof search, it provides a more general and uniform account of semantic links between the restrictor of the universal quantifier and the subject of the subsequent discourse.

5 Conclusion

In this article, we have argued for an account of dependency relations between objects as dependent functions in dependent type theory. This contrasts with approaches in the dynamic semantics tradition, where a function does not serve as a discourse referent, and the enriched notion of assignment functions plays an essential role in handling dependencies. We have seen that the proposed account is capable of explaining the dependent interpretation of pronouns by integrating with the anaphora resolution mechanism of DTS. This new account may also offer a basis for the proof-theoretic analysis of plural anaphora.