The Mirror Principle

[Bak85]'s Mirror Principle: "Morphological derivations must directly reflect syntactic derivations (and vice versa)" ([Bak85] (4)). Each grammatical-function-changing rule — passive, causative, applicative, reflexive/reciprocal — simultaneously adds an affix to the verb and changes the grammatical functions of arguments, so affix layering must match the order of rule application.

[Bak85] §6 argues the principle should not be stipulated but should follow from the architecture: where the morphological and syntactic effects of a GF-rule are one process, mirroring holds by construction. Derivation realizes that architecture — a single list of DerivationSteps, each a rule with the affix it adds on the side it attaches — and the word's surface is derived from it by attachment (surface): the affixes of each side read outward from the root in the order the rules applied (surface_eq).

Main definitions

• GFRuleType: the GF-changing rules, with toMorphCategory mapping them into [Byb85]'s relevance hierarchy.
• Derivation, ruleOrder, surface: single-process derivations, their syntactic projection, and the surface they derive.
• AgreementPattern, referenceAt, deriveReference: agreement position relative to a GF-rule morpheme, the grammatical-function level visible once given rules have applied, and the level derivational timing makes visible at that position.
• MorphDomain.InScope: the principle's scope — concatenative morphology, excluding cliticization and nonconcatenative processes ([Bak85] §5).

GF-rules

inductive Morphology.MirrorPrinciple.GFRuleType : Type

Grammatical-function-changing rules: the processes that both add an affix to the verb and rearrange the grammatical functions of its arguments ([Bak85] §§2–4).

• passive : GFRuleType
• causative : GFRuleType
• applicative : GFRuleType
• reflexReciprocal : GFRuleType

@[instance_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqGFRuleType : DecidableEq GFRuleType

Equations

• Morphology.MirrorPrinciple.instDecidableEqGFRuleType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.MirrorPrinciple.instReprGFRuleType.repr : GFRuleType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.MirrorPrinciple.instReprGFRuleType : Repr GFRuleType

Equations

• Morphology.MirrorPrinciple.instReprGFRuleType = { reprPrec := Morphology.MirrorPrinciple.instReprGFRuleType.repr }

def Morphology.MirrorPrinciple.GFRuleType.toMorphCategory : GFRuleType → MorphCategory

Map GF-rules to [Byb85]'s morphological categories: passive marks voice; causative, applicative, and reflexive/reciprocal change valence.

Equations

• Morphology.MirrorPrinciple.GFRuleType.passive.toMorphCategory = Morphology.MorphCategory.voice
• Morphology.MirrorPrinciple.GFRuleType.causative.toMorphCategory = Morphology.MorphCategory.valence
• Morphology.MirrorPrinciple.GFRuleType.applicative.toMorphCategory = Morphology.MorphCategory.valence
• Morphology.MirrorPrinciple.GFRuleType.reflexReciprocal.toMorphCategory = Morphology.MorphCategory.valence

theorem Morphology.MirrorPrinciple.GFRuleType.toMorphCategory_relevanceLT_agreement (r : GFRuleType) : r.toMorphCategory.RelevanceLT (MorphCategory.agreement Agreement.Controller.subj)

GF-rule categories are strictly more stem-relevant than subject agreement on [Byb85]'s hierarchy. A relevance-order fact, not a positional universal: prefixal agreement can sit inside a GF-rule morpheme, as in Chamorro na'-fan-otchu ([Bak85] (15c)).

Derivations

structure Morphology.MirrorPrinciple.DerivationStep : Type

A derivational step bundling a GF-rule with the affix it adds and the side on which it attaches. Because the morphological and syntactic effects travel together, the Mirror Principle holds by construction ([Bak85] §6). An infix attaches after its host, as Word.Tree.toList linearizes it.

• rule : GFRuleType
• affix : String
• side : Morph.Side

def Morphology.MirrorPrinciple.instDecidableEqDerivationStep.decEq (x✝ x✝¹ : DerivationStep) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqDerivationStep : DecidableEq DerivationStep

Equations

• Morphology.MirrorPrinciple.instDecidableEqDerivationStep = Morphology.MirrorPrinciple.instDecidableEqDerivationStep.decEq

def Morphology.MirrorPrinciple.instReprDerivationStep.repr : DerivationStep → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.MirrorPrinciple.instReprDerivationStep : Repr DerivationStep

Equations

• Morphology.MirrorPrinciple.instReprDerivationStep = { reprPrec := Morphology.MirrorPrinciple.instReprDerivationStep.repr }

@[reducible, inline]

abbrev Morphology.MirrorPrinciple.Derivation : Type

Steps ordered first-applied (innermost affix) to last-applied (outermost).

Equations

• Morphology.MirrorPrinciple.Derivation = List Morphology.MirrorPrinciple.DerivationStep

def Morphology.MirrorPrinciple.ruleOrder (d : Derivation) : List GFRuleType

The syntactic projection of a derivation: its GF-rules in order of application.

Equations

• Morphology.MirrorPrinciple.ruleOrder d = List.map (fun (x : Morphology.MirrorPrinciple.DerivationStep) => x.rule) d

def Morphology.MirrorPrinciple.toTree (root : String) (d : Derivation) : Word.Tree String

The word a derivation builds on a root: each affix attached on its side, in order of application.

Equations

• Morphology.MirrorPrinciple.toTree root d = Morphology.Word.Tree.attachAll root (List.map (fun (st : Morphology.MirrorPrinciple.DerivationStep) => (st.side, st.affix)) d)

def Morphology.MirrorPrinciple.surface (root : String) (d : Derivation) : List String

The surface a derivation derives on a root.

Equations

• Morphology.MirrorPrinciple.surface root d = (Morphology.MirrorPrinciple.toTree root d).toList

theorem Morphology.MirrorPrinciple.surface_eq (root : String) (d : Derivation) : surface root d = (List.map (fun (x : DerivationStep) => x.affix) (List.filter (fun (x : DerivationStep) => decide (x.side = Morph.Side.before)) d)).reverse ++ root :: List.map (fun (x : DerivationStep) => x.affix) (List.filter (fun (x : DerivationStep) => decide (x.side = Morph.Side.after)) d)

The Mirror Principle ([Bak85] (4)): the surface is the prefixes in reverse order of application, the root, and the suffixes in order of application — on each side, affix order outward from the root is rule order.

Agreement and derivational timing

inductive Morphology.MirrorPrinciple.AgreementPosition : Type

Position of an agreement morpheme relative to a GF-rule morpheme: closer to the verb root (inner) or farther out (outer).

• inner : AgreementPosition
• outer : AgreementPosition

@[instance_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqAgreementPosition : DecidableEq AgreementPosition

Equations

• Morphology.MirrorPrinciple.instDecidableEqAgreementPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Morphology.MirrorPrinciple.instReprAgreementPosition : Repr AgreementPosition

Equations

• Morphology.MirrorPrinciple.instReprAgreementPosition = { reprPrec := Morphology.MirrorPrinciple.instReprAgreementPosition.repr }

def Morphology.MirrorPrinciple.instReprAgreementPosition.repr : AgreementPosition → ℕ → Std.Format

Equations

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

inductive Morphology.MirrorPrinciple.GFReference : Type

The level of grammatical functions an agreement morpheme references: semantic (pre-rule) or surface (post-rule).

• semantic : GFReference
• surface : GFReference

@[instance_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqGFReference : DecidableEq GFReference

Equations

• Morphology.MirrorPrinciple.instDecidableEqGFReference x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.MirrorPrinciple.instReprGFReference.repr : GFReference → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.MirrorPrinciple.instReprGFReference : Repr GFReference

Equations

• Morphology.MirrorPrinciple.instReprGFReference = { reprPrec := Morphology.MirrorPrinciple.instReprGFReference.repr }

structure Morphology.MirrorPrinciple.AgreementPattern : Type

An agreement morpheme's position relative to a GF-rule morpheme, paired with the level of grammatical functions it references.

• position : AgreementPosition
• reference : GFReference

def Morphology.MirrorPrinciple.instDecidableEqAgreementPattern.decEq (x✝ x✝¹ : AgreementPattern) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqAgreementPattern : DecidableEq AgreementPattern

Equations

• Morphology.MirrorPrinciple.instDecidableEqAgreementPattern = Morphology.MirrorPrinciple.instDecidableEqAgreementPattern.decEq

@[instance_reducible]

instance Morphology.MirrorPrinciple.instReprAgreementPattern : Repr AgreementPattern

Equations

• Morphology.MirrorPrinciple.instReprAgreementPattern = { reprPrec := Morphology.MirrorPrinciple.instReprAgreementPattern.repr }

def Morphology.MirrorPrinciple.instReprAgreementPattern.repr : AgreementPattern → ℕ → Std.Format

Equations

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

def Morphology.MirrorPrinciple.referenceAt (applied : List GFRuleType) : GFReference

The grammatical functions visible once the given GF-rules have applied: the semantic ones before any rule, the surface ones after.

Equations

• Morphology.MirrorPrinciple.referenceAt applied = if applied.isEmpty = true then Morphology.MirrorPrinciple.GFReference.semantic else Morphology.MirrorPrinciple.GFReference.surface

def Morphology.MirrorPrinciple.deriveReference : AgreementPosition → GFReference

The GF reference derivational timing dictates: an inner agreement morpheme is added before the GF-rule and sees semantic grammatical functions; an outer one is added after and sees surface ones.

Equations

• Morphology.MirrorPrinciple.deriveReference Morphology.MirrorPrinciple.AgreementPosition.inner = Morphology.MirrorPrinciple.GFReference.semantic
• Morphology.MirrorPrinciple.deriveReference Morphology.MirrorPrinciple.AgreementPosition.outer = Morphology.MirrorPrinciple.GFReference.surface

theorem Morphology.MirrorPrinciple.deriveReference_eq_referenceAt (r : GFRuleType) (pos : AgreementPosition) : deriveReference pos = referenceAt (match pos with | AgreementPosition.inner => [] | AgreementPosition.outer => [r])

Relative to one GF-rule, an inner agreement morpheme attaches with no rule applied and an outer one after it: deriveReference is referenceAt at the rules applied before the morpheme.

Scope

inductive Morphology.MirrorPrinciple.MorphDomain : Type

The kinds of morphology [Bak85] §5 distinguishes when delimiting the Mirror Principle's scope.

• concatenative : MorphDomain
• cliticization : MorphDomain
• nonconcatenative : MorphDomain

@[instance_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqMorphDomain : DecidableEq MorphDomain

Equations

• Morphology.MirrorPrinciple.instDecidableEqMorphDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.MirrorPrinciple.instReprMorphDomain.repr : MorphDomain → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.MirrorPrinciple.instReprMorphDomain : Repr MorphDomain

Equations

• Morphology.MirrorPrinciple.instReprMorphDomain = { reprPrec := Morphology.MirrorPrinciple.instReprMorphDomain.repr }

def Morphology.MirrorPrinciple.MorphDomain.InScope (d : MorphDomain) : Prop

The Mirror Principle's domain: concatenative (agglutinative) morphology, leaving cliticization and nonconcatenative morphology outside its scope ([Bak85] §5).

Equations

• d.InScope = (d = Morphology.MirrorPrinciple.MorphDomain.concatenative)

@[instance_reducible]

instance Morphology.MirrorPrinciple.instDecidablePredMorphDomainInScope : DecidablePred MorphDomain.InScope

Equations

• Morphology.MirrorPrinciple.instDecidablePredMorphDomainInScope d = Morphology.MirrorPrinciple.instDecidablePredMorphDomainInScope._aux_1 d