Zhaohui Luo
email: zhaohui.luo@hotmail.co.uk

Sergei Soloviev
email: sergei.soloviev@irit.fr

Dependent Event Types

This paper studies how dependent types can be employed for a refined treatment of event types, offering a nice improvement to Davidson's event semantics. We consider dependent event types indexed by thematic roles and illustrate how, in the presence of refined event types, subtyping plays an essential role in semantic interpretations. We consider two extensions with dependent event types: first, the extension of Church's simple type theory as employed in Montague semantics that is familiar with many linguistic semanticists and, secondly, the extension of a modern type theory as employed in MTT-semantics. The former uses subsumptive subtyping, while the latter uses coercive subtyping, to capture the subtyping relationships between dependent event types. Both of these extensions have nice meta-theoretic properties such as normalisation and logical consistency; in particular, we shall show that the former can be faithfully embedded into the latter and hence has expected meta-theoretic properties. As an example of applications, it is shown that dependent event types give a natural solution to the incompatibility problem (sometimes called the event quantification problem) in combining event semantics with the traditional compositional semantics, both in the Montagovian setting with the simple type theory and in the setting of MTT-semantics.

Introduction

The event semantics, whose study was initiated by Davidson [6] and further studied in its neo-Davidsonian turn (see [17] among others), has several notable advantages including Davidson's original motive to provide a satisfactory semantics for adverbial modifications. Dependent types, as those found in Modern Type Theories such as Martin-Löf's type theory [START_REF] Martin-Löf | Intuitionistic Type Theory[END_REF] and UTT [START_REF] Luo | Computation and Reasoning: A Type Theory for Computer Science[END_REF], provide a useful tool in formalising event types and a nice treatment of the event semantics.

In this paper, we shall study event types that may depend on thematic roles such as agents and patients of the events. For example, we can consider the type Evt AP (a, p) of events whose agent and patient are a and p, respectively. We shall investigate subtyping relations between event types which include dependent types such as Evt AP (a, p) and the non-dependent type Event of all events (the latter is found in the traditional setting). For example, it may be natural to have Evt AP (a, p) ≤ Evt A (a), that is, the type of events with agent a and patient p is a subtype of that with agent a. With such subtyping relations in place, the semantics of verb phrases can now take the usual non-dependent types, as in the traditional setting, although dependent event types are considered.

It is shown that such dependent event types give a natural solution to the incompatibility problem in combining event semantics with the traditional Montague semantics [START_REF] Champollion | The interaction of compositional semantics and event semantics[END_REF][START_REF] Winter | Event semantics and abstract categorial grammar[END_REF] (sometimes called the event quantification problem [START_REF] De Groote | A type-logical account of quantification in event semantics[END_REF]). When introducing events into formal semantics, one faces a problem, which is long-standing and has seemed intractable: it comes from the issue of scopes for two kinds of quantifiers -the existential quantifier over an event variable and the other quantifiers such as one that arises from a quantificational noun phrase (see Sect. 5 for examples). It is in general expected that the correct semantics is obtained when the event quantifier takes the lower scope, but the problem is that, even when the event quantifier takes a wider scope, which would give an incorrect semantics, the resulting semantic formula is still well-formed formally. This has led to many proposals such as that considered by Champollion [START_REF] Champollion | The interaction of compositional semantics and event semantics[END_REF] or the related Scope Domain Principle proposed by Landman [START_REF] Landman | Plurality[END_REF], but all of them are rather ad hoc. Dependent event types will solve this problem: they give a solution where the correct semantics are accepted while the incorrect ones are excluded by typing because they would be ill-typed and hence formally illegal.

Dependent event types (DETs) were first considered in an example in [START_REF] Asher | Formalisation of coercions in lexical semantics[END_REF] to study linguistic coercions in formal semantics, where types of events are indexed by their agents: Evt(h) is the type of events conducted by h : Human. In this paper, we shall study event types dependent on thematic roles in event semantics both in the traditional Montague semantics [START_REF] Montague | Events in the Semantics of English[END_REF] and in formal semantics in modern type theories (MTT-semantics, for short) [START_REF] Chatzikyriakidis | Formal Semantics in Modern Type Theories[END_REF][START_REF] Luo | Formal semantics in modern type theories with coercive subtyping[END_REF][START_REF] Ranta | Type-Theoretical Grammar[END_REF]. For the former, we extend Church's simple type theory [START_REF] Church | A formulation of the simple theory of types[END_REF], as employed in Montague semantics that is familiar with many linguistic semanticists, by means of dependent event types, resulting in the system C e , where the subtyping relationships between DETs are captured by subsumptive subtyping. For the latter, we extend an MTT (in particular, the type theory UTT [START_REF] Luo | Computation and Reasoning: A Type Theory for Computer Science[END_REF]) with DETs whose subtyping relationships are reflected by coercive subtyping [START_REF] Luo | Coercive subtyping in type theory[END_REF][START_REF] Luo | Coercive subtyping: theory and implementation[END_REF], resulting in the type system UTT[E]. Both of these extensions have nice meta-theoretic properties such as normalisation and logical consistency; in particular, we shall show that C e can be faithfully embedded into UTT[E] and hence has desirable properties.

The rest of the paper is organised as follows. In Sect. 2, we shall describe the basics of DETs, introducing notations and examples. Subtyping between event types is described in Sect. 3, where we show, for example, how VPs can take the traditional non-dependent type, while we consider DETs. The formal systems C e and U T T [E] and the embedding of C e in UTT[E] are studied in Sect. 4. Section 5 considers the solution of the event quantification problem by means of DETs:

In the Davidsonian event semantics in the traditional Montagovian setting [START_REF] Davidson | The logical form of action sentences[END_REF]17], there is only one type Event of all events. For example, the sentence (1) is interpreted as (2): where in [START_REF] Champollion | The interaction of compositional semantics and event semantics[END_REF], Event is the type of all events, kiss, passionate : Event → t are predicates over events, and agent, patient : Event → e → t are relations between events and entities. 1 Please note that, in the above neo-Davidson's semantics (2), adverbial modifications and thematic role relations are all propositional conjuncts in parallel with the verb description, an advantageous point as compared with an interpretation without events.

We propose to consider refined types of events. Rather than a single type Event of events, we introduce types of events that are dependent on some parameters. For instance, an event type can be dependent on agents and patients. Let Agent and P atient be the types of agents and patients, respectively. Then, for a : Agent and p : P atient, the dependent type

Evt AP (a, p)
is the type of events whose agents are a and whose patients are p. With such dependent event types, the above sentence (1) can now be interpreted as: 2 (3) ∃e : Evt AP (j, m). kiss(e) & passionate(e) Note that, besides other things we are going to explain below, we do not need to consider the relations agent and patient as found in (2) because they can now be 'recovered' from typing. For example, for a : Agent and p : P atient, we In logical formulas or lambda-expressions, people often omit the type labels of events and entities: for example, (2) would just be written as ∃e. kiss(e) & agent(e, j) & patient(e, m) & passionate(e), since traditionally there are only one type of events and one type of entities; we shall put in the type labels explicitly. Another note on notations is: e and t in boldface stand for the type of entities and the type of truth values, respectively, as in MG, while e and t not in boldface stand for different things (for example, e would usually be used as a variable of an event type). Please note here that, for kiss(e) and passionate(e) to be well-typed, the type of event e must be the same as the domain of kiss and passionate -see the next section about subtyping, which allows them to be well-typed.

can define functions agent AP [a, p] and patient AP [a, p] such that, for any event e : Evt AP (a, p), agent AP [a, p](e) = a and patient AP [a, p](e) = p. 3The parameters of dependent event types are usually names of thematic roles such as agents and patients. Formally, the dependent event types are parameterised by objects of types A 1 , . . . , A n . Event types with n parameters are called n-ary event types. In this paper, we shall only consider n-ary event types with n = 0, 1, 2:

-When n = 0, the event type, usually written as Event, has no parameters.

Event corresponds to the type of all events in the traditional setting. -When n = 1, we only consider Evt A (a) and Evt P (p), where a : Agent and p : P atient; i.e., these are event types dependent on agents a and those dependent on patients p. For example, if John is an agent with interpretation j, Evt A (j) is the type of events whose agents are John. -When n = 2, we only consider Evt AP (a, p) for a : Agent and p : P atient, i.e., the event type dependent on agent a and patients p. For example, if agent John and patient Mary, Evt AP (j, m) is the type of events whose agents and patients are John and Mary, respectively (cf., the example (3) above).

Introducing dependent event types has several advantages. In this paper, we shall detail one of them, that is, it gives a natural solution to the event quantification problem -see Sect. 5. Before doing that, we shall first consider in Sect. 3 the subtyping relationship between event types which, among other things, simplifies the semantic interpretations of VPs in the semantics with dependent event types, and then in Sect. 4 the formal systems that underlie the proposed semantic treatments and their meta-theoretic properties.

Subtyping Between Event Types

Event types have natural subtyping relationships between them. For example, an event whose agent is a and patient is p is an event with agent a. In other words, for a : Agent and p : P atient, the type Evt AP (a, p) is a subtype of Evt A (a). If we only consider the event types Event, Evt A (a), Evt P (p) and Evt AP (a, p) (cf., the last section), they have the following subtypnig relationships: It is also reflexive and transitive. The underlying type theory for formal semantics can be extended by dependent event types together with the subtyping relations. The underlying type theory can either be the simple type theory [START_REF] Church | A formulation of the simple theory of types[END_REF] in the Montagovian semantics or a Modern Type Theory such as UTT [START_REF] Luo | Computation and Reasoning: A Type Theory for Computer Science[END_REF] in MTTsemantics as considered in, for example, [START_REF] Luo | Formal semantics in modern type theories with coercive subtyping[END_REF]. If the former, extending it with dependent event types results in the formal system C e with subsumptive subtyping, and if the latter, the resulting theory is UTT[E] with coercive subtyping whose basic coercion relationships in E characterise the subtyping relationships between event types (see Sect. 4 for more details). 4The incorporation of subtyping between event types is not only natural but plays an essential role in semantic interpretations. This can best be explained by considering how verb phrases are interpreted. In the neo-Davidson's event semantics (with only Event as the type of events), a verb phrase is interpreted as a predicate over events, as the following example shows. With dependent event types such as Evt A (j), how can we interpret talk and (5)? In analogy, the desired semantics of (5) would be [START_REF] De Groote | A type-logical account of quantification in event semantics[END_REF], where the agent of the event e can be obtained as agent A (e) = j:

Evt AP (a, p) ≤ Evt A (a) ≤ Event Evt AP (a, p) ≤ Evt P (p) ≤ Event
(7) ∃e : Evt A (j). talk(e) & loud(e)
However, if talk is of type Event → t, talk(e) would be ill-typed since e is of type Evt A (j), not of type Event. Is [START_REF] De Groote | A type-logical account of quantification in event semantics[END_REF] well-typed? The answer is, if we do not have subtyping, it is not. But, if we have subtyping as described above, it is! To elaborate, because e : Evt A (j) ≤ Event, talk(e) is well-typed by the subsumption rule ( * ). Similarly, we have loud : Event → t and, therefore, loud(e) is well-typed for e : Evt A (j) ≤ Event as well.

To summarise, the subtyping relations have greatly simplified the event semantics in the presence of refined dependent event types.

Remark 1. The subtyping relations also facilitate a natural relationship between the functions such as agent AP and agent A (see Sect. 2 and Footnote 3). For example, because of the subtyping relations as depicted in Fig. 1, for e : Evt AP (a, p) ≤ Evt A (a), we have, by definition: agent AP [a, p](e) = agent A [a](e) = a.

The Underlying Systems C e and UTT[E]

In this section, we describe the formal systems C e and UTT[E]: C e extends the simple type theory [START_REF] Church | A formulation of the simple theory of types[END_REF] and UTT[E] extends the modern type theory UTT [START_REF] Luo | Computation and Reasoning: A Type Theory for Computer Science[END_REF], both with dependent event types and their subtyping relationships as informally described in Sects. 2 and 3. 5 C e is the underlying type theory when we consider formal semantics in the traditional Montagovian setting (as familiar by most of the linguistic semanticists) and UTT[E] when we consider formal semantics in a modern type theory (see, for example, [START_REF] Chatzikyriakidis | Formal Semantics in Modern Type Theories[END_REF][START_REF] Luo | Formal semantics in modern type theories with coercive subtyping[END_REF]). We also outline the construction of an embedding of C e into UTT[E] that shows that, like UTT[E], C e has nice meta-theoretic properties such as normalisation and logical consistency. Contexts. A context is a sequence of entries either of the form x : A or of the form P true. Informally, the former assumes that the variable x be of type A and the latter that the proposition P be true. Only valid contexts are legal and context validity is governed by the following rules:

valid Γ ⊢ A type x ∈ F V (Γ )
Γ, x : A valid Γ ⊢ P : t Γ, P true valid where is the empty sequence and F V (Γ ) is the set of free variables in Γ defined as: [START_REF] Asher | Formalisation of coercions in lexical semantics[END_REF]

F V ( ) = ∅; (2) F V (Γ, x : A) = F V (Γ ) ∪ {x}; (3) F V (Γ, P true) = F V (Γ ).
Judgements. Judgements are sentences in C e , whose correctness are governed by the inference rules below. In C e , there are five forms of judgements:

-Γ valid, which means that Γ is a valid context (the rules of deriving context validity are given above).

Γ valid Γ e type Γ valid Γ t type Γ, x:A, Γ valid Γ, x:A, Γ

x : A Γ, P true, Γ valid Γ, P true, Γ P true -Γ ⊢ A type, which means that A is a type under context Γ .

Γ A type Γ B type Γ A → B type Γ, x:A b : B x F V (B) Γ λx:A.b : A → B Γ f : A → B Γ a : A Γ f (a) : B Γ P : t Γ Q : t Γ P ⊃ Q : t Γ, P true Q true Γ P ⊃ Q true Γ P ⊃ Q true Γ P true Γ Q true Γ A type Γ, x:A P : t Γ ∀(A, x.P ) : t Γ, x:A P true Γ ∀(A, x.P ) true Γ (A, x.P [x]) true Γ a : A Γ P [a] true
-Γ ⊢ a : A, which means that a is an object of type A under context Γ .

-Γ ⊢ P true, which means that P is a true proposition under context Γ .

-Γ ⊢ A ≤ B, which means that A is a subtype of B under context Γ .

Inference Rules. The inference rules for C e consist of:

1. Rules for context validity (the three rules above); 2. Figure 2: the rules for Church's simple type theory including those for (1) the basic types e and t of entities and truth values, (2) function types with β-conversion ((λx :

A.b[x])(a) ≃ b[a]
), and (3) logical formulas7 ; and 3. Figure 3: the rules for dependent event types including those for (1) dependent event types and (2) their subtyping relations, and (3) general subtyping rules including subsumption. Some explanations of the rules are in order: -In the λ-rule in Fig. 2, we have added a side condition x ∈ F V (B), i.e.,

x does not occur free in B. This is necessary because we have dependent event types like Evt A (a): for example, we need to forbid to derive Γ ⊢ (λx : Agent.λe : Evt A (x).e) : Agent → Evt A (x) → Evt A (x) from Γ, x : Agent ⊢ (λe : Evt A (x).e) : Evt A (x) → Evt A (x), where in the former judgement, x in Agent → Evt A (x) → Evt A (x) would be a free variable that has not been declared in Γ . Note that, in Church's formulation [START_REF] Church | A formulation of the simple theory of types[END_REF], the side condition is not needed because, there, there are no dependent types (and x does not occur free in B for sure). -In the rules in Fig. 3, since all of the judgements have the same contexts, we have omitted the contexts. For example, the first rule in its third row should have been, if written in full:

Γ ⊢ a : Agent Γ ⊢ p : P atient Γ ⊢ Evt AP (a, p) ≤ Evt A (a)
(p) ≤ Event A type A ≤ A A ≤ B B ≤ C A ≤ C A ≤ A B ≤ B A → B ≤ A → B A B A ≤ B a : A A ≤ B
a : B Fig. 3. Rules for dependent event types.

The Type System UTT[E]

The type theory UTT (Chap. 9 of [START_REF] Luo | Computation and Reasoning: A Type Theory for Computer Science[END_REF]) is a dependent type theory with inductive types, type universes and higher-order logic. UTT is a typical Modern Type Theory (MTT) as employed in MTT-semantics [START_REF] Chatzikyriakidis | Formal Semantics in Modern Type Theories[END_REF][START_REF] Luo | Formal semantics in modern type theories with coercive subtyping[END_REF] (actually, it is the MTT the first author and colleagues have employed in developing MTT-semantics). Its meta-theory was studied in the Ph.D. thesis by Goguen [START_REF] Goguen | A typed operational semantics for type theory[END_REF]. Coercive subtyping [START_REF] Luo | Coercive subtyping in type theory[END_REF][START_REF] Luo | Coercive subtyping: theory and implementation[END_REF] has been developed by the authors and colleagues for modern type theories such as Martin-Löf's type theory and UTT.

Besides the type constructors in UTT as described in [START_REF] Luo | Computation and Reasoning: A Type Theory for Computer Science[END_REF], UTT[E] has the following constant types and constant type families for dependent event types:

-Entity : T ype -Agent, P atient : T ype.

-Event : T ype, Evt A : (Agent)T ype, Evt P : (P atient)T ype, and Evt AP : (Agent)(P atient)T ype.

The coercive subtyping relations in UTT[E] are given by subtyping judgements in E: they specify the subtyping relationships between dependent event types by means of the following parameterised constant coercions c i (i = 1, . . . , 4) in E, where a : Agent and p : P atient:

Evt AP (a, p) ≤ c1[a,p] Evt A (a), Evt AP (a, p) ≤ c2[a,p] Evt P (p), Evt A (a) ≤ c3[a] Event, Evt P (p) ≤ c4[p] Event,
The coercions also satisfy the coherence condition

c 3 [a] • c 1 [a, p] = c 4 [p] • c 2 [a, p].
Based on the study in [START_REF] Luo | Coercive subtyping: theory and implementation[END_REF][START_REF] Xue | Theory and implementation of coercive subtyping[END_REF], it is straightforward to show that UTT[E] is a well-behaved extension of UTT and hence preserves its nice meta-theoretic properties, including Church-Rosser, subject reduction, strong normalisation, and logical consistency.

Remark 2. As mentioned above, UTT[E] underlies the development of MTTsemantics by the first author and colleagues [START_REF] Chatzikyriakidis | Formal Semantics in Modern Type Theories[END_REF][START_REF] Luo | Formal semantics in modern type theories with coercive subtyping[END_REF]. In the recent trend of using rich type theories in formal semantics (see, for example, some of the papers in [START_REF]Modern Perspectives in Type-Theoretical Semantics[END_REF]), the development of MTT-semantics provides a full-blown alternative to the traditional Montague semantics with many advantages and has its further potentials to be developed in the future. It is worth remarking that UTT[E] underlies the event semantics in dependent type theories (or MTT-semantics with events) which contain, in particular, dependent event types.

Embedding of C e into UTT[E]

In this subsection, we show that C e can be faithfully embedded into UTT[E] and hence has nice meta-theoretic properties. The embedding of C e into UTT[E] is defined as follows and it is faithful as the theorem below shows.

Definition 1 (embedding). The embedding [[ ]]

from C e to UTT[E] is inductively defined as follows: 8

Constant types and dependent event types:

-

[[e]] Γ = Entity.
-[[t]] Γ = P rop. For the other constant types and dependent event types, they are mapped to the 'same' types in UTT[E], since we have overloaded their names. For example, -

[[Agent]] = Agent -[[Evt A (a)]] = Evt A ([[a]]) 2. Non-constant terms: -[[x]] Γ = x -[[A → B]] Γ = [[A]] Γ → [[B]] Γ -[[λx : A.b]] Γ = λ([[A]] Γ , T, [x : [[A]] Γ ] [[b]] Γ,x:A ), if [[Γ, x : A]] ⊢ [[b]] Γ,x:A : T -[[f (a)]] Γ = app(S, T, [[f ]] Γ , [[a]] Γ ), if [[Γ ]] ⊢ [[f ]] Γ : S → T and [[Γ ]] ⊢ [[a]] Γ : S 0 , where [[Γ ]] ⊢ S 0 ≤ S -[[P ⊃ Q]] Γ = [[P ]] Γ ⊃ [[Q]] Γ -[[∀(A, x.P )]] Γ = ∀([[A]] Γ , [x : [[A]] Γ ]. [[P ]] Γ,x:A ) 3. Contexts: -[[ ]] = (the empty context in UTT[E]) -[[Γ, x : A]] = [[Γ ]], x : [[A]] Γ 8
Formally, this is a partial function -it is only defined when certain conditions hold.

The embedding theorem shows that the embedding is total for well-typed terms. Also, a notional note: we shall use S and T to stand for types in UTT[E] where function types are special cases of Π-types: for any types S and T , S → T = Π(S, [ : S]T ).

-

[[Γ, P true]] = [[Γ ]], x : Prf([[P ]] Γ ), where x does not occur free in [[Γ ]].
The following theorem shows that the embedding is well-defined and faithful (in the sense of the theorem) and hence C e has nice meta-theoretic properties (the corollary). Its proof is based on the embedding of Church's simple type theory into the calculus of constructions [START_REF] Luo | A problem of adequacy: conservativity of calculus of constructions over higher-order logic[END_REF]. We omit the discussion of technical details, for otherwise we would have to detail the syntax and rules of UTT and coercive subtyping [START_REF] Luo | Computation and Reasoning: A Type Theory for Computer Science[END_REF][START_REF] Luo | Coercive subtyping: theory and implementation[END_REF], except remarking that a key reason that the proof goes through is because the coercions to model subtyping for dependent event types are constants and coherent (see Sect. 4.2) and hence model subsumptive subtyping in C e faithfully.

Theorem 2 (faithfulness). The embedding in Definition 1 is defined for every well-typed term in C e and, furthermore, we have:

1. If Γ valid in C e , then [[Γ ]] valid in UTT[E]. 2. If Γ ⊢ A type in C e , then [[Γ ]] ⊢ [[A]] : T ype in UTT[E]. 3. If Γ ⊢ a : A in C e , then in UTT[E], [[Γ ]] ⊢ [[a]] : T for some T such that [[Γ ]] ⊢ T ≤ d [[A]] for some d. 4. If Γ ⊢ P true in C e , then [[Γ ]] ⊢ p : Prf([[P ]]) for some p in UTT[E]. 5. If Γ ⊢ A ≤ B in C e , then [[Γ ]] ⊢ [[A]] ≤ c [[B]] for some unique c in UTT[E].
Corollary 3. C e inherits nice meta-theoretic properties from UTT[E], including strong normalisation and logical consistency. Remark 3. Instead of the embedding method we have described here, one may consider a more direct approach to metatheory of C e by directly showing that it has nice properties such as Church-Rosser and strong normalisation (as suggested by an anonymous reviewer). However, we think the above is simpler, which is of course a subjective view, and also demonstrates a generic approach to such meta-theoretic studies.

Event Quantification Problem

It is known that, when considering (neo-)Davidsonian event semantics where existential quantifiers for event variables are introduced, there is a problem in dealing with the scopes of the quantifiers when other quantificational phrases are involved. It has been argued that there is some incompatibility between event semantics and the traditional compositional semantics [START_REF] Champollion | The interaction of compositional semantics and event semantics[END_REF][START_REF] Winter | Event semantics and abstract categorial grammar[END_REF]. De Groote and Winter [START_REF] De Groote | A type-logical account of quantification in event semantics[END_REF] have called this as the event quantification problem (EQP for short).

Consider the following sentence (8) which, under the traditional event semantics with bark : Event → t, could have two possible interpretations ( 9) and [START_REF] Luo | A problem of adequacy: conservativity of calculus of constructions over higher-order logic[END_REF], where [START_REF] Luo | A problem of adequacy: conservativity of calculus of constructions over higher-order logic[END_REF] is incorrect. Formally, the incorrect interpretation is acceptable just as the correct one: [START_REF] Luo | A problem of adequacy: conservativity of calculus of constructions over higher-order logic[END_REF] is a legal formula. In order to avoid such incorrect interpretations as [START_REF] Luo | A problem of adequacy: conservativity of calculus of constructions over higher-order logic[END_REF], people have made several proposals (see, for example, [START_REF] Champollion | The interaction of compositional semantics and event semantics[END_REF][START_REF] Winter | Event semantics and abstract categorial grammar[END_REF]) which involve, for instance, consideration of quantification not over events but over sets of events [START_REF] Champollion | The interaction of compositional semantics and event semantics[END_REF], or some informal (and somewhat ad hoc) principles whose adherence would disallow the incorrect interpretations (see, for example, the related Scope Domain Principle proposed by Landman [START_REF] Landman | Plurality[END_REF]).

We shall study this with dependent event types as informally studied in Sects. 2 and 3, both in the Montagovian setting (i.e., in C e as described in Sect. 4.1) and in the MTT-semantics (i.e., in UTT[E] as described in Sect. 4.2). It is shown that, with dependent event types, the incorrect semantics are blocked as illegal since they are ill-typed.

EQP in Montague Semantics with Dependent Event Types

In the Montagovian setting with dependent event types (formally, C e in Sect. 4.1), this problem is solved naturally and formally -the incorrect semantic interpretations are excluded because they are ill-typed (in the empty context, where semantic interpretations of whole sentences like (8) are considered).

For example, (8) will be interpreted as [START_REF] Luo | Computation and Reasoning: A Type Theory for Computer Science[END_REF], while the 'incorrect' interpretation [START_REF] Luo | Coercive subtyping in type theory[END_REF] is not available (the formula ( 12) is ill-typed because x in Evt A (x), outside the scope of second/bound x (although intuitively it refers to it), is a free variable without being declared.) This offers a natural solution to the event quantification problem. Compared with existing solutions with informal ad hoc principles such as those mentioned above, our solution comes naturally as a 'side effect' of introducing dependent event types: it is formally disciplined and natural.

EQP in MTT-semantics with Dependent Event Types

In this paper, we have focussed on extending the traditional Montague semantics with dependent event types (formally, C e ), since the simple type theory is what the most semanticists are familiar with. One can also extend the MTT-semantics [START_REF] Chatzikyriakidis | Formal Semantics in Modern Type Theories[END_REF][START_REF] Luo | Formal semantics in modern type theories with coercive subtyping[END_REF] with dependent event types (formally, UTT[E], if we use UTT for MTTsemantics) and hence consider such refined event semantics in the setting of MTT-semantics. Here, we give an example to show how this is done.

Still consider the sentence (8): No dog barks. In the MTT-semantics, where CNs are interpreted as types (rather than predicates), the verb bark is given a dependent type as its semantics:

(13) bark : Πx : Dog. Evt A (x) → P rop It is also the case that the correct semantics ( 14) for ( 8) is legal (well-typed), while the incorrect one (15) is not:

(14) ¬∃x : Dog. ∃e : Evt A (x). bark(x, e) (15) (#) ∃e : Evt A (x). ¬∃x : Dog. bark(x, e)

Note that ( 15) is ill-typed for two reasons now: the first x is a variable not assumed anywhere and the term bark(x, e) is ill-typed as well.

Employing dependent event types in the Montagovian semantics (i.e., in C e as described in Sect. 4.1), would still leave a small possibility of some formally legal but incorrect semantics. For instance, one might consider the following semantics for ( 8 Note that, although ( 16) is incorrect, it is still well-typed because e is just an event, not an event with x as agent. 9 This, however, would not happen in the MTT-semantic setting where the type of the verb bark is the dependent type (13) and the following semantic sentence is ill-typed:

(17) (#) ∃e : Event. ¬∃x : Dog. bark(x, e), because bark(x, e) is not well-typed (it requires e to be of type Evt A (x), not just of type Event).

Conclusion

In this paper, we have introduced dependent event types for formal semantics. Subtyping is shown to play an essential role in this setting. We have also considered how dependent event types naturally solve the event quantification problem in combining event semantics with the traditional compositional semantics.

The notion of event types as studied in this paper is intensional, rather than extensional. For instance, when considering inverse verb pairs such as buy and sell, one may think that the events in [START_REF] Ranta | Type-Theoretical Grammar[END_REF] and ( 19) are the same [START_REF] Williams | Arguments in Syntax and Semantics[END_REF]. [START_REF] Ranta | Type-Theoretical Grammar[END_REF] John bought the book from Mary. [START_REF] Williams | Arguments in Syntax and Semantics[END_REF] Mary sold the book to John.

If one considers this from the angle of extensionality/intensionality, the buying event and the selling event in the above situation are extensionally the same, but intensionally different. More generally, this is related to how to understand the sameness of events in the setting with dependent event types. Work need be done to study event structures and relevant inference patterns.

Another interesting research topic is to study whether all thematic roles should be considered as parameters of dependent event types. Unlike agents and patients, some thematic roles considered in the literature may not be suitable to play the role of indexing dependent event types. In such cases, we would still propose that they should be formalised by means of logical predicates/relations. In the other direction, event types may depend on other entities other than thematic roles and further studies are called for to understand this better.

Z. Luo -

 Luo Partially supported by EU COST Action CA15123 and CAS/SAFEA International Partnership Program. S. Soloviev-Also an associated researcher at ITMO Univ, St. Petersburg, Russia. Partially supported by EU COST Action CA15123 and Russian Federation Grant 074-U01.

( 1 )

 1 John kissed Mary passionately. (2) ∃e : Event. kiss(e) & agent(e, j) & patient(e, m) & passionate(e)

Fig. 1 .

 1 Fig.1. Subtyping between event types with a : Agent and p : P atient.

( 4 )

 4 talk : Event → t. (5) John talked loudly. (6) ∃e : Event. talk(e) & loud(e) & agent(e, j)

6

 6

4. 1

 1 The Types System C e We shall first explain what a context is and what a judgement is in the system C e , and then describe the rules of C e .

Fig. 2 .

 2 Fig. 2. Rules for Church's STT.

( 8 )

 8 No dog barks. (9) ¬∃x : e. dog(x) & ∃e : Event. bark(e) & agent(e, x) (10) (#) ∃e : Event. ¬∃x : e. dog(x) & bark(e) & agent(e, x)

( 11 )

 11 ¬∃x : e. (dog(x) & ∃e : Evt A (x). bark(e)) (12) (#) ∃e : Evt A (x). ¬∃x : e. dog(x) & bark(e)

  ): (16) (#) ∃e : Event. ¬∃x : e. dog(x) & bark(e)

Formally, we have agentAP [a, p] = λe : EvtAP (a, p).a, of type EvtAP (a, p) → Agent. Usually we simply write, for example, agentAP (e) for agentAP [a, p](e).

It may be worth mentioning that, in the setting of MTT-semantics, coercive subtyping[START_REF] Luo | Coercive subtyping in type theory[END_REF][START_REF] Luo | Coercive subtyping: theory and implementation[END_REF] is used and, for uniformity, we may adopt coercive subtyping rather than subsumptive subtyping, although in general subsumptive subtyping is simpler.

A notational remark: in Ce, C stands for 'Church' and e for 'event'. The notation UTT[E] comes from the work of coercive subtyping (see, for example,[START_REF] Luo | Coercive subtyping: theory and implementation[END_REF]) where T[C] denotes type theory T extended by coercive subtyping whose basic subtyping are given as the set C of subtyping judgements.

This section is rather formal and, for a reader less interested in formal matters, its details might be safely skipped if one wishes so.

We only consider the intuitionistic ⊃ and ∀ here, omitting other operators including, in particular, those about, e.g. negation/classical logic in[START_REF] Church | A formulation of the simple theory of types[END_REF]. Also, we shall not assume extensionality.

Of course, one can argue that this is not intended since the agent is known, but formally, nothing prevents one from doing it.

Acknowledgement. Thanks go to Stergios Chatzikyriakidis, David Corfield, Koji Mineshima and Christian Retoré for helpful comments on this work.


Elena Manishina

Mouna Kamel

Cassia Trojahn

Nathalie Aussenac-Gilles

Unsupervised relation extraction from scientific texts using self-organizing maps

Keywords: Open relation extraction, clustering, self-organizing maps

Scientific texts represent a rich source of unstructured knowledge. Extracting this knowledge in a supervised manner can become highly expensive in time and human resources. Moreover supervised models are domain-and language-dependent which make them hard to maintain and extend. Hence unsupervised methods have received a lot of attention from researchers in the fields of information extraction and data mining. In this paper, we present our experiments with self-organizing maps (SOMs) for the task of open relation extraction. We combine contextual features of different level (lemmas and parts-of-speech) to help the algorithm to automatically discover lexical and morphological patterns in the corpus. The evaluation results show that our model yields a better performance than the widely used K-means clustering algorithm with the same feature set.

Introduction

With the ever growing quantity of available unstructured texts in various domains containing a large amount of information about the world, the need for efficient knowledge extraction techniques becomes apparent. This is especially true for scientific fields : new entities and the corresponding scientific terms as well as relations between them are discovered and updated regularly. Oftentimes this information is stored in the domain ontologies which need to be maintained and populated with newly discovered terms and relations. Updating ontologies is a laborious process involving domain experts and requiring extensive manual work.

Recent advances in automatic term and relation extraction procedures are designed to solve this problem for domains with significant amounts of annotated data. Unfortunately not all domains have annotated training resources ; most scientific texts available in sufficient quantities do not contain any kind of annotation necessary to train supervised relation extraction models. The manual annotation being costly in time and human resources, more and more researchers turn to unsupervised learning techniques, with various clustering algorithms being among the most widely used ones. A number of unsupervised learning techniques have been successfully implemented and tested on the general domain corpora. However their performance on the domain-specific texts is yet to be evaluated.

In this paper we present our relation extraction model which uses self-organizing maps -a neural-network-based clustering algorithm -which allows for flexible clustering unconstrained by random factors like the initial number of clusters and the the initial centroid coordinates.

A SOM organizes the data, mapping the space of training instances to a two-dimensional neural grid. This grid format allows for data examination as well as interactive assignment and labeling of data clusters. In addition, the SOM grid allows to explore the topology of the data (feature space) and adjust the feature set respectively. This paper is structured as follows : in section 2 we give a brief outline of the work carried out previously in the domain of unsupervised relation extraction and the application of SOM in similar tasks ; in section 3 we outline the theory behind our implementation of the SOM for the task of relation extraction as well as its place among similar clustering frameworks (like K-means) ; in section 4 we present the experiments with the SOM and the results ; finally we conclude the paper with a discussion and some future directions for our work.

Background

Various supervised learning algorithms have been successfully applied to the task of relation extraction (RE) : tree kernels within a Support Vector Machine [START_REF] Sorensen | Dependency tree kernels for relation extraction[END_REF]), Maximum Entropy models [START_REF] Kambhatla | Combining lexical, syntactic, and semantic features with maximum entropy models for extracting relations[END_REF], etc.

Neural networks (NN) are among the most recent learning techniques applied to RE. Specifically convolutional deep neural network (DNN) have been used to learn relation representations [START_REF] Xu | Semantic relation classification via convolutional neural networks with simple negative sampling[END_REF]) as well as to extract lexical and sentence level features [START_REF] Zeng | Relation classification via convolutional[END_REF] and [START_REF] Nguyen | Relation extraction : Perspective from convolutional neural networks[END_REF]).

The lack of annotated training data triggered the interest in semi-supervised and unsupervised learning for RE. In the domain of semi-supervised learning : Chen et al. (2006) implements a label propagation (LP) algorithm as applied to RE, [START_REF] Krause | Large-scale learning of relation-extraction rules with distant supervision from the web[END_REF] learns grammar-based RE rules from the Web by utilizing large numbers of relation instances as seed, etc.

Among the examples of a successful application of unsupervised learning to relation extraction in general domains are : [START_REF] Gonzalez | Unsupervised relation extraction by massive clustering[END_REF] with the adaptation of K-means and Expectation Maximization algorithms ; custom semantic clustering heuristic based on WordNet path distance [START_REF] Eichler | Unsupervised relation extraction from web documents[END_REF], etc.

Unsupervised NN algorithms, like Self-organizing map (SOM) which has traditionally been used for data visualization applications has also been successfully applied to NLP domains such as document clustering [START_REF] Chifu | Discovering web document clusters with self-organizing maps[END_REF]), co-reference resolution [START_REF] Burkovski | Self organizing maps in nlp : Exploration of coreference feature space[END_REF]) and relation extraction [START_REF] Bloehdorn | A self organizing map for relation extraction from wikipedia using structured data representations[END_REF]).

Unsupervised learning techniques and SOM specifically also showed a good performance comparable to those of supervised algorithms on large datasets where supervised methods often exhaust their computational capacities and end up over-fitting the training data.

Methodology

Relation extraction consists in identifying the entities (terms) and semantic relations between them in a corpus of text (a scientific article in our case). For example in a sentence : Proteinogenic amino acids, such as glutamate (standard glutamic acid) and gamma-amino-butyric acid also play critical non-protein roles within the body. -the terms glutamate and gammaamino-butyric acid are hyponyms of proteinogenic amino acid, i.e. they are both types of proteinogenic amino acid.

Relation extraction, especially using domain-specific corpus, is an important preliminary step in building domain ontologies and knowledge bases. In this context scientific articles present an invaluable source of knowledge. Apart from the typical unstructured text (paragraphs) scientific articles contain other data representation structures that may contain a lot of additional information and thus require a separate study : tables, figures, enumerative structures, etc. In this section we present the theoretical ground for our relation extraction model applied to paragraphs of text.

Relation extraction as a classification problem

We transform the relation extraction into a classification problem : given a pair of terms occurring in the same sentence we want to classify these terms as related or not related and consequently cluster the related terms by the relation type. Each instance pair is represented by the concatenated context vectors of its component terms on the lexical and POS level. The proximity of those vectors in the search space should suggest the similarity between the instances (term couples) and supposedly similar relations between the terms.

Self-Organizing Maps

The SOM is a type of artificial neural network for unsupervised learning and data visualization which builds the map from input examples using vector quantization and a topological layout of the prototype vectors. SOMs allow for a mapping of high-dimensional input vectors onto a low dimensional output space. A map itself represents a grid of nodes or neurons. Each node is represented by a weight vector of the same length as the input data vectors and a given position on the map. Placing a vector from data space onto the map consists in finding the node with the closest weight vector to the data space vector. The proximity between the two instances on the SOM allows to suggest that the term couples share the same semantic relation. Based on the inherent properties of SOM, we derive the following hypotheses :

-The instances in a cluster point to sets of features that are often shared across contexts, and hence may indicate relatedness of entity pairs. -The proximity of two term couples on the SOM suggests that these couples have semantically and syntactically similar contexts and thus are related in similar way, i.e. by the same relation. To evaluate the potential of SOM we compare it to a widely used K-means algorithm which uses the same feature set.

Word embeddings as training instance format

Concerning data format, one of the important innovations in recent years was the revival of word embeddings [START_REF] Mikolov | Efficient estimation of word representations in vector space[END_REF]) which became the most current training instance format for unsupervised RE [START_REF] Gupta | Domain ontology induction using word embeddings[END_REF], [START_REF] Hashimoto | Task-oriented learning of word embeddings for semantic relation classification[END_REF]). The intuition behind this is the following : word embeddings represent a word as a numerical vector, based on the context in which it appears ; this vector representation allows to perform vector operations and more importantly calculate the distance between vectors which can be seen as finding similar patterns in an unsupervised manner based on the distance between the context vectors. These vector properties make them an ideal data representation for unsupervised learning (specifically clustering algorithms).

In this section we present our experiments with SOM and K-means. Both algorithms use the same corpus and the same feature set.

Corpus

For our experiments we collected a corpus of articles from the Nature journal of the ISTEX digital library dating from 2000 till 2012. For this first experiment we removed structured data presentations (tables, figures) as well as vertical enumerative structures (lists) from the text. For each type of the removed data structure we constituted a separate corpus which is to be processed separately with a specific term annotation procedure and a different feature set. For the present experiment we kept only the text from the paragraphs. The corpus statistics is presented in Table 1. The first version of the corpus (Nature A) is the one annotated with the terms extracted using the weighed combination of terminological extractors. The second version (Nature B) is annotated with the terms from the NCIT ontology. Both annotation procedures are described in Section 4.2 below. POS-tagging is performed using TreeTagger [START_REF] Schmid | Improvements in part-of-speech tagging with an application to german[END_REF]) in order to build POS context vectors at the feature extraction stage.

Term identification

The original term extraction paradigm included running the weighed combination of the two term extractors on our corpus : Termsuite [START_REF] Cram | Termsuite : Terminology extraction with term variant detection[END_REF]) and Yatea [START_REF] Aubin | Improving term extraction with terminological resources[END_REF]). Combining these tools yields a sufficiently accurate and comprehensive terminological annotation of our corpus. This procedure however does not allow us to test our model as in this case the manual evaluation of the output would be necessary and would require human expertise in the field of medical science. Thus in order to objectively test the viability of our method we resort to a domain ontology. We opted for the National Cancer Institute Thesaurus (NCIT) 1 which combines the vocabulary for clinical care, translational and basic research, as well as the vocabulary for public information and administrative activities. NCIT ontology has a total of 118941 classes and 173 properties. This ontology was selected for having the best coverage on our corpus (76% terminology coverage according to the medical ontology recommendation portal 2 )].

Thus to test our implementation of the SOM algorithm we project the terms from the NCIT ontology on the corpus. We obtain 2412 unique terms in total (Table 1). After term projection multi-unit terms are replaced with a single token.

Features

To obtain the training instances we build the term couples according to the procedure described in Section 3. We apply the following constraints : both terms must be in the same sentence and the number of terms in between the two terms under consideration does not exceed 1 (i.e. maximum one term between the two target terms). Thus if a phrase contains 4 terms, 5 term couples will be extracted. For word2vec models we use two different formats of the training corpus : the first format represents the lemmas and the second one -POS tags. We train two models using skip-gram algorithm with the vector size of 100 and the window of 10 words on each corpus. Then for each couple of terms we generate an instance in the form of a feature vector. This feature vector represents a concatenation of the context word embedding vectors of the word tokens and the POS. In order to tackle the inherent computational complexity of the SOM training we opted for a smaller size of the word embeddings than the recommended defaults which resulted in a reduced dimensionality of the feature vectors. Another solution is to take the average of contextual vectors. We exploit both setups in our current experiments ; the results are presented in Section 4.5.

SOM implementation

For the implementation of the SOM algorithm we used the somoclu3 python library [START_REF] Wittek | Somoclu : An efficient parallel library for self-organizing maps[END_REF]) along with scikit-learn4 for a K-means implementation. Somoclu is a parallel implementation of self-organizing maps which includes a sparse kernel. For this first experiment we picked a 30x50 grid. Given the dimension of the feature vectors and a relatively high number of instances in the corpus this grid size seemed like a satisfactory compromise between the computation time and the expected accuracy of the data projection. Figure 1b shows the resulting SOM.

Results

We compared our SOM method with a classical K-means algorithm on the same feature set.

Here we focus on 8 relations from the NCIT ontology which emerge as the cluster-defining ones :

-Gene_Prod_Plays_Role_In_Bio_Process (GRB) -Conceptual_Part_Of (CPO) -EO_Disease_Has_Property_Or_Attribute (DPA) -Gene_Plays_Role_In_Process (GPRP) -Gene_Product_Has_Organism_Source (GPOS) -Procedure_Has_Excised_Anatomy (PEA) -Procedure_Uses_Manufactured_Object (PMO) -Procedure_Has_Target_Disease (PTD) As we can see from the table above the performance of the classifiers for different relations varies with no one specific trend : in general SOM shows better results than K-means. But the difference in concatenated versus average vector values with SOM does not seem to have a welldefined general pattern and is indeed relation-specific. The difference in F-score for different relations may be explained by the specificities and the variety of the lexical realizations of each relation type, but this phenomenon requires a thorough analysis which is currently under way.

Conclusions and Future work

In this article we presented our unsupervised approach to relation extraction based on SOM neural network as applied to paragraph text in the corpus of scientific articles. The approach is language-and domain-independent and does not require external resources (apart from the evaluation stage).

As we mentioned above, one of the objectives of the study was, among other things, developing a paradigm for automatic populating of domain ontologies. Though our model does not reach 100% accuracy and thus the extracted terms and relations cannot be integrated into the ontology directly, the results of the first raw extraction can be validated and refined by domain experts before integrating the new relations into the ontology.

As for our future work, we extend this approach to cover other information presentation formats : lists, tables, and images.

Acknowledgments

This work is funded by ISTEX project : ANR-10-IDEX-0004-02.

Références

  FIGURE 1 -Training instances distribution

TABLE 1 -

 1 Corpus statistics

	Corpus	Nsents	Nterms	Ncouples
	Nature A	81706	2528	42611
	Nature B	81706	2412	39611

TABLE 2

 2

	-F-score : SOM average vectors (F1), SOM concatenated vectors (F2) and K-means
	concatenated vectors (F3) (30x50 grid)
	Relation	F1	F2	F3
	EO_Disease_Has_Property_Or_Attribute	0.3	0.25	0.11
	Gene_Product_Has_Organism_Source	0.34	0.31	0.24
	Gene_Plays_Role_In_Process	0.59	0.22	0.11
	Conceptual_Part_Of	0.44	0.43	0.18
	Procedure_Has_Excised_Anatomy	0.43	0.52	0.25
	Gene_Prod_Plays_Role_In_Bio_Process	0.5	0.33	0.08
	Procedure_Has_Target_Disease	0.25	0.21	0.14
	Procedure_Uses_Manufactured_Object	0.43	0.46	0.1

https ://github.com/peterwittek/somoclu

http ://scikit-learn.org/stable/