Cyclic Agree over articulated person probes

Person is decomposed into the privative segments of Minimalist.PersonSegment. Every person bears π, speech-act participants also participant, and the innermost segments speaker and addressee distinguish first from second person according to a geometry, which fixes which segments a language uses. A probe is a list of unvalued segments. A probe on v first meets the internal argument and checks every segment it bears; the segments left over, its residue, probe again from the next projection of v, where the external argument is the closest goal. The context is direct when the external argument checks some residue, and inverse otherwise, when the core probe never Agrees with it and its person goes unlicensed. A context is a scenario (Clause.Scenario) of the external over the internal argument, and under a chain geometry it is direct exactly when it is downstream on the number of probe segments each person bears.

Main definitions

• Minimalist.CyclicAgree.PersonGeometry: the standard, addressee and branching geometries.
• Minimalist.CyclicAgree.personSpec: the segments a person bears under a geometry.
• Minimalist.CyclicAgree.AgreementSystem: a geometry and an articulated probe, with the residue, the direct and inverse contexts, the controller of the agreement slot, person licensing of the external argument, and the rank of a person, the number of probe segments it bears.

Main results

• Minimalist.CyclicAgree.AgreementSystem.eaLicensed_iff_isDirect: the core probe licenses the external argument exactly in direct contexts.
• Minimalist.CyclicAgree.AgreementSystem.isDirect_iff_kind_eq_downstream: under a chain geometry a context is direct iff it is downstream on the system's rank.
• Minimalist.CyclicAgree.AgreementSystem.IsDirect.mono: a more articulated probe has more direct contexts.
• Minimalist.CyclicAgree.AgreementSystem.flat_isInverse: a flat probe makes every context inverse.

References

• [BR09]
• [HR02]

Person geometries

inductive Minimalist.CyclicAgree.PersonGeometry : Type

A person geometry fixes which innermost segment distinguishes first from second person. It is speaker under standard and addressee under addressee, and under branching both are sister leaves of participant ([HR02]).

• standard : PersonGeometry
• addressee : PersonGeometry
• branching : PersonGeometry

@[instance_reducible]

instance Minimalist.CyclicAgree.instDecidableEqPersonGeometry : DecidableEq PersonGeometry

Equations

• Minimalist.CyclicAgree.instDecidableEqPersonGeometry x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.CyclicAgree.instReprPersonGeometry : Repr PersonGeometry

Equations

• Minimalist.CyclicAgree.instReprPersonGeometry = { reprPrec := Minimalist.CyclicAgree.instReprPersonGeometry.repr }

def Minimalist.CyclicAgree.instReprPersonGeometry.repr : PersonGeometry → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.CyclicAgree.instFintypePersonGeometry : Fintype PersonGeometry

Equations

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

def Minimalist.CyclicAgree.PersonGeometry.nodes : PersonGeometry → List PersonSegment

The segments a geometry uses, from the root down.

Equations

• Minimalist.CyclicAgree.PersonGeometry.standard.nodes = [Minimalist.PersonSegment.pi, Minimalist.PersonSegment.participant, Minimalist.PersonSegment.speaker]
• Minimalist.CyclicAgree.PersonGeometry.addressee.nodes = [Minimalist.PersonSegment.pi, Minimalist.PersonSegment.participant, Minimalist.PersonSegment.addressee]
• Minimalist.CyclicAgree.PersonGeometry.branching.nodes = [Minimalist.PersonSegment.pi, Minimalist.PersonSegment.participant, Minimalist.PersonSegment.speaker, Minimalist.PersonSegment.addressee]

def Minimalist.CyclicAgree.personSpec (geom : PersonGeometry) (p : Person) : List PersonSegment

The segments a person bears under a geometry, from the root down.

Equations

• Minimalist.CyclicAgree.personSpec geom p = List.filter (fun (x : Minimalist.PersonSegment) => decide (x ∈ Minimalist.PersonSegment.spec p)) geom.nodes

theorem Minimalist.CyclicAgree.pi_mem_personSpec (geom : PersonGeometry) (p : Person) : PersonSegment.pi ∈ personSpec geom p

Every person bears π under every geometry.

def Minimalist.CyclicAgree.PersonGeometry.IsChain (geom : PersonGeometry) : Prop

A geometry is a chain when the persons' specifications are linearly ordered by inclusion.

Equations

• geom.IsChain = IsChain (fun (l m : List Minimalist.PersonSegment) => l ⊆ m) (Set.range (Minimalist.CyclicAgree.personSpec geom))

theorem Minimalist.CyclicAgree.PersonGeometry.standard_isChain : standard.IsChain

theorem Minimalist.CyclicAgree.PersonGeometry.addressee_isChain : addressee.IsChain

theorem Minimalist.CyclicAgree.PersonGeometry.not_branching_isChain : ¬branching.IsChain

Articulated probes and agreement systems

@[reducible, inline]

abbrev Minimalist.Probe.Articulation : Type

An articulated probe is a list of unvalued segments, from the most general to the most specific.

Equations

• Minimalist.Probe.Articulation = List Minimalist.PersonSegment

def Minimalist.CyclicAgree.flatProbe : Probe.Articulation

The flat probe [uπ].

Equations

• Minimalist.CyclicAgree.flatProbe = [Minimalist.PersonSegment.pi]

def Minimalist.CyclicAgree.partialProbe : Probe.Articulation

The partial probe [uπ, uparticipant], which distinguishes participants from third person.

Equations

• Minimalist.CyclicAgree.partialProbe = [Minimalist.PersonSegment.pi, Minimalist.PersonSegment.participant]

def Minimalist.CyclicAgree.fullProbe (geom : PersonGeometry) : Probe.Articulation

The full probe of a geometry, every segment the geometry uses.

Equations

• Minimalist.CyclicAgree.fullProbe geom = geom.nodes

structure Minimalist.CyclicAgree.AgreementSystem : Type

A language's agreement system is a person geometry together with an articulated probe.

• geometry : PersonGeometry

  The person geometry.

• probe : Probe.Articulation

  The articulated probe.

def Minimalist.CyclicAgree.instDecidableEqAgreementSystem.decEq (x✝ x✝¹ : AgreementSystem) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Minimalist.CyclicAgree.instDecidableEqAgreementSystem : DecidableEq AgreementSystem

Equations

• Minimalist.CyclicAgree.instDecidableEqAgreementSystem = Minimalist.CyclicAgree.instDecidableEqAgreementSystem.decEq

@[instance_reducible]

instance Minimalist.CyclicAgree.instReprAgreementSystem : Repr AgreementSystem

Equations

• Minimalist.CyclicAgree.instReprAgreementSystem = { reprPrec := Minimalist.CyclicAgree.instReprAgreementSystem.repr }

def Minimalist.CyclicAgree.instReprAgreementSystem.repr : AgreementSystem → ℕ → Std.Format

Equations

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

inductive Minimalist.CyclicAgree.Argument : Type

One of the two arguments of a transitive clause.

• ia : Argument
• ea : Argument

@[instance_reducible]

instance Minimalist.CyclicAgree.instDecidableEqArgument : DecidableEq Argument

Equations

• Minimalist.CyclicAgree.instDecidableEqArgument x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.CyclicAgree.instReprArgument.repr : Argument → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.CyclicAgree.instReprArgument : Repr Argument

Equations

• Minimalist.CyclicAgree.instReprArgument = { reprPrec := Minimalist.CyclicAgree.instReprArgument.repr }

@[reducible, inline]

abbrev Minimalist.CyclicAgree.AgreementSystem.spec (sys : AgreementSystem) (p : Person) : List PersonSegment

The segments a person bears under the system's geometry.

Equations

• sys.spec p = Minimalist.CyclicAgree.personSpec sys.geometry p

def Minimalist.CyclicAgree.AgreementSystem.residue (sys : AgreementSystem) (ia : Person) : Probe.Articulation

The residue of the probe after Agree with the internal argument, the segments it does not bear.

Equations

• sys.residue ia = List.filter (fun (x : Minimalist.PersonSegment) => decide (x ∉ sys.spec ia)) sys.probe

def Minimalist.CyclicAgree.AgreementSystem.IsDirect (sys : AgreementSystem) (s : Clause.Scenario Person) : Prop

A context, the scenario of the external over the internal argument, is direct when the external argument bears some segment of the residue.

Equations

• sys.IsDirect s = ∃ x ∈ sys.residue s.low, x ∈ sys.spec s.high

def Minimalist.CyclicAgree.AgreementSystem.IsInverse (sys : AgreementSystem) (s : Clause.Scenario Person) : Prop

A context is inverse when it is not direct.

Equations

• sys.IsInverse s = ¬sys.IsDirect s

@[instance_reducible]

instance Minimalist.CyclicAgree.AgreementSystem.instDecidablePredScenarioPersonIsDirect (sys : AgreementSystem) : DecidablePred sys.IsDirect

Equations

• sys.instDecidablePredScenarioPersonIsDirect x✝ = List.decidableBEx (Membership.mem (sys.spec x✝.high)) (sys.residue x✝.low)

@[instance_reducible]

instance Minimalist.CyclicAgree.AgreementSystem.instDecidablePredScenarioPersonIsInverse (sys : AgreementSystem) : DecidablePred sys.IsInverse

Equations

• sys.instDecidablePredScenarioPersonIsInverse x✝ = instDecidableNot

theorem Minimalist.CyclicAgree.AgreementSystem.isDirect_iff (sys : AgreementSystem) (s : Clause.Scenario Person) : sys.IsDirect s ↔ ∃ x ∈ sys.probe, x ∉ sys.spec s.low ∧ x ∈ sys.spec s.high

def Minimalist.CyclicAgree.AgreementSystem.controller (sys : AgreementSystem) (s : Clause.Scenario Person) : Argument

The argument controlling the agreement slot, the external argument in a direct context.

Equations

• sys.controller s = if sys.IsDirect s then Minimalist.CyclicAgree.Argument.ea else Minimalist.CyclicAgree.Argument.ia

def Minimalist.CyclicAgree.AgreementSystem.value (sys : AgreementSystem) (s : Clause.Scenario Person) : Person

The person the agreement slot realizes.

Equations

• sys.value s = if sys.IsDirect s then s.high else s.low

def Minimalist.CyclicAgree.AgreementSystem.cycles (sys : AgreementSystem) (s : Clause.Scenario Person) : Probe.Articulation × Probe.Articulation

The segments checked on each cycle, by the internal argument and then by the external one out of the residue.

Equations

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

def Minimalist.CyclicAgree.AgreementSystem.rank (sys : AgreementSystem) (p : Person) : ℕ

The rank of a person on the system's scale is the number of probe segments it bears.

Equations

• sys.rank p = (List.filter (fun (x : Minimalist.PersonSegment) => decide (x ∈ sys.spec p)) sys.probe).length

def Minimalist.CyclicAgree.AgreementSystem.segProbe (sys : AgreementSystem) (s : PersonSegment) : Probe Person

A segment of the probe searches its domain, halting at the closest goal, which bears π and so intervenes for every segment, and Agrees with that goal iff it bears the segment.

Equations

• sys.segProbe s = Minimalist.Probe.ofInt fun (p : Person) => decide (s ∈ sys.spec p)

def Minimalist.CyclicAgree.AgreementSystem.EALicensed (sys : AgreementSystem) (s : Clause.Scenario Person) : Prop

The external argument is licensed by the core probe when some segment of the residue Agrees with it from the next projection of v, whose domain has the external argument closest and the internal one below.

Equations

• sys.EALicensed s = ∃ x ∈ sys.residue s.low, (sys.segProbe x).agree [s.high, s.low] = some s.high

@[instance_reducible]

instance Minimalist.CyclicAgree.AgreementSystem.instDecidablePredScenarioPersonEALicensed (sys : AgreementSystem) : DecidablePred sys.EALicensed

Equations

• sys.instDecidablePredScenarioPersonEALicensed x✝ = List.decidableBEx (fun (x : Minimalist.PersonSegment) => (sys.segProbe x).agree [x✝.high, x✝.low] = some x✝.high) (sys.residue x✝.low)

theorem Minimalist.CyclicAgree.AgreementSystem.eaLicensed_iff_isDirect (sys : AgreementSystem) (s : Clause.Scenario Person) : sys.EALicensed s ↔ sys.IsDirect s

The core probe licenses the external argument exactly in direct contexts.

theorem Minimalist.CyclicAgree.AgreementSystem.isInverse_self (sys : AgreementSystem) (p : Person) : sys.IsInverse { high := p, low := p }

Arguments of the same person make an inverse context.

theorem Minimalist.CyclicAgree.AgreementSystem.IsDirect.mono (sys : AgreementSystem) (s : Clause.Scenario Person) {sys' : AgreementSystem} (hg : sys'.geometry = sys.geometry) (hp : sys.probe ⊆ sys'.probe) (h : sys.IsDirect s) : sys'.IsDirect s

A probe with more segments has more direct contexts.

theorem Minimalist.CyclicAgree.AgreementSystem.flat_isInverse (s : Clause.Scenario Person) (geom : PersonGeometry) : { geometry := geom, probe := flatProbe }.IsInverse s

A flat probe leaves no residue, since every internal argument bears π, so every context is inverse.

theorem Minimalist.CyclicAgree.AgreementSystem.spec_subset_or_subset {geom : PersonGeometry} (h : geom.IsChain) (p q : Person) : personSpec geom p ⊆ personSpec geom q ∨ personSpec geom q ⊆ personSpec geom p

theorem Minimalist.CyclicAgree.AgreementSystem.isDirect_iff_rank_lt (sys : AgreementSystem) (s : Clause.Scenario Person) (h : sys.geometry.IsChain) : sys.IsDirect s ↔ sys.rank s.low < sys.rank s.high

Under a chain geometry a context is direct iff the external argument bears more of the probe than the internal one does.

theorem Minimalist.CyclicAgree.AgreementSystem.isDirect_iff_kind_eq_downstream (sys : AgreementSystem) (s : Clause.Scenario Person) (h : sys.geometry.IsChain) : sys.IsDirect s ↔ (Clause.Scenario.map sys.rank s).kind = Clause.Scenario.Kind.downstream

Under a chain geometry a context is direct iff it is downstream on the system's rank, so the inverse contexts are the balanced and upstream scenarios.