Docs / Syntax / Minimalist / Probe / Cyclic

Cyclic Agree over articulated person probes

import Linglib.Syntax.Minimalist.Probe.Cyclic · namespace Minimalist.CyclicAgree

Person is decomposed into the privative segments of Phi.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

Béjar & Rezac 2009, Cyclic Agree formalized
Harley & Ritter 2002, Person and number in pronouns: A feature-geometric analysis formalized

Person geometries

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 (Harley & Ritter 2002).

inductive PersonGeometry L55–62

Type

standard : PersonGeometry
addressee : PersonGeometry
branching : PersonGeometry

Derives DecidableEq, Repr, Fintype.

Used by PersonGeometry.nodes, personSpec, pi_mem_personSpec, PersonGeometry.IsChain, fullProbe, AgreementSystem, AgreementSystem.flat_isInverse, AgreementSystem.spec_subset_or_subset

Used in BejarRezac2009

L64–68

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

def personSpec L70–72

(geom : PersonGeometry) (p : Person) :

List Phi.PersonSegment

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

Built from ,

Used by pi_mem_personSpec, PersonGeometry.IsChain, AgreementSystem.spec, AgreementSystem.spec_subset_or_subset

Used in BejarRezac2009, CoonKeine2021

Articulated probes and agreement systems

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

structure AgreementSystem L109–115

Type

geometry : PersonGeometry
The person geometry.
probe : Articulation
The articulated probe.

Derives DecidableEq, Repr.

Built from ,

Used by AgreementSystem.spec, AgreementSystem.residue, AgreementSystem.IsDirect, AgreementSystem.IsInverse, AgreementSystem.instDecidablePredScenarioPersonIsDirect, AgreementSystem.instDecidablePredScenarioPersonIsInverse, AgreementSystem.isDirect_iff, AgreementSystem.controller, AgreementSystem.value, AgreementSystem.cycles, AgreementSystem.rank, AgreementSystem.segProbe, AgreementSystem.EALicensed, AgreementSystem.instDecidablePredScenarioPersonEALicensed, AgreementSystem.eaLicensed_iff_isDirect, AgreementSystem.isInverse_self, AgreementSystem.IsDirect.mono, AgreementSystem.isDirect_iff_rank_lt, AgreementSystem.isDirect_iff_kind_eq_downstream

Used in BejarRezac2009, ClemDeal2026

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

theorem AgreementSystem.eaLicensed_iff_isDirect L178–181

(sys : AgreementSystem) (s : Clause.Scenario Person) :

sys.EALicensed s ↔ sys.IsDirect s

Built from , ,

L183–185

A probe with more segments has more direct contexts.

theorem AgreementSystem.IsDirect.mono L187–192

(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

Built from ,

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

theorem AgreementSystem.flat_isInverse L194–199

(s : Clause.Scenario Person) (geom : PersonGeometry) :

{ geometry := geom, probe := flatProbe }.IsInverse s

Built from , ,

L201–205

L207–229

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.

theorem AgreementSystem.isDirect_iff_kind_eq_downstream L231–235

(sys : AgreementSystem) (s : Clause.Scenario Person) (h : sys.geometry.IsChain) :

sys.IsDirect s ↔ (Clause.Scenario.map sys.rank s).kind = Clause.Scenario.Kind.downstream

Built from , , ,