The Coordinator operation on Denot carriers

The carrier-agnostic Coordinator.op (in Defs) specialised to the intensional-logic Denot carriers: and/or/but/nor denote the meet/join/complement of the Boolean algebra on whatever conjoinable type the conjuncts inhabit, and the [PR83] genConj/genDisj recursion is proven to be it. This file sits below the composition engine (the tryCoord mode, the CCG .coord rule), supplying the runtime-Ty-dispatch form engineOp it consumes.

Main definitions

• Coordinator.engineOp — the runtime-Ty-dispatch form (via genConj/genDisj/genNeg).

Main results

• genConj_eq_op_et, genDisj_eq_op_et, op_*_t — the [PR83] recursion ARE Coordinator.op at the Denot carriers (flow-through bucket (a)).

Bridges: the [PR83] recursion ARE op (bucket (a))

theorem Coordinator.genConj_eq_op_et {E W : Type} (f g : Intensional.Denot E W (Intensional.Ty.e ⇒ Intensional.Ty.t)) : Intensional.Conjunction.genConj (Intensional.Ty.e ⇒ Intensional.Ty.t) E W f g = op Role.j f g

theorem Coordinator.genDisj_eq_op_et {E W : Type} (f g : Intensional.Denot E W (Intensional.Ty.e ⇒ Intensional.Ty.t)) : Intensional.Conjunction.genDisj (Intensional.Ty.e ⇒ Intensional.Ty.t) E W f g = op Role.disj f g

theorem Coordinator.op_j_t {E W : Type} (p q : Intensional.Denot E W Intensional.Ty.t) : op Role.j p q = p ⊓ q

theorem Coordinator.op_disj_t {E W : Type} (p q : Intensional.Denot E W Intensional.Ty.t) : op Role.disj p q = p ⊔ q

theorem Coordinator.op_nor_t {E W : Type} (p q : Intensional.Denot E W Intensional.Ty.t) : op Role.negDisj p q = (p ⊔ q)ᶜ

def Coordinator.engineOp : Role → (τ : Intensional.Ty) → (E W : Type) → Intensional.Denot E W τ → Intensional.Denot E W τ → Intensional.Denot E W τ

Engine-side operation: runtime dispatch on the type τ via the recursion forms, which the bridges above prove equal to op at every conjoinable type. The engine needs runtime Ty dispatch where op would need a statically-resolved instance.

Equations

• Coordinator.engineOp Coordinator.Role.j x✝² x✝¹ x✝ = Intensional.Conjunction.genConj x✝² x✝¹ x✝
• Coordinator.engineOp Coordinator.Role.mu x✝² x✝¹ x✝ = Intensional.Conjunction.genConj x✝² x✝¹ x✝
• Coordinator.engineOp Coordinator.Role.advers x✝² x✝¹ x✝ = Intensional.Conjunction.genConj x✝² x✝¹ x✝
• Coordinator.engineOp Coordinator.Role.disj x✝² x✝¹ x✝ = Intensional.Conjunction.genDisj x✝² x✝¹ x✝
• Coordinator.engineOp Coordinator.Role.negDisj x✝² x✝¹ x✝ = fun (p q : Intensional.Denot x✝¹ x✝ x✝²) => Intensional.Conjunction.genNeg x✝² x✝¹ x✝ (Intensional.Conjunction.genDisj x✝² x✝¹ x✝ p q)
• Coordinator.engineOp Coordinator.Role.negCoord x✝² x✝¹ x✝ = fun (p q : Intensional.Denot x✝¹ x✝ x✝²) => Intensional.Conjunction.genNeg x✝² x✝¹ x✝ (Intensional.Conjunction.genDisj x✝² x✝¹ x✝ p q)

theorem Coordinator.engineOp_j (τ : Intensional.Ty) (E W : Type) : engineOp Role.j τ E W = Intensional.Conjunction.genConj τ E W

theorem Coordinator.engineOp_disj (τ : Intensional.Ty) (E W : Type) : engineOp Role.disj τ E W = Intensional.Conjunction.genDisj τ E W