The Coordinator unit — marking + operation

A coordinator (and / or / but / nor) is one thing: a lexical marking whose role selects a Boolean operation. This file is the carrier-agnostic core of the Coordinator API — it needs only Mathlib.Order.BooleanAlgebra, so Fragments import it directly to type their lexical coordinators (the Semantics/Verb/Defs.lean precedent: a word-class lexical-entry type at Semantics/{class}/Defs). The Denot-specific bridges (genConj = op, engineOp, the BooleanAlgebra (Denot) instances) live downstream in Semantics/Coordination/Basic.lean.

op is the at-issue truth-conditional operation: the role selects the Boolean method (⊓ / ⊔ / (·⊔·)ᶜ), the instance supplies the algebra. It is faithful for and (.j), or (.disj), nor (.negDisj/.negCoord); the additive .mu and adversative .advers collapse onto and's meet here (op_mu_eq_j/op_advers_eq_j), their surplus content (M&S additive/focus, adversative contrast) diverging to the relevant studies / the discourse layer.

Main definitions

• Coordinator.Role — which Boolean operation a coordinator denotes.
• Coordinator.op — the operation a role denotes, polymorphic over [BooleanAlgebra α].
• Coordinator — a lexical coordinator's marking (decidable data Fragments configure).

inductive Coordinator.Role : Type

The role of a coordinator — which Boolean operation it denotes.

• j : Role

  J particle: set intersection / conjunction proper (English "and", Hungarian "es", Georgian "da").

• mu : Role

  MU particle: subset/additive (Hungarian "is", Georgian "-c", Japanese "mo"); at-issue identical to j.

• disj : Role

  Disjunction (English "or", Hungarian "vagy").

• advers : Role

  Adversative (English "but", Hungarian "de"); at-issue identical to j.

• negDisj : Role

  Negative disjunction (Irish "na" = "nor").

• negCoord : Role

  Negative coordination (Latin "neque/nec" = "neither...nor").

@[implicit_reducible]

instance Coordinator.instDecidableEqRole : DecidableEq Role

Equations

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

@[implicit_reducible]

instance Coordinator.instReprRole : Repr Role

Equations

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

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

Equations

• Coordinator.instReprRole.repr Coordinator.Role.j prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coordinator.Role.j")).group prec✝
• Coordinator.instReprRole.repr Coordinator.Role.mu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coordinator.Role.mu")).group prec✝
• Coordinator.instReprRole.repr Coordinator.Role.disj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coordinator.Role.disj")).group prec✝
• Coordinator.instReprRole.repr Coordinator.Role.advers prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coordinator.Role.advers")).group prec✝
• Coordinator.instReprRole.repr Coordinator.Role.negDisj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coordinator.Role.negDisj")).group prec✝
• Coordinator.instReprRole.repr Coordinator.Role.negCoord prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coordinator.Role.negCoord")).group prec✝

@[implicit_reducible]

instance Coordinator.instBEqRole : BEq Role

Equations

• Coordinator.instBEqRole = { beq := Coordinator.instBEqRole.beq }

def Coordinator.instBEqRole.beq : Role → Role → Bool

Equations

• Coordinator.instBEqRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Coordinator.op {α : Type u_1} [BooleanAlgebra α] : Role → α → α → α

THE operation a role denotes, polymorphic over any Boolean carrier: the role selects the Boolean method (⊓ / ⊔ / (·⊔·)ᶜ), the instance supplies the algebra. Faithful for and (.j), or (.disj), nor (.negDisj/.negCoord); the additive .mu and adversative .advers give only the at-issue meet — {j, mu, advers} all collapse onto ⊓ here, the surplus diverging (see op_mu_eq_j/op_advers_eq_j).

Equations

• Coordinator.op Coordinator.Role.j = fun (x1 x2 : α) => x1 ⊓ x2
• Coordinator.op Coordinator.Role.mu = fun (x1 x2 : α) => x1 ⊓ x2
• Coordinator.op Coordinator.Role.advers = fun (x1 x2 : α) => x1 ⊓ x2
• Coordinator.op Coordinator.Role.disj = fun (x1 x2 : α) => x1 ⊔ x2
• Coordinator.op Coordinator.Role.negDisj = fun (p q : α) => (p ⊔ q)ᶜ
• Coordinator.op Coordinator.Role.negCoord = fun (p q : α) => (p ⊔ q)ᶜ

theorem Coordinator.op_mu_eq_j {α : Type u_1} [BooleanAlgebra α] : op Role.mu = op Role.j

Additive .mu has the same at-issue denotation as and; its M&S additive/focus dimension diverges (see Studies/MitrovicSauerland2016).

theorem Coordinator.op_advers_eq_j {α : Type u_1} [BooleanAlgebra α] : op Role.advers = op Role.j

Adversative .advers (but) has the same at-issue denotation as and; its contrast is a discourse relation outside op (and non-commutative there, which the commutative ⊓ cannot represent).

structure Coordinator : Type

A coordination morpheme's marking — decidable data Fragments configure. The denotation is not stored: it is Coordinator.op of role.

• form : String

  Surface form of the morpheme.

• gloss : String

  Gloss / translation.

• role : Role

  Which Boolean operation it denotes.

• boundness : Boundness

  Free word vs bound clitic/suffix.

• alsoAdditive : Bool

  Does this morpheme also serve as an additive/focus particle?

• alsoQuantifier : Bool

  Does this morpheme also serve as a quantifier particle? Japanese "mo" and "ka" both do — tracks the coordination-quantification connection.

• correlative : Bool

  Can this morpheme be used in correlative (bisyndetic) patterns? Latin "et...et", "aut...aut".

• note : String

  Notes on usage or distribution.

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

Equations

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

@[implicit_reducible]

instance instDecidableEqCoordinator : DecidableEq Coordinator

Equations

• instDecidableEqCoordinator = instDecidableEqCoordinator.decEq

@[implicit_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.

def instBEqCoordinator.beq : Coordinator → Coordinator → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqCoordinator.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqCoordinator : BEq Coordinator

Equations

• instBEqCoordinator = { beq := instBEqCoordinator.beq }