Word-order typology

Framework-agnostic per-language word-order substrate (WALS chapters 81–83), under a bare-root WordOrder namespace in Features/.

Main definitions

• BasicOrder, SVOrder, OVOrder : the WALS Ch 81/82/83 constituent-order classifications ([Dry13]).
• WordOrderProfile : the three classifications bundled per language, with the cross-field invariant WordOrderProfile.IsConsistent and the ISO-639-3 lookup constructor WordOrderProfile.ofWALS.
• HeadDirection : head-initial vs head-final (root-named; used for FOFC and the like).
• BasicOrder.IsSubjectBeforeObject : the antecedent of [Gre63] Universal 1.
• OVOrder.verbPosition : the verb position a basic order projects to.

Implementation notes

Each enum carries both .noDominant (a WALS-attested finding of no dominant order, e.g. German Ch 81) and .notInWALS (uncoded in that chapter); filtering on ≠ .noDominant would otherwise misread uncoded languages as nondominant. The three fields are bundled independently because WALS codes them independently (German is Ch 81 nondominant yet Ch 82 dominant), so WordOrderProfile.IsConsistent — not the type — enforces their entailments. The substrate is neutral on primacy: [Gre63] takes BasicOrder as primary, [Dry92] the OV/VO cut.

inductive HeadDirection : Type

Head direction of a construction: head-initial (VO, prepositions) vs head-final. Root-named (consumed across Fragments, Studies, Syntax); used for FOFC and the like.

• headInitial : HeadDirection
• headFinal : HeadDirection

def instReprHeadDirection.repr : HeadDirection → Nat → Std.Format

Equations

• instReprHeadDirection.repr HeadDirection.headInitial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HeadDirection.headInitial")).group prec✝
• instReprHeadDirection.repr HeadDirection.headFinal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HeadDirection.headFinal")).group prec✝

@[implicit_reducible]

instance instReprHeadDirection : Repr HeadDirection

Equations

• instReprHeadDirection = { reprPrec := instReprHeadDirection.repr }

@[implicit_reducible]

instance instDecidableEqHeadDirection : DecidableEq HeadDirection

Equations

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

Classifications

inductive WordOrder.BasicOrder : Type

WALS Ch 81: the six-way classification of basic constituent order.

• 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.

@[implicit_reducible]

instance WordOrder.instDecidableEqBasicOrder : DecidableEq BasicOrder

Equations

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

@[implicit_reducible]

instance WordOrder.instReprBasicOrder : Repr BasicOrder

Equations

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

def WordOrder.instReprBasicOrder.repr : BasicOrder → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• WordOrder.instReprBasicOrder.repr WordOrder.BasicOrder.sov prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.BasicOrder.sov")).group prec✝
• WordOrder.instReprBasicOrder.repr WordOrder.BasicOrder.svo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.BasicOrder.svo")).group prec✝
• WordOrder.instReprBasicOrder.repr WordOrder.BasicOrder.vso prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.BasicOrder.vso")).group prec✝
• WordOrder.instReprBasicOrder.repr WordOrder.BasicOrder.vos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.BasicOrder.vos")).group prec✝
• WordOrder.instReprBasicOrder.repr WordOrder.BasicOrder.ovs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.BasicOrder.ovs")).group prec✝
• WordOrder.instReprBasicOrder.repr WordOrder.BasicOrder.osv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.BasicOrder.osv")).group prec✝

inductive WordOrder.SVOrder : Type

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.

@[implicit_reducible]

instance WordOrder.instDecidableEqSVOrder : DecidableEq SVOrder

Equations

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

def WordOrder.instReprSVOrder.repr : SVOrder → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• WordOrder.instReprSVOrder.repr WordOrder.SVOrder.sv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.SVOrder.sv")).group prec✝
• WordOrder.instReprSVOrder.repr WordOrder.SVOrder.vs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.SVOrder.vs")).group prec✝
• WordOrder.instReprSVOrder.repr WordOrder.SVOrder.notInWALS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.SVOrder.notInWALS")).group prec✝

@[implicit_reducible]

instance WordOrder.instReprSVOrder : Repr SVOrder

Equations

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

inductive WordOrder.OVOrder : Type

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.

@[implicit_reducible]

instance WordOrder.instDecidableEqOVOrder : DecidableEq OVOrder

Equations

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

@[implicit_reducible]

instance WordOrder.instReprOVOrder : Repr OVOrder

Equations

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

def WordOrder.instReprOVOrder.repr : OVOrder → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• WordOrder.instReprOVOrder.repr WordOrder.OVOrder.ov prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.OVOrder.ov")).group prec✝
• WordOrder.instReprOVOrder.repr WordOrder.OVOrder.vo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.OVOrder.vo")).group prec✝
• WordOrder.instReprOVOrder.repr WordOrder.OVOrder.notInWALS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WordOrder.OVOrder.notInWALS")).group prec✝

structure WordOrder.WordOrderProfile : Type

A language's WALS Ch 81/82/83 word-order classifications, bundled.

• basicOrder : BasicOrder
• svOrder : SVOrder
• ovOrder : OVOrder

def WordOrder.instReprWordOrderProfile.repr : WordOrderProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance WordOrder.instReprWordOrderProfile : Repr WordOrderProfile

Equations

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

@[implicit_reducible]

instance WordOrder.instDecidableEqWordOrderProfile : DecidableEq WordOrderProfile

Equations

• WordOrder.instDecidableEqWordOrderProfile = WordOrder.instDecidableEqWordOrderProfile.decEq

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

Equations

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

WALS converters and ISO lookups

def WordOrder.BasicOrder.ofWALS81A : Data.WALS.F81A.BasicWordOrder → BasicOrder

Convert WALS F81A's BasicWordOrder value to a BasicOrder.

Equations

• WordOrder.BasicOrder.ofWALS81A Data.WALS.F81A.BasicWordOrder.sov = WordOrder.BasicOrder.sov
• WordOrder.BasicOrder.ofWALS81A Data.WALS.F81A.BasicWordOrder.svo = WordOrder.BasicOrder.svo
• WordOrder.BasicOrder.ofWALS81A Data.WALS.F81A.BasicWordOrder.vso = WordOrder.BasicOrder.vso
• WordOrder.BasicOrder.ofWALS81A Data.WALS.F81A.BasicWordOrder.vos = WordOrder.BasicOrder.vos
• WordOrder.BasicOrder.ofWALS81A Data.WALS.F81A.BasicWordOrder.ovs = WordOrder.BasicOrder.ovs
• WordOrder.BasicOrder.ofWALS81A Data.WALS.F81A.BasicWordOrder.osv = WordOrder.BasicOrder.osv
• WordOrder.BasicOrder.ofWALS81A Data.WALS.F81A.BasicWordOrder.noDominantOrder = WordOrder.BasicOrder.noDominant

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

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

Equations

• WordOrder.BasicOrder.ofWALS iso = match Data.WALS.Datapoint.lookupISO Data.WALS.F81A.allData iso with | some d => WordOrder.BasicOrder.ofWALS81A d.value | none => WordOrder.BasicOrder.notInWALS

def WordOrder.SVOrder.ofWALS82A : Data.WALS.F82A.SubjectVerbOrder → SVOrder

Convert WALS F82A's SubjectVerbOrder to an SVOrder.

Equations

• WordOrder.SVOrder.ofWALS82A Data.WALS.F82A.SubjectVerbOrder.sv = WordOrder.SVOrder.sv
• WordOrder.SVOrder.ofWALS82A Data.WALS.F82A.SubjectVerbOrder.vs = WordOrder.SVOrder.vs
• WordOrder.SVOrder.ofWALS82A Data.WALS.F82A.SubjectVerbOrder.noDominantOrder = WordOrder.SVOrder.noDominant

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

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

Equations

• WordOrder.SVOrder.ofWALS iso = match Data.WALS.Datapoint.lookupISO Data.WALS.F82A.allData iso with | some d => WordOrder.SVOrder.ofWALS82A d.value | none => WordOrder.SVOrder.notInWALS

def WordOrder.OVOrder.ofWALS83A : Data.WALS.F83A.ObjectVerbOrder → OVOrder

Convert WALS F83A's ObjectVerbOrder to an OVOrder.

Equations

• WordOrder.OVOrder.ofWALS83A Data.WALS.F83A.ObjectVerbOrder.ov = WordOrder.OVOrder.ov
• WordOrder.OVOrder.ofWALS83A Data.WALS.F83A.ObjectVerbOrder.vo = WordOrder.OVOrder.vo
• WordOrder.OVOrder.ofWALS83A Data.WALS.F83A.ObjectVerbOrder.noDominantOrder = WordOrder.OVOrder.noDominant

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

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

Equations

• WordOrder.OVOrder.ofWALS iso = match Data.WALS.Datapoint.lookupISO Data.WALS.F83A.allData iso with | some d => WordOrder.OVOrder.ofWALS83A d.value | none => WordOrder.OVOrder.notInWALS

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

Derive a WordOrderProfile by ISO-639-3 lookup against WALS Ch 81/82/83; each field falls back to .notInWALS when its chapter has no entry. The default Fragment backend — override per field where grammars disagree with or extend WALS.

Equations

• WordOrder.WordOrderProfile.ofWALS iso = { basicOrder := WordOrder.BasicOrder.ofWALS iso, svOrder := WordOrder.SVOrder.ofWALS iso, ovOrder := WordOrder.OVOrder.ofWALS iso }

Projections and consistency

def WordOrder.BasicOrder.entailedSV : BasicOrder → Option SVOrder

The SVOrder a basic order entails (none if the basic order is uninformative): subject precedes verb in SOV/SVO/OSV, verb precedes subject in VSO/VOS/OVS.

Equations

• WordOrder.BasicOrder.sov.entailedSV = some WordOrder.SVOrder.sv
• WordOrder.BasicOrder.svo.entailedSV = some WordOrder.SVOrder.sv
• WordOrder.BasicOrder.osv.entailedSV = some WordOrder.SVOrder.sv
• WordOrder.BasicOrder.vso.entailedSV = some WordOrder.SVOrder.vs
• WordOrder.BasicOrder.vos.entailedSV = some WordOrder.SVOrder.vs
• WordOrder.BasicOrder.ovs.entailedSV = some WordOrder.SVOrder.vs
• WordOrder.BasicOrder.noDominant.entailedSV = none
• WordOrder.BasicOrder.notInWALS.entailedSV = none

def WordOrder.BasicOrder.entailedOV : BasicOrder → Option OVOrder

The OVOrder a basic order entails.

Equations

• WordOrder.BasicOrder.sov.entailedOV = some WordOrder.OVOrder.ov
• WordOrder.BasicOrder.ovs.entailedOV = some WordOrder.OVOrder.ov
• WordOrder.BasicOrder.osv.entailedOV = some WordOrder.OVOrder.ov
• WordOrder.BasicOrder.svo.entailedOV = some WordOrder.OVOrder.vo
• WordOrder.BasicOrder.vso.entailedOV = some WordOrder.OVOrder.vo
• WordOrder.BasicOrder.vos.entailedOV = some WordOrder.OVOrder.vo
• WordOrder.BasicOrder.noDominant.entailedOV = none
• WordOrder.BasicOrder.notInWALS.entailedOV = none

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

A profile is consistent when svOrder and ovOrder each either match what basicOrder entails or are uninformative (.noDominant / .notInWALS) — the latter for languages coded in some WALS chapters but not others.

Equations

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

@[implicit_reducible]

instance WordOrder.instDecidableIsConsistent (p : WordOrderProfile) : Decidable p.IsConsistent

Equations

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

Classification predicates

abbrevs (transparent, so Decidable resolves via BasicOrder's DecidableEq).

@[reducible, inline]

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

b is SOV.

Equations

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

@[reducible, inline]

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

b is SVO.

Equations

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

@[reducible, inline]

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

b is VSO.

Equations

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

@[reducible, inline]

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

b has Subject before Object: SOV, SVO, or VSO. [Gre63] Universal 1's antecedent.

Equations

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

@[reducible, inline]

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

b has Object before Subject: VOS, OVS, or OSV. [Gre63] Universal 1's negative class.

Equations

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

@[reducible, inline]

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

o is OV (object precedes verb). [Dry92]'s primary typological classification under Branching Direction Theory.

Equations

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

@[reducible, inline]

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

o is VO (verb precedes object).

Equations

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

Verb position

inductive WordOrder.VerbPosition : Type

Verb position in the clause, projected from object–verb order: VO ⇒ verb precedes complement (head-initial), OV ⇒ verb follows complement (head-final).

• postverbal : VerbPosition

  Verb precedes complement (head-initial VP).

• preverbal : VerbPosition

  Verb follows complement (head-final VP).

@[implicit_reducible]

instance WordOrder.instDecidableEqVerbPosition : DecidableEq VerbPosition

Equations

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

def WordOrder.instReprVerbPosition.repr : VerbPosition → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance WordOrder.instReprVerbPosition : Repr VerbPosition

Equations

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

def WordOrder.OVOrder.verbPosition : OVOrder → Option VerbPosition

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

Equations

• WordOrder.OVOrder.vo.verbPosition = some WordOrder.VerbPosition.postverbal
• WordOrder.OVOrder.ov.verbPosition = some WordOrder.VerbPosition.preverbal
• WordOrder.OVOrder.noDominant.verbPosition = none
• WordOrder.OVOrder.notInWALS.verbPosition = none