Coordination in the composition engine

This file adds coordination to the composition engine of Composition/Tree.lean as a binary mode beside functional application, intensional application and predicate modification. Two sisters of the same conjoinable type combine by what their coordinator denotes on the pair, Coordinator.denote, in the pointwise complete Boolean algebra of that type, which the mode finds at runtime through Ty.Domain.completeBooleanAlgebra?. Predicate modification is the conjunctive case at ⟨e,t⟩, so the engine's modification mode already agrees with the coordinator's denotation.

Main definitions

• HeimKratzer.Tree.coordinate?: the coordination mode.

Main results

• combine?_eq_coordinate?_of_conjunctive: predicate modification is conjunctive coordination at ⟨e,t⟩.

References

• [HK98]

def HeimKratzer.Tree.coordinate? {E W : Type} {M : Type → Type} [Applicative M] (c : Coordinator) (d1 d2 : Montague.Denotation E W M) : Option (Montague.Denotation E W M)

coordinate? c d1 d2 combines two sisters of the same conjoinable type by what the coordinator c denotes on the pair, in the complete Boolean algebra of their type, threaded through the effect M, and is none on sisters of different or non-conjoinable types.

Equations

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

theorem HeimKratzer.Tree.combine?_eq_coordinate?_of_conjunctive {E W : Type} {M : Type → Type} [Applicative M] {c : Coordinator} (hc : c.role = Coordinator.Role.conjunctive) (d1 d2 : Montague.Denotation E W M) (h1 : d1.fst = (Montague.Ty.e ⇒ Montague.Ty.t)) (h2 : d2.fst = (Montague.Ty.e ⇒ Montague.Ty.t)) : Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} => Mode.evalM) d1 d2 = coordinate? c d1 d2

Predicate modification is generalized conjunction at ⟨e,t⟩.