Word order

The order of a head relative to one of its dependents, and the linear arrangement of a finite set of constituents, in particular of the subject, object and verb of a clause.

HeadDirection is the two-valued order of a head and a dependent, head-initial when the head precedes; HeadDirection.swap is the opposite direction, HeadDirection.ofLT the direction read off two positions, HeadDirection.dependentEdge the side of the head on which its dependents lie, and HeadDirection.nearest picks, from dependents in linear order on one side of their head, the one next to it. WordOrder.Arrangement α n is a linear arrangement of the elements of α over n ranks, a bijection onto Fin n, so that precedence, adjacency, the head direction of any pair, the ends and the mirror image are read off the ranks. Arrangement Constituent 3 arranges the three clausal constituents, and its six values are the basic word orders of the typological literature, Arrangement.sov and its siblings, each labelled by its list of constituents.

Main declarations

• HeadDirection, HeadDirection.swap, HeadDirection.ofLT, HeadDirection.dependentEdge: the two directions, the involution exchanging them, the direction of a head and a dependent at given positions, and the edge of the head on which the dependents lie.
• HeadDirection.nearest: the dependent next to the head, such as the conjunct of a coordination that a selector or a probe next to it sees.
• WordOrder.Arrangement, Arrangement.Precedes, Arrangement.Adjacent, Arrangement.headDirection, Arrangement.mirror: an arrangement of a finite type over ranks, precedence and adjacency of two elements, the head direction of a pair, and the reversed arrangement.
• Arrangement.IsEnd, Arrangement.IsInitial, Arrangement.IsFinal, Arrangement.IsMedial: an element that heads every other in one direction, standing first or last, or neither.
• Arrangement.toList: the elements of an arrangement in their order.
• WordOrder.Constituent, Arrangement.sov and its siblings, Arrangement.label, Arrangement.ofLabel?: the subject, object and verb, their six arrangements, and the labels "SOV", … that name them.

Implementation notes

The WALS classification of a language's dominant orders, with its "no dominant order" value, is data (WALS Feature 81A and its siblings). A fragment records the arrangements a language admits as a Finset (Arrangement Constituent 3); the pairwise orders the language fixes are the ones every member agrees on, so no separate consistency invariant is needed. The rank count is a parameter rather than Fintype.card α, so that numerals and decide reduce, and the ends are defined by rank for the same reason.

References

• [Dry92]
• [Dry13]
• [Gre63]

inductive HeadDirection : Type

The order of a head and one of its dependents, head-initial when the head precedes, as a verb precedes its object in VO order and a preposition its noun phrase, head-final otherwise.

• headInitial : HeadDirection
• headFinal : HeadDirection

@[instance_reducible]

instance instDecidableEqHeadDirection : DecidableEq HeadDirection

Equations

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

@[instance_reducible]

instance instReprHeadDirection : Repr HeadDirection

Equations

• instReprHeadDirection = { reprPrec := instReprHeadDirection.repr }

def instReprHeadDirection.repr : HeadDirection → ℕ → 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✝

@[instance_reducible]

instance instFintypeHeadDirection : Fintype HeadDirection

Equations

• instFintypeHeadDirection = { elems := { val := ↑HeadDirection.enumList, nodup := HeadDirection.enumList_nodup }, complete := instFintypeHeadDirection._proof_1 }

def HeadDirection.swap : HeadDirection → HeadDirection

The opposite direction.

Equations

• HeadDirection.headInitial.swap = HeadDirection.headFinal
• HeadDirection.headFinal.swap = HeadDirection.headInitial

@[simp]

theorem HeadDirection.swap_headInitial : headInitial.swap = headFinal

@[simp]

theorem HeadDirection.swap_headFinal : headFinal.swap = headInitial

@[simp]

theorem HeadDirection.swap_swap (d : HeadDirection) : d.swap.swap = d

theorem HeadDirection.swap_involutive : Function.Involutive swap

theorem HeadDirection.swap_injective : Function.Injective swap

theorem HeadDirection.swap_ne_self (d : HeadDirection) : d.swap ≠ d

theorem HeadDirection.swap_eq_iff_eq_swap {d e : HeadDirection} : d.swap = e ↔ d = e.swap

theorem HeadDirection.eq_or_eq_swap (d e : HeadDirection) : e = d ∨ e = d.swap

A direction is a given one or its opposite.

def HeadDirection.ofLT {α : Type u_1} [LT α] [DecidableLT α] (head dep : α) : HeadDirection

The direction of a head at position head with a dependent at position dep.

Equations

• HeadDirection.ofLT head dep = if head < dep then HeadDirection.headInitial else HeadDirection.headFinal

@[simp]

theorem HeadDirection.ofLT_eq_headInitial {α : Type u_1} [LT α] [DecidableLT α] {head dep : α} : ofLT head dep = headInitial ↔ head < dep

@[simp]

theorem HeadDirection.ofLT_eq_headFinal {α : Type u_1} [LT α] [DecidableLT α] {head dep : α} : ofLT head dep = headFinal ↔ ¬head < dep

theorem HeadDirection.ofLT_swap {α : Type u_1} [LinearOrder α] {head dep : α} (h : head ≠ dep) : ofLT dep head = (ofLT head dep).swap

Exchanging the positions of a head and a dependent reverses the direction.

def HeadDirection.dependentEdge : HeadDirection → Edge

The edge of a head on which its dependents lie, the right one for a head-initial head.

Equations

• HeadDirection.headInitial.dependentEdge = Edge.right
• HeadDirection.headFinal.dependentEdge = Edge.left

@[simp]

theorem HeadDirection.dependentEdge_headInitial : headInitial.dependentEdge = Edge.right

@[simp]

theorem HeadDirection.dependentEdge_headFinal : headFinal.dependentEdge = Edge.left

@[simp]

theorem HeadDirection.dependentEdge_swap (d : HeadDirection) : d.swap.dependentEdge = d.dependentEdge.swap

The opposite direction puts the dependents on the other edge.

theorem HeadDirection.dependentEdge_injective : Function.Injective dependentEdge

def HeadDirection.Orders {α : Type u_1} [LT α] : HeadDirection → α → α → Prop

d.Orders head dep holds when the dependent at dep lies in direction d of the head at head, after it for a head-initial head and before it for a head-final one. Unlike ofLT, it fails when the two positions coincide.

Equations

• HeadDirection.headInitial.Orders x✝¹ x✝ = (x✝¹ < x✝)
• HeadDirection.headFinal.Orders x✝¹ x✝ = (x✝ < x✝¹)

@[instance_reducible]

instance HeadDirection.instDecidableOrdersOfDecidableLT {α : Type u_1} [LT α] [DecidableLT α] (d : HeadDirection) (head dep : α) : Decidable (d.Orders head dep)

Equations

• HeadDirection.headInitial.instDecidableOrdersOfDecidableLT x✝¹ x✝ = HeadDirection.instDecidableOrdersOfDecidableLT._aux_1 x✝¹ x✝
• HeadDirection.headFinal.instDecidableOrdersOfDecidableLT x✝¹ x✝ = HeadDirection.instDecidableOrdersOfDecidableLT._aux_3 x✝¹ x✝

@[simp]

theorem HeadDirection.headInitial_orders {α : Type u_1} {head dep : α} [LT α] : headInitial.Orders head dep ↔ head < dep

@[simp]

theorem HeadDirection.headFinal_orders {α : Type u_1} {head dep : α} [LT α] : headFinal.Orders head dep ↔ dep < head

theorem HeadDirection.orders_iff_ofLT {α : Type u_1} {d : HeadDirection} {head dep : α} [LinearOrder α] : d.Orders head dep ↔ head ≠ dep ∧ ofLT head dep = d

Orders is ofLT on distinct positions.

def HeadDirection.nearest {α : Type u_1} : HeadDirection → List α → Option α

d.nearest l is the element of l, dependents in linear order on one side of their head, that is next to the head, the first when the head precedes them and the last when it follows.

Equations

• HeadDirection.headInitial.nearest x✝ = x✝.head?
• HeadDirection.headFinal.nearest x✝ = x✝.getLast?

@[simp]

theorem HeadDirection.nearest_headInitial {α : Type u_1} (l : List α) : headInitial.nearest l = l.head?

@[simp]

theorem HeadDirection.nearest_headFinal {α : Type u_1} (l : List α) : headFinal.nearest l = l.getLast?

theorem HeadDirection.mem_of_mem_nearest {α : Type u_1} {d : HeadDirection} {l : List α} {a : α} (h : a ∈ d.nearest l) : a ∈ l

theorem HeadDirection.nearest_swap_reverse {α : Type u_1} (d : HeadDirection) (l : List α) : d.swap.nearest l.reverse = d.nearest l

Reversing the dependents and the side of the head picks out the same one.

theorem HeadDirection.nearest_eq_head?_iff {α : Type u_1} [Nontrivial α] {d : HeadDirection} : (∀ (l : List α), d.nearest l = l.head?) ↔ d = headInitial

The dependent next to the head is the first on every list exactly when the head precedes.

theorem HeadDirection.rel_nearest {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β} (h : List.Forall₂ R l₁ l₂) (d : HeadDirection) : Option.Rel R (d.nearest l₁) (d.nearest l₂)

Lists related pointwise have related nearest elements.

@[reducible, inline]

abbrev WordOrder.Arrangement (α : Type u_1) (n : ℕ) : Type u_1

A linear arrangement of the elements of α over n ranks, each element sent to its rank.

Equations

• WordOrder.Arrangement α n = (α ≃ Fin n)

def WordOrder.Arrangement.Precedes {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x y : α) : Prop

x precedes y.

Equations

• a.Precedes x y = (a x < a y)

@[instance_reducible]

instance WordOrder.Arrangement.instDecidablePrecedes {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x y : α) : Decidable (a.Precedes x y)

Equations

• a.instDecidablePrecedes x y = { decide := (↑(a x)).succ.ble ↑(a y), reflects_decide := ⋯ }

def WordOrder.Arrangement.Adjacent {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x y : α) : Prop

x and y stand next to each other, one rank covering the other.

Equations

• a.Adjacent x y = (a x ⋖ a y ∨ a y ⋖ a x)

def WordOrder.Arrangement.headDirection {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x y : α) : HeadDirection

The direction of the head x with respect to its dependent y.

Equations

• a.headDirection x y = HeadDirection.ofLT (a x) (a y)

def WordOrder.Arrangement.mirror {α : Type u_1} {n : ℕ} (a : Arrangement α n) : Arrangement α n

The mirror image, every rank reversed.

Equations

• a.mirror = Equiv.trans a Fin.revPerm

def WordOrder.Arrangement.IsEnd {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x : α) : HeadDirection → Prop

a.IsEnd x d holds when x is a head in direction d of every other element: x stands first when d is head-initial and last when it is head-final.

Equations

• a.IsEnd x HeadDirection.headInitial = (↑(a x) = 0)
• a.IsEnd x HeadDirection.headFinal = (↑(a x) + 1 = n)

@[reducible, inline]

abbrev WordOrder.Arrangement.IsInitial {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x : α) : Prop

x stands first.

Equations

• a.IsInitial x = a.IsEnd x HeadDirection.headInitial

@[reducible, inline]

abbrev WordOrder.Arrangement.IsFinal {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x : α) : Prop

x stands last.

Equations

• a.IsFinal x = a.IsEnd x HeadDirection.headFinal

def WordOrder.Arrangement.IsMedial {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x : α) : Prop

x stands neither first nor last.

Equations

• a.IsMedial x = (¬a.IsInitial x ∧ ¬a.IsFinal x)

@[instance_reducible]

instance WordOrder.Arrangement.instDecidableIsEnd {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x : α) (d : HeadDirection) : Decidable (a.IsEnd x d)

Equations

• a.instDecidableIsEnd x HeadDirection.headInitial = { decide := (↑(a x)).beq 0, reflects_decide := ⋯ }
• a.instDecidableIsEnd x HeadDirection.headFinal = { decide := (↑(a x) + 1).beq n, reflects_decide := ⋯ }

@[instance_reducible]

instance WordOrder.Arrangement.instDecidableIsMedial {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x : α) : Decidable (a.IsMedial x)

Equations

• a.instDecidableIsMedial x = { decide := decide ¬a.IsInitial x && decide ¬a.IsFinal x, reflects_decide := ⋯ }

@[simp]

theorem WordOrder.Arrangement.headDirection_eq_headInitial {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} : a.headDirection x y = HeadDirection.headInitial ↔ a.Precedes x y

@[simp]

theorem WordOrder.Arrangement.headDirection_eq_headFinal {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} : a.headDirection x y = HeadDirection.headFinal ↔ ¬a.Precedes x y

theorem WordOrder.Arrangement.Precedes.trans {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y z : α} (h₁ : a.Precedes x y) (h₂ : a.Precedes y z) : a.Precedes x z

theorem WordOrder.Arrangement.Precedes.asymm {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} (h : a.Precedes x y) : ¬a.Precedes y x

The mirror image

@[simp]

theorem WordOrder.Arrangement.mirror_apply {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} : a.mirror x = (a x).rev

@[simp]

theorem WordOrder.Arrangement.mirror_mirror {α : Type u_1} {n : ℕ} (a : Arrangement α n) : a.mirror.mirror = a

theorem WordOrder.Arrangement.mirror_involutive {α : Type u_1} {n : ℕ} : Function.Involutive mirror

theorem WordOrder.Arrangement.precedes_mirror {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} : a.mirror.Precedes x y ↔ a.Precedes y x

The mirror image reverses every precedence.

theorem WordOrder.Arrangement.headDirection_mirror {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} (h : x ≠ y) : a.mirror.headDirection x y = (a.headDirection x y).swap

The mirror image reverses the direction of every head with respect to a distinct dependent.

Adjacency

theorem WordOrder.Arrangement.adjacent_iff_val {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} : a.Adjacent x y ↔ ↑(a x) + 1 = ↑(a y) ∨ ↑(a y) + 1 = ↑(a x)

@[instance_reducible]

instance WordOrder.Arrangement.instDecidableAdjacent {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} : Decidable (a.Adjacent x y)

Equations

• WordOrder.Arrangement.instDecidableAdjacent = decidable_of_iff (↑(a x) + 1 = ↑(a y) ∨ ↑(a y) + 1 = ↑(a x)) ⋯

theorem WordOrder.Arrangement.adjacent_comm {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} : a.Adjacent x y ↔ a.Adjacent y x

theorem WordOrder.Arrangement.Adjacent.ne {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} (h : a.Adjacent x y) : x ≠ y

@[simp]

theorem WordOrder.Arrangement.adjacent_mirror {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x y : α} : a.mirror.Adjacent x y ↔ a.Adjacent x y

The mirror image keeps every adjacency.

Ends

theorem WordOrder.Arrangement.isInitial_iff_val {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} : a.IsInitial x ↔ ↑(a x) = 0

theorem WordOrder.Arrangement.isFinal_iff_val {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} : a.IsFinal x ↔ ↑(a x) + 1 = n

theorem WordOrder.Arrangement.isInitial_iff {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} : a.IsInitial x ↔ ∀ (y : α), y ≠ x → a.Precedes x y

The first element precedes every other.

theorem WordOrder.Arrangement.isFinal_iff {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} : a.IsFinal x ↔ ∀ (y : α), y ≠ x → a.Precedes y x

The last element follows every other.

theorem WordOrder.Arrangement.isEnd_iff {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} {d : HeadDirection} : a.IsEnd x d ↔ ∀ (y : α), y ≠ x → a.headDirection x y = d

x stands at the d end exactly when it is a d-head of every other element.

theorem WordOrder.Arrangement.isEnd_mirror {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} {d : HeadDirection} : a.mirror.IsEnd x d ↔ a.IsEnd x d.swap

The mirror image exchanges the two ends.

theorem WordOrder.Arrangement.isInitial_mirror {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} : a.mirror.IsInitial x ↔ a.IsFinal x

theorem WordOrder.Arrangement.isFinal_mirror {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} : a.mirror.IsFinal x ↔ a.IsInitial x

theorem WordOrder.Arrangement.isMedial_mirror {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} : a.mirror.IsMedial x ↔ a.IsMedial x

theorem WordOrder.Arrangement.adjacent_iff_not_isMedial {α : Type u_1} {a : Arrangement α 3} {x y z : α} (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) : a.Adjacent x y ↔ ¬a.IsMedial z

Of three elements over three ranks, two are adjacent exactly when the third is not medial.

The elements before and after an element

def WordOrder.Arrangement.after {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x : α) [Fintype α] : Finset α

The elements after x.

Equations

• a.after x = {c : α | a.Precedes x c}

def WordOrder.Arrangement.before {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x : α) [Fintype α] : Finset α

The elements before x.

Equations

• a.before x = {c : α | a.Precedes c x}

@[simp]

theorem WordOrder.Arrangement.mem_after {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} [Fintype α] {c : α} : c ∈ a.after x ↔ a.Precedes x c

@[simp]

theorem WordOrder.Arrangement.mem_before {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} [Fintype α] {c : α} : c ∈ a.before x ↔ a.Precedes c x

theorem WordOrder.Arrangement.notMem_after_self {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} [Fintype α] : x ∉ a.after x

theorem WordOrder.Arrangement.before_eq_after_mirror {α : Type u_1} {n : ℕ} {a : Arrangement α n} {x : α} [Fintype α] : a.before x = a.mirror.after x

Lists

def WordOrder.Arrangement.toList {α : Type u_1} {n : ℕ} (a : Arrangement α n) : List α

The elements in their order.

Equations

• a.toList = List.map (⇑(Equiv.symm a)) (List.finRange n)

@[simp]

theorem WordOrder.Arrangement.length_toList {α : Type u_1} {n : ℕ} (a : Arrangement α n) : a.toList.length = n

theorem WordOrder.Arrangement.toList_nodup {α : Type u_1} {n : ℕ} (a : Arrangement α n) : a.toList.Nodup

theorem WordOrder.Arrangement.mem_toList {α : Type u_1} {n : ℕ} (a : Arrangement α n) (x : α) : x ∈ a.toList

inductive WordOrder.Constituent : Type

The three constituents of a transitive clause.

• subject : Constituent
• object : Constituent
• verb : Constituent

@[instance_reducible]

instance WordOrder.instDecidableEqConstituent : DecidableEq Constituent

Equations

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

def WordOrder.instReprConstituent.repr : Constituent → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance WordOrder.instReprConstituent : Repr Constituent

Equations

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

@[instance_reducible]

instance WordOrder.instFintypeConstituent : Fintype Constituent

Equations

• WordOrder.instFintypeConstituent = { elems := { val := ↑WordOrder.Constituent.enumList, nodup := WordOrder.Constituent.enumList_nodup }, complete := WordOrder.instFintypeConstituent._proof_1 }

def WordOrder.Constituent.letter : Constituent → Char

The letter of a constituent in the labels "SOV", "SVO", … of the typological literature.

Equations

• WordOrder.Constituent.subject.letter = 'S'
• WordOrder.Constituent.object.letter = 'O'
• WordOrder.Constituent.verb.letter = 'V'

def WordOrder.Arrangement.sov : Arrangement Constituent 3

Subject, object, verb.

Equations

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

def WordOrder.Arrangement.svo : Arrangement Constituent 3

Subject, verb, object.

Equations

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

def WordOrder.Arrangement.vso : Arrangement Constituent 3

Verb, subject, object.

Equations

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

def WordOrder.Arrangement.vos : Arrangement Constituent 3

Verb, object, subject.

Equations

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

def WordOrder.Arrangement.ovs : Arrangement Constituent 3

Object, verb, subject.

Equations

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

def WordOrder.Arrangement.osv : Arrangement Constituent 3

Object, subject, verb.

Equations

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

def WordOrder.Arrangement.basicOrders : List (Arrangement Constituent 3)

The six basic orders.

Equations

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

theorem WordOrder.Arrangement.mem_basicOrders (a : Arrangement Constituent 3) : a ∈ basicOrders

Every arrangement of the three constituents is a basic order.

def WordOrder.Arrangement.label (a : Arrangement Constituent 3) : String

The label of an arrangement of the three constituents, "SOV" for sov.

Equations

• a.label = String.ofList (List.map WordOrder.Constituent.letter a.toList)

def WordOrder.Arrangement.ofLabel? (s : String) : Option (Arrangement Constituent 3)

The basic order with the label s, if any.

Equations

• WordOrder.Arrangement.ofLabel? s = List.find? (fun (x : WordOrder.Arrangement WordOrder.Constituent 3) => decide (x.label = s)) WordOrder.Arrangement.basicOrders

@[simp]

theorem WordOrder.Arrangement.ofLabel?_label (a : Arrangement Constituent 3) : ofLabel? a.label = some a