Béjar and Rezac 2009: Cyclic Agree

Béjar and Rezac derive person-hierarchy effects in agreement from a single articulated person probe on v that meets the internal argument first and, with whatever segments it leaves unchecked, the external argument from the next projection of v. A language's articulation of the probe fixes which persons count as more specified, so the external argument controls the agreement slot only when it can check what the internal argument left. In the remaining, inverse contexts the core probe never reaches the external argument and its person goes unlicensed; property P adds a probe that licenses it, spelled out as extra agreement or as a special Case on the internal argument, and that probe converges only in inverse contexts, since in direct ones it and the core probe are valued alike on the same projection. The Person Case Constraint, which the authors had derived from the same licensing condition, follows from the same probes once a segment may not reach past a goal bearing π.

Main definitions

• BejarRezac2009.swahili, basque, nishnaabemwin, kashmiri: the flat, partial and two full articulations of the probe.
• BejarRezac2009.Converges: a transitive derivation, with or without property P, licenses the external argument and values no two probes alike on one projection.
• BejarRezac2009.segmentProbe: a segment of the probe searching nominals with Case.

Main results

• BejarRezac2009.basque_ranks_first_eq_second, BejarRezac2009.full_ranks: no ranking of persons picks Basque's controller, while specification picks it for a full probe.
• BejarRezac2009.basque_isDirect_iff, BejarRezac2009.nishnaabemwin_isDirect_iff: the direct contexts of (22).
• BejarRezac2009.converges_iff: a derivation converges iff it has property P exactly in an inverse context.
• BejarRezac2009.highestValue_eq_spec: the probe valued last spells out the external argument.
• BejarRezac2009.segmentProbe_pi, BejarRezac2009.pcc: the root segment is the person probe of the 2003 paper, and no segment reaches a nominal behind an oblique one.
• BejarRezac2009.controller_rows, context_rows, repair_rows: the examples.

Implementation notes

Checking is membership of a segment in a goal's specification, and the value a probe copies is the goal's whole specification. Third persons are not differentiated, so 3N3 is inverse; the paper's direct 3N3 forms, with differently specified third persons, are outside the model, and Table 9 leaves the Basque 3N3 cell unshaded although (22a) counts it inverse. Only arguments with structural Case establish an inverse context, which the model, without Case on the arguments of a transitive clause, does not state. The prose on p. 37 says (2a) tracks the external argument; the annotations and p. 38 show it is (2d).

TODO

The Nishnaabemwin theme suffix (27) and the portmanteaus i and ku as allomorphy of the core probe; Table 1's Georgian, Karok and Erza columns; inherent Case as invisibility to the probe, which would bring the Kashmiri past tense (31b) into the model.

References

• [BR09]
• [BR03]
• [Bej03]
• [HR02]

The systems

def BejarRezac2009.swahili : Minimalist.CyclicAgree.AgreementSystem

Swahili has the flat system [u-3], as in (7) and (10).

Equations

• BejarRezac2009.swahili = { geometry := Minimalist.CyclicAgree.PersonGeometry.standard, probe := Minimalist.CyclicAgree.flatProbe }

def BejarRezac2009.basque : Minimalist.CyclicAgree.AgreementSystem

Basque and Georgian have the partial system [u-3-2], as in (8).

Equations

• BejarRezac2009.basque = { geometry := Minimalist.CyclicAgree.PersonGeometry.standard, probe := Minimalist.CyclicAgree.partialProbe }

def BejarRezac2009.nishnaabemwin : Minimalist.CyclicAgree.AgreementSystem

Nishnaabemwin has the full system [u-3-1-2], under which second person is the most specified, as in (17) and Table 2C.

Equations

• BejarRezac2009.nishnaabemwin = { geometry := Minimalist.CyclicAgree.PersonGeometry.addressee, probe := Minimalist.CyclicAgree.fullProbe Minimalist.CyclicAgree.PersonGeometry.addressee }

def BejarRezac2009.kashmiri : Minimalist.CyclicAgree.AgreementSystem

Mohawk and Kashmiri have the full system [u-3-2-1], as in (9) and Tables 7 and 11.

Equations

• BejarRezac2009.kashmiri = { geometry := Minimalist.CyclicAgree.PersonGeometry.standard, probe := Minimalist.CyclicAgree.fullProbe Minimalist.CyclicAgree.PersonGeometry.standard }

Person hierarchies (§2)

def BejarRezac2009.Ranks (r : Person → ℕ) (f : Clause.Scenario Person → Person) : Prop

A ranking of persons picks the controller of an agreement slot when the external argument controls it in the scenarios downstream on the ranking and the internal one in those upstream.

Equations

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

theorem BejarRezac2009.basque_ranks_first_eq_second (r : Person → ℕ) (h : Ranks r basque.value) : r Person.first = r Person.second

A ranking that picks Basque's controller ranks first and second person alike, so it cannot decide (2a) and (2c), where each wins over the other (p. 38).

theorem BejarRezac2009.full_ranks (geom : Minimalist.CyclicAgree.PersonGeometry) (h : geom.IsChain) : Ranks (fun (p : Person) => (Minimalist.CyclicAgree.personSpec geom p).length) { geometry := geom, probe := Minimalist.CyclicAgree.fullProbe geom }.value

Under a chain geometry the depth of specification picks the controller of a full probe, so a hierarchy describes the full systems of Mohawk and Algonquian (p. 38).

Direct and inverse contexts (22)

theorem BejarRezac2009.basque_isDirect_iff (s : Clause.Scenario Person) : basque.IsDirect s ↔ s.low = Person.third ∧ s.high ≠ Person.third

Basque's direct contexts are those of a participant over a third person (22b).

theorem BejarRezac2009.nishnaabemwin_isDirect_iff (s : Clause.Scenario Person) : nishnaabemwin.IsDirect s ↔ (s.high = Person.second ∨ s.high = Person.firstInclusive) ∧ (s.low = Person.first ∨ s.low = Person.firstExclusive ∨ s.low = Person.third) ∨ (s.high = Person.first ∨ s.high = Person.firstExclusive) ∧ s.low = Person.third

Nishnaabemwin's direct contexts are 2N1, 2N3 and 1N3 (22b), the inclusive patterning with the second person (fn. 9).

theorem BejarRezac2009.basque_isDirect_imp_kashmiri {s : Clause.Scenario Person} (h : basque.IsDirect s) : kashmiri.IsDirect s

A context direct for Basque's partial probe is direct for the full probe, and 1N2 is inverse for the first and direct for the second, which is why Basque marks 1N2 with the added probe and Mohawk does not (p. 62).

theorem BejarRezac2009.kashmiri_participant_direct_iff (s : Clause.Scenario Person) : kashmiri.IsDirect s ∧ Minimalist.PersonSegment.participant ∈ kashmiri.spec s.high ∧ Minimalist.PersonSegment.participant ∈ kashmiri.spec s.low ↔ (s.high = Person.first ∨ s.high = Person.firstInclusive ∨ s.high = Person.firstExclusive) ∧ s.low = Person.second

In the full system of Mohawk the only direct context whose two arguments bear [participant] is 1N2, the cell of the portmanteau ku (26).

The added probe (§4.1)

inductive BejarRezac2009.Locus : Type

The first projection of v, from which the core probe meets the internal argument, and the second, from which it meets the external one.

• vI : Locus
• vII : Locus

@[instance_reducible]

instance BejarRezac2009.instDecidableEqLocus : DecidableEq Locus

Equations

• BejarRezac2009.instDecidableEqLocus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BejarRezac2009.instReprLocus : Repr Locus

Equations

• BejarRezac2009.instReprLocus = { reprPrec := BejarRezac2009.instReprLocus.repr }

def BejarRezac2009.instReprLocus.repr : Locus → ℕ → Std.Format

Equations

• BejarRezac2009.instReprLocus.repr BejarRezac2009.Locus.vI prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BejarRezac2009.Locus.vI")).group prec✝
• BejarRezac2009.instReprLocus.repr BejarRezac2009.Locus.vII prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BejarRezac2009.Locus.vII")).group prec✝

def BejarRezac2009.valuations (sys : Minimalist.CyclicAgree.AgreementSystem) (hasP : Bool) (s : Clause.Scenario Person) : List (Locus × List Minimalist.PersonSegment)

The valuations of v's probes pair each probe's locus with the value it copies, the goal's whole specification as in (12b). The core probe copies the internal argument on vI when some segment matches and the external argument on vII in a direct context, and when the core probe has property P the added probe copies the external argument on vII, as in (23).

Equations

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

def BejarRezac2009.Converges (sys : Minimalist.CyclicAgree.AgreementSystem) (hasP : Bool) (s : Clause.Scenario Person) : Prop

A derivation converges when the core probe or the added one licenses the external argument's person, as the PLC (13) requires, and no two probes are valued alike on one projection, which would leave them indistinguishable (p. 58).

Equations

• BejarRezac2009.Converges sys hasP s = ((sys.EALicensed s ∨ hasP = true) ∧ (BejarRezac2009.valuations sys hasP s).Nodup)

@[instance_reducible]

instance BejarRezac2009.instDecidablePredScenarioPersonConverges (sys : Minimalist.CyclicAgree.AgreementSystem) (hasP : Bool) : DecidablePred (Converges sys hasP)

Equations

• BejarRezac2009.instDecidablePredScenarioPersonConverges sys hasP x✝ = id inferInstance

theorem BejarRezac2009.converges_iff (sys : Minimalist.CyclicAgree.AgreementSystem) (hasP : Bool) (s : Clause.Scenario Person) : Converges sys hasP s ↔ (hasP = true ↔ sys.IsInverse s)

A derivation converges iff its core probe has property P exactly in an inverse context. Without P an inverse context leaves the external argument unlicensed, and with P a direct context values the core and the added probe alike on vII, as in (25) and Table 6.

def BejarRezac2009.highestValue (sys : Minimalist.CyclicAgree.AgreementSystem) (hasP : Bool) (s : Clause.Scenario Person) : Option (List Minimalist.PersonSegment)

The value of the probe valued on the highest projection of v, the only probe Kashmiri spells out by (24a).

Equations

• BejarRezac2009.highestValue sys hasP s = Option.map Prod.snd (BejarRezac2009.valuations sys hasP s).getLast?

theorem BejarRezac2009.highestValue_eq_spec {sys : Minimalist.CyclicAgree.AgreementSystem} {hasP : Bool} {s : Clause.Scenario Person} (h : Converges sys hasP s) : highestValue sys hasP s = some (sys.spec s.high)

In a convergent derivation the probe valued last is valued by the external argument, so Kashmiri's one agreement slot tracks it in direct and inverse contexts alike, and the internal argument bears R-Case exactly when the core probe has P, in inverse contexts (Table 11).

The Person Case Constraint (14), (15)

def BejarRezac2009.segmentProbe (geom : Minimalist.CyclicAgree.PersonGeometry) (s : Minimalist.PersonSegment) : Minimalist.Probe BejarRezac2003.Nominal

The segment s of the probe searches nominals with Case. The search halts at the closest nominal, which bears π and so intervenes for every segment (fn. 6), and Agrees with it iff its Case is unvalued and it bears the segment.

Equations

• BejarRezac2009.segmentProbe geom s = Minimalist.Probe.ofInt fun (n : BejarRezac2003.Nominal) => n.isActive && decide (s ∈ Minimalist.CyclicAgree.personSpec geom n.cell.person)

theorem BejarRezac2009.segmentProbe_pi (geom : Minimalist.CyclicAgree.PersonGeometry) : segmentProbe geom Minimalist.PersonSegment.pi = BejarRezac2003.phiProbe

The root segment π is the person probe of [BR03].

theorem BejarRezac2009.pcc (geom : Minimalist.CyclicAgree.PersonGeometry) (s : Minimalist.PersonSegment) (cd cn : Agreement.Bundle) : (segmentProbe geom s).agree [BejarRezac2003.Nominal.dat cd, BejarRezac2003.Nominal.caseless cn] = none

No segment reaches a nominal behind an oblique one, so a participant there goes unlicensed, the Person Case Constraint (14).

The examples

def BejarRezac2009.person? (e : Datum) (key : String) : Option Person

person? e key is the person an example's feature key names.

Equations

• BejarRezac2009.person? e key = e.parse? key [("1", Person.first), ("2", Person.second), ("3", Person.third)]

def BejarRezac2009.config? (e : Datum) : Option (Minimalist.CyclicAgree.AgreementSystem × Clause.Scenario Person)

config? e is the agreement system of an example's language with the scenario of its external over its internal argument.

Equations

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

theorem BejarRezac2009.controller_rows (e : Datum) : e ∈ Examples.all → ∀ c ∈ config? e, ∀ p ∈ person? e "controller", c.1.value c.2 = p

The controller the paper reports for an example in (2), (3), (17) and (18) is the one cyclic Agree gives.

theorem BejarRezac2009.context_rows (e : Datum) : e ∈ Examples.all → ∀ c ∈ config? e, ∀ x ∈ e.feature? "context", x = "inverse" ↔ c.1.IsInverse c.2

The direct and inverse contexts of the examples in (22) and (29) are those of cyclic Agree.

theorem BejarRezac2009.repair_rows (e : Datum) : e ∈ Examples.all → ∀ c ∈ config? e, ∀ x ∈ e.feature? "repair", Converges c.1 true c.2

Every example showing a repair, the added probe of Bizkaian Basque or the R-Case of Kashmiri, is a convergent derivation with property P (Table 9, (29)–(31)).

def BejarRezac2009.slotPrefix? (e : Datum) : Option Morphology.Morph

The first morph of an example's last word, a prefix.

Equations

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

theorem BejarRezac2009.basque_prefix_rows (e : Datum) : e ∈ Examples.all → e.language = "basq1248" → ∀ c ∈ config? e, ∀ x ∈ person? e "controller", ∃ n ∈ [Number.singular, Number.plural], (((match c.1.controller c.2 with | Minimalist.CyclicAgree.Argument.ia => Basque.absolutive | Minimalist.CyclicAgree.Argument.ea => Basque.displacedErgative).realize (Agreement.Bundle.personNumber (c.1.value c.2) n)).bind fun (x : List Morphology.Morph) => x.head?) = slotPrefix? e

The auxiliaries of (2) begin with the Fragment's prefix for the controller's person, in some number, which is the absolutive when the internal argument controls and the displaced ergative when the external one does, as in (2d).

def BejarRezac2009.georgianSet : Minimalist.CyclicAgree.Argument → Georgian.AffixSet

The Georgian affix set that spells the core probe in (21) is Set B when the internal argument values it on the first cycle and Set A when the external argument values it on the second.

Equations

• BejarRezac2009.georgianSet Minimalist.CyclicAgree.Argument.ia = Georgian.AffixSet.B
• BejarRezac2009.georgianSet Minimalist.CyclicAgree.Argument.ea = Georgian.AffixSet.A

theorem BejarRezac2009.georgian_prefix_rows (e : Datum) : e ∈ Examples.all → e.language = "nucl1302" → ∀ c ∈ config? e, (((georgianSet (c.1.controller c.2)).paradigm.realize (Agreement.Bundle.personNumber (c.1.value c.2) Number.singular)).bind fun (x : List Morphology.Morph) => x.head?) = slotPrefix? e

In the second-cycle morphology of (18), the 1st person singular is m- of Set B when the internal argument values the probe and v- of Set A when the external argument does.