Typology.Negation

[Dry13] [Has13b] [Mie05]

Per-language typological substrate for the standard sentential negation marker of a language: form, morphological status, position, symmetric/ asymmetric status, asymmetry subtype, and negative-indefinite strategy.

Mirrors the Linglib/Features/Possession.lean (Possession), Question.lean (Question), and Case.lean (Case) substrate-extension pattern: the substrate carries (a) per-paradigm-entry schema (NegMarkerEntry, NegationSystem), (b) the WALS-bundled per-language NegationProfile, (c) WALS converters and sample-counting helpers.

What lives here

• NegMorphemeType — direct projection from WALS Ch 112A's 6-way classification (negativeAffix, negativeParticle, negativeAuxiliaryVerb, negativeWordUnclearIfVerbOrParticle, variationBetweenNegativeWordAndAffix, doubleNegation). This is Dryer's WALS Ch 112 morpheme typology, NOT [Mie05]'s construction-level typology — Miestamo classifies constructions, not morphemes. The substrate carries Dryer's classification for cross-linguistic indexing; Miestamo's framework lives in Studies/Miestamo2005.lean.
• NegMarkerPosition — coarsening of WALS Ch 144A.
• NegMarkerEntry — one language's standard sentential negation marker.
• NegationSystem — bundles markers + WALS Ch 112A/143A/144A datapoints. The Fragment-side joint: every Fragments/{Lang}/Negation.lean exposes def negationSystem : NegationSystem.
• NegSymmetry, AsymmetrySubtype, NegIndefiniteStrategy, NegVerbPosition, NegMorphemePosition — WALS Ch 113-115/143A feature enums.
• NegStrategy — AVC-oriented classification of the negation strategy ([And06a], [Hei93]), with bridges to Anderson's AVC patterns (expectedInflPattern), Heine's grammaticalization cline (toGramStage), and WALS Ch 112 (toNegMorphemeType).
• NegationProfile — sibling per-language schema bundling Ch 112-115 + Greco's negIsHead + JinKoenig's enAttested. Each Fragment exposes def negationProfile : NegationProfile alongside def negationSystem: the marker-side joint is independent from the typology-feature joint.
• ofWALS112A/fromWALS113A/114A/115A/143A converters.
• countByMorphemeType/countBySymmetry sample-counting helpers (consumed by Studies/Dryer2013Negation.lean).

Theory-laden caveats

NegSymmetry and AsymmetrySubtype are WALS Ch 113/114 values ([DH13a]). [Mie05]'s richer two-dimension framework (constructional vs paradigmatic asymmetry, derived vs independent source) lives in Studies/Miestamo2005.lean because it goes beyond what WALS encodes.

Out of scope

Polarity-sensitive items (n-words, NPIs, FCIs) are NOT marker-side data; they live in Typology/PolarityItem.lean and in each language's Fragments/{Lang}/PolarityItems.lean. Cross-linguistic theorems consuming Fragment per-language data live in Studies/Dryer2013Negation.lean (Ch 112/143A/144A grounding) and Studies/Miestamo2005.lean (Ch 113-115 grounding).

Substrate enums

inductive Syntax.Negation.NegMorphemeType : Type

Type of the standard negation morpheme [Dry13].

Six categories anchored on WALS Ch 112A (negative morpheme classification). Direct projection from Data.WALS.F112A.NegativeMorphemeType via ofWALS112A; the substrate enum exists for ergonomic pattern-matching in Fragment files.

• affix : NegMorphemeType

  Negative affix on the verb (e.g., Kolyma Yukaghir el-jaqa-te-je 'NEG-achieve-FUT-1SG').

• particle : NegMorphemeType

  Free negative particle, no verbal inflection (e.g., English not, Italian non).

• auxVerb : NegMorphemeType

  Negative auxiliary verb inflecting for verbal categories (e.g., Finnish e-n 'NEG-1SG').

• wordUnclear : NegMorphemeType

  Negative word whose status as verb or particle is unclear, typically in isolating languages (e.g., Maori kaahore).

• variation : NegMorphemeType

  Language uses both negative word and negative affix in different constructions (e.g., Rama).

• doubleNeg : NegMorphemeType

  Bipartite negation: two co-occurring morphemes flanking the verb (e.g., French ne...pas, Izi to-...-du).

@[implicit_reducible]

instance Syntax.Negation.instDecidableEqNegMorphemeType : DecidableEq NegMorphemeType

Equations

• Syntax.Negation.instDecidableEqNegMorphemeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Syntax.Negation.instBEqNegMorphemeType : BEq NegMorphemeType

Equations

• Syntax.Negation.instBEqNegMorphemeType = { beq := Syntax.Negation.instBEqNegMorphemeType.beq }

def Syntax.Negation.instBEqNegMorphemeType.beq : NegMorphemeType → NegMorphemeType → Bool

Equations

• Syntax.Negation.instBEqNegMorphemeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Syntax.Negation.instReprNegMorphemeType : Repr NegMorphemeType

Equations

• Syntax.Negation.instReprNegMorphemeType = { reprPrec := Syntax.Negation.instReprNegMorphemeType.repr }

def Syntax.Negation.instReprNegMorphemeType.repr : NegMorphemeType → ℕ → Std.Format

Equations

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

inductive Syntax.Negation.NegMarkerPosition : Type

Position of the negation morpheme relative to the verb.

One-way coarsening of WALS Ch 144A's full S/O/V grid. The wals144A field on NegationSystem preserves the precise WALS classification for callers that need decoarsening.

• preverbal : NegMarkerPosition
• postverbal : NegMarkerPosition
• discontinuous : NegMarkerPosition
• morphological : NegMarkerPosition
• other : NegMarkerPosition

@[implicit_reducible]

instance Syntax.Negation.instDecidableEqNegMarkerPosition : DecidableEq NegMarkerPosition

Equations

• Syntax.Negation.instDecidableEqNegMarkerPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Negation.instBEqNegMarkerPosition.beq : NegMarkerPosition → NegMarkerPosition → Bool

Equations

• Syntax.Negation.instBEqNegMarkerPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Syntax.Negation.instBEqNegMarkerPosition : BEq NegMarkerPosition

Equations

• Syntax.Negation.instBEqNegMarkerPosition = { beq := Syntax.Negation.instBEqNegMarkerPosition.beq }

@[implicit_reducible]

instance Syntax.Negation.instReprNegMarkerPosition : Repr NegMarkerPosition

Equations

• Syntax.Negation.instReprNegMarkerPosition = { reprPrec := Syntax.Negation.instReprNegMarkerPosition.repr }

def Syntax.Negation.instReprNegMarkerPosition.repr : NegMarkerPosition → ℕ → Std.Format

Equations

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

inductive Syntax.Negation.NegSymmetry : Type

WALS Ch 113A: whether negation changes clause structure beyond adding the negative marker. Symmetric: no structural change. Asymmetric: changes in finiteness, verb paradigm, or TAM marking.

• symmetric : NegSymmetry
• asymmetric : NegSymmetry
• both : NegSymmetry

  Both symmetric and asymmetric (Type SymAsy): some constructions symmetric, others asymmetric.

@[implicit_reducible]

instance Syntax.Negation.instDecidableEqNegSymmetry : DecidableEq NegSymmetry

Equations

• Syntax.Negation.instDecidableEqNegSymmetry x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Negation.instBEqNegSymmetry.beq : NegSymmetry → NegSymmetry → Bool

Equations

• Syntax.Negation.instBEqNegSymmetry.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Syntax.Negation.instBEqNegSymmetry : BEq NegSymmetry

Equations

• Syntax.Negation.instBEqNegSymmetry = { beq := Syntax.Negation.instBEqNegSymmetry.beq }

@[implicit_reducible]

instance Syntax.Negation.instReprNegSymmetry : Repr NegSymmetry

Equations

• Syntax.Negation.instReprNegSymmetry = { reprPrec := Syntax.Negation.instReprNegSymmetry.repr }

def Syntax.Negation.instReprNegSymmetry.repr : NegSymmetry → ℕ → Std.Format

Equations

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

inductive Syntax.Negation.AsymmetrySubtype : Type

WALS Ch 114A: which grammatical domain is affected by asymmetric negation. The four primary subtypes correspond to [Mie05]'s A/Fin (finiteness), A/NonReal (reality status), A/Emph (emphasis), A/Cat (other categories) plus combined codings.

Note: WALS Ch 114 does not encode A/Emph as a separate value ([Mie05] Table 2 distinguishes it; WALS collapses it).

• finiteness : AsymmetrySubtype
• realityStatus : AsymmetrySubtype
• emphasis : AsymmetrySubtype
• otherCategories : AsymmetrySubtype
• finAndNonReal : AsymmetrySubtype
• finAndEmph : AsymmetrySubtype
• finAndCat : AsymmetrySubtype
• nonRealAndCat : AsymmetrySubtype
• emphAndCat : AsymmetrySubtype
• nonAssignable : AsymmetrySubtype

  Non-assignable: language has only symmetric negation.

@[implicit_reducible]

instance Syntax.Negation.instDecidableEqAsymmetrySubtype : DecidableEq AsymmetrySubtype

Equations

• Syntax.Negation.instDecidableEqAsymmetrySubtype x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Syntax.Negation.instBEqAsymmetrySubtype : BEq AsymmetrySubtype

Equations

• Syntax.Negation.instBEqAsymmetrySubtype = { beq := Syntax.Negation.instBEqAsymmetrySubtype.beq }

def Syntax.Negation.instBEqAsymmetrySubtype.beq : AsymmetrySubtype → AsymmetrySubtype → Bool

Equations

• Syntax.Negation.instBEqAsymmetrySubtype.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Syntax.Negation.instReprAsymmetrySubtype.repr : AsymmetrySubtype → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Negation.instReprAsymmetrySubtype : Repr AsymmetrySubtype

Equations

• Syntax.Negation.instReprAsymmetrySubtype = { reprPrec := Syntax.Negation.instReprAsymmetrySubtype.repr }

inductive Syntax.Negation.NegIndefiniteStrategy : Type

WALS Ch 115A: how negative indefinites interact with predicate negation.

• cooccur : NegIndefiniteStrategy

  Negative indefinites co-occur with predicate negation (negative concord). Dominant pattern worldwide.

• preclude : NegIndefiniteStrategy

  Negative indefinites preclude predicate negation.

• mixed : NegIndefiniteStrategy

  Mixed (position-dependent or different indefinite series).

• negExistential : NegIndefiniteStrategy

  Negative existential construction.

@[implicit_reducible]

instance Syntax.Negation.instDecidableEqNegIndefiniteStrategy : DecidableEq NegIndefiniteStrategy

Equations

• Syntax.Negation.instDecidableEqNegIndefiniteStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Negation.instBEqNegIndefiniteStrategy.beq : NegIndefiniteStrategy → NegIndefiniteStrategy → Bool

Equations

• Syntax.Negation.instBEqNegIndefiniteStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Syntax.Negation.instBEqNegIndefiniteStrategy : BEq NegIndefiniteStrategy

Equations

• Syntax.Negation.instBEqNegIndefiniteStrategy = { beq := Syntax.Negation.instBEqNegIndefiniteStrategy.beq }

def Syntax.Negation.instReprNegIndefiniteStrategy.repr : NegIndefiniteStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Negation.instReprNegIndefiniteStrategy : Repr NegIndefiniteStrategy

Equations

• Syntax.Negation.instReprNegIndefiniteStrategy = { reprPrec := Syntax.Negation.instReprNegIndefiniteStrategy.repr }

inductive Syntax.Negation.NegVerbPosition : Type

WALS Ch 143A: position of negative morpheme relative to verb. Single-negation types (NegV/VNeg/[Neg-V]/[V-Neg]) plus multi-negation types (obligatory/optional double, optional triple).

• preverbalParticle : NegVerbPosition

  Preverbal negative particle: NegV.

• postverbalParticle : NegVerbPosition

  Postverbal negative particle: VNeg.

• preverbalAffix : NegVerbPosition

  Preverbal negative affix: [Neg-V].

• postverbalAffix : NegVerbPosition

  Postverbal negative affix: [V-Neg].

• negativeTone : NegVerbPosition
• mixedSingle : NegVerbPosition
• obligDoublNeg : NegVerbPosition
• optDoubleNeg : NegVerbPosition
• tripleNeg : NegVerbPosition
• optSingleNeg : NegVerbPosition

@[implicit_reducible]

instance Syntax.Negation.instDecidableEqNegVerbPosition : DecidableEq NegVerbPosition

Equations

• Syntax.Negation.instDecidableEqNegVerbPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Syntax.Negation.instBEqNegVerbPosition : BEq NegVerbPosition

Equations

• Syntax.Negation.instBEqNegVerbPosition = { beq := Syntax.Negation.instBEqNegVerbPosition.beq }

def Syntax.Negation.instBEqNegVerbPosition.beq : NegVerbPosition → NegVerbPosition → Bool

Equations

• Syntax.Negation.instBEqNegVerbPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Syntax.Negation.instReprNegVerbPosition.repr : NegVerbPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Negation.instReprNegVerbPosition : Repr NegVerbPosition

Equations

• Syntax.Negation.instReprNegVerbPosition = { reprPrec := Syntax.Negation.instReprNegVerbPosition.repr }

inductive Syntax.Negation.NegMorphemePosition : Type

WALS Ch 143E/F: whether a language has preverbal and/or postverbal negative morphemes.

• preverbalOnly : NegMorphemePosition
• postverbalOnly : NegMorphemePosition
• preverbalAffixOnly : NegMorphemePosition
• postverbalAffixOnly : NegMorphemePosition
• both : NegMorphemePosition
• none : NegMorphemePosition

@[implicit_reducible]

instance Syntax.Negation.instDecidableEqNegMorphemePosition : DecidableEq NegMorphemePosition

Equations

• Syntax.Negation.instDecidableEqNegMorphemePosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Negation.instBEqNegMorphemePosition.beq : NegMorphemePosition → NegMorphemePosition → Bool

Equations

• Syntax.Negation.instBEqNegMorphemePosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Syntax.Negation.instBEqNegMorphemePosition : BEq NegMorphemePosition

Equations

• Syntax.Negation.instBEqNegMorphemePosition = { beq := Syntax.Negation.instBEqNegMorphemePosition.beq }

@[implicit_reducible]

instance Syntax.Negation.instReprNegMorphemePosition : Repr NegMorphemePosition

Equations

• Syntax.Negation.instReprNegMorphemePosition = { reprPrec := Syntax.Negation.instReprNegMorphemePosition.repr }

def Syntax.Negation.instReprNegMorphemePosition.repr : NegMorphemePosition → ℕ → Std.Format

Equations

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

NegMarkerEntry / NegationSystem (Fragment marker-side joint)

structure Syntax.Negation.NegMarkerEntry : Type

One language's standard sentential negation marker.

• form : String

  Surface form. For affixal negation this is an abstract citation form (e.g., Turkish -mE- for the harmony-conditioned -ma- / -me- alternants). For tonal/morphological negation use position := .morphological and document the realization in the def docstring.

• gloss : String

  Standard interlinear gloss. Defaults to the WALS-style "NEG".

• morphemeType : NegMorphemeType

  Morphological status: affix, free particle, auxiliary, etc.

• position : NegMarkerPosition

  Coarse position relative to the verb.

def Syntax.Negation.instReprNegMarkerEntry.repr : NegMarkerEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Negation.instReprNegMarkerEntry : Repr NegMarkerEntry

Equations

• Syntax.Negation.instReprNegMarkerEntry = { reprPrec := Syntax.Negation.instReprNegMarkerEntry.repr }

structure Syntax.Negation.NegationSystem : Type

A language's standard negation system.

The Fragment-side joint: every Fragments/{Lang}/Negation.lean exposes def negationSystem : NegationSystem. Multiple markers handle languages with mood/aspect/lexical-class alternation (Greek, Mandarin, Korean). Length-1 for most languages.

WALS datapoints are bundled at the system level — in WALS coding, F112A/F143A/F144A take one value per language regardless of how many markers the language has.

• markers : List NegMarkerEntry

  Standard negation marker(s). Order is editorial; Fragment files should put the unmarked / default-context marker first.

• wals112A : Option Data.WALS.F112A.NegativeMorphemeType

  WALS Ch 112A: morpheme classification. Should not be hand-encoded in Fragment files — use NegationSystem.ofISO to populate from the Data.WALS data, which is the single source of truth.

• wals143A : Option Data.WALS.F143A.NegVerbOrder

  WALS Ch 143A: NegV / VNeg / double-negation pattern. Populated by NegationSystem.ofISO.

• wals144A : Option Data.WALS.F144A.PositionOfNegativeWordWithRespectToSubjectObjectAndVerb

  WALS Ch 144A: full S/O/V positional classification. Populated by NegationSystem.ofISO.

def Syntax.Negation.instReprNegationSystem.repr : NegationSystem → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Negation.instReprNegationSystem : Repr NegationSystem

Equations

• Syntax.Negation.instReprNegationSystem = { reprPrec := Syntax.Negation.instReprNegationSystem.repr }

NegationProfile (Fragment typology-feature joint)

structure Syntax.Negation.NegationProfile : Type

A language's negation profile across WALS Chapters 112-115, plus fields from [Gre20] (negIsHead) and [JK21] (enAttested).

Sibling Fragment-side joint to NegationSystem: every Fragments/{Lang}/Negation.lean exposes def negationProfile : NegationProfile. The two joints are independent because the data partition is real: negationSystem.markers is consumed by lexical code; negationProfile is consumed by typology studies.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• morphemeType : NegMorphemeType

  Ch 112: how standard negation is expressed.

• symmetry : NegSymmetry

  Ch 113: symmetric, asymmetric, or both.

• asymmetrySubtype : AsymmetrySubtype

  Ch 114: asymmetry subtype (nonAssignable if symmetric only).

• negIndefinite : Option NegIndefiniteStrategy

  Ch 115: strategy for negative indefinites, if attested.

• negMarkers : List String

  Illustrative negative marker form(s).

• negIsHead : Option Bool

  Is the negation marker a syntactic head (X°) rather than a phrase (XP)? Relevant for [Gre20]: only head-status markers can merge in CP to produce surprise negation.

• enAttested : Option Bool

  Is expletive negation attested in this language? [JK21] (722-language survey: EN in 74 languages) and [Ret26].

def Syntax.Negation.instReprNegationProfile.repr : NegationProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Negation.instReprNegationProfile : Repr NegationProfile

Equations

• Syntax.Negation.instReprNegationProfile = { reprPrec := Syntax.Negation.instReprNegationProfile.repr }

Expletive negation triggers

structure Syntax.Negation.ENTriggerNegator : Type

An expletive-negation trigger and the negator it licenses.

Trigger classes are the [JK21] Table 5 labels (FEAR, BEFORE, UNLESS, THAN, ...). The Fragment-side joint: EN-attesting Fragments/{Lang}/Negation.lean files expose def enTriggerNegators : List ENTriggerNegator.

• triggerClass : String

  The trigger class label (from [JK21] Table 5).

• triggerForm : String

  The language's lexical trigger.

• enNegatorForm : String

  The EN negator form.

• enNegatorGloss : Option String

  Gloss for the EN negator, when it differs from standard negation.

• highEntrenchment : Option Bool

  Whether the EN use is highly entrenched (grammaticalized), when the source classifies it.

@[implicit_reducible]

instance Syntax.Negation.instReprENTriggerNegator : Repr ENTriggerNegator

Equations

• Syntax.Negation.instReprENTriggerNegator = { reprPrec := Syntax.Negation.instReprENTriggerNegator.repr }

def Syntax.Negation.instReprENTriggerNegator.repr : ENTriggerNegator → ℕ → Std.Format

Equations

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

def Syntax.Negation.instBEqENTriggerNegator.beq : ENTriggerNegator → ENTriggerNegator → Bool

Equations

• One or more equations did not get rendered due to their size.
• Syntax.Negation.instBEqENTriggerNegator.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Syntax.Negation.instBEqENTriggerNegator : BEq ENTriggerNegator

Equations

• Syntax.Negation.instBEqENTriggerNegator = { beq := Syntax.Negation.instBEqENTriggerNegator.beq }

@[implicit_reducible]

instance Syntax.Negation.instDecidableEqENTriggerNegator : DecidableEq ENTriggerNegator

Equations

• Syntax.Negation.instDecidableEqENTriggerNegator = Syntax.Negation.instDecidableEqENTriggerNegator.decEq

def Syntax.Negation.instDecidableEqENTriggerNegator.decEq (x✝ x✝¹ : ENTriggerNegator) : Decidable (x✝ = x✝¹)

Equations

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

WALS converters

def Syntax.Negation.ofWALS112A : Data.WALS.F112A.NegativeMorphemeType → NegMorphemeType

WALS Ch 112A → NegMorphemeType.

Equations

• Syntax.Negation.ofWALS112A Data.WALS.F112A.NegativeMorphemeType.negativeAffix = Syntax.Negation.NegMorphemeType.affix
• Syntax.Negation.ofWALS112A Data.WALS.F112A.NegativeMorphemeType.negativeParticle = Syntax.Negation.NegMorphemeType.particle
• Syntax.Negation.ofWALS112A Data.WALS.F112A.NegativeMorphemeType.negativeAuxiliaryVerb = Syntax.Negation.NegMorphemeType.auxVerb
• Syntax.Negation.ofWALS112A Data.WALS.F112A.NegativeMorphemeType.negativeWordUnclearIfVerbOrParticle = Syntax.Negation.NegMorphemeType.wordUnclear
• Syntax.Negation.ofWALS112A Data.WALS.F112A.NegativeMorphemeType.variationBetweenNegativeWordAndAffix = Syntax.Negation.NegMorphemeType.variation
• Syntax.Negation.ofWALS112A Data.WALS.F112A.NegativeMorphemeType.doubleNegation = Syntax.Negation.NegMorphemeType.doubleNeg

def Syntax.Negation.fromWALS113A : Data.WALS.F113A.NegationSymmetry → NegSymmetry

WALS Ch 113A → NegSymmetry.

Equations

• Syntax.Negation.fromWALS113A Data.WALS.F113A.NegationSymmetry.symmetric = Syntax.Negation.NegSymmetry.symmetric
• Syntax.Negation.fromWALS113A Data.WALS.F113A.NegationSymmetry.asymmetric = Syntax.Negation.NegSymmetry.asymmetric
• Syntax.Negation.fromWALS113A Data.WALS.F113A.NegationSymmetry.both = Syntax.Negation.NegSymmetry.both

def Syntax.Negation.fromWALS114A : Data.WALS.F114A.AsymmetricNegationSubtype → AsymmetrySubtype

WALS Ch 114A → AsymmetrySubtype.

Equations

• Syntax.Negation.fromWALS114A Data.WALS.F114A.AsymmetricNegationSubtype.aFin = Syntax.Negation.AsymmetrySubtype.finiteness
• Syntax.Negation.fromWALS114A Data.WALS.F114A.AsymmetricNegationSubtype.aNonreal = Syntax.Negation.AsymmetrySubtype.realityStatus
• Syntax.Negation.fromWALS114A Data.WALS.F114A.AsymmetricNegationSubtype.aCat = Syntax.Negation.AsymmetrySubtype.otherCategories
• Syntax.Negation.fromWALS114A Data.WALS.F114A.AsymmetricNegationSubtype.aFinAndANonreal = Syntax.Negation.AsymmetrySubtype.finAndNonReal
• Syntax.Negation.fromWALS114A Data.WALS.F114A.AsymmetricNegationSubtype.aFinAndACat = Syntax.Negation.AsymmetrySubtype.finAndCat
• Syntax.Negation.fromWALS114A Data.WALS.F114A.AsymmetricNegationSubtype.aNonrealAndACat = Syntax.Negation.AsymmetrySubtype.nonRealAndCat
• Syntax.Negation.fromWALS114A Data.WALS.F114A.AsymmetricNegationSubtype.nonAssignable = Syntax.Negation.AsymmetrySubtype.nonAssignable

def Syntax.Negation.fromWALS115A : Data.WALS.F115A.NegativeIndefiniteType → NegIndefiniteStrategy

WALS Ch 115A → NegIndefiniteStrategy.

Equations

• Syntax.Negation.fromWALS115A Data.WALS.F115A.NegativeIndefiniteType.predicateNegationAlsoPresent = Syntax.Negation.NegIndefiniteStrategy.cooccur
• Syntax.Negation.fromWALS115A Data.WALS.F115A.NegativeIndefiniteType.noPredicateNegation = Syntax.Negation.NegIndefiniteStrategy.preclude
• Syntax.Negation.fromWALS115A Data.WALS.F115A.NegativeIndefiniteType.mixedBehaviour = Syntax.Negation.NegIndefiniteStrategy.mixed
• Syntax.Negation.fromWALS115A Data.WALS.F115A.NegativeIndefiniteType.negativeExistentialConstruction = Syntax.Negation.NegIndefiniteStrategy.negExistential

def Syntax.Negation.fromWALS143A : Data.WALS.F143A.NegVerbOrder → NegVerbPosition

WALS Ch 143A → NegVerbPosition.

Equations

• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.negv = Syntax.Negation.NegVerbPosition.preverbalParticle
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.vneg = Syntax.Negation.NegVerbPosition.postverbalParticle
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.negV = Syntax.Negation.NegVerbPosition.preverbalAffix
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.vNeg = Syntax.Negation.NegVerbPosition.postverbalAffix
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.negativeTone = Syntax.Negation.NegVerbPosition.negativeTone
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.type1Type2 = Syntax.Negation.NegVerbPosition.mixedSingle
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.type1Type3 = Syntax.Negation.NegVerbPosition.mixedSingle
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.type1Type4 = Syntax.Negation.NegVerbPosition.mixedSingle
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.type2Type3 = Syntax.Negation.NegVerbPosition.mixedSingle
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.type2Type4 = Syntax.Negation.NegVerbPosition.mixedSingle
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.type3Type4 = Syntax.Negation.NegVerbPosition.mixedSingle
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.type3NegativeInfix = Syntax.Negation.NegVerbPosition.mixedSingle
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.optsingleneg = Syntax.Negation.NegVerbPosition.optSingleNeg
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.obligdoubleneg = Syntax.Negation.NegVerbPosition.obligDoublNeg
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.optdoubleneg = Syntax.Negation.NegVerbPosition.optDoubleNeg
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.opttriplenegObligdoubleneg = Syntax.Negation.NegVerbPosition.tripleNeg
• Syntax.Negation.fromWALS143A Data.WALS.F143A.NegVerbOrder.opttriplenegOptdoubleneg = Syntax.Negation.NegVerbPosition.tripleNeg

def Syntax.Negation.NegationSystem.ofISO (iso : String) (markers : List NegMarkerEntry) : NegationSystem

Build a NegationSystem for a language identified by ISO 639-3 code, pulling F112A / F143A / F144A values from the Data.WALS data.

Equations

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

NegationProfile helpers (Fragment-consumed)

def Syntax.Negation.NegationProfile.hasMorphemeType (p : NegationProfile) (t : NegMorphemeType) : Bool

Does a language use a given morpheme type?

Equations

• p.hasMorphemeType t = (p.morphemeType == t)

def Syntax.Negation.NegationProfile.hasSymmetric (p : NegationProfile) : Bool

Does a language have symmetric negation (either symmetric only or both)?

Equations

• p.hasSymmetric = (p.symmetry == Syntax.Negation.NegSymmetry.symmetric || p.symmetry == Syntax.Negation.NegSymmetry.both)

def Syntax.Negation.NegationProfile.hasAsymmetric (p : NegationProfile) : Bool

Does a language have asymmetric negation (either asymmetric only or both)?

Equations

• p.hasAsymmetric = (p.symmetry == Syntax.Negation.NegSymmetry.asymmetric || p.symmetry == Syntax.Negation.NegSymmetry.both)

def Syntax.Negation.NegationProfile.hasNegConcord (p : NegationProfile) : Bool

Does a language show negative concord?

Equations

• p.hasNegConcord = (p.negIndefinite == some Syntax.Negation.NegIndefiniteStrategy.cooccur)

def Syntax.Negation.countByMorphemeType (langs : List NegationProfile) (t : NegMorphemeType) : ℕ

Count of languages in a sample with a given morpheme type.

Equations

• Syntax.Negation.countByMorphemeType langs t = (List.filter (fun (x : Syntax.Negation.NegationProfile) => x.hasMorphemeType t) langs).length

def Syntax.Negation.countBySymmetry (langs : List NegationProfile) (s : NegSymmetry) : ℕ

Count of languages in a sample with a given symmetry type.

Equations

• Syntax.Negation.countBySymmetry langs s = (List.filter (fun (x : Syntax.Negation.NegationProfile) => x.symmetry == s) langs).length

Negation strategy and the AVC bridge

[And06a] [Hei93] [Mie05]

Some languages express sentential negation through a negative auxiliary verb that hosts inflection (tense, agreement) while the lexical verb appears in a nonfinite form (Finnish ei mene 'NEG.3SG go') — a special case of the aux-headed AVC pattern of AuxiliaryVerbs. NegStrategy classifies negation strategies at this AVC-relevant grain and bridges them to Anderson's inflectional patterns, Heine's grammaticalization cline, and the WALS Ch 112 morpheme typology.

inductive Syntax.Negation.NegStrategy : Type

Strategy for expressing sentential negation.

• negVerb : NegStrategy

  Negative auxiliary verb that inflects (Finnish ei, Komi oz).

• negAffix : NegStrategy

  Bound negative morpheme (e.g., Turkish -mE-).

• negParticle : NegStrategy

  Free negative particle (English not, Italian non).

@[implicit_reducible]

instance Syntax.Negation.instDecidableEqNegStrategy : DecidableEq NegStrategy

Equations

• Syntax.Negation.instDecidableEqNegStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Negation.instReprNegStrategy.repr : NegStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Negation.instReprNegStrategy : Repr NegStrategy

Equations

• Syntax.Negation.instReprNegStrategy = { reprPrec := Syntax.Negation.instReprNegStrategy.repr }

def Syntax.Negation.NegStrategy.expectedInflPattern : NegStrategy → Option AuxiliaryVerbs.InflPattern

A negative verb creates an AVC and therefore has an expected inflectional pattern: aux-headed (the neg verb hosts inflection). Affixes and particles do not create AVCs.

Equations

• Syntax.Negation.NegStrategy.negVerb.expectedInflPattern = some AuxiliaryVerbs.InflPattern.auxHeaded
• Syntax.Negation.NegStrategy.negAffix.expectedInflPattern = none
• Syntax.Negation.NegStrategy.negParticle.expectedInflPattern = none

def Syntax.Negation.NegStrategy.isVerbal : NegStrategy → Bool

Is this strategy verbal (i.e., does it create an AVC)?

Equations

• Syntax.Negation.NegStrategy.negVerb.isVerbal = true
• x✝.isVerbal = false

def Syntax.Negation.NegStrategy.toGramStage : NegStrategy → Option Grammaticalization.GramStage

Project a negation strategy onto its grammaticalization-cline stage ([Hei93], [And06a] ch. 7). A negative verb (Finnish ei, Komi oz) sits at the auxiliary stage; a negative affix (bound morpheme) is one stage further along the cline. A free negative particle (English not, Italian non) is not on the verbal cline at all — particles are not bleached verbs and don't have a "stage" of grammaticalization in Heine's/Anderson's verbal sense. Returning none for .negParticle rather than collapsing it onto .auxiliary (an earlier formaliser shorthand) preserves [Mie05]'s particle-vs-verb morphological distinction; the cross-framework equivalence theorem auxiliary_stage_iff_aux_verb_morpheme in Studies/Anderson2006.lean makes the Anderson-cline / Miestamo-morpheme-type agreement Lean-checkable.

Equations

• Syntax.Negation.NegStrategy.negVerb.toGramStage = some Grammaticalization.GramStage.auxiliary
• Syntax.Negation.NegStrategy.negAffix.toGramStage = some Grammaticalization.GramStage.affix
• Syntax.Negation.NegStrategy.negParticle.toGramStage = none

def Syntax.Negation.NegStrategy.toNegMorphemeType : NegStrategy → NegMorphemeType

Map from AVC-oriented NegStrategy to WALS-oriented NegMorphemeType: both classify the morphological status of the negative marker.

Equations

• Syntax.Negation.NegStrategy.negVerb.toNegMorphemeType = Syntax.Negation.NegMorphemeType.auxVerb
• Syntax.Negation.NegStrategy.negAffix.toNegMorphemeType = Syntax.Negation.NegMorphemeType.affix
• Syntax.Negation.NegStrategy.negParticle.toNegMorphemeType = Syntax.Negation.NegMorphemeType.particle