Sister schemas

Two schemas with coindexed variables are sisters ([JA20] §4.8; [Boo10b]'s second-order schemas, notated with ≈): the linked variables must be filled alike across a paired instantiation (Sister.Pairs). The binary case formalized here is the canonical instance of their "two or more schemas" relation; the n-ary generalization is out of scope. The link is a bare relation on the two variable spaces — deliberately minimal substrate; J&A's stronger "the very same variable" reads as partial matching, which the link relation does not commit to.

Sisterhood is nondirectional by construction: Sister.swap transposes the pair, and pairs_swap shows paired instantiation is preserved. This is where the nondirectionality lives — on the packaging, not on any one realization.

Rules of referral in Paradigm Function Morphology recast as a variety of sister schemas ([JA20], crediting [Ble16]): a referred cell realizes exactly as its referent's exponence-only evaluation (Morphology.PFM.evalBlockForm_referral), so the two cells share realization — the realization-sharing a sister link expresses. The equation itself is directional (it evaluates the referral); the direction-of-referral problem [Ble16] raises is dissolved by reading the shared realization as a symmetric sister link, which is J&A's conceptual claim, carried by swap.

Main declarations

• Morphology.PFM.mem_expoFragment_expo — members of a block's exponence fragment carry exponence payloads
• Morphology.PFM.evalBlockForm_referral — a referred cell realizes as its referent's exponence-only evaluation
• Sister — two schemas with a variable link
• Sister.Pairs — paired instantiation sharing fillers at linked variables
• Sister.swap, Sister.pairs_swap — nondirectionality of the sister relation

theorem Morphology.PFM.mem_expoFragment_expo {L : Type u_1} {Z : Type u_2} {P : Type u_3} {b : Block L Z P} {r : Rule L P (Action Z P)} (h : r ∈ expoFragment b) : ∃ (f : P → Z → Z), r.payload = Action.expo f

Every member of a block's exponence fragment carries an exponence payload.

theorem Morphology.PFM.evalBlockForm_referral {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] {Lindex : Z → L} {b : Block L Z P} {w : Z} {σ : P} {r : Rule L P (Action Z P)} {retarget : P → P} (hr : Exponence.selectMinimal b (Lindex w, σ) = some r) (hpay : r.payload = Action.referral retarget) : evalBlockForm Lindex b (w, σ) = evalBlockForm Lindex (expoFragment b) (w, retarget σ)

A referred cell realizes exactly as its referent's exponence-only evaluation: when the narrowest rule at (w, σ) is a referral to retarget, evaluating the block equals evaluating its exponence fragment at the retargeted cell. The two cells share realization — the sister link recast from [Ble16]'s rules of referral.

structure Morphology.Construction.Sister (V₁ : Type u_4) (V₂ : Type u_5) (α : Type u_6) [PartialOrder α] : Type (max (max u_4 u_5) u_6)

Two schemas with coindexed variables: link v₁ v₂ marks a variable of fst as the same as a variable of snd.

• fst : Schema V₁ α

  The first schema.

• snd : Schema V₂ α

  The second schema.

• link : V₁ → V₂ → Prop

  The variable coindices.

def Morphology.Construction.Sister.Pairs {V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} [PartialOrder α] (S : Sister V₁ V₂ α) (w₁ : V₁ → α) (w₂ : V₂ → α) : Prop

A paired instantiation: each schema is instantiated, and linked variables are filled alike.

Equations

• S.Pairs w₁ w₂ = (S.fst.Instantiates w₁ ∧ S.snd.Instantiates w₂ ∧ ∀ ⦃v₁ : V₁⦄ ⦃v₂ : V₂⦄, S.link v₁ v₂ → w₁ v₁ = w₂ v₂)

def Morphology.Construction.Sister.swap {V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} [PartialOrder α] (S : Sister V₁ V₂ α) : Sister V₂ V₁ α

The transposed sister: swap the two schemas and the link.

Equations

• S.swap = { fst := S.snd, snd := S.fst, link := fun (v₂ : V₂) (v₁ : V₁) => S.link v₁ v₂ }

theorem Morphology.Construction.Sister.pairs_swap {V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} [PartialOrder α] {S : Sister V₁ V₂ α} {w₁ : V₁ → α} {w₂ : V₂ → α} : S.swap.Pairs w₂ w₁ ↔ S.Pairs w₁ w₂

Sisterhood is nondirectional: transposing preserves paired instantiation.