Documentation

Linglib.Semantics.Composition.Coordination

Coordination in the composition engine #

tryCoord wires Coordinator.op into [HK98] type-driven interpretation — the composition-engine mode that is the sibling of tryFA/tryIFA/tryPM. tryPM (intersective predicate modification) is its ⟨e,t⟩ conjunction case (tryPM_eq_tryCoord_j), so the engine's existing modification mode already routes through the Coordinator API.

tryCoord is an engine mode (the tryX convention), not part of the Coordinator API surface; it invokes Coordinator.engineOp.

source
def Semantics.Composition.Tree.tryCoord {E W : Type} {M : Type → Type} [Applicative M] (role : Coordinator.Role) (d1 d2 : TypedDenot E W M) :
Option (TypedDenot E W M)

Coordination composition mode — the sibling of tryFA/tryIFA/tryPM. Two same-conjoinable-type sisters combine via Coordinator.op (through its runtime form Coordinator.engineOp), threaded through the effect functor M. Non-conjoinable or type-mismatched sisters yield none.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Semantics.Composition.Tree.tryPM_eq_tryCoord_j {E W : Type} {M : Type → Type} [Applicative M] (d1 d2 : TypedDenot E W M) (h1 : d1.ty = (Intensional.Ty.e ⇒ Intensional.Ty.t)) (h2 : d2.ty = (Intensional.Ty.e ⇒ Intensional.Ty.t)) :
    tryPM d1 d2 = tryCoord Coordinator.Role.j d1 d2

    tryPM is the ⟨e,t⟩ conjunction case of tryCoord: intersective predicate modification is generalized conjunction at ⟨e,t⟩.