Arad (2005): Roots and Patterns: Hebrew Morpho-Syntax

Arad builds every Hebrew verb from a consonantal root under v and Voice. The binyan under v is a CV template with vowel slots but no vowels, the root associates with it as McCarthy proposed, and Voice fills the vowel slots by a spell-out rule whose context is the binyan; a nominal pattern (mišqal) carries its own vowels. A root is interpreted at the first category head merged with it, so a verb formed from a noun does not see the root and is a stem modification of the noun instead. Conjugation classes pair the binyanim of an alternation, and two tendencies, against conjugating a binyan with itself and against mixing geminate and non-geminate templates, single out the natural pairs.

Main statements

• words_derived_seg: over the fragment's roots and segments, every root-derived word of the data is derived but five verbs whose guttural, metathesis or geminate-root phonology is not modelled.
• spirantize_before_degeminate: the opposite order would give *sifer, *qivel, *hitraxex.
• denominals: every noun-derived verb is a stem modification of its base, except the {o, e} verbs of (41a, b), and none is the verb its base's root derives.
• conjugations_natural: conjugation classes 1–4 are the natural pairs of (57), and 5 and 6 each break one tendency.

Implementation notes

• Root-to-template association follows McCarthy, as p. 43 says it does. CVCCVC and hitCVCCVC undergo McCarthy's Erasure, like Arabic II and V. The book gives the extra slot (p. 28) but no association apparatus of its own (Ch. 6, fn. 1).
• The book states no stem-modification rule (p. 50). IsStemModification checks the properties it names instead: the prefix is carried, the base's consonants occur in order, and the vowels are Voice's (Bat El's melodic overwriting, p. 47). A + in the base marks the suffixes (32) prints as outside the stem.
• The derivations run over the book's transcription, and a relabeling lifts them to the fragment's segments. There the alternating stops are archisegments that spirantization realizes by continuancy, as the one stop or fricative of the inventory that refines them.
• The data's patterns 1–7 are the numbers of (3). Ch. 7 prints CaCaC, hiCCiC, CiCCeC and hitCaCCeC, which p. 43 equates with them.
• The prose of p. 226 says "insertable below v" where its grid says "above". The grid is read.

TODO

• Guttural lowering (hexšiv, heʔedim), t–sibilant metathesis (histager) and the biliteral allomorphy of √mss (namas, hemes, fn. 33).
• The {o, e} vocalism of (41a, b), which (25) does not list.
• (34)–(35), failed stem modification and recognizability, whose phonology the book leaves open.
• Conditions on insertion (16), the diacritic spell-out rules of §6.2.6.4, and the arguments against Doron's and Aronoff's analyses of the binyanim (Ch. 5).

References

• [Ara05]
• [McC81]
• [BE94]
• [Dor03]
• [Aro94]

The binyanim (24b)

inductive Arad2005.Binyan : Type

A binyan is one of the five templates of (24b). Patterns 4 and 6 of (3) are the passive vocalisms of CVCCVC and hVCCVC (25).

• cvcvc : Binyan
• nvccvc : Binyan
• cvccvc : Binyan
• hvccvc : Binyan
• hitcvccvc : Binyan

@[instance_reducible]

instance Arad2005.instDecidableEqBinyan : DecidableEq Binyan

Equations

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

def Arad2005.instReprBinyan.repr : Binyan → ℕ → Std.Format

Equations

• Arad2005.instReprBinyan.repr Arad2005.Binyan.cvcvc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Binyan.cvcvc")).group prec✝
• Arad2005.instReprBinyan.repr Arad2005.Binyan.nvccvc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Binyan.nvccvc")).group prec✝
• Arad2005.instReprBinyan.repr Arad2005.Binyan.cvccvc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Binyan.cvccvc")).group prec✝
• Arad2005.instReprBinyan.repr Arad2005.Binyan.hvccvc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Binyan.hvccvc")).group prec✝
• Arad2005.instReprBinyan.repr Arad2005.Binyan.hitcvccvc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Binyan.hitcvccvc")).group prec✝

@[instance_reducible]

instance Arad2005.instReprBinyan : Repr Binyan

Equations

• Arad2005.instReprBinyan = { reprPrec := Arad2005.instReprBinyan.repr }

@[instance_reducible]

instance Arad2005.instFintypeBinyan : Fintype Binyan

Equations

• Arad2005.instFintypeBinyan = { elems := { val := ↑Arad2005.Binyan.enumList, nodup := Arad2005.Binyan.enumList_nodup }, complete := Arad2005.instFintypeBinyan._proof_1 }

structure Arad2005.Prefixes (α : Type u_3) : Type u_3

Prefixes α holds the prefixal segments, the n- of nVCCVC, h- of hVCCVC, h-i-t of hitCVCCVC, and m-, t- of the mišqalim (24a).

• n : α

  n is the n of nVCCVC.

• h : α

  h is the h of hVCCVC and hitCVCCVC.

• i : α

  i is the i of hitCVCCVC.

• t : α

  t is the t of hitCVCCVC and taCCiC.

• m : α

  m is the m of the mišqalim.

def Arad2005.Prefixes.map {α : Type u_1} {β : Type u_2} (f : α → β) (px : Prefixes α) : Prefixes β

px.map f relabels the prefixes by f.

Equations

• Arad2005.Prefixes.map f px = { n := f px.n, h := f px.h, i := f px.i, t := f px.t, m := f px.m }

def Arad2005.Binyan.template : Binyan → Morphology.CVTemplate

b.template is the CV template of the binyan b.

Equations

• One or more equations did not get rendered due to their size.
• Arad2005.Binyan.cvcvc.template = McCarthy1981.cvcvc
• Arad2005.Binyan.nvccvc.template = McCarthy1981.cvccvc
• Arad2005.Binyan.cvccvc.template = McCarthy1981.cvccvc
• Arad2005.Binyan.hvccvc.template = McCarthy1981.cvccvc

def Arad2005.Binyan.prefix {α : Type u_1} (px : Prefixes α) : Binyan → List α

b.prefix px is the prefix of the binyan b.

Equations

• Arad2005.Binyan.prefix px Arad2005.Binyan.cvcvc = []
• Arad2005.Binyan.prefix px Arad2005.Binyan.cvccvc = []
• Arad2005.Binyan.prefix px Arad2005.Binyan.nvccvc = [px.n]
• Arad2005.Binyan.prefix px Arad2005.Binyan.hvccvc = [px.h]
• Arad2005.Binyan.prefix px Arad2005.Binyan.hitcvccvc = [px.h, px.i, px.t]

def Arad2005.Binyan.erasure : Binyan → Bool

The binyanim that undergo McCarthy's Erasure are CVCCVC and hitCVCCVC, the Hebrew counterparts of Arabic II and V, whose extra slot holds the geminate (p. 28).

Equations

• Arad2005.Binyan.cvccvc.erasure = true
• Arad2005.Binyan.hitcvccvc.erasure = true
• x✝.erasure = false

def Arad2005.place {α : Type u_1} (pre : List α) (t : Morphology.CVTemplate) (r : Morphology.ConsonantalRoot α) : Morphology.TemplateMatch α

place pre t r puts the prefix pre on the leftmost slots of t, with the root r not yet associated.

Equations

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

def Arad2005.consonantism {α : Type u_1} (px : Prefixes α) (b : Binyan) (r : Morphology.ConsonantalRoot α) : Morphology.TemplateMatch α

The consonantism of a binyan places its prefix, associates the root by the conventions and, under Erasure, applies the conventions again ([McC81]).

Equations

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

Voice (25)

inductive Arad2005.Voice : Type

Voice is the value of the Voice head, active or passive.

• active : Voice
• passive : Voice

@[instance_reducible]

instance Arad2005.instDecidableEqVoice : DecidableEq Voice

Equations

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

def Arad2005.instReprVoice.repr : Voice → ℕ → Std.Format

Equations

• Arad2005.instReprVoice.repr Arad2005.Voice.active prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Voice.active")).group prec✝
• Arad2005.instReprVoice.repr Arad2005.Voice.passive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Voice.passive")).group prec✝

@[instance_reducible]

instance Arad2005.instReprVoice : Repr Voice

Equations

• Arad2005.instReprVoice = { reprPrec := Arad2005.instReprVoice.repr }

@[instance_reducible]

instance Arad2005.instFintypeVoice : Fintype Voice

Equations

• Arad2005.instFintypeVoice = { elems := { val := ↑Arad2005.Voice.enumList, nodup := Arad2005.Voice.enumList_nodup }, complete := Arad2005.instFintypeVoice._proof_1 }

inductive Arad2005.Vowel : Type

Vowel lists the vowels of the transcription.

• a : Vowel
• e : Vowel
• i : Vowel
• o : Vowel
• u : Vowel

@[instance_reducible]

instance Arad2005.instDecidableEqVowel : DecidableEq Vowel

Equations

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

@[instance_reducible]

instance Arad2005.instReprVowel : Repr Vowel

Equations

• Arad2005.instReprVowel = { reprPrec := Arad2005.instReprVowel.repr }

def Arad2005.instReprVowel.repr : Vowel → ℕ → Std.Format

Equations

• Arad2005.instReprVowel.repr Arad2005.Vowel.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Vowel.a")).group prec✝
• Arad2005.instReprVowel.repr Arad2005.Vowel.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Vowel.e")).group prec✝
• Arad2005.instReprVowel.repr Arad2005.Vowel.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Vowel.i")).group prec✝
• Arad2005.instReprVowel.repr Arad2005.Vowel.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Vowel.o")).group prec✝
• Arad2005.instReprVowel.repr Arad2005.Vowel.u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Vowel.u")).group prec✝

inductive Arad2005.Feature : Type

A feature of Voice's vocabulary is a value of Voice or the binyan inserted under v.

• voice (v : Voice) : Feature
• binyan (b : Binyan) : Feature

def Arad2005.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

• Arad2005.instDecidableEqFeature.decEq (Arad2005.Feature.voice a) (Arad2005.Feature.voice b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Arad2005.instDecidableEqFeature.decEq (Arad2005.Feature.voice v) (Arad2005.Feature.binyan b) = isFalse ⋯
• Arad2005.instDecidableEqFeature.decEq (Arad2005.Feature.binyan b) (Arad2005.Feature.voice v) = isFalse ⋯
• Arad2005.instDecidableEqFeature.decEq (Arad2005.Feature.binyan a) (Arad2005.Feature.binyan b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Arad2005.instDecidableEqFeature : DecidableEq Feature

Equations

• Arad2005.instDecidableEqFeature = Arad2005.instDecidableEqFeature.decEq

@[instance_reducible]

instance Arad2005.instReprFeature : Repr Feature

Equations

• Arad2005.instReprFeature = { reprPrec := Arad2005.instReprFeature.repr }

def Arad2005.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

inductive Arad2005.Exponent : Type

An exponent of Voice is a vocalism for the binyan's vowel slots, or a binyan with its own vowels in place of the one under v, as niCCaC is the passive of CaCaC (fn. 13).

• vocalism (vs : List Vowel) : Exponent
• rewrite (b : Binyan) (vs : List Vowel) : Exponent

def Arad2005.instDecidableEqExponent.decEq (x✝ x✝¹ : Exponent) : Decidable (x✝ = x✝¹)

Equations

• Arad2005.instDecidableEqExponent.decEq (Arad2005.Exponent.vocalism a) (Arad2005.Exponent.vocalism b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Arad2005.instDecidableEqExponent.decEq (Arad2005.Exponent.vocalism vs) (Arad2005.Exponent.rewrite b vs_1) = isFalse ⋯
• Arad2005.instDecidableEqExponent.decEq (Arad2005.Exponent.rewrite b vs) (Arad2005.Exponent.vocalism vs_1) = isFalse ⋯
• Arad2005.instDecidableEqExponent.decEq (Arad2005.Exponent.rewrite a a_1) (Arad2005.Exponent.rewrite b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Arad2005.instDecidableEqExponent : DecidableEq Exponent

Equations

• Arad2005.instDecidableEqExponent = Arad2005.instDecidableEqExponent.decEq

def Arad2005.instReprExponent.repr : Exponent → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Arad2005.instReprExponent : Repr Exponent

Equations

• Arad2005.instReprExponent = { reprPrec := Arad2005.instReprExponent.repr }

def Arad2005.voiceSpellout : List (DistributedMorphology.VocabularyItem Feature Exponent)

voiceSpellout lists the Voice spell-out (25), each item in the context of a binyan inserted under v.

Equations

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

def Arad2005.voiceNode (b : Binyan) (v : Voice) : DistributedMorphology.Neighborhood (List Feature)

The Voice node, once v has been spelled out, carries its value and has the binyan as its inner neighbor.

Equations

• Arad2005.voiceNode b v = { focus := [Arad2005.Feature.voice v], leftCtx := [[Arad2005.Feature.binyan b]] }

def Arad2005.realizeVoice (b : Binyan) (v : Voice) : Option (Binyan × List Vowel)

realizeVoice b v is the binyan and the vowels of a verb, Voice being spelled out in the context of b.

Equations

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

def Arad2005.Binyan.Intransitive (b : Binyan) : Prop

The binyanim (11) marks [−tr.].

Equations

• b.Intransitive = (b = Arad2005.Binyan.nvccvc ∨ b = Arad2005.Binyan.hitcvccvc)

@[instance_reducible]

instance Arad2005.instDecidablePredBinyanIntransitive : DecidablePred Binyan.Intransitive

Equations

• Arad2005.instDecidablePredBinyanIntransitive x✝ = { decide := decide (x✝ = Arad2005.Binyan.nvccvc) || decide (x✝ = Arad2005.Binyan.hitcvccvc), reflects_decide := ⋯ }

theorem Arad2005.realizeVoice_isSome : (∀ (b : Binyan) (v : Voice), (realizeVoice b v).isSome = true ↔ v = Voice.active ∨ ¬b.Intransitive) ∧ ∀ x ∈ realizeVoice Binyan.cvcvc Voice.passive, x.1.Intransitive

Voice is spelled out in every binyan in the active, and in the passive exactly in the binyanim (11) does not mark [−tr.]; the binyan that replaces CVCVC in the passive is one (11) marks.

The stem

def Arad2005.vocalize {α : Type u_1} (px : Prefixes α) (v : Vowel → α) (b : Binyan) (vs : List Vowel) (r : Morphology.ConsonantalRoot α) : Morphology.TemplateMatch α

vocalize associates a vocalism with the consonantism by the conventions.

Equations

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

def Arad2005.stem {α : Type u_1} (px : Prefixes α) (v : Vowel → α) (b : Binyan) (voice : Voice) (r : Morphology.ConsonantalRoot α) : Option (Morphology.TemplateMatch α)

The stem of a root-derived verb has the binyan under v, Voice's vowels in its context and the root associated with it (p. 43). It is none where Voice has no exponent.

Equations

• Arad2005.stem px v b voice r = Option.map (fun (x : Arad2005.Binyan × List Arad2005.Vowel) => Arad2005.vocalize px v x.1 x.2 r) (Arad2005.realizeVoice b voice)

Spirantization and degemination (pp. 28–29)

def Arad2005.sameElement (a b : Morphology.Association) : Bool

sameElement a b says that two lines come from one melodic element.

Equations

• Arad2005.sameElement a b = (a.source == b.source && a.melodyIndex == b.melodyIndex)

def Arad2005.linked {α : Type u_1} (m : Morphology.TemplateMatch α) : List (ℕ × Morphology.Association × α)

linked m lists each slot with its first line and that line's segment.

Equations

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

def Arad2005.spirantize {α : Type u_1} (f : Bool → α → α) (m : Morphology.TemplateMatch α) : List (ℕ × Morphology.Association × α)

spirantize f m realizes each segment by f, given whether it follows a V-slot and is not the first slot of a geminate, whose element also occupies the next slot.

Equations

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

def Arad2005.degeminate {α : Type u_1} (l : List (ℕ × Morphology.Association × α)) : List α

Since Modern Hebrew has no geminates (p. 28), slots linked to one element surface once.

Equations

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

def Arad2005.surface {α : Type u_1} (f : Bool → α → α) (m : Morphology.TemplateMatch α) : List α

surface f m is the stem spirantized by f and degeminated.

Equations

• Arad2005.surface f m = Arad2005.degeminate (Arad2005.spirantize f m)

def Arad2005.verb {α : Type u_1} (px : Prefixes α) (v : Vowel → α) (f : Bool → α → α) (b : Binyan) (voice : Voice) (r : Morphology.ConsonantalRoot α) : Option (List α)

verb is the surface of the stem of a root-derived verb.

Equations

• Arad2005.verb px v f b voice r = Option.map (Arad2005.surface f) (Arad2005.stem px v b voice r)

def Arad2005.surfaceDegeminatedFirst {α : Type u_1} (isV : α → Bool) (f : Bool → α → α) (m : Morphology.TemplateMatch α) : List α

surfaceDegeminatedFirst applies the rules in the order the book rules out, degemination before the spirantization of whatever follows a vowel.

Equations

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

The mišqalim (24a)

inductive Arad2005.Mishqal : Type

Mishqal lists the nominal patterns of (24a) and those Ch. 7 prints.

• miCCaC : Mishqal
• miCCoC : Mishqal
• maCCeC : Mishqal
• taCCiC : Mishqal
• CCaC : Mishqal
• CaCiC : Mishqal
• CeCeC : Mishqal
• CaCeC : Mishqal
• CuCaC : Mishqal

@[instance_reducible]

instance Arad2005.instDecidableEqMishqal : DecidableEq Mishqal

Equations

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

def Arad2005.instReprMishqal.repr : Mishqal → ℕ → Std.Format

Equations

• Arad2005.instReprMishqal.repr Arad2005.Mishqal.miCCaC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Mishqal.miCCaC")).group prec✝
• Arad2005.instReprMishqal.repr Arad2005.Mishqal.miCCoC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Mishqal.miCCoC")).group prec✝
• Arad2005.instReprMishqal.repr Arad2005.Mishqal.maCCeC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Mishqal.maCCeC")).group prec✝
• Arad2005.instReprMishqal.repr Arad2005.Mishqal.taCCiC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Mishqal.taCCiC")).group prec✝
• Arad2005.instReprMishqal.repr Arad2005.Mishqal.CCaC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Mishqal.CCaC")).group prec✝
• Arad2005.instReprMishqal.repr Arad2005.Mishqal.CaCiC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Mishqal.CaCiC")).group prec✝
• Arad2005.instReprMishqal.repr Arad2005.Mishqal.CeCeC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Mishqal.CeCeC")).group prec✝
• Arad2005.instReprMishqal.repr Arad2005.Mishqal.CaCeC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Mishqal.CaCeC")).group prec✝
• Arad2005.instReprMishqal.repr Arad2005.Mishqal.CuCaC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Mishqal.CuCaC")).group prec✝

@[instance_reducible]

instance Arad2005.instReprMishqal : Repr Mishqal

Equations

• Arad2005.instReprMishqal = { reprPrec := Arad2005.instReprMishqal.repr }

@[instance_reducible]

instance Arad2005.instFintypeMishqal : Fintype Mishqal

Equations

• Arad2005.instFintypeMishqal = { elems := { val := ↑Arad2005.Mishqal.enumList, nodup := Arad2005.Mishqal.enumList_nodup }, complete := Arad2005.instFintypeMishqal._proof_1 }

def Arad2005.Mishqal.template : Mishqal → Morphology.CVTemplate

q.template is the CV template of the mišqal q.

Equations

• Arad2005.Mishqal.miCCaC.template = McCarthy1981.cvccvc
• Arad2005.Mishqal.miCCoC.template = McCarthy1981.cvccvc
• Arad2005.Mishqal.maCCeC.template = McCarthy1981.cvccvc
• Arad2005.Mishqal.taCCiC.template = McCarthy1981.cvccvc
• Arad2005.Mishqal.CCaC.template = { slots := [Morphology.CVSlot.C, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C] }
• Arad2005.Mishqal.CaCiC.template = McCarthy1981.cvcvc
• Arad2005.Mishqal.CeCeC.template = McCarthy1981.cvcvc
• Arad2005.Mishqal.CaCeC.template = McCarthy1981.cvcvc
• Arad2005.Mishqal.CuCaC.template = McCarthy1981.cvcvc

def Arad2005.Mishqal.prefix {α : Type u_1} (px : Prefixes α) : Mishqal → List α

q.prefix px is the prefix of the mišqal q.

Equations

• Arad2005.Mishqal.prefix px Arad2005.Mishqal.miCCaC = [px.m]
• Arad2005.Mishqal.prefix px Arad2005.Mishqal.miCCoC = [px.m]
• Arad2005.Mishqal.prefix px Arad2005.Mishqal.maCCeC = [px.m]
• Arad2005.Mishqal.prefix px Arad2005.Mishqal.taCCiC = [px.t]
• Arad2005.Mishqal.prefix px x✝ = []

def Arad2005.Mishqal.vowels : Mishqal → List Vowel

q.vowels are the mišqal's own vowels.

Equations

• Arad2005.Mishqal.miCCaC.vowels = [Arad2005.Vowel.i, Arad2005.Vowel.a]
• Arad2005.Mishqal.miCCoC.vowels = [Arad2005.Vowel.i, Arad2005.Vowel.o]
• Arad2005.Mishqal.maCCeC.vowels = [Arad2005.Vowel.a, Arad2005.Vowel.e]
• Arad2005.Mishqal.taCCiC.vowels = [Arad2005.Vowel.a, Arad2005.Vowel.i]
• Arad2005.Mishqal.CCaC.vowels = [Arad2005.Vowel.a]
• Arad2005.Mishqal.CaCiC.vowels = [Arad2005.Vowel.a, Arad2005.Vowel.i]
• Arad2005.Mishqal.CeCeC.vowels = [Arad2005.Vowel.e, Arad2005.Vowel.e]
• Arad2005.Mishqal.CaCeC.vowels = [Arad2005.Vowel.a, Arad2005.Vowel.e]
• Arad2005.Mishqal.CuCaC.vowels = [Arad2005.Vowel.u, Arad2005.Vowel.a]

def Arad2005.nounStem {α : Type u_1} (px : Prefixes α) (v : Vowel → α) (q : Mishqal) (r : Morphology.ConsonantalRoot α) : Morphology.TemplateMatch α

The stem of a root-derived noun associates the root and the mišqal's own vowels with its template.

Equations

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

Relabeling

theorem Arad2005.place_map {α : Type u_1} {β : Type u_2} (f : α → β) (pre : List α) (t : Morphology.CVTemplate) (r : Morphology.ConsonantalRoot α) : place (List.map f pre) t (Morphology.ConsonantalRoot.map f r) = (place pre t r).map f

theorem Arad2005.prefix_map {α : Type u_1} {β : Type u_2} (f : α → β) (px : Prefixes α) (b : Binyan) : Binyan.prefix (Prefixes.map f px) b = List.map f (Binyan.prefix px b)

theorem Arad2005.consonantism_map {α : Type u_1} {β : Type u_2} (f : α → β) (px : Prefixes α) (b : Binyan) (r : Morphology.ConsonantalRoot α) : consonantism (Prefixes.map f px) b (Morphology.ConsonantalRoot.map f r) = (consonantism px b r).map f

theorem Arad2005.vocalize_map {α : Type u_1} {β : Type u_2} (f : α → β) (px : Prefixes α) (v : Vowel → α) (b : Binyan) (vs : List Vowel) (r : Morphology.ConsonantalRoot α) : vocalize (Prefixes.map f px) (f ∘ v) b vs (Morphology.ConsonantalRoot.map f r) = (vocalize px v b vs r).map f

theorem Arad2005.stem_map {α : Type u_1} {β : Type u_2} (f : α → β) (px : Prefixes α) (v : Vowel → α) (b : Binyan) (voice : Voice) (r : Morphology.ConsonantalRoot α) : stem (Prefixes.map f px) (f ∘ v) b voice (Morphology.ConsonantalRoot.map f r) = Option.map (fun (x : Morphology.TemplateMatch α) => x.map f) (stem px v b voice r)

theorem Arad2005.nounStem_map {α : Type u_1} {β : Type u_2} (f : α → β) (px : Prefixes α) (v : Vowel → α) (q : Mishqal) (r : Morphology.ConsonantalRoot α) : nounStem (Prefixes.map f px) (f ∘ v) q (Morphology.ConsonantalRoot.map f r) = (nounStem px v q r).map f

theorem Arad2005.linked_map {α : Type u_1} {β : Type u_2} (f : α → β) (m : Morphology.TemplateMatch α) : linked (m.map f) = List.map (fun (x : ℕ × Morphology.Association × α) => match x with | (i, a, x) => (i, a, f x)) (linked m)

theorem Arad2005.spirantize_map {α : Type u_1} {β : Type u_2} (g h : α → β) (f : Bool → α → α) (f' : Bool → β → β) (hf : ∀ (b : Bool) (x : α), f' b (g x) = h (f b x)) (m : Morphology.TemplateMatch α) : spirantize f' (m.map g) = List.map (fun (x : ℕ × Morphology.Association × α) => match x with | (i, a, x) => (i, a, h x)) (spirantize f m)

Spirantization commutes with relabeling the underlying segments by g and the surface segments by h, where the two realizations agree.

theorem Arad2005.surface_map {α : Type u_1} {β : Type u_2} (g h : α → β) (f : Bool → α → α) (f' : Bool → β → β) (hf : ∀ (b : Bool) (x : α), f' b (g x) = h (f b x)) (m : Morphology.TemplateMatch α) : surface f' (m.map g) = List.map h (surface f m)

theorem Arad2005.verb_map {α : Type u_1} {β : Type u_2} (g h : α → β) (f : Bool → α → α) (f' : Bool → β → β) (hf : ∀ (b : Bool) (x : α), f' b (g x) = h (f b x)) (px : Prefixes α) (v : Vowel → α) (b : Binyan) (voice : Voice) (r : Morphology.ConsonantalRoot α) : verb (Prefixes.map g px) (g ∘ v) f' b voice (Morphology.ConsonantalRoot.map g r) = Option.map (fun (x : List α) => List.map h x) (verb px v f b voice r)

A verb over relabeled underlying segments is the relabeled surface verb.

The geminate slot and the vowel slots

def Arad2005.numeralPx : Prefixes ℕ

numeralPx numbers the prefixes for symbolic statements.

Equations

• Arad2005.numeralPx = { n := 100, h := 101, i := 102, t := 103, m := 104 }

def Arad2005.numeralVowel : Vowel → ℕ

numeralVowel numbers the vowels.

Equations

• Arad2005.numeralVowel Arad2005.Vowel.a = 200
• Arad2005.numeralVowel Arad2005.Vowel.e = 201
• Arad2005.numeralVowel Arad2005.Vowel.i = 202
• Arad2005.numeralVowel Arad2005.Vowel.o = 203
• Arad2005.numeralVowel Arad2005.Vowel.u = 204

def Arad2005.label {α : Type u_1} (px : Prefixes α) (v : Vowel → α) (rad : List α) (d : α) : ℕ → α

label sends the numerals back to radicals, prefixes and vowels.

Equations

• Arad2005.label px v rad d 100 = px.n
• Arad2005.label px v rad d 101 = px.h
• Arad2005.label px v rad d 102 = px.i
• Arad2005.label px v rad d 103 = px.t
• Arad2005.label px v rad d 104 = px.m
• Arad2005.label px v rad d 200 = v Arad2005.Vowel.a
• Arad2005.label px v rad d 201 = v Arad2005.Vowel.e
• Arad2005.label px v rad d 202 = v Arad2005.Vowel.i
• Arad2005.label px v rad d 203 = v Arad2005.Vowel.o
• Arad2005.label px v rad d 204 = v Arad2005.Vowel.u
• Arad2005.label px v rad d x✝ = rad.getD x✝ d

theorem Arad2005.numeralPx_map {α : Type u_1} (px : Prefixes α) (v : Vowel → α) (rad : List α) (d : α) : Prefixes.map (label px v rad d) numeralPx = px

theorem Arad2005.label_comp_numeralVowel {α : Type u_1} (px : Prefixes α) (v : Vowel → α) (rad : List α) (d : α) : label px v rad d ∘ numeralVowel = v

theorem Arad2005.consonantism_cvccvc {α : Type u_1} (px : Prefixes α) (w x y z : α) : (consonantism px Binyan.cvccvc { segments := [x, y, z] }).spellout = [x, y, y, z] ∧ (consonantism px Binyan.cvccvc { segments := [w, x, y, z] }).spellout = [w, x, y, z]

In CVCCVC a triliteral root doubles its middle radical, one element on two slots, and a quadriliteral root fills the extra slot, as in tirgem (p. 28).

theorem Arad2005.freeBearers_vocalism {α : Type u_1} (px : Prefixes α) (v : Vowel → α) (x y z : α) : (∀ (b : Binyan), ((consonantism px b { segments := [x, y, z] }).freeBearers Morphology.AssocSource.vocalism).length = 2) ∧ ∀ (q : Mishqal), (nounStem px v q { segments := [x, y, z] }).freeBearers Morphology.AssocSource.vocalism = []

A binyan has two vowel slots that the root leaves empty for Voice, while a mišqal fills its own (24), which is the noun–verb asymmetry of §2.5.

The data

def Arad2005.transcribedPx : Prefixes String

transcribedPx gives the prefixes in the book's transcription.

Equations

• Arad2005.transcribedPx = { n := "n", h := "h", i := "i", t := "t", m := "m" }

def Arad2005.Vowel.transcription : Vowel → String

v.transcription is the vowel v in the book's transcription.

Equations

• Arad2005.Vowel.a.transcription = "a"
• Arad2005.Vowel.e.transcription = "e"
• Arad2005.Vowel.i.transcription = "i"
• Arad2005.Vowel.o.transcription = "o"
• Arad2005.Vowel.u.transcription = "u"

def Arad2005.isVowel (s : String) : Bool

isVowel s says that the transcribed segment s is a vowel.

Equations

• Arad2005.isVowel s = decide (s ∈ ["a", "e", "i", "o", "u"])

def Arad2005.fricative : Bool → String → String

fricative post x is the radical x after a vowel (post) or elsewhere, the stops p, b, k spirantizing to f, v, x after a vowel (p. 29).

Equations

• Arad2005.fricative true "p" = "f"
• Arad2005.fricative true "b" = "v"
• Arad2005.fricative true "k" = "x"
• Arad2005.fricative x✝¹ x✝ = x✝

def Arad2005.binyan? : String → Option (Binyan × Voice)

binyan? reads a pattern number of (3) as a binyan and a voice, 4 and 6 being the passives of 3 and 5.

Equations

• Arad2005.binyan? "1" = some (Arad2005.Binyan.cvcvc, Arad2005.Voice.active)
• Arad2005.binyan? "2" = some (Arad2005.Binyan.nvccvc, Arad2005.Voice.active)
• Arad2005.binyan? "3" = some (Arad2005.Binyan.cvccvc, Arad2005.Voice.active)
• Arad2005.binyan? "4" = some (Arad2005.Binyan.cvccvc, Arad2005.Voice.passive)
• Arad2005.binyan? "5" = some (Arad2005.Binyan.hvccvc, Arad2005.Voice.active)
• Arad2005.binyan? "6" = some (Arad2005.Binyan.hvccvc, Arad2005.Voice.passive)
• Arad2005.binyan? "7" = some (Arad2005.Binyan.hitcvccvc, Arad2005.Voice.active)
• Arad2005.binyan? x✝ = none

def Arad2005.mishqal? : String → Option Mishqal

mishqal? reads a printed pattern as a mišqal.

Equations

• Arad2005.mishqal? "miCCaC" = some Arad2005.Mishqal.miCCaC
• Arad2005.mishqal? "miCCoC" = some Arad2005.Mishqal.miCCoC
• Arad2005.mishqal? "maCCeC" = some Arad2005.Mishqal.maCCeC
• Arad2005.mishqal? "taCCiC" = some Arad2005.Mishqal.taCCiC
• Arad2005.mishqal? "CCaC" = some Arad2005.Mishqal.CCaC
• Arad2005.mishqal? "CaCiC" = some Arad2005.Mishqal.CaCiC
• Arad2005.mishqal? "CeCeC" = some Arad2005.Mishqal.CeCeC
• Arad2005.mishqal? "CaCeC" = some Arad2005.Mishqal.CaCeC
• Arad2005.mishqal? "CuCaC" = some Arad2005.Mishqal.CuCaC
• Arad2005.mishqal? x✝ = none

def Arad2005.root? : String → Option (Morphology.ConsonantalRoot String)

root? label is the root of a label of the data in the book's transcription, in which q is the /k/ of ק and b, k, p spirantize.

Equations

• Arad2005.root? "lmd" = some { segments := ["l", "m", "d"] }
• Arad2005.root? "spr" = some { segments := ["s", "p", "r"] }
• Arad2005.root? "qlt" = some { segments := ["q", "l", "t"] }
• Arad2005.root? "pll" = some { segments := ["p", "l", "l"] }
• Arad2005.root? "npc" = some { segments := ["n", "p", "c"] }
• Arad2005.root? "xlq" = some { segments := ["x", "l", "q"] }
• Arad2005.root? "str" = some { segments := ["s", "t", "r"] }
• Arad2005.root? "pqd" = some { segments := ["p", "q", "d"] }
• Arad2005.root? "šmr" = some { segments := ["š", "m", "r"] }
• Arad2005.root? "trgm" = some { segments := ["t", "r", "g", "m"] }
• Arad2005.root? "qbl" = some { segments := ["q", "b", "l"] }
• Arad2005.root? "rkk" = some { segments := ["r", "k", "k"] }
• Arad2005.root? "šmn" = some { segments := ["š", "m", "n"] }
• Arad2005.root? "xšb" = some { segments := ["x", "š", "b"] }
• Arad2005.root? "sgr" = some { segments := ["s", "g", "r"] }
• Arad2005.root? "ptx" = some { segments := ["p", "t", "x"] }
• Arad2005.root? "qpʔ" = some { segments := ["q", "p", "ʔ"] }
• Arad2005.root? "mss" = some { segments := ["m", "s", "s"] }
• Arad2005.root? "xmm" = some { segments := ["x", "m", "m"] }
• Arad2005.root? "bhr" = some { segments := ["b", "h", "r"] }
• Arad2005.root? "ʔdm" = some { segments := ["ʔ", "d", "m"] }
• Arad2005.root? x✝ = none

def Arad2005.verbCell? (a : Forms.Analysis) : Option (Binyan × Voice × Morphology.ConsonantalRoot String)

verbCell? reads the binyan, voice and root of a root-derived verb of the book's analysis.

Equations

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

def Arad2005.nounCell? (a : Forms.Analysis) : Option (Mishqal × Morphology.ConsonantalRoot String)

nounCell? reads the mišqal and root of a root-derived noun of the book's analysis.

Equations

• Arad2005.nounCell? a = (a.pattern.bind Arad2005.mishqal?).bind fun (q : Arad2005.Mishqal) => Option.map (fun (x : Morphology.ConsonantalRoot String) => (q, x)) (a.root.bind Arad2005.root?)

theorem Arad2005.isSome_verbCell? (a : Forms.Analysis) : a ∈ Forms.analyses → a.root.isSome = true → a.form.lexeme.pos = ↑UD.UPOS.VERB → (verbCell? a).isSome = true

Every verb with a root has its cell.

theorem Arad2005.verbs_derived : List.map (fun (x : Forms.Analysis) => x.form.form) (List.filter (fun (a : Forms.Analysis) => decide (a.conjugation = none ∧ ∃ x ∈ verbCell? a, verb transcribedPx Vowel.transcription fricative x.1 x.2.1 x.2.2 ≠ some a.form.segments)) Forms.analyses) = ["hexšiv", "histager"]

The derivation produces every root-derived verb of Ch. 2 and Ch. 7 except two. hexšiv lowers i next to the guttural, and histager metathesizes t and the sibilant.

theorem Arad2005.nouns_derived (a : Forms.Analysis) : a ∈ Forms.analyses → ∀ x ∈ nounCell? a, surface fricative (nounStem transcribedPx Vowel.transcription x.1 x.2) = a.form.segments

The derivation produces every noun of the data in a mišqal of (24a) or of Ch. 7, with the mišqal's own vowels.

theorem Arad2005.passive_lamad : verb transcribedPx Vowel.transcription fricative Binyan.cvcvc Voice.passive { segments := ["l", "m", "d"] } = some ["n", "i", "l", "m", "a", "d"]

The passive of lamad is the binyan nVCCVC, nilmad (25), (3).

theorem Arad2005.spirantize_before_degeminate : List.map (fun (x : Binyan × Morphology.ConsonantalRoot String) => match x with | (b, r) => Option.map (fun (m : Morphology.TemplateMatch String) => (surface fricative m, surfaceDegeminatedFirst isVowel fricative m)) (stem transcribedPx Vowel.transcription b Voice.active r)) [(Binyan.cvccvc, { segments := ["s", "p", "r"] }), (Binyan.cvccvc, { segments := ["q", "b", "l"] }), (Binyan.hitcvccvc, { segments := ["r", "k", "k"] })] = [some (["s", "i", "p", "e", "r"], ["s", "i", "f", "e", "r"]), some (["q", "i", "b", "e", "l"], ["q", "i", "v", "e", "l"]), some (["h", "i", "t", "r", "a", "k", "e", "x"], ["h", "i", "t", "r", "a", "x", "e", "x"])]

Spirantization applies before degemination. In the opposite order the geminate would spirantize, giving *sifer, *qivel, *hitraxex for siper, qibel, hitrakex (p. 29).

Noun-derived verbs (§2.6, §7.5)

def Arad2005.consonants {α : Type u_1} (isV : α → Bool) (w : List α) : List α

consonants isV w keeps the consonants of w.

Equations

• Arad2005.consonants isV w = List.filter (fun (x : α) => !isV x) w

def Arad2005.vowels {α : Type u_1} (isV : α → Bool) (w : List α) : List α

vowels isV w keeps the vowels of w.

Equations

• Arad2005.vowels isV w = List.filter isV w

def Arad2005.clusters {α : Type u_1} (isV : α → Bool) (w : List α) : List (List α)

clusters isV w lists the maximal consonant clusters of w.

Equations

• Arad2005.clusters isV w = List.filter (fun (c : List α) => c.all fun (x : α) => !isV x) (List.splitBy (fun (x y : α) => !isV x && !isV y) w)

def Arad2005.IsStemModification {α : Type u_1} [DecidableEq α] (isV : α → Bool) (px : Prefixes α) (v : Vowel → α) (b : Binyan) (voice : Voice) (base w : List α) : Prop

A verb is a stem modification of a base with melodic overwriting ([BE94], p. 47) when, in the binyan Voice spells out, it is the binyan's prefix followed by a word whose consonants include the base's in order and whose vowels are Voice's.

Equations

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

@[instance_reducible]

instance Arad2005.instDecidableIsStemModification {α : Type u_1} [DecidableEq α] (isV : α → Bool) (px : Prefixes α) (v : Vowel → α) (b : Binyan) (voice : Voice) (base w : List α) : Decidable (IsStemModification isV px v b voice base w)

Equations

• Arad2005.instDecidableIsStemModification isV px v b voice base w = Arad2005.instDecidableIsStemModification._aux_1 isV px v b voice base w

def Arad2005.KeepsClusters {α : Type u_1} [DecidableEq α] (isV : α → Bool) (base w : List α) : Prop

A verb keeps the clusters of its base (39) when every consonant cluster of the base is contiguous in it.

Equations

• Arad2005.KeepsClusters isV base w = ∀ c ∈ Arad2005.clusters isV base, c <:+: w

@[instance_reducible]

instance Arad2005.instDecidableKeepsClusters {α : Type u_1} [DecidableEq α] (isV : α → Bool) (base w : List α) : Decidable (KeepsClusters isV base w)

Equations

• Arad2005.instDecidableKeepsClusters isV base w = Arad2005.instDecidableKeepsClusters._aux_1 isV base w

def Arad2005.baseStem (f : Data.Forms.Form Forms.Cell) : List String

baseStem f is the stem of a base, its segments before a boundary +. (32) prints the suffixes after it outside the stem.

Equations

• Arad2005.baseStem f = List.takeWhile (fun (x : String) => decide (x ≠ "+")) f.segments

def Arad2005.candidates (a : Forms.Analysis) : List (Binyan × Voice)

candidates a lists the binyan and voice of a verb where the book prints them, and every active binyan where it does not.

Equations

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

theorem Arad2005.denominals : List.map (fun (x : Data.Forms.FormRelation Forms.Analysis) => x.target.form.form) (List.filter (fun (rel : Data.Forms.FormRelation Forms.Analysis) => decide ¬∃ x ∈ candidates rel.target, IsStemModification isVowel transcribedPx Vowel.transcription x.1 x.2 (baseStem rel.form.form) rel.target.form.segments) Forms.analysisRelations) = ["xoqeq", "qoded"] ∧ ∀ rel ∈ Forms.analysisRelations, ∀ r ∈ rel.form.root.bind root?, ∀ x ∈ candidates rel.target, verb transcribedPx Vowel.transcription fricative x.1 x.2 r ≠ some rel.target.form.segments

Every noun-derived verb of the data is a stem modification of its base except xoqeq and qoded (41a, b), whose {o, e} (25) does not list. None is the verb the root of its base derives in its binyan, so misger is not siger, musgar not sugar and mixšev not xišev.

theorem Arad2005.not_isStemModification : ¬IsStemModification isVowel transcribedPx Vowel.transcription Binyan.cvccvc Voice.active ["m", "i", "s", "g", "e", "r", "e", "t"] ["m", "i", "s", "g", "e", "r"] ∧ ¬IsStemModification isVowel transcribedPx Vowel.transcription Binyan.cvccvc Voice.active ["t", "e", "l", "e", "f", "o", "n"] ["t", "i", "l", "e", "f", "o", "n"]

Without its stem boundary the suffix -et of misgeret would have to be kept, which the book leaves unexplained (fn. 2, p. 246); a verb keeping a vowel of its base, *tilefon, is not a stem modification.

theorem Arad2005.keepsClusters : KeepsClusters isVowel ["t", "r", "a", "n", "s", "f", "e", "r"] ["t", "r", "i", "n", "s", "f", "e", "r"] ∧ KeepsClusters isVowel ["s", "t", "r", "e", "p", "t", "i", "z"] ["s", "t", "r", "i", "p", "t", "e", "z"] ∧ KeepsClusters isVowel ["s", "i", "n", "x", "r", "o", "n", "i"] ["s", "i", "n", "x", "r", "e", "n"] ∧ ¬KeepsClusters isVowel ["t", "r", "a", "n", "s", "f", "e", "r"] ["t", "i", "r", "n", "s", "f", "e", "r"] ∧ ¬KeepsClusters isVowel ["s", "t", "r", "e", "p", "t", "i", "z"] ["s", "t", "i", "r", "p", "t", "e", "z"] ∧ ¬KeepsClusters isVowel ["s", "i", "n", "x", "r", "o", "n", "i"] ["s", "n", "i", "x", "r", "e", "n"] ∧ ¬KeepsClusters isVowel ["x", "r", "o", "p"] ["x", "a", "r", "a", "p"]

The borrowed verbs of (39) keep the clusters of their bases, unlike *tirnsfer, *stirptez, *snixren, which Hebrew phonology would allow (p. 266); xarap breaks the cluster of xrop (29c), so cluster transfer is not a condition of stem modification.

The locality of root interpretation (Ch. 7 (8))

inductive Arad2005.Head : Type

Head lists the heads above a root, the category heads n, a, v and Voice.

• n : Head
• a : Head
• v : Head
• voice : Head

@[instance_reducible]

instance Arad2005.instDecidableEqHead : DecidableEq Head

Equations

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

@[instance_reducible]

instance Arad2005.instReprHead : Repr Head

Equations

• Arad2005.instReprHead = { reprPrec := Arad2005.instReprHead.repr }

def Arad2005.instReprHead.repr : Head → ℕ → Std.Format

Equations

• Arad2005.instReprHead.repr Arad2005.Head.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Head.n")).group prec✝
• Arad2005.instReprHead.repr Arad2005.Head.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Head.a")).group prec✝
• Arad2005.instReprHead.repr Arad2005.Head.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Head.v")).group prec✝
• Arad2005.instReprHead.repr Arad2005.Head.voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Head.voice")).group prec✝

@[instance_reducible]

instance Arad2005.instFintypeHead : Fintype Head

Equations

• Arad2005.instFintypeHead = { elems := { val := ↑Arad2005.Head.enumList, nodup := Arad2005.Head.enumList_nodup }, complete := Arad2005.instFintypeHead._proof_1 }

def Arad2005.cyclic (h : Head) : Prop

cyclic picks out the category-assigning heads, at which a root is interpreted (8).

Equations

• Arad2005.cyclic h = (h = Arad2005.Head.n ∨ h = Arad2005.Head.a ∨ h = Arad2005.Head.v)

@[instance_reducible]

instance Arad2005.instDecidablePredHeadCyclic : DecidablePred cyclic

Equations

• Arad2005.instDecidablePredHeadCyclic x✝ = { decide := decide (x✝ = Arad2005.Head.n) || decide (x✝ = Arad2005.Head.a ∨ x✝ = Arad2005.Head.v), reflects_decide := ⋯ }

def Arad2005.verbSpine (base : Option Head) : DistributedMorphology.ComplexHead DistributedMorphology.Root Head

verbSpine base is the structure of a verb, (26) and (7b), with v and Voice above the root, or above the category head of the word it is formed from.

Equations

• Arad2005.verbSpine base = { root := { index := 0 }, heads := base.toList ++ [Arad2005.Head.v, Arad2005.Head.voice] }

theorem Arad2005.verbSpine_rootLocal (base : Option Head) : (∀ c ∈ base, c = Head.n ∨ c = Head.a) → ∀ (i : Fin (verbSpine base).heads.length), (verbSpine base).heads[i] = Head.v → ((verbSpine base).RootLocal cyclic i ↔ base = none)

By (8), the v of a verb is local to the root exactly when no category head intervenes, so only a root-derived verb's v sees the root and a noun-derived verb's sees the noun.

Conjugation classes (§6.2.6)

def Arad2005.Binyan.Geminated (b : Binyan) : Prop

A binyan geminates when a triliteral root's middle radical is one element on two of its slots.

Equations

• b.Geminated = (2 ≤ McCarthy1981.linkCount (Arad2005.consonantism Arad2005.numeralPx b { segments := [0, 1, 2] }) Morphology.AssocSource.root 1)

@[instance_reducible]

instance Arad2005.instDecidablePredBinyanGeminated : DecidablePred Binyan.Geminated

Equations

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

def Arad2005.Natural (b b' : Binyan) : Prop

Two binyanim form a natural pair when they obey the two tendencies of pp. 225–226, against conjugating a binyan with itself and against mixing geminate and non-geminate binyanim.

Equations

• Arad2005.Natural b b' = (b ≠ b' ∧ (b.Geminated ↔ b'.Geminated))

@[instance_reducible]

instance Arad2005.instDecidableNatural (b b' : Binyan) : Decidable (Natural b b')

Equations

• Arad2005.instDecidableNatural b b' = { decide := decide (b ≠ b') && decide (b.Geminated ↔ b'.Geminated), reflects_decide := ⋯ }

def Arad2005.natural57 : List (Sym2 Binyan)

natural57 lists the four natural types of binyan pairs (57).

Equations

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

theorem Arad2005.natural_iff (b b' : Binyan) : Natural b b' ↔ s(b, b') ∈ natural57

The tendencies derive (57).

def Arad2005.conjugations : List (String × Binyan × Binyan)

conjugations reads each conjugation of (47)–(52), with the binyan of its causative and of its other alternant, off the verbs of the data.

Equations

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

theorem Arad2005.conjugation_verbs_derived : List.map (fun (x : Forms.Analysis) => x.form.form) (List.filter (fun (a : Forms.Analysis) => decide (a.conjugation ≠ none ∧ ∃ x ∈ verbCell? a, verb transcribedPx Vowel.transcription fricative x.1 x.2.1 x.2.2 ≠ some a.form.segments)) Forms.analyses) = ["namas", "hemes", "heʔedim", "heʔedim"]

The derivation produces the verbs of the conjugation classes except namas and hemes, the biliteral allomorphy of √mss (fn. 33), and heʔedim, lowered next to the guttural.

theorem Arad2005.conjugations_natural : (∀ x ∈ conjugations, (Natural x.2.1 x.2.2 ↔ x.1 ∈ ["1", "2", "3", "4"]) ∧ (x.2.1 = x.2.2 ↔ x.1 = "6") ∧ (¬(x.2.1.Geminated ↔ x.2.2.Geminated) ↔ x.1 = "5")) ∧ (∀ p ∈ natural57, ∃ x ∈ conjugations, s(x.2.1, x.2.2) = p) ∧ ∀ x ∈ conjugations, ¬(x.2.1.Intransitive ↔ x.2.2.Intransitive) → ¬x.2.1.Intransitive

Conjugations 1–4 are natural and every natural pair is one of them; conjugation 5 crosses the gemination border and conjugation 6 conjugates P5 with itself. Wherever (11) marks one alternant [−tr.], the causative is the other (p. 226).

Over the fragment's segments

def Arad2005.uncovered : List String

uncovered lists the root-derived verbs the derivation leaves out, for guttural lowering in hexšiv and heʔedim, t–sibilant metathesis in histager, and the biliteral allomorphy of √mss.

Equations

• Arad2005.uncovered = ["hexšiv", "histager", "namas", "hemes", "heʔedim"]

def Arad2005.fillContinuant (post : Bool) (s : Phonology.Segment) : Phonology.Segment

fillContinuant post s realizes an alternating stop, a consonant unspecified for continuancy, as its fricative after a vowel and as its stop elsewhere; any other segment is itself.

Equations

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

theorem Arad2005.naturalClass_fillContinuant (post : Bool) (a : Phonology.Segment) : a ∈ [Hebrew.Phonology.B, Hebrew.Phonology.K, Hebrew.Phonology.P] → (a.setFeature Phonology.Feature.continuant post).naturalClass Hebrew.Phonology.consonants = {fillContinuant post a}

The rule realizes each alternating stop as the one consonant that refines it with the contextual continuancy.

def Arad2005.segment : String → Phonology.Segment

segment x reads a letter of the book's transcription as a segment of the fragment, b, k, p as the archisegments of the alternating stops, q as the /k/ of ק, r as /ʁ/, c as /ts/ and e as /ɛ/.

Equations

• Arad2005.segment "b" = Hebrew.Phonology.B
• Arad2005.segment "k" = Hebrew.Phonology.K
• Arad2005.segment "p" = Hebrew.Phonology.P
• Arad2005.segment "q" = Hebrew.Phonology.k
• Arad2005.segment "d" = Hebrew.Phonology.d
• Arad2005.segment "f" = Hebrew.Phonology.f
• Arad2005.segment "g" = Hebrew.Phonology.«ɡ»
• Arad2005.segment "h" = Hebrew.Phonology.h
• Arad2005.segment "y" = Hebrew.Phonology.j
• Arad2005.segment "l" = Hebrew.Phonology.l
• Arad2005.segment "m" = Hebrew.Phonology.m
• Arad2005.segment "n" = Hebrew.Phonology.n
• Arad2005.segment "r" = Hebrew.Phonology.«ʁ»
• Arad2005.segment "s" = Hebrew.Phonology.s
• Arad2005.segment "š" = Hebrew.Phonology.«ʃ»
• Arad2005.segment "t" = Hebrew.Phonology.t
• Arad2005.segment "c" = Hebrew.Phonology.ts
• Arad2005.segment "v" = Hebrew.Phonology.v
• Arad2005.segment "x" = Hebrew.Phonology.x
• Arad2005.segment "z" = Hebrew.Phonology.z
• Arad2005.segment "ʔ" = Hebrew.Phonology.«ʔ»
• Arad2005.segment "a" = Hebrew.Phonology.a
• Arad2005.segment "e" = Hebrew.Phonology.«ɛ»
• Arad2005.segment "i" = Hebrew.Phonology.i
• Arad2005.segment "o" = Hebrew.Phonology.o
• Arad2005.segment "u" = Hebrew.Phonology.u
• Arad2005.segment x✝ = ⊥

def Arad2005.surfaceSegment (x : String) : Phonology.Segment

surfaceSegment x reads a letter of a surface form, an alternating stop as the stop.

Equations

• Arad2005.surfaceSegment x = Arad2005.fillContinuant false (Arad2005.segment x)

theorem Arad2005.fillContinuant_eq_self {s : Phonology.Segment} (h : ¬(s.Unspecified Phonology.Feature.continuant ∧ s.IsConsonant)) (post : Bool) : fillContinuant post s = s

theorem Arad2005.not_alternating_segment (x : String) (hp : x ≠ "p") (hb : x ≠ "b") (hk : x ≠ "k") : ¬((segment x).Unspecified Phonology.Feature.continuant ∧ (segment x).IsConsonant)

Only b, k and p read as alternating stops.

theorem Arad2005.fillContinuant_segment (post : Bool) (x : String) : fillContinuant post (segment x) = surfaceSegment (fricative post x)

Filling continuancy over the fragment's segments agrees with spirantizing the transcription.

def Arad2005.fragmentRoots : List (String × Morphology.ConsonantalRoot Phonology.Segment)

The roots of the data in the fragment, by label; Arad's √qlt is the fragment's √klt.

Equations

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

theorem Arad2005.root?_map_segment (p : String × Morphology.ConsonantalRoot Phonology.Segment) : p ∈ fragmentRoots → Option.map (fun (x : Morphology.ConsonantalRoot String) => Morphology.ConsonantalRoot.map segment x) (root? p.1) = some p.2

Each root of the transcription, read letter by letter, is the fragment's root.

theorem Arad2005.words_derived_seg (p : String × Morphology.ConsonantalRoot Phonology.Segment) : p ∈ fragmentRoots → ∀ a ∈ Forms.analyses, a.root = some p.1 → (∀ x ∈ verbCell? a, a.form.form ∉ uncovered → verb (Prefixes.map segment transcribedPx) (segment ∘ Vowel.transcription) fillContinuant x.1 x.2.1 p.2 = some (List.map surfaceSegment a.form.segments)) ∧ ∀ x ∈ nounCell? a, surface fillContinuant (nounStem (Prefixes.map segment transcribedPx) (segment ∘ Vowel.transcription) x.1 p.2) = List.map surfaceSegment a.form.segments

Over the fragment's roots and segments, the derivation produces every root-derived word of the data read as segments, the alternating stops realized by continuancy, except the verbs it leaves out.

Multiple Contextualized Meaning (Ch. 3, Ch. 7)

def Arad2005.pattern? (a : Forms.Analysis) : Option String

pattern? a is the pattern of a word, its binyan number or its mišqal.

Equations

• Arad2005.pattern? a = a.binyan.orElse fun (x : Unit) => a.pattern

def Arad2005.rootForms (root pattern : String) : Finset String

rootForms lists the words of a root in a pattern.

Equations

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

def Arad2005.rootMeanings (root pattern : String) : Finset String

rootMeanings lists the concepts of a root in a pattern.

Equations

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

def Arad2005.roots : Morphology.Realization.Interpreted String String String String

roots is the interpreted realization system of roots over the patterns.

Equations

• Arad2005.roots = { realize := Arad2005.rootForms, interp := Arad2005.rootMeanings }

theorem Arad2005.roots_allosemous : roots.IsAllosemous "sgr" ∧ roots.IsAllosemous "qlt" ∧ roots.IsAllosemous "xšb" ∧ roots.IsAllosemous "šmn"

√sgr is 'close' in P1 and 'extradite' in P5, √qlt 'input' in CeCeC and 'a record' in taCCiC, √xšb 'think' in P1 and 'computer' in maCCeC, √šmn 'oil' in CeCeC and 'cream' in CaCCeCet (Ch. 7 (2)–(5)).