Documentation

Linglib.Features.Accessibility

Accessibility Marking Scale — Referential Form Taxonomy #

@cite{ariel-2001} @cite{arnold-wasow-losongco-ginstrom-2000}

Per-entry feature taxonomy classifying referring expressions by accessibility — the degree to which the referent's mental representation is available to the addressee. Speakers choose between reduced (pronoun) and full (name, description) forms based on this accessibility (@cite{ariel-2001}).

The Accessibility Marking Scale #

AccessibilityLevel is @cite{ariel-2001}'s 18-level ordering from least accessible (full name + modifier) to most accessible (zero / pro-drop). This replaces the earlier conflation with DefinitenessLevel — the accessibility and definiteness scales are non-monotonically related (names are less accessible than definite descriptions but more prominent for DOM), so they must be separate types. A coarsening function toDefLevel bridges to the DOM/DSM scale when needed.

Layer position #

Features/. Sibling of Features/Givenness.lean (the GHZ-6 hierarchy). Both are per-entry feature taxonomies for cognitive status: AccessibilityLevel classifies forms by their accessibility-marking behavior; GivennessStatus classifies entities by cognitive status. Ariel argues (her chapter pp. 62-65) that AccessibilityLevel's 18 tiers are better empirically supported than GHZ-6's 6 tiers; both retained as substrate because they serve different consumer profiles. The GivennessStatus.toAccessibility projection (in Phenomena/Reference/Studies/Ariel2001.lean) bridges them.

This module connects Phenomena/Reference/ (form choice) to Phenomena/WordOrder/ (position choice) via the shared dimension of NP weight/reduction.

inductive Features.AccessibilityLevel :

@cite{ariel-2001}'s Accessibility Marking Scale: a fine-grained ordering of referential form types from least to most accessible.

Each constructor represents a class of referring expressions. Speakers use more reduced forms for more accessible referents.

fullNameMod : AccessibilityLevel
fullName : AccessibilityLevel
longDefDescription : AccessibilityLevel
shortDefDescription : AccessibilityLevel
lastName : AccessibilityLevel
firstName : AccessibilityLevel
distalDemMod : AccessibilityLevel
proxDemMod : AccessibilityLevel
distalDemNP : AccessibilityLevel
proxDemNP : AccessibilityLevel
distalDem : AccessibilityLevel
proxDem : AccessibilityLevel
stressedPronGesture : AccessibilityLevel
stressedPron : AccessibilityLevel
unstressedPron : AccessibilityLevel
cliticizedPron : AccessibilityLevel
verbalAgreement : AccessibilityLevel
zero : AccessibilityLevel

Instances For

@[implicit_reducible]

instance Features.instDecidableEqAccessibilityLevel :

DecidableEq AccessibilityLevel

Equations

Features.instDecidableEqAccessibilityLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprAccessibilityLevel :

Repr AccessibilityLevel

Equations

Features.instReprAccessibilityLevel = { reprPrec := Features.instReprAccessibilityLevel.repr }

def Features.instReprAccessibilityLevel.repr :

AccessibilityLevel → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Features.instFintypeAccessibilityLevel :

Fintype AccessibilityLevel

Equations

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

@[implicit_reducible]

instance Features.instInhabitedAccessibilityLevel :

Inhabited AccessibilityLevel

Equations

Features.instInhabitedAccessibilityLevel = { default := Features.instInhabitedAccessibilityLevel.default }

def Features.instInhabitedAccessibilityLevel.default :

AccessibilityLevel

Equations

Features.instInhabitedAccessibilityLevel.default = Features.AccessibilityLevel.fullNameMod

Instances For

def Features.AccessibilityLevel.rank :

AccessibilityLevel → ℕ

Numeric rank: 0 (lowest accessibility) to 17 (highest). Higher rank = higher accessibility = more reduced form.

Equations

Instances For

theorem Features.AccessibilityLevel.rank_injective :

Function.Injective rank

Distinct accessibility levels have distinct ranks.

@[implicit_reducible]

instance Features.instLinearOrderAccessibilityLevel :

LinearOrder AccessibilityLevel

Total order on AccessibilityLevel via the rank pullback, matching the LinearOrder GivennessStatus / BinaryGivenness pattern in Features/Givenness.lean.

Equations

Features.instLinearOrderAccessibilityLevel = LinearOrder.lift' Features.AccessibilityLevel.rank Features.AccessibilityLevel.rank_injective

def Features.AccessibilityLevel.toDefLevel :

AccessibilityLevel → Prominence.DefinitenessLevel

Coarsening: each accessibility level maps to one of the 5 DefinitenessLevel categories used for differential argument marking. This is a many-to-one, non-monotone mapping — names are less accessible than definite descriptions but more prominent for DOM.

Equations

Instances For

@[reducible, inline]

abbrev Features.ReferentialForm :

Referential form options for referring to a discourse entity. Uses @cite{ariel-2001}'s 18-level accessibility marking scale.

Equations

Features.ReferentialForm = Features.AccessibilityLevel

Instances For

theorem Features.pronoun_more_reduced_than_name :

AccessibilityLevel.unstressedPron.rank > AccessibilityLevel.fullName.rank

An unstressed pronoun is more reduced than a full name.

inductive Features.NextMentionBias :

Next-mention bias: how likely a discourse referent is to be mentioned again in the subsequent utterance. Driven by thematic roles, coherence relations, and discourse structure.

high : NextMentionBias
low : NextMentionBias

Instances For

@[implicit_reducible]

instance Features.instDecidableEqNextMentionBias :

DecidableEq NextMentionBias

Equations

Features.instDecidableEqNextMentionBias x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprNextMentionBias.repr :

NextMentionBias → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Features.instReprNextMentionBias :

Repr NextMentionBias

Equations

Features.instReprNextMentionBias = { reprPrec := Features.instReprNextMentionBias.repr }

def Features.NextMentionBias.predictedForm :

NextMentionBias → ReferentialForm

Accessibility prediction: high next-mention bias licenses reduced referential form (unstressed pronoun); low bias requires full form (full name).

This is the monotone link at the heart of @cite{ariel-2001}'s Accessibility Marking Scale: more accessible referents → more reduced forms. The same relationship underlies the Probabilistic Reduction Hypothesis (more predictable → shorter/more reduced).

Equations

Instances For

theorem Features.high_bias_more_reduced :

AccessibilityLevel.rank NextMentionBias.high.predictedForm > AccessibilityLevel.rank NextMentionBias.low.predictedForm

The predicted form for high-bias referents is more reduced than for low-bias referents.

def Features.ReferentialForm.typicalWeight :

ReferentialForm → ℕ

NP weight correlate: reduced referential forms are lighter. Approximate number of words in a typical instance of each form. This connects form selection to constituent ordering (heavy NP shift, DLM).

The same choice that makes a referent "more reduced" also makes it "lighter", linking @cite{ariel-2001}'s accessibility hierarchy to @cite{arnold-wasow-losongco-ginstrom-2000}'s heaviness effects.

Equations

Instances For

theorem Features.pronoun_lightest :

ReferentialForm.typicalWeight AccessibilityLevel.unstressedPron ≤ ReferentialForm.typicalWeight AccessibilityLevel.shortDefDescription

Pronouns are at most as heavy as definite descriptions.

inductive Features.DiscourseElaboration :

How elaborated a referent's discourse representation is.

@cite{arnold-2026} §2: the key criterion for underspecified singular they is "discourse specificity" — whether the speaker intends to evoke a detailed mental representation for the addressee.

This extends @cite{newman-1992}'s "solidity" (existence of a specific concrete referent) and @cite{newman-1998}'s "individuation" (referents treated as individuals with identity-relevant details).

The scale runs from underspecified (the referent is barely sketched in the discourse model — quantified, indefinite, or mentioned only in passing) to elaborated (the referent has a rich, detailed representation — named, described, central to the narrative).

underspecified : DiscourseElaboration
The referent's discourse representation is minimal: quantified, indefinite, epicene, or not developed. Identity is unknown or unimportant. "Everyone should make their bed."
elaborated : DiscourseElaboration
The referent has a rich, detailed discourse representation: named, described, topical, with known personal attributes. "Asia Kate Dillon (born November 15, 1984) is an American actor. They are known for their roles as…"

Instances For

@[implicit_reducible]

instance Features.instDecidableEqDiscourseElaboration :

DecidableEq DiscourseElaboration

Equations

Features.instDecidableEqDiscourseElaboration x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprDiscourseElaboration.repr :

DiscourseElaboration → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Features.instReprDiscourseElaboration :

Repr DiscourseElaboration

Equations

Features.instReprDiscourseElaboration = { reprPrec := Features.instReprDiscourseElaboration.repr }

def Features.instBEqDiscourseElaboration.beq :

DiscourseElaboration → DiscourseElaboration → Bool

Equations

Features.instBEqDiscourseElaboration.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Features.instBEqDiscourseElaboration :

BEq DiscourseElaboration

Equations

Features.instBEqDiscourseElaboration = { beq := Features.instBEqDiscourseElaboration.beq }

def Features.AccessibilityLevel.toElaboration (a : AccessibilityLevel) :

DiscourseElaboration

Bridge from Ariel's accessibility scale to discourse elaboration.

@cite{ariel-2001}'s Accessibility Marking Scale describes which referential form is appropriate given how accessible a referent is. Arnold's discourse elaboration is related but distinct: low accessibility tends to co-occur with underspecified elaboration (a referent you haven't mentioned much is both less accessible and less elaborated), but they are not identical.

This coarsening maps high-accessibility forms (pronouns, agreement, zero) to elaborated (these forms require a well-established referent) and low-accessibility forms (full names, descriptions) to underspecified (these forms are used when the referent is being newly introduced or is not yet established). The boundary is approximate.

Equations

a.toElaboration = if a.rank ≥ 13 then Features.DiscourseElaboration.elaborated else Features.DiscourseElaboration.underspecified

Instances For

theorem Features.pronoun_implies_elaborated :

AccessibilityLevel.unstressedPron.toElaboration = DiscourseElaboration.elaborated

Pronouns (high accessibility) correlate with elaborated discourse representations — you use a pronoun for a referent that is already well-established in the discourse.

theorem Features.fullName_implies_underspecified :

AccessibilityLevel.fullName.toElaboration = DiscourseElaboration.underspecified

Full names (low accessibility) correlate with underspecified discourse representations — the referent is being (re-)introduced.