Documentation

Linglib.Core.Morphology.MorphProfile

Morphological Profile Types #

Framework-agnostic types for cross-linguistic morphological typology, grounding functions from WALS data, and the MorphProfile structure.

Types correspond to WALS chapters 20--29 plus supplementary chapters (21B, 62A, 79A/B, 80A). Grounding functions map WALS auto-generated data to these coarser local classifications.

inductive Core.Morphology.Fusion :

WALS Ch 20: How inflectional formatives are attached to stems.

Note: this captures fusion only — the degree of phonological boundedness between formative and stem. The traditional labels "agglutinating" and "fusional" conflate fusion with flexivity (see Flexivity below). Both concatenative + nonflexive (Turkish) and concatenative + flexive (Russian) map to .concatenative here. @cite{bickel-nichols-2001}

isolating : Fusion
concatenative : Fusion
nonlinear : Fusion

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqFusion :

DecidableEq Fusion

Equations

Core.Morphology.instDecidableEqFusion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instReprFusion :

Equations

Core.Morphology.instReprFusion = { reprPrec := Core.Morphology.instReprFusion.repr }

def Core.Morphology.instReprFusion.repr :

Fusion → Nat → Std.Format

Equations

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

Instances For

inductive Core.Morphology.Flexivity :

Whether inflectional formatives show item-based allomorphic variation.

@cite{bickel-nichols-2001} argue this is the crucial parameter that the traditional typology conflates with fusion:

nonflexive ("agglutinating"): formatives have invariant or rule-governed shape (Turkish -ler ~ -lar is vowel-harmony, not item-based allomorphy)
flexive ("fusional"): formatives vary unpredictably by inflectional class (Latin -ī ~~-ae~~ -ūs for genitive singular depending on declension class)

Orthogonal to Fusion: a language can be concatenative + nonflexive (Turkish), concatenative + flexive (Russian), nonlinear + flexive (Arabic), or isolating (flexivity N/A).

nonflexive : Flexivity
flexive : Flexivity

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqFlexivity :

DecidableEq Flexivity

Equations

Core.Morphology.instDecidableEqFlexivity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instReprFlexivity :

Equations

Core.Morphology.instReprFlexivity = { reprPrec := Core.Morphology.instReprFlexivity.repr }

def Core.Morphology.instReprFlexivity.repr :

Flexivity → Nat → Std.Format

Equations

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

Instances For

inductive Core.Morphology.Exponence :

WALS Ch 21: How many grammatical categories a single case formative expresses. Specifically about case formatives and whether they bundle number, TAM, etc.

Distinct from ExponenceScope (B&N's broader cumulative/separative parameter which applies to all morphological categories, not just case). @cite{bickel-nichols-2001}

monoexponential : Exponence
polyexponential : Exponence
noCase : Exponence

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqExponence :

DecidableEq Exponence

Equations

Core.Morphology.instDecidableEqExponence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprExponence.repr :

Exponence → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprExponence :

Equations

Core.Morphology.instReprExponence = { reprPrec := Core.Morphology.instReprExponence.repr }

inductive Core.Morphology.ExponenceScope :

Whether a single formative expresses multiple grammatical categories simultaneously (cumulative) or each formative expresses exactly one category (separative).

@cite{bickel-nichols-2001}: this is a general morphological parameter applying across all category pairs, not limited to case+number (cf. WALS Ch 21 Exponence). Latin -ō (1sg.pres.act.ind) is cumulative; Turkish verb suffixes are separative (each suffix = one category).

cumulative : ExponenceScope
separative : ExponenceScope

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqExponenceScope :

DecidableEq ExponenceScope

Equations

Core.Morphology.instDecidableEqExponenceScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instReprExponenceScope :

Repr ExponenceScope

Equations

Core.Morphology.instReprExponenceScope = { reprPrec := Core.Morphology.instReprExponenceScope.repr }

def Core.Morphology.instReprExponenceScope.repr :

ExponenceScope → Nat → Std.Format

Equations

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

Instances For

inductive Core.Morphology.VerbSynthesis :

WALS Ch 22: How many inflectional categories are expressed on the verb.

low : VerbSynthesis
moderate : VerbSynthesis
high : VerbSynthesis

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqVerbSynthesis :

DecidableEq VerbSynthesis

Equations

Core.Morphology.instDecidableEqVerbSynthesis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprVerbSynthesis.repr :

VerbSynthesis → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprVerbSynthesis :

Repr VerbSynthesis

Equations

Core.Morphology.instReprVerbSynthesis = { reprPrec := Core.Morphology.instReprVerbSynthesis.repr }

inductive Core.Morphology.LocusOfMarking :

Locus of marking: where grammatical relations are marked. Derived from WALS Ch 25A @cite{nichols-bickel-2013a}.

headMarking : LocusOfMarking
dependentMarking : LocusOfMarking
doubleMarking : LocusOfMarking
zeroMarking : LocusOfMarking
inconsistentOrOther : LocusOfMarking

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqLocusOfMarking :

DecidableEq LocusOfMarking

Equations

Core.Morphology.instDecidableEqLocusOfMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprLocusOfMarking.repr :

LocusOfMarking → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprLocusOfMarking :

Repr LocusOfMarking

Equations

Core.Morphology.instReprLocusOfMarking = { reprPrec := Core.Morphology.instReprLocusOfMarking.repr }

inductive Core.Morphology.PrefixSuffix :

WALS Ch 26: Whether a language predominantly uses prefixes or suffixes.

stronglySuffixing : PrefixSuffix
weaklySuffixing : PrefixSuffix
equalPrefixSuffix : PrefixSuffix
weaklyPrefixing : PrefixSuffix
stronglyPrefixing : PrefixSuffix
littleAffixation : PrefixSuffix

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqPrefixSuffix :

DecidableEq PrefixSuffix

Equations

Core.Morphology.instDecidableEqPrefixSuffix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instReprPrefixSuffix :

Repr PrefixSuffix

Equations

Core.Morphology.instReprPrefixSuffix = { reprPrec := Core.Morphology.instReprPrefixSuffix.repr }

def Core.Morphology.instReprPrefixSuffix.repr :

PrefixSuffix → Nat → Std.Format

Equations

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

Instances For

inductive Core.Morphology.Reduplication :

WALS Ch 27: Whether the language has productive reduplication.

productiveFull : Reduplication
fullOnly : Reduplication
noProductive : Reduplication

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqReduplication :

DecidableEq Reduplication

Equations

Core.Morphology.instDecidableEqReduplication x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprReduplication.repr :

Reduplication → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprReduplication :

Repr Reduplication

Equations

Core.Morphology.instReprReduplication = { reprPrec := Core.Morphology.instReprReduplication.repr }

inductive Core.Morphology.LocusClause :

WALS Ch 23: Where grammatical relations are marked in clausal syntax. @cite{nichols-bickel-2013b}

headMarking : LocusClause
dependentMarking : LocusClause
doubleMarking : LocusClause
noMarking : LocusClause
other : LocusClause

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqLocusClause :

DecidableEq LocusClause

Equations

Core.Morphology.instDecidableEqLocusClause x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instReprLocusClause :

Repr LocusClause

Equations

Core.Morphology.instReprLocusClause = { reprPrec := Core.Morphology.instReprLocusClause.repr }

def Core.Morphology.instReprLocusClause.repr :

LocusClause → Nat → Std.Format

Equations

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

Instances For

inductive Core.Morphology.LocusPossessive :

WALS Ch 24: Where grammatical relations are marked in possessive NPs. @cite{nichols-bickel-2013c}

headMarking : LocusPossessive
dependentMarking : LocusPossessive
doubleMarking : LocusPossessive
noMarking : LocusPossessive
other : LocusPossessive

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqLocusPossessive :

DecidableEq LocusPossessive

Equations

Core.Morphology.instDecidableEqLocusPossessive x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instReprLocusPossessive :

Repr LocusPossessive

Equations

Core.Morphology.instReprLocusPossessive = { reprPrec := Core.Morphology.instReprLocusPossessive.repr }

def Core.Morphology.instReprLocusPossessive.repr :

LocusPossessive → Nat → Std.Format

Equations

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

Instances For

inductive Core.Morphology.WholeLanguageMarking :

WALS Ch 25A: Whole-language locus-of-marking classification. @cite{nichols-bickel-2013a}

headMarking : WholeLanguageMarking
dependentMarking : WholeLanguageMarking
doubleMarking : WholeLanguageMarking
zeroMarking : WholeLanguageMarking
inconsistentOrOther : WholeLanguageMarking

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqWholeLanguageMarking :

DecidableEq WholeLanguageMarking

Equations

Core.Morphology.instDecidableEqWholeLanguageMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprWholeLanguageMarking.repr :

WholeLanguageMarking → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprWholeLanguageMarking :

Repr WholeLanguageMarking

Equations

Core.Morphology.instReprWholeLanguageMarking = { reprPrec := Core.Morphology.instReprWholeLanguageMarking.repr }

inductive Core.Morphology.ZeroMarkingAP :

WALS Ch 25B: Whether A and P arguments are zero-marked. @cite{nichols-bickel-2013d}

zeroMarking : ZeroMarkingAP
nonZeroMarking : ZeroMarkingAP

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqZeroMarkingAP :

DecidableEq ZeroMarkingAP

Equations

Core.Morphology.instDecidableEqZeroMarkingAP x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprZeroMarkingAP.repr :

ZeroMarkingAP → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprZeroMarkingAP :

Repr ZeroMarkingAP

Equations

Core.Morphology.instReprZeroMarkingAP = { reprPrec := Core.Morphology.instReprZeroMarkingAP.repr }

inductive Core.Morphology.CaseSyncretism :

WALS Ch 28: Whether a language exhibits case syncretism.

noCaseMarking : CaseSyncretism
coreCasesOnly : CaseSyncretism
coreAndNonCore : CaseSyncretism
noSyncretism : CaseSyncretism

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqCaseSyncretism :

DecidableEq CaseSyncretism

Equations

Core.Morphology.instDecidableEqCaseSyncretism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instReprCaseSyncretism :

Repr CaseSyncretism

Equations

Core.Morphology.instReprCaseSyncretism = { reprPrec := Core.Morphology.instReprCaseSyncretism.repr }

def Core.Morphology.instReprCaseSyncretism.repr :

CaseSyncretism → Nat → Std.Format

Equations

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

Instances For

inductive Core.Morphology.VerbalSyncretism :

WALS Ch 29: Whether a language exhibits syncretism in verbal person/number.

noSubjectMarking : VerbalSyncretism
syncretic : VerbalSyncretism
notSyncretic : VerbalSyncretism

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqVerbalSyncretism :

DecidableEq VerbalSyncretism

Equations

Core.Morphology.instDecidableEqVerbalSyncretism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instReprVerbalSyncretism :

Repr VerbalSyncretism

Equations

Core.Morphology.instReprVerbalSyncretism = { reprPrec := Core.Morphology.instReprVerbalSyncretism.repr }

def Core.Morphology.instReprVerbalSyncretism.repr :

VerbalSyncretism → Nat → Std.Format

Equations

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

Instances For

inductive Core.Morphology.TAMExponence :

WALS Ch 21B: What categories co-occur with TAM in a single formative.

monoexponential : TAMExponence
tamAgreement : TAMExponence
tamAgreementDiathesis : TAMExponence
tamAgreementConstruct : TAMExponence
tamPolarity : TAMExponence
noTam : TAMExponence

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqTAMExponence :

DecidableEq TAMExponence

Equations

Core.Morphology.instDecidableEqTAMExponence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprTAMExponence.repr :

TAMExponence → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprTAMExponence :

Repr TAMExponence

Equations

Core.Morphology.instReprTAMExponence = { reprPrec := Core.Morphology.instReprTAMExponence.repr }

inductive Core.Morphology.ActionNominal :

WALS Ch 62: How a language constructs action nominals.

sentential : ActionNominal
possessiveAccusative : ActionNominal
ergativePossessive : ActionNominal
doublePossessive : ActionNominal
other : ActionNominal
mixed : ActionNominal
restricted : ActionNominal
noActionNominals : ActionNominal

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqActionNominal :

DecidableEq ActionNominal

Equations

Core.Morphology.instDecidableEqActionNominal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprActionNominal.repr :

ActionNominal → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprActionNominal :

Repr ActionNominal

Equations

Core.Morphology.instReprActionNominal = { reprPrec := Core.Morphology.instReprActionNominal.repr }

inductive Core.Morphology.SuppletionTA :

WALS Ch 79A: Whether suppletion is conditioned by tense, aspect, or both.

tense : SuppletionTA
aspect : SuppletionTA
tenseAndAspect : SuppletionTA
none : SuppletionTA

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqSuppletionTA :

DecidableEq SuppletionTA

Equations

Core.Morphology.instDecidableEqSuppletionTA x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprSuppletionTA.repr :

SuppletionTA → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprSuppletionTA :

Repr SuppletionTA

Equations

Core.Morphology.instReprSuppletionTA = { reprPrec := Core.Morphology.instReprSuppletionTA.repr }

inductive Core.Morphology.SuppletionImperative :

WALS Ch 79B: Whether a language has suppletive imperatives/hortatives.

alternating : SuppletionImperative
imperative : SuppletionImperative
hortative : SuppletionImperative
imperativeAndHortative : SuppletionImperative
none : SuppletionImperative

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqSuppletionImperative :

DecidableEq SuppletionImperative

Equations

Core.Morphology.instDecidableEqSuppletionImperative x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instReprSuppletionImperative :

Repr SuppletionImperative

Equations

Core.Morphology.instReprSuppletionImperative = { reprPrec := Core.Morphology.instReprSuppletionImperative.repr }

def Core.Morphology.instReprSuppletionImperative.repr :

SuppletionImperative → Nat → Std.Format

Equations

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

Instances For

inductive Core.Morphology.VerbalNumber :

WALS Ch 80A: Whether a language has verbal number marking.

none : VerbalNumber
pairsNoSuppletion : VerbalNumber
pairsSuppletion : VerbalNumber
triplesNoSuppletion : VerbalNumber
triplesSuppletion : VerbalNumber

Instances For

@[implicit_reducible]

instance Core.Morphology.instDecidableEqVerbalNumber :

DecidableEq VerbalNumber

Equations

Core.Morphology.instDecidableEqVerbalNumber x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.instReprVerbalNumber.repr :

VerbalNumber → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprVerbalNumber :

Repr VerbalNumber

Equations

Core.Morphology.instReprVerbalNumber = { reprPrec := Core.Morphology.instReprVerbalNumber.repr }

structure Core.Morphology.MorphProfile :

A language's morphological profile, combining dimensions from WALS Chapters 20--29 plus supplementary chapters. Required fields are derived from WALS where possible; optional fields are populated when the language appears in the relevant WALS chapter.

language : String
iso : String
fusion : Fusion
Ch 20: Fusion type
exponence : Exponence
Ch 21: Exponence type
verbSynthesis : VerbSynthesis
Ch 22: Inflectional synthesis of the verb
locus : LocusOfMarking
Locus of marking (derived from Ch 23 clause-level; fallback for absent languages)
prefixSuffix : PrefixSuffix
Ch 26: Prefixing vs suffixing
reduplication : Reduplication
Ch 27: Productive reduplication
locusClause : Option LocusClause
Ch 23: Locus of marking in the clause (optional)
locusPossessive : Option LocusPossessive
Ch 24: Locus of marking in possessive NP (optional)
wholeLanguageMarking : Option WholeLanguageMarking
Ch 25A: Whole-language marking typology (optional)
zeroMarkingAP : Option ZeroMarkingAP
Ch 25B: Zero marking of A and P arguments (optional)
caseSyncretism : Option CaseSyncretism
Ch 28: Case syncretism (optional)
verbalSyncretism : Option VerbalSyncretism
Ch 29: Syncretism in verbal person/number marking (optional)
tamExponence : Option TAMExponence
Ch 21B: Exponence of TAM inflection (optional)
actionNominal : Option ActionNominal
Ch 62A: Action nominal constructions (optional)
suppletionTA : Option SuppletionTA
Ch 79A: Suppletion according to tense and aspect (optional)
suppletionImperative : Option SuppletionImperative
Ch 79B: Suppletion in imperatives and hortatives (optional)
verbalNumber : Option VerbalNumber
Ch 80A: Verbal number and suppletion (optional)
flexivity : Option Flexivity
@cite{bickel-nichols-2001}: Flexivity — whether inflectional formatives show item-based allomorphic variation (flexive) or are phonologically invariant (nonflexive). Orthogonal to fusion. Not derivable from WALS.
bnExponence : Option ExponenceScope
@cite{bickel-nichols-2001}: Exponence scope — whether single formatives bundle multiple categories (cumulative) or each expresses one (separative). Broader than WALS Ch 21 exponence (which is case-specific).

Instances For

def Core.Morphology.instReprMorphProfile.repr :

MorphProfile → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Morphology.instReprMorphProfile :

Repr MorphProfile

Equations

Core.Morphology.instReprMorphProfile = { reprPrec := Core.Morphology.instReprMorphProfile.repr }

@[implicit_reducible]

instance Core.Morphology.instDecidableEqMorphProfile :

DecidableEq MorphProfile

Equations

Core.Morphology.instDecidableEqMorphProfile = Core.Morphology.instDecidableEqMorphProfile.decEq

def Core.Morphology.instDecidableEqMorphProfile.decEq (x✝ x✝¹ : MorphProfile) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Core.Morphology.fromWALS20A :

Data.WALS.F20A.FusionType → Option Fusion

Convert WALS 20A fusion type to the local three-way Fusion classification. Returns none for mixed categories that do not map cleanly.

Equations

Instances For

def Core.Morphology.fromWALS21A :

Data.WALS.F21A.ExponenceType → Option Exponence

Convert WALS 21A exponence type to the local Exponence classification. Returns none for noCase (no information about overall exponence).

Equations

Instances For

def Core.Morphology.fromWALS22A :

Data.WALS.F22A.InflectionalSynthesis → VerbSynthesis

Convert WALS 22A inflectional synthesis to the local three-way classification.

Equations

Instances For

def Core.Morphology.fromWALS26A :

Data.WALS.F26A.PrefixSuffixPreference → PrefixSuffix

Equations

Instances For

def Core.Morphology.fromWALS27A :

Data.WALS.F27A.ReduplicationType → Reduplication

Equations

Instances For

def Core.Morphology.fromWALS23A :

Data.WALS.F23A.LocusOfMarkingInTheClause → LocusClause

Equations

Instances For

def Core.Morphology.fromWALS24A :

Data.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases → LocusPossessive

Equations

Instances For

def Core.Morphology.fromWALS25A :

Data.WALS.F25A.LocusOfMarkingWholeLanguageTypology → WholeLanguageMarking

Equations

Instances For

def Core.Morphology.fromWALS25B :

Data.WALS.F25B.ZeroMarkingOfAAndPArguments → ZeroMarkingAP

Equations

Instances For

def Core.Morphology.fromWALS28A :

Data.WALS.F28A.CaseSyncretism → CaseSyncretism

Equations

Instances For

def Core.Morphology.fromWALS29A :

Data.WALS.F29A.SyncretismInVerbalPersonNumberMarking → VerbalSyncretism

Equations

Instances For

def Core.Morphology.fromWALS21B :

Data.WALS.F21B.ExponenceOfTenseAspectMoodInflection → TAMExponence

Equations

Instances For

def Core.Morphology.fromWALS62A :

Data.WALS.F62A.ActionNominalConstructions → ActionNominal

Equations

Instances For

def Core.Morphology.fromWALS79A :

Data.WALS.F79A.SuppletionAccordingToTenseAndAspect → SuppletionTA

Equations

Instances For

def Core.Morphology.fromWALS79B :

Data.WALS.F79B.SuppletionInImperativesAndHortatives → SuppletionImperative

Equations

Instances For

def Core.Morphology.fromWALS80A :

Data.WALS.F80A.VerbalNumberAndSuppletion → VerbalNumber

Equations

Instances For

def Core.Morphology.locusClauseToLocus :

LocusClause → LocusOfMarking

Map clause-level locus (F23A) to the 5-way whole-language classification.

Equations

Instances For

WALS lookup helpers derive MorphProfile field values from auto-generated WALS data. Each returns Option, yielding none when the language is absent from that chapter or the grounding function is uninformative. Profile definitions use .getD fallback so the fallback is only reached when WALS cannot help.

def Core.Morphology.walsFusion (iso : String) :

Option Fusion

Equations

Core.Morphology.walsFusion iso = (Data.WALS.F20A.lookupISO iso).bind fun (x : Data.WALS.Datapoint Data.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value

Instances For

def Core.Morphology.walsExponence (iso : String) :

Option Exponence

Equations

Core.Morphology.walsExponence iso = (Data.WALS.F21A.lookupISO iso).bind fun (x : Data.WALS.Datapoint Data.WALS.F21A.ExponenceType) => Core.Morphology.fromWALS21A x.value

Instances For

def Core.Morphology.walsVerbSynthesis (iso : String) :

Option VerbSynthesis

Equations

Core.Morphology.walsVerbSynthesis iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Data.WALS.F22A.lookupISO iso)

Instances For

def Core.Morphology.walsLocus (iso : String) :

Option LocusOfMarking

Equations

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

Instances For

def Core.Morphology.walsPrefixSuffix (iso : String) :

Option PrefixSuffix

Equations

Core.Morphology.walsPrefixSuffix iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Data.WALS.F26A.lookupISO iso)

Instances For

def Core.Morphology.walsReduplication (iso : String) :

Option Reduplication

Equations

Core.Morphology.walsReduplication iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F27A.ReduplicationType) => Core.Morphology.fromWALS27A x.value) (Data.WALS.F27A.lookupISO iso)

Instances For

def Core.Morphology.walsLocusClause (iso : String) :

Option LocusClause

Equations

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

Instances For

def Core.Morphology.walsLocusPossessive (iso : String) :

Option LocusPossessive

Equations

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

Instances For

def Core.Morphology.walsWholeLanguageMarking (iso : String) :

Option WholeLanguageMarking

Equations

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

Instances For

def Core.Morphology.walsZeroMarkingAP (iso : String) :

Option ZeroMarkingAP

Equations

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

Instances For

def Core.Morphology.walsCaseSyncretism (iso : String) :

Option CaseSyncretism

Equations

Core.Morphology.walsCaseSyncretism iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Data.WALS.F28A.lookupISO iso)

Instances For

def Core.Morphology.walsVerbalSyncretism (iso : String) :

Option VerbalSyncretism

Equations

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

Instances For

def Core.Morphology.walsTAMExponence (iso : String) :

Option TAMExponence

Equations

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

Instances For

def Core.Morphology.walsActionNominal (iso : String) :

Option ActionNominal

Equations

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

Instances For

def Core.Morphology.walsSuppletionTA (iso : String) :

Option SuppletionTA

Equations

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

Instances For

def Core.Morphology.walsSuppletionImperative (iso : String) :

Option SuppletionImperative

Equations

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

Instances For

def Core.Morphology.walsVerbalNumber (iso : String) :

Option VerbalNumber

Equations

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

Instances For

def Core.Morphology.MorphProfile.fromWALS (language iso : String) (fusionFb : Fusion) (exponenceFb : Exponence) (verbSynthesisFb : VerbSynthesis) (locusFb : LocusOfMarking) (prefixSuffixFb : PrefixSuffix) (reduplicationFb : Reduplication) (flexivity : Option Flexivity := none) (bnExponence : Option ExponenceScope := none) :

Build a MorphProfile from an ISO 639-3 code via WALS lookups.

Required-field fallbacks (fusionFb, exponenceFb, …) must be supplied for the six WALS chapters where the lookup may return none (language absent from chapter, or grounding function uninformative — e.g. WALS 20A isolatingConcatenative does not map cleanly to the local 3-way Fusion enum and yields none). When WALS has data the lookup wins; the fallback is exercised only when WALS is silent.

Optional WALS fields (locusClause, locusPossessive, …) auto-populate from their lookup helpers and remain none if absent.

The B&N 2001 parameters flexivity and bnExponence are NOT derivable from any WALS chapter — they are paper-stipulated per @cite{bickel-nichols-2001} and must be passed explicitly when known.

Equations

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

Instances For

Mathlib-style Prop-typed predicates with Decidable instances and @[simp] _iff lemmas. Filter sites that need Bool should call decide at the boundary. The _iff lemmas are Iff.rfl (unfolding- only) but make the decomposition visible to simp and to mathlib- pattern decidable_of_iff derivations.

def Core.Morphology.MorphProfile.IsConcatenative (p : MorphProfile) :

Equations

p.IsConcatenative = (p.fusion = Core.Morphology.Fusion.concatenative)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isConcatenative_iff (p : MorphProfile) :

p.IsConcatenative ↔ p.fusion = Fusion.concatenative

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsConcatenative :

DecidablePred IsConcatenative

Equations

p.instDecidablePredIsConcatenative = decidable_of_iff (p.fusion = Core.Morphology.Fusion.concatenative) ⋯

def Core.Morphology.MorphProfile.IsIsolating (p : MorphProfile) :

Equations

p.IsIsolating = (p.fusion = Core.Morphology.Fusion.isolating)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isIsolating_iff (p : MorphProfile) :

p.IsIsolating ↔ p.fusion = Fusion.isolating

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsIsolating :

DecidablePred IsIsolating

Equations

p.instDecidablePredIsIsolating = decidable_of_iff (p.fusion = Core.Morphology.Fusion.isolating) ⋯

def Core.Morphology.MorphProfile.IsNonlinear (p : MorphProfile) :

Equations

p.IsNonlinear = (p.fusion = Core.Morphology.Fusion.nonlinear)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isNonlinear_iff (p : MorphProfile) :

p.IsNonlinear ↔ p.fusion = Fusion.nonlinear

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsNonlinear :

DecidablePred IsNonlinear

Equations

p.instDecidablePredIsNonlinear = decidable_of_iff (p.fusion = Core.Morphology.Fusion.nonlinear) ⋯

def Core.Morphology.MorphProfile.IsMono (p : MorphProfile) :

Equations

p.IsMono = (p.exponence = Core.Morphology.Exponence.monoexponential)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isMono_iff (p : MorphProfile) :

p.IsMono ↔ p.exponence = Exponence.monoexponential

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsMono :

DecidablePred IsMono

Equations

p.instDecidablePredIsMono = decidable_of_iff (p.exponence = Core.Morphology.Exponence.monoexponential) ⋯

def Core.Morphology.MorphProfile.IsPoly (p : MorphProfile) :

Equations

p.IsPoly = (p.exponence = Core.Morphology.Exponence.polyexponential)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isPoly_iff (p : MorphProfile) :

p.IsPoly ↔ p.exponence = Exponence.polyexponential

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsPoly :

DecidablePred IsPoly

Equations

p.instDecidablePredIsPoly = decidable_of_iff (p.exponence = Core.Morphology.Exponence.polyexponential) ⋯

def Core.Morphology.MorphProfile.HasRedup (p : MorphProfile) :

Equations

p.HasRedup = (p.reduplication = Core.Morphology.Reduplication.productiveFull ∨ p.reduplication = Core.Morphology.Reduplication.fullOnly)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.hasRedup_iff (p : MorphProfile) :

p.HasRedup ↔ p.reduplication = Reduplication.productiveFull ∨ p.reduplication = Reduplication.fullOnly

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredHasRedup :

DecidablePred HasRedup

Equations

p.instDecidablePredHasRedup = decidable_of_iff (p.reduplication = Core.Morphology.Reduplication.productiveFull ∨ p.reduplication = Core.Morphology.Reduplication.fullOnly) ⋯

def Core.Morphology.MorphProfile.IsSuffixing (p : MorphProfile) :

Equations

p.IsSuffixing = (p.prefixSuffix = Core.Morphology.PrefixSuffix.stronglySuffixing ∨ p.prefixSuffix = Core.Morphology.PrefixSuffix.weaklySuffixing)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isSuffixing_iff (p : MorphProfile) :

p.IsSuffixing ↔ p.prefixSuffix = PrefixSuffix.stronglySuffixing ∨ p.prefixSuffix = PrefixSuffix.weaklySuffixing

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsSuffixing :

DecidablePred IsSuffixing

Equations

p.instDecidablePredIsSuffixing = decidable_of_iff (p.prefixSuffix = Core.Morphology.PrefixSuffix.stronglySuffixing ∨ p.prefixSuffix = Core.Morphology.PrefixSuffix.weaklySuffixing) ⋯

def Core.Morphology.MorphProfile.IsPrefixing (p : MorphProfile) :

Equations

p.IsPrefixing = (p.prefixSuffix = Core.Morphology.PrefixSuffix.stronglyPrefixing ∨ p.prefixSuffix = Core.Morphology.PrefixSuffix.weaklyPrefixing)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isPrefixing_iff (p : MorphProfile) :

p.IsPrefixing ↔ p.prefixSuffix = PrefixSuffix.stronglyPrefixing ∨ p.prefixSuffix = PrefixSuffix.weaklyPrefixing

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsPrefixing :

DecidablePred IsPrefixing

Equations

p.instDecidablePredIsPrefixing = decidable_of_iff (p.prefixSuffix = Core.Morphology.PrefixSuffix.stronglyPrefixing ∨ p.prefixSuffix = Core.Morphology.PrefixSuffix.weaklyPrefixing) ⋯

def Core.Morphology.MorphProfile.IsLowSynthesis (p : MorphProfile) :

Equations

p.IsLowSynthesis = (p.verbSynthesis = Core.Morphology.VerbSynthesis.low)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isLowSynthesis_iff (p : MorphProfile) :

p.IsLowSynthesis ↔ p.verbSynthesis = VerbSynthesis.low

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsLowSynthesis :

DecidablePred IsLowSynthesis

Equations

p.instDecidablePredIsLowSynthesis = decidable_of_iff (p.verbSynthesis = Core.Morphology.VerbSynthesis.low) ⋯

def Core.Morphology.MorphProfile.IsHighSynthesis (p : MorphProfile) :

Equations

p.IsHighSynthesis = (p.verbSynthesis = Core.Morphology.VerbSynthesis.high)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isHighSynthesis_iff (p : MorphProfile) :

p.IsHighSynthesis ↔ p.verbSynthesis = VerbSynthesis.high

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsHighSynthesis :

DecidablePred IsHighSynthesis

Equations

p.instDecidablePredIsHighSynthesis = decidable_of_iff (p.verbSynthesis = Core.Morphology.VerbSynthesis.high) ⋯

def Core.Morphology.MorphProfile.IsFlexive (p : MorphProfile) :

Equations

p.IsFlexive = (p.flexivity = some Core.Morphology.Flexivity.flexive)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isFlexive_iff (p : MorphProfile) :

p.IsFlexive ↔ p.flexivity = some Flexivity.flexive

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsFlexive :

DecidablePred IsFlexive

Equations

p.instDecidablePredIsFlexive = decidable_of_iff (p.flexivity = some Core.Morphology.Flexivity.flexive) ⋯

def Core.Morphology.MorphProfile.IsNonflexive (p : MorphProfile) :

Equations

p.IsNonflexive = (p.flexivity = some Core.Morphology.Flexivity.nonflexive)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isNonflexive_iff (p : MorphProfile) :

p.IsNonflexive ↔ p.flexivity = some Flexivity.nonflexive

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsNonflexive :

DecidablePred IsNonflexive

Equations

p.instDecidablePredIsNonflexive = decidable_of_iff (p.flexivity = some Core.Morphology.Flexivity.nonflexive) ⋯

def Core.Morphology.MorphProfile.IsCumulative (p : MorphProfile) :

Equations

p.IsCumulative = (p.bnExponence = some Core.Morphology.ExponenceScope.cumulative)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isCumulative_iff (p : MorphProfile) :

p.IsCumulative ↔ p.bnExponence = some ExponenceScope.cumulative

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsCumulative :

DecidablePred IsCumulative

Equations

p.instDecidablePredIsCumulative = decidable_of_iff (p.bnExponence = some Core.Morphology.ExponenceScope.cumulative) ⋯

def Core.Morphology.MorphProfile.IsSeparative (p : MorphProfile) :

Equations

p.IsSeparative = (p.bnExponence = some Core.Morphology.ExponenceScope.separative)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isSeparative_iff (p : MorphProfile) :

p.IsSeparative ↔ p.bnExponence = some ExponenceScope.separative

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsSeparative :

DecidablePred IsSeparative

Equations

p.instDecidablePredIsSeparative = decidable_of_iff (p.bnExponence = some Core.Morphology.ExponenceScope.separative) ⋯

def Core.Morphology.MorphProfile.IsAgglutinating (p : MorphProfile) :

Traditional "agglutinating" = concatenative + nonflexive + separative. @cite{bickel-nichols-2001} decomposition of the traditional typology.

Equations

p.IsAgglutinating = (p.IsConcatenative ∧ p.IsNonflexive ∧ p.IsSeparative)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isAgglutinating_iff (p : MorphProfile) :

p.IsAgglutinating ↔ p.IsConcatenative ∧ p.IsNonflexive ∧ p.IsSeparative

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsAgglutinating :

DecidablePred IsAgglutinating

Equations

p.instDecidablePredIsAgglutinating = decidable_of_iff (p.IsConcatenative ∧ p.IsNonflexive ∧ p.IsSeparative) ⋯

def Core.Morphology.MorphProfile.IsFusional (p : MorphProfile) :

Traditional "fusional" = concatenative + flexive + cumulative. @cite{bickel-nichols-2001} decomposition of the traditional typology.

Equations

p.IsFusional = (p.IsConcatenative ∧ p.IsFlexive ∧ p.IsCumulative)

Instances For

@[simp]

theorem Core.Morphology.MorphProfile.isFusional_iff (p : MorphProfile) :

p.IsFusional ↔ p.IsConcatenative ∧ p.IsFlexive ∧ p.IsCumulative

@[implicit_reducible]

instance Core.Morphology.MorphProfile.instDecidablePredIsFusional :

DecidablePred IsFusional

Equations

p.instDecidablePredIsFusional = decidable_of_iff (p.IsConcatenative ∧ p.IsFlexive ∧ p.IsCumulative) ⋯

Mutual exclusion #

The traditional types "agglutinating" and "fusional" are mutually exclusive because they require contradictory values on the flexivity dimension (nonflexive vs flexive). This follows from the B&N decomposition — it is not an empirical observation but a structural consequence of the definitions.

theorem Core.Morphology.MorphProfile.nonflexive_flexive_exclusive (p : MorphProfile) :

¬(p.IsNonflexive ∧ p.IsFlexive)

Nonflexive and flexive are contradictory: a language cannot be both.

theorem Core.Morphology.MorphProfile.cumulative_separative_exclusive (p : MorphProfile) :

¬(p.IsCumulative ∧ p.IsSeparative)

Cumulative and separative are contradictory: a language cannot be both.

theorem Core.Morphology.MorphProfile.agglutinating_fusional_exclusive (p : MorphProfile) :

¬(p.IsAgglutinating ∧ p.IsFusional)

Agglutinating and fusional are mutually exclusive: they require opposite flexivity values (nonflexive vs flexive). Follows from the B&N decomposition; not an empirical observation.