Corpus word-order data: schema

Typed schema for the word-order data a paper draws from corpora: per-language counts of the two relative orders of a nominal subject and object, per-language printed statistics of that order (its Shannon entropy and the mutual information between case marking and syntactic role), and individually annotated clauses recording the order of object and verb together with the text type, the object's length, and its animacy. Generated rows live in Data/WordOrder/Corpus/<Paper>.lean, emitted from the canonical <Paper>.json by scripts/gen_word_order_corpus.py.

This is data: it imports nothing from Linglib/ and states no theorems; the order and text-type enumerations carry the discrete measurable structure so that consumers can take laws over them. Counts are the dataset's integers; printed statistics are scaled integers, in thousandths of a bit, at the precision the dataset prints, so that consumers compute over them by decide. Language codes are ISO 639-3 codes as the datasets print them.

References

• [LNAT+23]

inductive Data.WordOrder.Corpus.SubjectObject : Type

The relative order of a nominal subject and a nominal object in a clause.

• subjectFirst : SubjectObject
• objectFirst : SubjectObject

@[instance_reducible]

instance Data.WordOrder.Corpus.instDecidableEqSubjectObject : DecidableEq SubjectObject

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instReprSubjectObject : Repr SubjectObject

Equations

• Data.WordOrder.Corpus.instReprSubjectObject = { reprPrec := Data.WordOrder.Corpus.instReprSubjectObject.repr }

def Data.WordOrder.Corpus.instReprSubjectObject.repr : SubjectObject → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instFintypeSubjectObject : Fintype SubjectObject

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instMeasurableSpaceSubjectObject : MeasurableSpace SubjectObject

Equations

• Data.WordOrder.Corpus.instMeasurableSpaceSubjectObject = ⊤

instance Data.WordOrder.Corpus.instMeasurableSingletonClassSubjectObject : MeasurableSingletonClass SubjectObject

inductive Data.WordOrder.Corpus.ObjectVerb : Type

The relative order of a nominal object and its verb in a clause.

• objectFirst : ObjectVerb
• verbFirst : ObjectVerb

@[instance_reducible]

instance Data.WordOrder.Corpus.instDecidableEqObjectVerb : DecidableEq ObjectVerb

Equations

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

def Data.WordOrder.Corpus.instReprObjectVerb.repr : ObjectVerb → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instReprObjectVerb : Repr ObjectVerb

Equations

• Data.WordOrder.Corpus.instReprObjectVerb = { reprPrec := Data.WordOrder.Corpus.instReprObjectVerb.repr }

@[instance_reducible]

instance Data.WordOrder.Corpus.instFintypeObjectVerb : Fintype ObjectVerb

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instMeasurableSpaceObjectVerb : MeasurableSpace ObjectVerb

Equations

• Data.WordOrder.Corpus.instMeasurableSpaceObjectVerb = ⊤

instance Data.WordOrder.Corpus.instMeasurableSingletonClassObjectVerb : MeasurableSingletonClass ObjectVerb

inductive Data.WordOrder.Corpus.TextType : Type

The text type of a corpus sample.

• conversation : TextType
• fiction : TextType
• news : TextType

@[instance_reducible]

instance Data.WordOrder.Corpus.instDecidableEqTextType : DecidableEq TextType

Equations

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

def Data.WordOrder.Corpus.instReprTextType.repr : TextType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instReprTextType : Repr TextType

Equations

• Data.WordOrder.Corpus.instReprTextType = { reprPrec := Data.WordOrder.Corpus.instReprTextType.repr }

@[instance_reducible]

instance Data.WordOrder.Corpus.instFintypeTextType : Fintype TextType

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instMeasurableSpaceTextType : MeasurableSpace TextType

Equations

• Data.WordOrder.Corpus.instMeasurableSpaceTextType = ⊤

instance Data.WordOrder.Corpus.instMeasurableSingletonClassTextType : MeasurableSingletonClass TextType

structure Data.WordOrder.Corpus.SubjectObjectCounts : Type

One language's counts of subject-before-object and object-before-subject clauses in a corpus.

• language : String

  The language name as the dataset prints it.

• isoCode : String

  The ISO 639-3 language code.

• subjectFirst : ℕ

  The number of clauses with the subject before the object.

• objectFirst : ℕ

  The number of clauses with the object before the subject.

@[instance_reducible]

instance Data.WordOrder.Corpus.instDecidableEqSubjectObjectCounts : DecidableEq SubjectObjectCounts

Equations

• Data.WordOrder.Corpus.instDecidableEqSubjectObjectCounts = Data.WordOrder.Corpus.instDecidableEqSubjectObjectCounts.decEq

def Data.WordOrder.Corpus.instDecidableEqSubjectObjectCounts.decEq (x✝ x✝¹ : SubjectObjectCounts) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instReprSubjectObjectCounts : Repr SubjectObjectCounts

Equations

• Data.WordOrder.Corpus.instReprSubjectObjectCounts = { reprPrec := Data.WordOrder.Corpus.instReprSubjectObjectCounts.repr }

def Data.WordOrder.Corpus.instReprSubjectObjectCounts.repr : SubjectObjectCounts → ℕ → Std.Format

Equations

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

structure Data.WordOrder.Corpus.SubjectObjectStatistics : Type

One language's printed statistics of subject–object order in a corpus, the Shannon entropy of the order and the mutual information between case marking and syntactic role, both in thousandths of a bit.

• language : String

  The language name as the dataset prints it.

• entropy1000 : ℕ

  The Shannon entropy of subject–object order, in thousandths of a bit.

• caseMutualInformation1000 : ℕ

  The mutual information between case marking and syntactic role, in thousandths of a bit.

@[instance_reducible]

instance Data.WordOrder.Corpus.instDecidableEqSubjectObjectStatistics : DecidableEq SubjectObjectStatistics

Equations

• Data.WordOrder.Corpus.instDecidableEqSubjectObjectStatistics = Data.WordOrder.Corpus.instDecidableEqSubjectObjectStatistics.decEq

def Data.WordOrder.Corpus.instDecidableEqSubjectObjectStatistics.decEq (x✝ x✝¹ : SubjectObjectStatistics) : Decidable (x✝ = x✝¹)

Equations

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

def Data.WordOrder.Corpus.instReprSubjectObjectStatistics.repr : SubjectObjectStatistics → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instReprSubjectObjectStatistics : Repr SubjectObjectStatistics

Equations

• Data.WordOrder.Corpus.instReprSubjectObjectStatistics = { reprPrec := Data.WordOrder.Corpus.instReprSubjectObjectStatistics.repr }

structure Data.WordOrder.Corpus.Clause : Type

One annotated declarative clause, with its text type and source text, the order of object and verb, the object's length in words, and whether the object is animate.

• textType : TextType
• source : String

  The title of the source text as the dataset prints it.

• order : ObjectVerb
• objectLength : ℕ

  The length of the object in words.

• animate : Bool

@[instance_reducible]

instance Data.WordOrder.Corpus.instDecidableEqClause : DecidableEq Clause

Equations

• Data.WordOrder.Corpus.instDecidableEqClause = Data.WordOrder.Corpus.instDecidableEqClause.decEq

def Data.WordOrder.Corpus.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Data.WordOrder.Corpus.instReprClause : Repr Clause

Equations

• Data.WordOrder.Corpus.instReprClause = { reprPrec := Data.WordOrder.Corpus.instReprClause.repr }

def Data.WordOrder.Corpus.instReprClause.repr : Clause → ℕ → Std.Format

Equations

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