Documentation

Linglib.Discourse.Accessibility

Accessibility marking #

The Accessibility Marking Scale of [Ari90], as printed in [Ari01]: the classes of referring expression, from a modified full name to a zero, ordered by the accessibility of the referent they code, so that a more reduced form codes a more accessible referent (AccessibilityLevel). A form is classified by its head, whether it is modified, whether it carries lexical content, whether a name is full, its deixis, its stress and whether it is bound (AccessibilityLevel.head and the other features), and the three criteria the scale is claimed to reflect are read off the features: informativity, the lexical information a form carries; rigidity, its ability to pick out a referent by form alone; and attenuation, its phonological size. Each is compared, never counted: a form is more informative than another when it carries everything the other does, and the rigidity and attenuation scales are the chapter's own.

Main definitions #

Discourse.AccessibilityLevel: the scale, as a linear order.
AccessibilityLevel.head, modified, lexical, full, deixis, stressed, bound: the features of a form class.
AccessibilityLevel.informativity, rigidity, attenuation: the criteria, from the features, valued in the information a form carries (Information, ordered by inclusion), its Rigidity and its Attenuation.

Implementation notes #

The scale is the paper's ordering of its English form classes, taken as data; the criteria are not individually monotone along it, and which comparisons each criterion predicts is the business of Studies/Ariel2001.lean. The cognitive statuses of referents, as against the forms that code them, are Discourse.GivennessStatus.

References #

inductive Discourse.AccessibilityLevel :

An accessibility level is a class of referring expression on the Accessibility Marking Scale of [Ari90], from the least to the most accessible referent it codes.

fullNameMod : AccessibilityLevel
A modified full name, the former governor of Alaska, Sarah Palin.
fullName : AccessibilityLevel
A full name, Sarah Palin.
longDefDescription : AccessibilityLevel
A long definite description, the former governor of Alaska.
shortDefDescription : AccessibilityLevel
A short definite description, the governor.
lastName : AccessibilityLevel
A last name, Palin.
firstName : AccessibilityLevel
A first name, Sarah.
distalDemMod : AccessibilityLevel
A modified distal demonstrative phrase, that tall woman over there.
proxDemMod : AccessibilityLevel
A modified proximate demonstrative phrase, this tall woman.
distalDemNP : AccessibilityLevel
A distal demonstrative phrase, that woman.
proxDemNP : AccessibilityLevel
A proximate demonstrative phrase, this woman.
distalDem : AccessibilityLevel
A distal demonstrative, that.
proxDem : AccessibilityLevel
A proximate demonstrative, this.
stressedPronGesture : AccessibilityLevel
A stressed pronoun with a pointing gesture.
stressedPron : AccessibilityLevel
A stressed pronoun, SHE.
unstressedPron : AccessibilityLevel
An unstressed pronoun, she.
cliticizedPron : AccessibilityLevel
A cliticized pronoun, 'er.
verbalAgreement : AccessibilityLevel
Person inflection on the verb.
zero : AccessibilityLevel
A zero.

Instances For

@[instance_reducible]

instance Discourse.instDecidableEqAccessibilityLevel :

DecidableEq AccessibilityLevel

Equations

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

@[instance_reducible]

instance Discourse.instReprAccessibilityLevel :

Repr AccessibilityLevel

Equations

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

def Discourse.instReprAccessibilityLevel.repr :

AccessibilityLevel → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Discourse.instFintypeAccessibilityLevel :

Fintype AccessibilityLevel

Equations

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

@[instance_reducible]

instance Discourse.instInhabitedAccessibilityLevel :

Inhabited AccessibilityLevel

Equations

Discourse.instInhabitedAccessibilityLevel = { default := Discourse.instInhabitedAccessibilityLevel.default }

def Discourse.AccessibilityLevel.rank :

AccessibilityLevel → ℕ

The rank of a form class, higher for the more accessible referent.

Equations

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instLinearOrder :

LinearOrder AccessibilityLevel

The scale orders the levels fullNameMod < ⋯ < zero.

Equations

Discourse.AccessibilityLevel.instLinearOrder = LinearOrder.lift' Discourse.AccessibilityLevel.rank Discourse.AccessibilityLevel.instLinearOrder._proof_1

Features #

inductive Discourse.AccessibilityLevel.Head :

The head of a form class.

name : Head
description : Head
demonstrative : Head
pronoun : Head
inflection : Head
zero : Head

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidableEqHead :

DecidableEq Head

Equations

Discourse.AccessibilityLevel.instDecidableEqHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Discourse.AccessibilityLevel.instReprHead.repr :

Head → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instReprHead :

Repr Head

Equations

Discourse.AccessibilityLevel.instReprHead = { reprPrec := Discourse.AccessibilityLevel.instReprHead.repr }

@[instance_reducible]

instance Discourse.AccessibilityLevel.instFintypeHead :

Fintype Head

Equations

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

def Discourse.AccessibilityLevel.head :

AccessibilityLevel → Head

The head of a form class.

Equations

Instances For

def Discourse.AccessibilityLevel.modified :

AccessibilityLevel → Prop

A form carries a modifier, or is the long form of a description.

Equations

Discourse.AccessibilityLevel.fullNameMod.modified = True
Discourse.AccessibilityLevel.longDefDescription.modified = True
Discourse.AccessibilityLevel.distalDemMod.modified = True
Discourse.AccessibilityLevel.proxDemMod.modified = True
x✝.modified = False

Instances For

def Discourse.AccessibilityLevel.lexical :

AccessibilityLevel → Prop

A form carries lexical content beyond its head, a noun or a name.

Equations

Instances For

def Discourse.AccessibilityLevel.full :

AccessibilityLevel → Prop

A form is a full rather than a partial name.

Equations

Discourse.AccessibilityLevel.fullNameMod.full = True
Discourse.AccessibilityLevel.fullName.full = True
x✝.full = False

Instances For

def Discourse.AccessibilityLevel.deixis :

AccessibilityLevel → Option (Finset (Finset Role))

The deictic content of a proximate demonstrative form is the participant sets containing the speaker, and that of a distal form is the others.

Equations

Instances For

def Discourse.AccessibilityLevel.stressed :

AccessibilityLevel → Prop

A form is a stressed pronoun.

Equations

Discourse.AccessibilityLevel.stressedPronGesture.stressed = True
Discourse.AccessibilityLevel.stressedPron.stressed = True
x✝.stressed = False

Instances For

def Discourse.AccessibilityLevel.bound :

AccessibilityLevel → Prop

A form is a bound pronominal, cliticized or verbal agreement.

Equations

Discourse.AccessibilityLevel.cliticizedPron.bound = True
Discourse.AccessibilityLevel.verbalAgreement.bound = True
x✝.bound = False

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidablePredModified :

DecidablePred modified

Equations

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

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidablePredLexical :

DecidablePred lexical

Equations

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

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidablePredFull :

DecidablePred full

Equations

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

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidablePredStressed :

DecidablePred stressed

Equations

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

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidablePredBound :

DecidablePred bound

Equations

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

The criteria #

inductive Discourse.AccessibilityLevel.Information :

A piece of the lexical information a form carries.

lexical : Information
A lexical head, a noun or a name.
modifier : Information
A modifier, or the long form of a description.
fullName : Information
A full rather than a partial name.

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidableEqInformation :

DecidableEq Information

Equations

Discourse.AccessibilityLevel.instDecidableEqInformation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Discourse.AccessibilityLevel.instReprInformation.repr :

Information → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instReprInformation :

Repr Information

Equations

Discourse.AccessibilityLevel.instReprInformation = { reprPrec := Discourse.AccessibilityLevel.instReprInformation.repr }

@[instance_reducible]

instance Discourse.AccessibilityLevel.instFintypeInformation :

Fintype Information

Equations

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

def Discourse.AccessibilityLevel.Information.CarriedBy :

Information → AccessibilityLevel → Prop

A form carries a piece of information.

Equations

Discourse.AccessibilityLevel.Information.lexical.CarriedBy x✝ = x✝.lexical
Discourse.AccessibilityLevel.Information.modifier.CarriedBy x✝ = x✝.modified
Discourse.AccessibilityLevel.Information.fullName.CarriedBy x✝ = x✝.full

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidablePredInformationCarriedBy (l : AccessibilityLevel) :

DecidablePred fun (x : Information) => x.CarriedBy l

Equations

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

def Discourse.AccessibilityLevel.informativity (l : AccessibilityLevel) :

Finset Information

The informativity of a form is the lexical information it carries, one form being more informative than another when it carries everything the other does.

Equations

l.informativity = {x : Discourse.AccessibilityLevel.Information | x.CarriedBy l}

Instances For

inductive Discourse.AccessibilityLevel.Rigidity :

How far a form picks out its referent by its form alone.

pronominal : Rigidity
A pronominal form picks its referent out by features only.
descriptive : Rigidity
A lexical description picks its referent out by its content.
rigid : Rigidity
A name.

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidableEqRigidity :

DecidableEq Rigidity

Equations

Discourse.AccessibilityLevel.instDecidableEqRigidity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Discourse.AccessibilityLevel.instReprRigidity :

Equations

Discourse.AccessibilityLevel.instReprRigidity = { reprPrec := Discourse.AccessibilityLevel.instReprRigidity.repr }

def Discourse.AccessibilityLevel.instReprRigidity.repr :

Rigidity → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instFintypeRigidity :

Fintype Rigidity

Equations

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

@[instance_reducible]

instance Discourse.AccessibilityLevel.instLinearOrderRigidity :

LinearOrder Rigidity

pronominal < descriptive < rigid.

Equations

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

def Discourse.AccessibilityLevel.rigidity (l : AccessibilityLevel) :

The rigidity of a form is how it picks out its referent, by form alone for a name, by its content for a lexical description, and by features only for a pronominal form.

Equations

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

Instances For

inductive Discourse.AccessibilityLevel.Attenuation :

The phonological size of a form.

phrase : Attenuation
A lexical phrase is a name, a description or a demonstrative with a noun.
stressedWord : Attenuation
A stressed word is a stressed pronoun or a bare demonstrative.
unstressedWord : Attenuation
An unstressed word.
clitic : Attenuation
A clitic.
inflection : Attenuation
Verbal inflection.
zero : Attenuation
Nothing.

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instDecidableEqAttenuation :

DecidableEq Attenuation

Equations

Discourse.AccessibilityLevel.instDecidableEqAttenuation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Discourse.AccessibilityLevel.instReprAttenuation.repr :

Attenuation → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Discourse.AccessibilityLevel.instReprAttenuation :

Repr Attenuation

Equations

Discourse.AccessibilityLevel.instReprAttenuation = { reprPrec := Discourse.AccessibilityLevel.instReprAttenuation.repr }

@[instance_reducible]

instance Discourse.AccessibilityLevel.instFintypeAttenuation :

Fintype Attenuation

Equations

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

@[instance_reducible]

instance Discourse.AccessibilityLevel.instLinearOrderAttenuation :

LinearOrder Attenuation

The more attenuated a form, the higher it is in the order phrase < stressedWord < unstressedWord < clitic < inflection < zero.

Equations

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

def Discourse.AccessibilityLevel.attenuation (l : AccessibilityLevel) :

The attenuation of a form is its phonological reduction, from a lexical phrase through bare demonstratives and stressed, unstressed and cliticized pronouns and verbal agreement to a zero.

Equations

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

Instances For