Baker 1985: the Mirror Principle

[Bak85]'s Mirror Principle (4): morphological derivations must directly reflect syntactic derivations. Passive, causative, applicative and reciprocal formation each add an affix to the verb and rearrange the grammatical functions of its arguments, so the order of the affixes outward from the root is the order in which the syntactic components applied. Given the independently known behaviour of each process, this explains why Chamorro's plural agreement fan- registers the surface subject outside the passive marker, the semantic subject inside the causative marker, and an intermediate subject between the two; why a reciprocal inside a causative links the root's agent and patient while a causative inside a reciprocal links the causer to the patient in Quechua but to the agent in Bemba, whose causative makes the old subject the object; and why an applied argument becomes the passive subject only with the applied affix inside the passive affix, so that the patient-subject reading is out in Chi-Mwi:ni and in only in Kinyarwanda, whose passive reaches a second object independently.

Baker argues (§6) that the principle should not be stipulated but follow from an architecture in which the morphological and the syntactic effect of a process are one thing. A Derivation here is that one thing, a list of processes each with the affix it adds, from which the word (word, a Word.Tree of morphs) and the grammatical functions (outcomes, a run of voices moving the participants) are both read. The word determines the sequence of processes (word_injective), and the universal restriction on agreement (27) holds by construction (registered_agree_apply, registered_apply_agree).

Main definitions

• passiveAt, causativeChamorro, causativeQuechua, applicativeOf, reciprocalOf: the GF-rules as the voice of each frame, Baker's schemas with the remaining material carried along.
• Stage: the substrate's Voice.Stage over the paper's participants.
• Process, Grammar, outcomes: the paper's processes, a language's settings, and the stages a sequence of processes reaches.
• Derivation, word: a derivation and the word it builds.
• derivation, processes, initialOf: a row's derivation, read off its segmentation.

Main results

• causativeChamorro_intransitive, reciprocalOf_np, passiveAt_fateOfRole, applicativeOf_isValencyIncreasing: Baker's rules are the substrate's voices where the frames meet.
• word_injective: the morphological derivation determines the processes (§2.1).
• registered_agree_apply, registered_apply_agree: (27), an agreement morpheme inside a GF-rule morpheme references semantic and one outside it surface grammatical functions.
• applied_subject_needs_applicative_first, applied_subject_of_applicative_first: an applied argument becomes the subject only with the applied affix inside the passive affix (§4.2).
• rows_word, rows_agreement, rows_links, rows_subject: the paper's examples.

Implementation notes

• A row's derivation is read off its segmentation: the prefixes from the root outward and then the suffixes, each a morph bound on its side (§2.1). The Chamorro passive -in- is an infix; the paper treats it as a prefix in a generalized sense (§3.1, §5) and the rows list it before the root, so it is a Morph.pref here.
• Baker's passive (12) keeps the demoted subject as an oblique where [Cre24]'s Voice.passive records it as implicit; the two agree on the fate of every core term (passiveAt_fateOfRole). His applicative (53) promotes an initial oblique where Voice.applicative introduces the applied participant.

References

• [Bak85]
• [Gib80] — Chamorro
• [Muy81] — Quechua
• [Giv76] — Bemba
• [Com82], [KA77], [Kim80] — Huichol, Chi-Mwi:ni, Kinyarwanda
• [Cre24]

Grammatical-function rules

Each rule is the voice of the frame it applies to, Baker's schema with the "…" material carried along ([Bak85] §2.2): the subject is the external argument, the objects are the nominal complements and the obliques the adpositional ones.

def Baker1985.demote : ArgumentFrame.Position → ArgumentFrame.Position

A nominal position demoted to an oblique.

Equations

• Baker1985.demote ArgumentFrame.Position.nominal = ArgumentFrame.Position.adpositional
• Baker1985.demote x✝ = x✝

def Baker1985.passiveAt (j : ℕ) (fr : ArgumentFrame) : Option Voice

Passive (12) promoting the j-th complement, if nominal: it becomes the subject and the old subject an oblique after the remaining complements.

Equations

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

def Baker1985.causativeChamorro (fr : ArgumentFrame) : Voice

The Chamorro-type causative (18), (50): a causer is the new subject, the old subject becomes the object and the old objects become obliques.

Equations

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

def Baker1985.causativeQuechua (fr : ArgumentFrame) : Voice

The Quechua-type causative (42): of a transitive, the objects stay and the old subject becomes an oblique; of an intransitive, the Chamorro type.

Equations

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

def Baker1985.applicativeOf (fr : ArgumentFrame) : Option Voice

The applicative (53) makes the first oblique the object and the old object a second object after it.

Equations

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

def Baker1985.reciprocalOf (fr : ArgumentFrame) : Option Voice

Reflexive-reciprocal formation (44): the object is bound to the subject and becomes the subject.

Equations

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

theorem Baker1985.causativeChamorro_intransitive : causativeChamorro ArgumentFrame.intransitive = Voice.causative

Both causative types treat an intransitive alike (§4.1), as [Cre24]'s causative.

theorem Baker1985.causativeQuechua_intransitive : causativeQuechua ArgumentFrame.intransitive = Voice.causative

theorem Baker1985.reciprocalOf_np : reciprocalOf ArgumentFrame.np = some Voice.reflexive

Of a transitive, reflexive-reciprocal formation is [Cre24]'s reflexive.

theorem Baker1985.passiveAt_fateOfRole (r : Voice.TermRole) (v : Voice) : v ∈ passiveAt 0 ArgumentFrame.np → v.fateOfRole r = Voice.passive.fateOfRole r

Baker's passive and [Cre24]'s agree on the fate of every core term.

theorem Baker1985.applicativeOf_isValencyIncreasing (v : Voice) : v ∈ applicativeOf ArgumentFrame.np_pp → v.IsValencyIncreasing

Baker's applicative is valency-increasing, as [Cre24]'s.

Participants and stages

inductive Baker1985.Arg : Type

The nominals a clause may host are the root's agent and patient, NP1 and NP2 of the paper's schemas, the oblique an applicative promotes, NP3, and the causer a causative introduces.

• agent : Arg
• patient : Arg
• applied : Arg
• causer : Arg

@[instance_reducible]

instance Baker1985.instDecidableEqArg : DecidableEq Arg

Equations

• Baker1985.instDecidableEqArg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Baker1985.instReprArg.repr : Arg → ℕ → Std.Format

Equations

• Baker1985.instReprArg.repr Baker1985.Arg.agent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Arg.agent")).group prec✝
• Baker1985.instReprArg.repr Baker1985.Arg.patient prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Arg.patient")).group prec✝
• Baker1985.instReprArg.repr Baker1985.Arg.applied prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Arg.applied")).group prec✝
• Baker1985.instReprArg.repr Baker1985.Arg.causer prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Arg.causer")).group prec✝

@[instance_reducible]

instance Baker1985.instReprArg : Repr Arg

Equations

• Baker1985.instReprArg = { reprPrec := Baker1985.instReprArg.repr }

@[reducible, inline]

abbrev Baker1985.Stage : Type

A derivational stage over the paper's participants.

Equations

• Baker1985.Stage = Voice.Stage Baker1985.Arg

The universal restriction on agreement

Of the four combinations of an agreement morpheme's position relative to a GF-rule morpheme with the level of grammatical functions it references, (27), only two occur: agreement inside the GF-rule morpheme references semantic functions and agreement outside it surface functions. With the morphological and the syntactic effect of a process one thing, the restriction holds by construction ([Bak85] §6): agreement attached before a GF-rule registers the subject before the rule applied, and agreement attached after it the subject after.

theorem Baker1985.registered_agree_apply (s : Stage) (v : Voice) (a : Option Arg) : ((Voice.Stage.agree s).apply v a).registered = s.registered ++ Voice.Stage.subjects s

Agreement inside the GF-rule morpheme registers the semantic subject (27a).

theorem Baker1985.registered_apply_agree (s : Stage) (v : Voice) (a : Option Arg) : (Voice.Stage.apply s v a).agree.registered = s.registered ++ (Voice.Stage.apply s v a).subjects

Agreement outside the GF-rule morpheme registers the surface subject (27d).

Processes and grammars

inductive Baker1985.Process : Type

The paper's processes are the GF-rules (§2.2) and number agreement (§3.1).

• passive : Process
• causative : Process
• applicative : Process
• reciprocal : Process
• agreement : Process

@[instance_reducible]

instance Baker1985.instDecidableEqProcess : DecidableEq Process

Equations

• Baker1985.instDecidableEqProcess x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Baker1985.instReprProcess.repr : Process → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Baker1985.instReprProcess.repr Baker1985.Process.passive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Process.passive")).group prec✝
• Baker1985.instReprProcess.repr Baker1985.Process.causative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Process.causative")).group prec✝
• Baker1985.instReprProcess.repr Baker1985.Process.agreement prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Process.agreement")).group prec✝

@[instance_reducible]

instance Baker1985.instReprProcess : Repr Process

Equations

• Baker1985.instReprProcess = { reprPrec := Baker1985.instReprProcess.repr }

inductive Baker1985.CausativeType : Type

Of the two causative types (§4.1), the Quechua type leaves a transitive root's object in place and demotes its subject, and the Chamorro type makes the old subject the object.

• quechua : CausativeType
• chamorro : CausativeType

@[instance_reducible]

instance Baker1985.instDecidableEqCausativeType : DecidableEq CausativeType

Equations

• Baker1985.instDecidableEqCausativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Baker1985.instReprCausativeType : Repr CausativeType

Equations

• Baker1985.instReprCausativeType = { reprPrec := Baker1985.instReprCausativeType.repr }

def Baker1985.instReprCausativeType.repr : CausativeType → ℕ → Std.Format

Equations

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

structure Baker1985.Grammar : Type

A language's settings are its causative type and whether its passive can promote the second of two objects (58).

• causative : CausativeType
• passiveSecond : Bool

@[instance_reducible]

instance Baker1985.instDecidableEqGrammar : DecidableEq Grammar

Equations

• Baker1985.instDecidableEqGrammar = Baker1985.instDecidableEqGrammar.decEq

def Baker1985.instDecidableEqGrammar.decEq (x✝ x✝¹ : Grammar) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Baker1985.instReprGrammar : Repr Grammar

Equations

• Baker1985.instReprGrammar = { reprPrec := Baker1985.instReprGrammar.repr }

def Baker1985.instReprGrammar.repr : Grammar → ℕ → Std.Format

Equations

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

def Baker1985.Grammar.causativeOf : Grammar → ArgumentFrame → Voice

The causative voice of a frame under the grammar.

Equations

• { causative := Baker1985.CausativeType.chamorro, passiveSecond := passiveSecond }.causativeOf = Baker1985.causativeChamorro
• { causative := Baker1985.CausativeType.quechua, passiveSecond := passiveSecond }.causativeOf = Baker1985.causativeQuechua

def Baker1985.Grammar.passivesOf (g : Grammar) (fr : ArgumentFrame) : List Voice

The passive voices of a frame under the grammar.

Equations

• g.passivesOf fr = (Baker1985.passiveAt 0 fr).toList ++ if g.passiveSecond = true then (Baker1985.passiveAt 1 fr).toList else []

def Baker1985.Process.apply (g : Grammar) : Process → Stage → List Stage

A process derives stages from a stage: the GF-rules apply their voices, the causative introducing the causer, and number agreement applies to a clause with no object (16).

Equations

• Baker1985.Process.apply g Baker1985.Process.passive x✝ = List.map (fun (x : Voice) => Voice.Stage.apply x✝ x none) (g.passivesOf x✝.frame)
• Baker1985.Process.apply g Baker1985.Process.causative x✝ = [Voice.Stage.apply x✝ (g.causativeOf x✝.frame) (some Baker1985.Arg.causer)]
• Baker1985.Process.apply g Baker1985.Process.applicative x✝ = List.map (fun (x : Voice) => Voice.Stage.apply x✝ x none) (Baker1985.applicativeOf x✝.frame).toList
• Baker1985.Process.apply g Baker1985.Process.reciprocal x✝ = List.map (fun (x : Voice) => Voice.Stage.apply x✝ x none) (Baker1985.reciprocalOf x✝.frame).toList
• Baker1985.Process.apply g Baker1985.Process.agreement x✝ = if x✝.frame.HasNominal then [] else [Voice.Stage.agree x✝]

def Baker1985.outcomes (g : Grammar) (ps : List Process) (s : Stage) : List Stage

The stages a sequence of processes can reach from a stage.

Equations

• Baker1985.outcomes g ps s = List.foldl (fun (ss : List Baker1985.Stage) (p : Baker1985.Process) => List.flatMap (Baker1985.Process.apply g p) ss) [s] ps

def Baker1985.initial (transitive applied : Bool) : Stage

The initial stage of a root has the agent as subject, the patient as object if transitive, and the oblique an applicative will promote.

Equations

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

theorem Baker1985.applied_subject_needs_applicative_first (g : Grammar) (transitive applied : Bool) (st : Stage) : st ∈ outcomes g [Process.passive, Process.applicative] (initial transitive applied) → Arg.applied ∉ Voice.Stage.subjects st

An applied argument becomes the subject only with the applied affix inside the passive affix (§4.2): with the passive applied first, no grammar and no root yields it.

theorem Baker1985.applied_subject_of_applicative_first (g : Grammar) : ∃ st ∈ outcomes g [Process.applicative, Process.passive] (initial true true), Voice.Stage.subjects st = [Arg.applied]

With the applied affix inside the passive affix, the applied argument is the subject.

Derivations and words

@[reducible, inline]

abbrev Baker1985.Derivation : Type

A derivation lists the processes with the affix each adds, in order of application; it is the single object whose two projections are the word and the grammatical functions ([Bak85] §6).

Equations

• Baker1985.Derivation = List (Baker1985.Process × Morphology.Morph)

def Baker1985.word (root : Morphology.Morph) (d : Derivation) : Morphology.Word.Tree Morphology.Morph

The word a derivation builds on a root attaches each affix on its side, in order of application (§2.1).

Equations

• Baker1985.word root d = Morphology.Word.Tree.attachMorphs root (List.map (fun (x : Baker1985.Process × Morphology.Morph) => x.2) d)

theorem Baker1985.word_injective (root : Morphology.Morph) {μ : Process → Morphology.Morph} (hμ : Function.Injective μ) (hside : ∀ (p : Process), (μ p).kind.side?.isSome = true) : Function.Injective fun (ps : List Process) => word root (List.map (fun (p : Process) => (p, μ p)) ps)

The morphological derivation determines the syntactic one (§2.1): for a language marking each process by its own morph bound on a side, the word is injective in the sequence of processes.

The paper's examples

def Baker1985.morphKeys : List (String × String)

The keys of a row's segmentation name the gloss label and the form of each morph.

Equations

• Baker1985.morphKeys = [("m1", "f1"), ("m2", "f2"), ("m3", "f3"), ("m4", "f4"), ("m5", "f5"), ("m6", "f6")]

def Baker1985.segmentation (r : Datum) : List (String × String)

A row's segmentation lists the gloss label and form of each morph in surface order.

Equations

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

def Baker1985.rootLabel (r : Datum) : String

The gloss label of a row's root.

Equations

• Baker1985.rootLabel r = (r.feature? "root").getD ""

def Baker1985.prefixes (r : Datum) : List (String × String)

The morphs before the root, outermost first.

Equations

• Baker1985.prefixes r = List.takeWhile (fun (x : String × String) => decide (x.1 ≠ Baker1985.rootLabel r)) (Baker1985.segmentation r)

def Baker1985.suffixes (r : Datum) : List (String × String)

The morphs after the root, innermost first.

Equations

• Baker1985.suffixes r = List.drop 1 (List.dropWhile (fun (x : String × String) => decide (x.1 ≠ Baker1985.rootLabel r)) (Baker1985.segmentation r))

def Baker1985.rootMorph (r : Datum) : Morphology.Morph

A row's root morph.

Equations

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

def Baker1985.morphs (r : Datum) : List Morphology.Morph

A row's morphs are its prefixes, root and suffixes in surface order.

Equations

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

def Baker1985.process? : String → Option Process

The process a gloss label marks.

Equations

• Baker1985.process? "PASS" = some Baker1985.Process.passive
• Baker1985.process? "CAUS" = some Baker1985.Process.causative
• Baker1985.process? "APPL" = some Baker1985.Process.applicative
• Baker1985.process? "BEN" = some Baker1985.Process.applicative
• Baker1985.process? "INSTR" = some Baker1985.Process.applicative
• Baker1985.process? "RECP" = some Baker1985.Process.reciprocal
• Baker1985.process? "REFL" = some Baker1985.Process.reciprocal
• Baker1985.process? "PL" = some Baker1985.Process.agreement
• Baker1985.process? x✝ = none

def Baker1985.derivation (r : Datum) : Derivation

A row's derivation lists its process-marking affixes in order of application, the prefixes from the root outward and then the suffixes, each bound on its side.

Equations

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

def Baker1985.processes (r : Datum) : List Process

A row's processes in order of application.

Equations

• Baker1985.processes r = List.map (fun (x : Baker1985.Process × Morphology.Morph) => x.1) (Baker1985.derivation r)

def Baker1985.initialOf (r : Datum) : Stage

A row's initial stage is transitive as recorded, with an oblique when an applicative applies.

Equations

• Baker1985.initialOf r = Baker1985.initial (decide (r.feature? "valence" = some "transitive")) (decide (Baker1985.Process.applicative ∈ Baker1985.processes r))

def Baker1985.grammar? (r : Datum) : Option Grammar

In a row's language settings, Chamorro, Bemba, Huichol and Chi-Mwi:ni have the Chamorro causative and Quechua its own, and Kinyarwanda's passive reaches a second object.

Equations

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

theorem Baker1985.rows_word (r : Datum) : r ∈ Examples.all → (word (rootMorph r) (derivation r)).toList.Sublist (morphs r)

The word a row's derivation builds linearizes to its process-marking morphs around the root in the row's order.

inductive Baker1985.Level : Type

The level of grammatical functions an agreement references is the surface subject, the semantic subject, or an intermediate one.

• surface : Level
• semantic : Level
• intermediate : Level

@[instance_reducible]

instance Baker1985.instDecidableEqLevel : DecidableEq Level

Equations

• Baker1985.instDecidableEqLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Baker1985.instReprLevel : Repr Level

Equations

• Baker1985.instReprLevel = { reprPrec := Baker1985.instReprLevel.repr }

def Baker1985.instReprLevel.repr : Level → ℕ → Std.Format

Equations

• Baker1985.instReprLevel.repr Baker1985.Level.surface prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Level.surface")).group prec✝
• Baker1985.instReprLevel.repr Baker1985.Level.semantic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Level.semantic")).group prec✝
• Baker1985.instReprLevel.repr Baker1985.Level.intermediate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Baker1985.Level.intermediate")).group prec✝

def Baker1985.level? (r : Datum) : Option Level

The subject a row reports its agreement registering.

Equations

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

def Baker1985.level (start final : Stage) : Option Level

The level of a single registration is the surface subject, the semantic subject, or neither.

Equations

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

theorem Baker1985.rows_agreement (r : Datum) : r ∈ Examples.all → ∀ g ∈ grammar? r, ∀ w ∈ level? r, ∀ st ∈ outcomes g (processes r) (initialOf r), level (initialOf r) st = some w

Every Chamorro row's fan- registers the subject the paper says it does: the surface subject outside the passive, the semantic subject inside the causative, and the subject between passive and causative in their combination.

def Baker1985.links? (r : Datum) : Option (Arg × Arg)

The dependency a row's translation records.

Equations

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

theorem Baker1985.rows_links (r : Datum) : r ∈ Examples.all → ∀ g ∈ grammar? r, ∀ l ∈ links? r, ∀ st ∈ outcomes g (processes r) (initialOf r), st.links = [l]

Reciprocal formation links the root's agent and patient when it applies before the causative, and the causer to the patient (Quechua) or the agent (Bemba) when after.

def Baker1985.surfaceSubject? (r : Datum) : Option Arg

The surface subject a row reports.

Equations

• Baker1985.surfaceSubject? r = r.parse? "surfaceSubject" [("applied object", Baker1985.Arg.applied), ("patient", Baker1985.Arg.patient)]

theorem Baker1985.rows_subject (r : Datum) : r ∈ Examples.all → ∀ g ∈ grammar? r, ∀ a ∈ surfaceSubject? r, r.judgment = Judgment.acceptable ↔ ∃ st ∈ outcomes g (processes r) (initialOf r), Voice.Stage.subjects st = [a]

A passive of an applicative is acceptable exactly when some run of the affix order makes the reported argument the subject: the applied object everywhere, the patient only in Kinyarwanda.