Documentation

Linglib.Studies.AckemaNeeleman2018

Ackema & Neeleman (2018): Features of Person #

[AN18] [Har16a] [Cys09]

Formalizes the person-feature system of Ch 2 ("Person Features: Deriving the Inventory of Persons"): two privative features PROX and DIST, interpreted as functions on a nested person space, derive exactly the attested inventory of persons (three singular, four plural) and the inclusive/exclusive distinction — with no negative features and without generating nonattested persons.

Opt-in, bridged to the neutral inventory #

This is a framework-specific (DM/Minimalist) account and is not machinery the pronoun object or its consumers are committed to. A&N's PROX/DIST geometry is one of several competing decompositions (cf. [Har16a]'s Studies/Harbour2016.lean); the widely-adopted, framework-neutral representation is person + number + clusivity, encapsulated typologically by [Cys09]'s Person.Category. The deliverable here is therefore specToCategory: a converter from an A&N feature structure to that neutral inventory. A consumer that wants the feature geometry imports it; everyone else uses the neutral category.

The person space (§2.2, (4)) #

A nested family of sets of atoms S_i ⊂ S_{i+u} ⊂ S_{i+u+o}, where S_i has the speaker (i) as obligatory member, S_{i+u} adds an addressee (u), and S_{i+u+o} = PRS (the full input) adds others (o). DIST delivers a layer (a difference), which is unstructured and terminal.

The features as functions (§2.2, (6)) #

PROX S = Pred S — discards the outermost layer.
DIST S = S − Pred S — selects the outermost layer.

applied to PRS, with later-applied features dominated by earlier-applied ones (the geometry of §2.2 (9)/(11)). Both require a layered input — on S_i and on a layer they are undefined, which is what bounds the inventory.

Main results #

eval_third/eval_second/eval_first/eval_incl — the canonical structures [DIST], [PROX,DIST], [PROX,PROX], [PROX] derive 3/2/1/inclusive.
excl_eq_first_singular — first-person exclusive and first-person singular share the structure [PROX,PROX], deriving [Cys09]'s homophony observation; inclusive ([PROX]) is distinct.
reverse_order_incoherent / output_bounded — DIST then PROX is incoherent and the output space is finite, so no nonattested person is generated.
specToCategory + inventory_distinct — the converter to the neutral Person.Category, faithful on the seven attested persons.

The person space and the two features #

inductive AckemaNeeleman2018.PFeature :

A privative person feature (§2.2), interpreted below as a function on the nested person space. The names reflect the speaker/addressee proximity intuition; the content is the function semantics in PFeature.apply.

prox : PFeature
dist : PFeature

Instances For

@[implicit_reducible]

instance AckemaNeeleman2018.instDecidableEqPFeature :

DecidableEq PFeature

Equations

AckemaNeeleman2018.instDecidableEqPFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AckemaNeeleman2018.instReprPFeature.repr :

PFeature → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance AckemaNeeleman2018.instReprPFeature :

Equations

AckemaNeeleman2018.instReprPFeature = { reprPrec := AckemaNeeleman2018.instReprPFeature.repr }

inductive AckemaNeeleman2018.PSet :

A point in the person space (§2.2, (4)): a nested level (S_i ⊂ S_{i+u} ⊂ S_{i+u+o}) or a layer that DIST selects. Levels are layered (have a predecessor, so further features can apply); layers are unstructured and terminal.

si : PSet
S_i: speaker (and any associates) obligatory.
siu : PSet
S_{i+u}: additionally an addressee obligatory.
siuo : PSet
S_{i+u+o} = PRS: the full input set.
uLayer : PSet
S_{i+u} − S_i: the addressee layer (the output of DIST on S_{i+u}).
oLayer : PSet
S_{i+u+o} − S_{i+u}: the others layer (the output of DIST on PRS).

Instances For

@[implicit_reducible]

instance AckemaNeeleman2018.instDecidableEqPSet :

DecidableEq PSet

Equations

AckemaNeeleman2018.instDecidableEqPSet x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AckemaNeeleman2018.instReprPSet.repr :

PSet → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance AckemaNeeleman2018.instReprPSet :

Repr PSet

Equations

AckemaNeeleman2018.instReprPSet = { reprPrec := AckemaNeeleman2018.instReprPSet.repr }

def AckemaNeeleman2018.PSet.pred :

PSet → Option PSet

Pred (§2.2, (5)): the predecessor in the nesting. Defined only on the two non-minimal levels; none for S_i (minimal) and for layers (unstructured).

Equations

AckemaNeeleman2018.PSet.siuo.pred = some AckemaNeeleman2018.PSet.siu
AckemaNeeleman2018.PSet.siu.pred = some AckemaNeeleman2018.PSet.si
x✝.pred = none

Instances For

def AckemaNeeleman2018.PFeature.apply (f : PFeature) (s : PSet) :

Option PSet

Apply a person feature (§2.2, (6)). PROX discards the outermost layer (= Pred); DIST selects it (= S − Pred S). Both require a layered input, so both are none on S_i and on a layer.

Equations

Instances For

@[reducible, inline]

abbrev AckemaNeeleman2018.PSpec :

A person feature structure: the sequence of features, host (applied first) at the head — the geometry of §2.2 (9)/(11).

Equations

AckemaNeeleman2018.PSpec = List AckemaNeeleman2018.PFeature

Instances For

def AckemaNeeleman2018.PSpec.eval (fs : PSpec) :

Option PSet

Evaluate a feature structure on PRS = S_{i+u+o}. Host-first: [PROX, DIST] is DIST (PROX PRS). none if any application is incoherent — i.e. the structure is not generable by the system.

Equations

fs.eval = List.foldl (fun (acc : Option AckemaNeeleman2018.PSet) (f : AckemaNeeleman2018.PFeature) => acc.bind f.apply) (some AckemaNeeleman2018.PSet.siuo) fs

Instances For

The canonical structures and their derivations (§2.2) #

def AckemaNeeleman2018.third :

Third person: [DIST] selects the others layer.

Equations

AckemaNeeleman2018.third = [AckemaNeeleman2018.PFeature.dist]

Instances For

def AckemaNeeleman2018.second :

Second person: [PROX, DIST] selects the addressee layer.

Equations

AckemaNeeleman2018.second = [AckemaNeeleman2018.PFeature.prox, AckemaNeeleman2018.PFeature.dist]

Instances For

def AckemaNeeleman2018.first :

First person (singular / exclusive): [PROX, PROX] reaches S_i, whose only obligatory member is the speaker.

Equations

AckemaNeeleman2018.first = [AckemaNeeleman2018.PFeature.prox, AckemaNeeleman2018.PFeature.prox]

Instances For

def AckemaNeeleman2018.incl :

First person inclusive: [PROX] reaches S_{i+u} (speaker + addressee); singular-incompatible, so attested only in the plural.

Equations

AckemaNeeleman2018.incl = [AckemaNeeleman2018.PFeature.prox]

Instances For

theorem AckemaNeeleman2018.eval_third :

third.eval = some PSet.oLayer

theorem AckemaNeeleman2018.eval_second :

second.eval = some PSet.uLayer

theorem AckemaNeeleman2018.eval_first :

first.eval = some PSet.si

theorem AckemaNeeleman2018.eval_incl :

incl.eval = some PSet.siu

Clusivity is derived (§2.2) #

First-person exclusive and first-person singular share the same feature structure [PROX, PROX]; the inclusive has a distinct structure [PROX]. This derives [Cys09]'s observation that the exclusive is regularly homophonous with the first-person singular while the inclusive is hardly ever.

theorem AckemaNeeleman2018.excl_eq_first_singular :

First-person exclusive is the first-person singular structure.

theorem AckemaNeeleman2018.incl_excl_distinct :

incl.eval = some PSet.siu ∧ first.eval = some PSet.si

The inclusive output contains the addressee (S_{i+u}); the exclusive output does not (S_i). Clusivity is read off the output set, not stipulated.

No nonattested persons (§2.2, p. 28–29) #

The opposite order of application is incoherent (DIST delivers an unstructured layer, to which PROX/DIST cannot apply), and the output space is finite — so the system generates exactly the attested structures and no others.

theorem AckemaNeeleman2018.reverse_order_incoherent :

PSpec.eval [PFeature.dist, PFeature.prox] = none ∧ PSpec.eval [PFeature.prox, PFeature.prox, PFeature.prox] = none

DIST then PROX is incoherent, and PROX cannot iterate past S_i.

theorem AckemaNeeleman2018.output_bounded (fs : PSpec) :

fs.eval = none ∨ fs.eval = some PSet.siuo ∨ fs.eval = some PSet.si ∨ fs.eval = some PSet.siu ∨ fs.eval = some PSet.uLayer ∨ fs.eval = some PSet.oLayer

Every evaluation lands in the finite output space: none, the bare input S_{i+u+o}, or one of the four attested person sets. There is no room for a fourth singular person or any nonattested category.

Bridge to the neutral inventory ([Cys09] `Category`) #

def AckemaNeeleman2018.outputToCategory :

PSet → Bool → Option Person.Category

Map an output set together with its number (plural) to the neutral [Cys09] person category. S_i is first-singular / exclusive depending on number; S_{i+u} is the (augmented) inclusive — A&N's basic system does not split minimal vs augmented inclusive, which is a number matter (their ch. 3), so it maps to .augIncl. none for the singular-incompatible inclusive and for the bare input.

Equations

Instances For

def AckemaNeeleman2018.specToCategory (fs : PSpec) (plural : Bool) :

Option Person.Category

Converter from an A&N feature structure (plus number) to the neutral [Cys09] Category. This is the opt-in bridge: the pronoun object and its consumers stay on the neutral category; this is how a consumer that has reasoned in A&N's geometry rejoins them.

Equations

AckemaNeeleman2018.specToCategory fs plural = fs.eval.bind fun (x : AckemaNeeleman2018.PSet) => AckemaNeeleman2018.outputToCategory x plural

Instances For

theorem AckemaNeeleman2018.inventory_distinct :

specToCategory first false = some Person.Category.s1 ∧ specToCategory second false = some Person.Category.s2 ∧ specToCategory third false = some Person.Category.s3 ∧ specToCategory first true = some Person.Category.excl ∧ specToCategory incl true = some Person.Category.augIncl ∧ specToCategory second true = some Person.Category.secondGrp ∧ specToCategory third true = some Person.Category.thirdGrp

The seven attested persons map onto seven distinct neutral categories, covering all of [Cys09]'s inventory except .minIncl (the minimal inclusive — a number refinement A&N defer to their ch. 3).

theorem AckemaNeeleman2018.incl_singular_undefined :

specToCategory incl false = none

The singular-incompatible inclusive ([PROX] with no number) has no category — A&N's reason the inclusive surfaces only in the plural.