Krifka2007: experimental results (generated)

Auto-generated from Linglib/Data/Experiments/Krifka2007.json by scripts/gen_experiments.py. Do not edit by hand: edit the JSON and re-run the generator.

Krifka's own corpus counts behind the alignment of expression simplicity with representation simplicity. Average syllable counts of English number words on scales of different granularity, and Google occurrence counts of March 4, 2005 for the words for the multiples of ten from 20 to 90 in decimal Norwegian and vigesimal Danish.

References

• [Kri07a]

inductive Krifka2007.SyllableScale : Type

A scale whose number words are counted for syllables.

• ones : SyllableScale

  ones: one, two, three, four, ... one hundred

• fives : SyllableScale

  fives: one, five, ten, fifteen, ... one hundred

• tens : SyllableScale

  tens: one, ten, twenty, thirty, ... one hundred

• threes : SyllableScale

  threes: three, six, nine, twelve, ... ninety-nine, the odd scale no decimal granularity motivates

• monthsByOne : SyllableScale

  months by one: ages of young children in months, 1 to 24

• monthsCoarse : SyllableScale

  months coarse: ages of young children at 1, 3, 6, 9, 12, 15, 18, 21 and 24 months

@[instance_reducible]

instance Krifka2007.instDecidableEqSyllableScale : DecidableEq SyllableScale

Equations

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

def Krifka2007.instReprSyllableScale.repr : SyllableScale → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Krifka2007.instReprSyllableScale : Repr SyllableScale

Equations

• Krifka2007.instReprSyllableScale = { reprPrec := Krifka2007.instReprSyllableScale.repr }

@[instance_reducible]

instance Krifka2007.instFintypeSyllableScale : Fintype SyllableScale

Equations

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

inductive Krifka2007.Language : Type

The two Scandinavian languages compared.

• norwegian : Language

  Norwegian: decimal number system

• danish : Language

  Danish: vigesimal number system from 50 up

@[instance_reducible]

instance Krifka2007.instDecidableEqLanguage : DecidableEq Language

Equations

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

def Krifka2007.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krifka2007.instReprLanguage.repr Krifka2007.Language.danish prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Language.danish")).group prec✝

@[instance_reducible]

instance Krifka2007.instReprLanguage : Repr Language

Equations

• Krifka2007.instReprLanguage = { reprPrec := Krifka2007.instReprLanguage.repr }

@[instance_reducible]

instance Krifka2007.instFintypeLanguage : Fintype Language

Equations

• Krifka2007.instFintypeLanguage = { elems := { val := ↑Krifka2007.Language.enumList, nodup := Krifka2007.Language.enumList_nodup }, complete := Krifka2007.instFintypeLanguage._proof_1 }

inductive Krifka2007.Word : Type

A Norwegian or Danish word for a multiple of ten.

• tjue : Word

  tjue: Norwegian 20

• tretti : Word

  tretti: Norwegian 30

• foerti : Word

  førti: Norwegian 40

• femti : Word

  femti: Norwegian 50

• seksti : Word

  seksti: Norwegian 60

• sytti : Word

  sytti: Norwegian 70

• aatti : Word

  åtti: Norwegian 80

• nitti : Word

  nitti: Norwegian 90

• tyve : Word

  tyve: Danish 20

• tredive : Word

  tredive: Danish 30

• fyrre : Word

  fyrre: Danish 40

• halvtreds : Word

  halvtreds: Danish 50, shortened from halvtredsindstyve, half-third-times-twenty

• tres : Word

  tres: Danish 60, a score word

• halvfjerds : Word

  halvfjerds: Danish 70, a half-score word

• firs : Word

  firs: Danish 80, a score word

• halvfems : Word

  halvfems: Danish 90, a half-score word

@[instance_reducible]

instance Krifka2007.instDecidableEqWord : DecidableEq Word

Equations

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

def Krifka2007.instReprWord.repr : Word → ℕ → Std.Format

Equations

• Krifka2007.instReprWord.repr Krifka2007.Word.tjue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.tjue")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.tretti prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.tretti")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.foerti prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.foerti")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.femti prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.femti")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.seksti prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.seksti")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.sytti prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.sytti")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.aatti prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.aatti")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.nitti prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.nitti")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.tyve prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.tyve")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.tredive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.tredive")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.fyrre prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.fyrre")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.halvtreds prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.halvtreds")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.tres prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.tres")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.halvfjerds prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.halvfjerds")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.firs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.firs")).group prec✝
• Krifka2007.instReprWord.repr Krifka2007.Word.halvfems prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Word.halvfems")).group prec✝

@[instance_reducible]

instance Krifka2007.instReprWord : Repr Word

Equations

• Krifka2007.instReprWord = { reprPrec := Krifka2007.instReprWord.repr }

@[instance_reducible]

instance Krifka2007.instFintypeWord : Fintype Word

Equations

• Krifka2007.instFintypeWord = { elems := { val := ↑Krifka2007.Word.enumList, nodup := Krifka2007.Word.enumList_nodup }, complete := Krifka2007.instFintypeWord._proof_1 }

def Krifka2007.halvtredsindstyveCount : ℕ

Occurrences of the complete Danish form halvtredsindstyve for 50. ((27) discussion, manuscript p. 10; checked against the page images.)

Equations

• Krifka2007.halvtredsindstyveCount = 1180

def Krifka2007.danishFemtiCount : ℕ

Occurrences of the mostly monetary Danish form femti for 50. ((27) discussion, manuscript p. 10; checked against the page images.)

Equations

• Krifka2007.danishFemtiCount = 988

structure Krifka2007.SyllableCount : Type

A row of (19), (20), manuscript p. 8; (22) averages, manuscript p. 9: the total syllables and the number of words on each scale.

• syllables : ℕ

  The total syllables of its number words.

• words : ℕ

  The number of its number words.

@[instance_reducible]

instance Krifka2007.instDecidableEqSyllableCount : DecidableEq SyllableCount

Equations

• Krifka2007.instDecidableEqSyllableCount = Krifka2007.instDecidableEqSyllableCount.decEq

def Krifka2007.instDecidableEqSyllableCount.decEq (x✝ x✝¹ : SyllableCount) : Decidable (x✝ = x✝¹)

Equations

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

def Krifka2007.instReprSyllableCount.repr : SyllableCount → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Krifka2007.instReprSyllableCount : Repr SyllableCount

Equations

• Krifka2007.instReprSyllableCount = { reprPrec := Krifka2007.instReprSyllableCount.repr }

def Krifka2007.syllableCounts : SyllableScale → SyllableCount

The cells of (19), (20), manuscript p. 8; (22) averages, manuscript p. 9, by scale; checked against the page images.

Equations

• Krifka2007.syllableCounts Krifka2007.SyllableScale.ones = { syllables := 273, words := 100 }
• Krifka2007.syllableCounts Krifka2007.SyllableScale.fives = { syllables := 46, words := 20 }
• Krifka2007.syllableCounts Krifka2007.SyllableScale.tens = { syllables := 21, words := 10 }
• Krifka2007.syllableCounts Krifka2007.SyllableScale.threes = { syllables := 92, words := 33 }
• Krifka2007.syllableCounts Krifka2007.SyllableScale.monthsByOne = { syllables := 44, words := 24 }
• Krifka2007.syllableCounts Krifka2007.SyllableScale.monthsCoarse = { syllables := 25, words := 9 }

structure Krifka2007.WordCount : Type

A row of (27), manuscript p. 10: the Google occurrence counts of March 4, 2005 for each word.

• language : Language

  Its language.

• number : ℕ

  The multiple of ten it names.

• count : ℕ

  Its occurrences.

@[instance_reducible]

instance Krifka2007.instDecidableEqWordCount : DecidableEq WordCount

Equations

• Krifka2007.instDecidableEqWordCount = Krifka2007.instDecidableEqWordCount.decEq

def Krifka2007.instDecidableEqWordCount.decEq (x✝ x✝¹ : WordCount) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Krifka2007.instReprWordCount : Repr WordCount

Equations

• Krifka2007.instReprWordCount = { reprPrec := Krifka2007.instReprWordCount.repr }

def Krifka2007.instReprWordCount.repr : WordCount → ℕ → Std.Format

Equations

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

def Krifka2007.counts : Word → WordCount

The cells of (27), manuscript p. 10, by word; checked against the page images.

Equations

• Krifka2007.counts Krifka2007.Word.tjue = { language := Krifka2007.Language.norwegian, number := 20, count := 61300 }
• Krifka2007.counts Krifka2007.Word.tretti = { language := Krifka2007.Language.norwegian, number := 30, count := 43700 }
• Krifka2007.counts Krifka2007.Word.foerti = { language := Krifka2007.Language.norwegian, number := 40, count := 39200 }
• Krifka2007.counts Krifka2007.Word.femti = { language := Krifka2007.Language.norwegian, number := 50, count := 81200 }
• Krifka2007.counts Krifka2007.Word.seksti = { language := Krifka2007.Language.norwegian, number := 60, count := 19400 }
• Krifka2007.counts Krifka2007.Word.sytti = { language := Krifka2007.Language.norwegian, number := 70, count := 10200 }
• Krifka2007.counts Krifka2007.Word.aatti = { language := Krifka2007.Language.norwegian, number := 80, count := 13100 }
• Krifka2007.counts Krifka2007.Word.nitti = { language := Krifka2007.Language.norwegian, number := 90, count := 13500 }
• Krifka2007.counts Krifka2007.Word.tyve = { language := Krifka2007.Language.danish, number := 20, count := 121000 }
• Krifka2007.counts Krifka2007.Word.tredive = { language := Krifka2007.Language.danish, number := 30, count := 25400 }
• Krifka2007.counts Krifka2007.Word.fyrre = { language := Krifka2007.Language.danish, number := 40, count := 26800 }
• Krifka2007.counts Krifka2007.Word.halvtreds = { language := Krifka2007.Language.danish, number := 50, count := 15500 }
• Krifka2007.counts Krifka2007.Word.tres = { language := Krifka2007.Language.danish, number := 60, count := 36400 }
• Krifka2007.counts Krifka2007.Word.halvfjerds = { language := Krifka2007.Language.danish, number := 70, count := 581 }
• Krifka2007.counts Krifka2007.Word.firs = { language := Krifka2007.Language.danish, number := 80, count := 3740 }
• Krifka2007.counts Krifka2007.Word.halvfems = { language := Krifka2007.Language.danish, number := 90, count := 540 }