Polarity items

[Lad79] [Zwa98] [Has97] [Lah98] [Isr96] [Isr01] [Isr11] [Chi06]

Polarity.Item, the lexical record for polarity-sensitive items, with its licensing parameters instantiated directly: licensor is the minimum Zwarts strength an environment must supply (none = not strength-licensed), freeChoice marks licensing by the generic-indefinite mechanism, and ppi marks positive-polarity blocking. Class labels are derived (isNPI, isFCI, isPPI), not stipulated: a weak NPI is an item with licensor = some .weak, a strict negative-concord item one with some .antiMorphic (clausal negation is the only anti-morphic environment), a non-strict one some .antiAdditive (concord under a negative quantifier is anti-additive licensing at this grain — the same requirement as an English strong NPI; the concord phenomenology itself is Features/NegativeConcord.lean territory). The item↔context licensing relation LicensingContext.licenses lives in Semantics/Polarity/Licensing.lean.

The record also carries the [Isr96] scalar direction and the [Lah98]-style morphological-composition typology. The full [Isr01] scalar-model classification is the extension bundle ScalarItem in Semantics/Polarity/ScalarModel.lean, built only for items that have one.

Main declarations

• Item — the polarity-item record.
• Item.isNPI, Item.isFCI, Item.isPPI — derived class labels.
• ScalarDirection — strengthening vs attenuating rhetorical force.
• NPIMorphology, AlternativeType — composition typology.

Scalar direction

inductive Polarity.ScalarDirection : Type

Rhetorical force: strengthening items (ever, any) make the assertion stronger than its scalar alternatives, attenuating ones (all that, long) weaker ([Isr96], [Isr11]). nonScalar is an editorial slot — Israel classifies most minimizers, including lift a finger, as scalar; leave the item's field none if unsure.

• strengthening : ScalarDirection
• attenuating : ScalarDirection
• nonScalar : ScalarDirection

@[instance_reducible]

instance Polarity.instDecidableEqScalarDirection : DecidableEq ScalarDirection

Equations

• Polarity.instDecidableEqScalarDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Polarity.instReprScalarDirection : Repr ScalarDirection

Equations

• Polarity.instReprScalarDirection = { reprPrec := Polarity.instReprScalarDirection.repr }

def Polarity.instReprScalarDirection.repr : ScalarDirection → ℕ → Std.Format

Equations

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

Force and composition typology

inductive Polarity.BaseForce : Type

Base quantificational force (when interpretable).

• existential : BaseForce
• universal : BaseForce
• degree : BaseForce
• temporal : BaseForce
• manner : BaseForce
• additive : BaseForce

@[instance_reducible]

instance Polarity.instDecidableEqBaseForce : DecidableEq BaseForce

Equations

• Polarity.instDecidableEqBaseForce x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Polarity.instReprBaseForce : Repr BaseForce

Equations

• Polarity.instReprBaseForce = { reprPrec := Polarity.instReprBaseForce.repr }

def Polarity.instReprBaseForce.repr : BaseForce → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Polarity.instReprBaseForce.repr Polarity.BaseForce.degree prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Polarity.BaseForce.degree")).group prec✝
• Polarity.instReprBaseForce.repr Polarity.BaseForce.manner prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Polarity.BaseForce.manner")).group prec✝

inductive Polarity.NPIMorphology : Type

Morphological composition of a polarity-sensitive item ([Lah98]: Hindi NPIs are transparently indefinite + even). indefPlusNeg covers genuine indefinite + negation morphology (Romanian nimic, some Slavic n-words).

• indefPlusEven : NPIMorphology
• indefPlusNeg : NPIMorphology
• plain : NPIMorphology
• idiomatic : NPIMorphology

@[instance_reducible]

instance Polarity.instDecidableEqNPIMorphology : DecidableEq NPIMorphology

Equations

• Polarity.instDecidableEqNPIMorphology x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Polarity.instReprNPIMorphology : Repr NPIMorphology

Equations

• Polarity.instReprNPIMorphology = { reprPrec := Polarity.instReprNPIMorphology.repr }

def Polarity.instReprNPIMorphology.repr : NPIMorphology → ℕ → Std.Format

Equations

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

inductive Polarity.AlternativeType : Type

Type of alternatives the item activates: cardinality (ek bhii), contextually salient properties (koii bhii) ([Lah98]), or subdomain alternatives ([Chi06]).

• cardinality : AlternativeType
• contextualProperty : AlternativeType
• domain : AlternativeType
• unspecified : AlternativeType

@[instance_reducible]

instance Polarity.instDecidableEqAlternativeType : DecidableEq AlternativeType

Equations

• Polarity.instDecidableEqAlternativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Polarity.instReprAlternativeType.repr : AlternativeType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Polarity.instReprAlternativeType : Repr AlternativeType

Equations

• Polarity.instReprAlternativeType = { reprPrec := Polarity.instReprAlternativeType.repr }

The polarity item

structure Polarity.Item : Type

A lexical entry for a polarity-sensitive item, with the licensing parameters instantiated directly: licensor (minimum Zwarts strength of a licensing environment), freeChoice (generic-indefinite mechanism), ppi (blocked in DE). Class labels derive from these — see isNPI/isFCI/isPPI and the docstring conventions in the module header. licensingContexts is the attested distribution the keystone (LicensingContext.licenses) checks the parameters against.

• form : String

  Surface form

• baseForce : BaseForce

  Base quantificational/semantic force

• licensor : Option DEStrength

  Minimum Zwarts strength of a licensing environment (none = not strength-licensed).

• freeChoice : Bool

  Licensed by the generic-indefinite mechanism (modals, generics, imperatives, free relatives).

• ppi : Bool

  Positive polarity: blocked in DE environments.

• licensingContexts : List LicensingContext

  Attested licensing environments (empty = needs positive contexts).

• scalarDirection : Option ScalarDirection

  Scalar direction ([Isr96]); none = unclassified.

• morphology : NPIMorphology

  Morphological composition ([Lah98])

• alternativeType : AlternativeType

  Type of alternatives introduced

@[instance_reducible]

instance Polarity.instReprItem : Repr Item

Equations

• Polarity.instReprItem = { reprPrec := Polarity.instReprItem.repr }

def Polarity.instReprItem.repr : Item → ℕ → Std.Format

Equations

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

Derived class labels

@[reducible, inline]

abbrev Polarity.Item.isNPI (e : Item) : Prop

An NPI is an item with a strength requirement.

Equations

• e.isNPI = (e.licensor.isSome = true)

@[reducible, inline]

abbrev Polarity.Item.isFCI (e : Item) : Prop

A free choice item is one licensed by the generic-indefinite mechanism (dual NPI/FCIs like any also carry a licensor).

Equations

• e.isFCI = (e.freeChoice = true)

@[reducible, inline]

abbrev Polarity.Item.isPPI (e : Item) : Prop

A positive polarity item.

Equations

• e.isPPI = (e.ppi = true)