Coordinators

A coordinator is a word or clitic that links the coordinands of a coordinate construction, such as and, or, but and nor. This file defines its lexical record, the morph, which says whether the coordinator is a free word or a bound clitic or affix, the gloss and the semantic type, and the relations that give the other uses its form has. What a coordinator denotes, an operation on the set of coordinands that its semantic type fixes, is Coordinator.denote in Semantics/Composition/Coordinator.lean.

Main definitions

• Coordinator.Role: the semantic type of a coordinator.
• Coordinator: the morph, gloss and semantic type of a coordinator.
• Coordinator.Correlative: a pair of correlative coordinators with the single coordinator of the plain construction.
• Coordinator.IsAlsoComitative: the coordinator's form is a form of a comitative marker, 'and' is 'with'.
• Coordinator.IsAlsoAdditive: the coordinator's form is that of an additive particle, 'and' is 'too'.

Implementation notes

• The other uses of a coordinator's form are relations to entries of other categories, not fields: a comitative use to a comitative marker of the language, an adposition or a case with its exponents, an additive use to an AdditiveParticle, and a quantifier use to an IndeterminateQuantifier of the language whose particle is the coordinator.
• Analyses that divide the conjunctive coordinators further, such as the two conjunction heads of Mitrović and Sauerland, classify the entries in their own studies.

References

• [Has97]
• [Has07]
• [MS16a]
• [Sta00]

inductive Coordinator.Role : Type

A coordinator's semantic type is conjunction, disjunction, adversative or negative coordination.

• conjunctive : Role

  Conjunction, English and.

• disjunctive : Role

  Disjunction, English or.

• adversative : Role

  Adversative coordination, English but.

• negative : Role

  Negative coordination, English nor, Latin neque.

@[instance_reducible]

instance Coordinator.instDecidableEqRole : DecidableEq Role

Equations

• Coordinator.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Coordinator.instReprRole : Repr Role

Equations

• Coordinator.instReprRole = { reprPrec := Coordinator.instReprRole.repr }

def Coordinator.instReprRole.repr : Role → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Coordinator.instReprRole.repr Coordinator.Role.negative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coordinator.Role.negative")).group prec✝

structure Coordinator : Type

A coordinator of a language. Its denotation is not stored, since its semantic type fixes it, Coordinator.denote.

• morph : Morphology.Morph

  The form, a free word or a clitic or affix bound on one side of its host.

• gloss : String

  The gloss.

• role : Role

  The semantic type.

@[instance_reducible]

instance instDecidableEqCoordinator : DecidableEq Coordinator

Equations

• instDecidableEqCoordinator = instDecidableEqCoordinator.decEq

def instDecidableEqCoordinator.decEq (x✝ x✝¹ : Coordinator) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instReprCoordinator : Repr Coordinator

Equations

• instReprCoordinator = { reprPrec := instReprCoordinator.repr }

def instReprCoordinator.repr : Coordinator → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure Coordinator.Correlative : Type

An emphatic coordination with correlative coordinators, English both … and, records the coordinators of the two coordinands and the single coordinator of the plain construction.

• first : List Morphology.Morph

  The form on the first coordinand.

• second : List Morphology.Morph

  The form on the second coordinand.

• single : Coordinator

  The coordinator of the plain construction.

def Coordinator.instDecidableEqCorrelative.decEq (x✝ x✝¹ : Correlative) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Coordinator.instDecidableEqCorrelative : DecidableEq Correlative

Equations

• Coordinator.instDecidableEqCorrelative = Coordinator.instDecidableEqCorrelative.decEq

@[instance_reducible]

instance Coordinator.instReprCorrelative : Repr Correlative

Equations

• Coordinator.instReprCorrelative = { reprPrec := Coordinator.instReprCorrelative.repr }

def Coordinator.instReprCorrelative.repr : Correlative → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Coordinator.toWord (c : Coordinator) : Morphology.Word

c.toWord is the coordinator as a word, of UD category CCONJ, its form in boundary notation.

Equations

• c.toWord = { form := toString c.morph, cat := UD.UPOS.CCONJ }

def Coordinator.IsAlsoComitative (c : Coordinator) (ms : List Morphology.Morph) (fs : Finset Case) : Prop

A coordinator is also comitative when its morph is one of the forms ms of a marker whose case values fs include the comitative, so that 'and' is 'with', [Sta00]'s lexical identity of the coordinator with the comitative marker. The marker is an adposition, with its morphs and functions, or a case of the language, with its exponents and functions.

Equations

• c.IsAlsoComitative ms fs = (c.morph ∈ ms ∧ Case.com ∈ fs)

@[instance_reducible]

instance Coordinator.instDecidableIsAlsoComitative (c : Coordinator) (ms : List Morphology.Morph) (fs : Finset Case) : Decidable (c.IsAlsoComitative ms fs)

Equations

• c.instDecidableIsAlsoComitative ms fs = { decide := decide (c.morph ∈ ms) && decide (Case.com ∈ fs), reflects_decide := ⋯ }

def Coordinator.IsAlsoAdditive (c : Coordinator) (a : AdditiveParticle) : Prop

A coordinator is also additive when its morph is that of an additive particle a, so that 'and' is 'too', the identity of the two that [Has97] notes and on which [MS16a] build.

Equations

• c.IsAlsoAdditive a = (c.morph = a.morph)

@[instance_reducible]

instance Coordinator.instDecidableIsAlsoAdditive (c : Coordinator) (a : AdditiveParticle) : Decidable (c.IsAlsoAdditive a)

Equations

• c.instDecidableIsAlsoAdditive a = Coordinator.instDecidableIsAlsoAdditive._aux_1 c a