Documentation

Linglib.Typology.WordOrder

Word-order typology: per-language profile substrate #

@cite{dryer-2013-wals} @cite{greenberg-1963} @cite{dryer-1992}

Framework-agnostic substrate for storing per-language word-order data (WALS Chs 81–83). Lives in Typology/ so that both Fragments/ (per-language profiles) and Phenomena/WordOrder/ (cross-linguistic generalisations) can import it without violating the layered dependency hierarchy.

The key record is WordOrderProfile, a flat bundle of three orthogonal WALS classifications. WordOrderProfile.ofWALS provides the canonical "derive from WALS by ISO lookup" convenience.

Epistemic distinction: `noDominant` vs `notInWALS` #

The three enums each carry both .noDominant (WALS-attested nondominance, e.g., German Ch 81 — itself a finding about the language) and .notInWALS (the language is not coded in this WALS chapter). A consumer that filtered on ≠ .noDominant would otherwise silently include unencoded languages as "genuinely nondominant".

Independence assumption and `IsConsistent` #

The three fields are bundled independently even though they are not logically independent: SOV basicOrder entails sv + ov projections, etc. WALS codes them independently for empirical-coverage reasons (a language can be Ch 81 nondominant but Ch 82 dominant — German is exactly this), so the substrate mirrors WALS rather than collapsing fields. The WordOrderProfile.IsConsistent predicate rules out internally contradictory combinations.

Greenbergian vs Dryerian primacy #

The substrate is neutral on which classification is theoretically primary. @cite{greenberg-1963} treated BasicOrder as primary; @cite{dryer-1992} explicitly demoted SOV/SVO/VSO in favour of OV/VO (Branching Direction Theory). Consumers downstream choose which fields to read.

Scope #

Covers WALS Chs 81–83 (clausal word-order features). Sibling substrates carry adjacent typology: Typology/Adposition.lean for Ch 85; nominal-internal and correlation-pair profiles can be added when consumers demand them. Cross-tabulation primitives for correlation tables (Gibson 2025-style 2×2 head-direction tables) live in their consuming Studies file (Phenomena/WordOrder/Studies/ Gibson2025.lean) until a second framework consumer materialises.

inductive Typology.WordOrder.BasicOrder :

WALS Ch 81: six-way classification of basic constituent order. noDominant is WALS's "lacking a dominant word order" code (a substantive finding about the language); notInWALS is absence from the chapter. The two are epistemically different and must not be conflated.

sov : BasicOrder
svo : BasicOrder
vso : BasicOrder
vos : BasicOrder
ovs : BasicOrder
osv : BasicOrder
noDominant : BasicOrder
WALS-attested "lacking a dominant word order" (Ch 81).
notInWALS : BasicOrder
Language not coded in WALS Ch 81.

Instances For

@[implicit_reducible]

instance Typology.WordOrder.instDecidableEqBasicOrder :

DecidableEq BasicOrder

Equations

Typology.WordOrder.instDecidableEqBasicOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.WordOrder.instReprBasicOrder.repr :

BasicOrder → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.WordOrder.instReprBasicOrder :

Repr BasicOrder

Equations

Typology.WordOrder.instReprBasicOrder = { reprPrec := Typology.WordOrder.instReprBasicOrder.repr }

inductive Typology.WordOrder.SVOrder :

WALS Ch 82: binary classification of subject–verb order.

sv : SVOrder
vs : SVOrder
noDominant : SVOrder
WALS-attested "lacking a dominant order" (Ch 82).
notInWALS : SVOrder
Language not coded in WALS Ch 82.

Instances For

@[implicit_reducible]

instance Typology.WordOrder.instDecidableEqSVOrder :

DecidableEq SVOrder

Equations

Typology.WordOrder.instDecidableEqSVOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.WordOrder.instReprSVOrder :

Equations

Typology.WordOrder.instReprSVOrder = { reprPrec := Typology.WordOrder.instReprSVOrder.repr }

def Typology.WordOrder.instReprSVOrder.repr :

SVOrder → Nat → Std.Format

Equations

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

Instances For

inductive Typology.WordOrder.OVOrder :

WALS Ch 83: binary classification of object–verb order.

ov : OVOrder
vo : OVOrder
noDominant : OVOrder
WALS-attested "lacking a dominant order" (Ch 83).
notInWALS : OVOrder
Language not coded in WALS Ch 83.

Instances For

@[implicit_reducible]

instance Typology.WordOrder.instDecidableEqOVOrder :

DecidableEq OVOrder

Equations

Typology.WordOrder.instDecidableEqOVOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.WordOrder.instReprOVOrder.repr :

OVOrder → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.WordOrder.instReprOVOrder :

Equations

Typology.WordOrder.instReprOVOrder = { reprPrec := Typology.WordOrder.instReprOVOrder.repr }

structure Typology.WordOrder.WordOrderProfile :

A bundle of WALS-style word-order classifications for a single language. The three fields are bundled independently because WALS codes them independently; the IsConsistent predicate captures the logical entailments between them.

basicOrder : BasicOrder
svOrder : SVOrder
ovOrder : OVOrder

Instances For

@[implicit_reducible]

instance Typology.WordOrder.instReprWordOrderProfile :

Repr WordOrderProfile

Equations

Typology.WordOrder.instReprWordOrderProfile = { reprPrec := Typology.WordOrder.instReprWordOrderProfile.repr }

def Typology.WordOrder.instReprWordOrderProfile.repr :

WordOrderProfile → Nat → Std.Format

Equations

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

Instances For

def Typology.WordOrder.instDecidableEqWordOrderProfile.decEq (x✝ x✝¹ : WordOrderProfile) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Typology.WordOrder.instDecidableEqWordOrderProfile :

DecidableEq WordOrderProfile

Equations

Typology.WordOrder.instDecidableEqWordOrderProfile = Typology.WordOrder.instDecidableEqWordOrderProfile.decEq

def Typology.WordOrder.BasicOrder.ofWALS81A :

Data.WALS.F81A.BasicWordOrder → BasicOrder

Convert WALS F81A's BasicWordOrder value to a BasicOrder.

Equations

Instances For

def Typology.WordOrder.BasicOrder.ofWALS (iso : String) :

Look up Ch 81 basic order for an ISO 639-3 code. Returns .notInWALS when the language is absent from the chapter.

Equations

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

Instances For

def Typology.WordOrder.SVOrder.ofWALS82A :

Data.WALS.F82A.SubjectVerbOrder → SVOrder

Convert WALS F82A's SubjectVerbOrder to an SVOrder.

Equations

Instances For

def Typology.WordOrder.SVOrder.ofWALS (iso : String) :

Look up Ch 82 subject–verb order for an ISO 639-3 code. Returns .notInWALS when the language is absent from the chapter.

Equations

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

Instances For

def Typology.WordOrder.OVOrder.ofWALS83A :

Data.WALS.F83A.ObjectVerbOrder → OVOrder

Convert WALS F83A's ObjectVerbOrder to an OVOrder.

Equations

Instances For

def Typology.WordOrder.OVOrder.ofWALS (iso : String) :

Look up Ch 83 object–verb order for an ISO 639-3 code. Returns .notInWALS when the language is absent from the chapter.

Equations

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

Instances For

def Typology.WordOrder.WordOrderProfile.ofWALS (iso : String) :

WordOrderProfile

Construct a WordOrderProfile for a language by ISO 639-3 lookup against WALS chapters 81/82/83. Each field independently falls back to .notInWALS if its WALS chapter has no entry. Use this as the default backend in Fragment files; override per-field when grammar-grounded sources disagree with WALS or fill its gaps.

Equations

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

Instances For

def Typology.WordOrder.BasicOrder.entailedSV :

BasicOrder → Option SVOrder

The SVOrder a basic order entails (none if basic order is itself uninformative). Subject precedes verb in SOV, SVO, OSV (V is final or last in those orders); verb precedes subject in VSO, VOS, OVS.

Equations

Instances For

def Typology.WordOrder.BasicOrder.entailedOV :

BasicOrder → Option OVOrder

The OVOrder a basic order entails.

Equations

Instances For

def Typology.WordOrder.WordOrderProfile.IsConsistent (p : WordOrderProfile) :

A profile is consistent if its svOrder and ovOrder either match what basicOrder entails, or are themselves uninformative (.noDominant / .notInWALS). The latter accommodates languages coded in some WALS chapters but not others (e.g., German has nondominant Ch 81 but dominant Ch 82). When basicOrder itself is uninformative, no constraint is imposed on the projections.

Equations

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

Instances For

@[implicit_reducible]

instance Typology.WordOrder.instDecidableIsConsistent (p : WordOrderProfile) :

Decidable p.IsConsistent

Equations

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

@[reducible, inline]

abbrev Typology.WordOrder.BasicOrder.IsSOV (b : BasicOrder) :

b is SOV.

Equations

b.IsSOV = (b = Typology.WordOrder.BasicOrder.sov)

Instances For

@[reducible, inline]

abbrev Typology.WordOrder.BasicOrder.IsSVO (b : BasicOrder) :

b is SVO.

Equations

b.IsSVO = (b = Typology.WordOrder.BasicOrder.svo)

Instances For

@[reducible, inline]

abbrev Typology.WordOrder.BasicOrder.IsVSO (b : BasicOrder) :

b is VSO.

Equations

b.IsVSO = (b = Typology.WordOrder.BasicOrder.vso)

Instances For

@[reducible, inline]

abbrev Typology.WordOrder.BasicOrder.IsSubjectBeforeObject (b : BasicOrder) :

b has Subject before Object: SOV, SVO, or VSO. @cite{greenberg-1963} Universal 1's antecedent.

Equations

b.IsSubjectBeforeObject = (b = Typology.WordOrder.BasicOrder.sov ∨ b = Typology.WordOrder.BasicOrder.svo ∨ b = Typology.WordOrder.BasicOrder.vso)

Instances For

@[reducible, inline]

abbrev Typology.WordOrder.BasicOrder.IsObjectBeforeSubject (b : BasicOrder) :

b has Object before Subject: VOS, OVS, or OSV. @cite{greenberg-1963} Universal 1's negative class.

Equations

b.IsObjectBeforeSubject = (b = Typology.WordOrder.BasicOrder.vos ∨ b = Typology.WordOrder.BasicOrder.ovs ∨ b = Typology.WordOrder.BasicOrder.osv)

Instances For

@[reducible, inline]

abbrev Typology.WordOrder.OVOrder.IsOV (o : OVOrder) :

o is OV (object precedes verb). @cite{dryer-1992}'s primary typological classification under Branching Direction Theory.

Equations

o.IsOV = (o = Typology.WordOrder.OVOrder.ov)

Instances For

@[reducible, inline]

abbrev Typology.WordOrder.OVOrder.IsVO (o : OVOrder) :

o is VO (verb precedes object).

Equations

o.IsVO = (o = Typology.WordOrder.OVOrder.vo)

Instances For

inductive Typology.WordOrder.VerbPosition :

Verb position in the clause as derived from object–verb order. Theory-neutral: VO ⇒ post-verbal object (verb precedes complement), OV ⇒ pre-verbal object (verb follows complement).

postverbal : VerbPosition
Verb precedes complement (head-initial VP).
preverbal : VerbPosition
Verb follows complement (head-final VP).

Instances For

@[implicit_reducible]

instance Typology.WordOrder.instDecidableEqVerbPosition :

DecidableEq VerbPosition

Equations

Typology.WordOrder.instDecidableEqVerbPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.WordOrder.instReprVerbPosition :

Repr VerbPosition

Equations

Typology.WordOrder.instReprVerbPosition = { reprPrec := Typology.WordOrder.instReprVerbPosition.repr }

def Typology.WordOrder.instReprVerbPosition.repr :

VerbPosition → Nat → Std.Format

Equations

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

Instances For

def Typology.WordOrder.OVOrder.verbPosition :

OVOrder → Option VerbPosition

Project an OVOrder to a VerbPosition. Returns none for uninformative orders (.noDominant, .notInWALS).

Equations

Instances For