Arad 2005: roots and patterns in Hebrew

Every Hebrew verb is a consonantal root in one of seven binyanim, while nouns may or may not carry a nominal pattern. The asymmetry follows from what the patterns are: a nominal pattern comes with its vowels, a binyan is a CV template with vowel slots and no vowels of its own, and the vowels a verb surfaces with are the exponent of Voice — a morphosyntactic feature that must be spelled out, by a rule whose context is the binyan already inserted under v. A verb therefore needs the template so that Voice has slots to fill; a noun that is pronounceable on its own needs nothing. The same root takes unrelated meanings in different patterns (Multiple Contextualized Meaning), whereas a verb formed from an existing noun keeps the noun's meaning: roots are interpreted at the first category head that merges with them, and a later head sees only that word. The contrast shows in the phonology too — a noun-derived verb is built by modifying the noun's own stem, carrying its prefix and its consonant clusters into the binyan, where a root-derived verb associates bare consonants to the template.

Main definitions

• Binyan, Binyan.skeleton: the five verbal templates as slot skeletons; mishqalim the nominal patterns with their vowels.
• voiceSpellout: the Voice vocabulary items in the context of the binyan; verb the root-derived verb; denominal the noun-derived verb by stem modification.
• rootMeanings: a root's glosses in a pattern, read off the rows.

References

• [arad-2005]
• [mccarthy-1981] — root-to-template association
• [bat-el-1994] — stem modification and cluster transfer

Binyanim as the spell-out of v and Voice (§2.5)

inductive Arad2005.Slot : Type

A slot of a pattern skeleton, in the book's subscripted notation: a root radical by index, an open vowel slot, or a fixed segment.

• radical (i : ℕ) : Slot
• vowel : Slot
• fixed (s : String) (slot : Morphology.CVSlot) : Slot

@[instance_reducible]

instance Arad2005.instDecidableEqSlot : DecidableEq Slot

Equations

• Arad2005.instDecidableEqSlot = Arad2005.instDecidableEqSlot.decEq

def Arad2005.instDecidableEqSlot.decEq (x✝ x✝¹ : Slot) : Decidable (x✝ = x✝¹)

Equations

• Arad2005.instDecidableEqSlot.decEq (Arad2005.Slot.radical a) (Arad2005.Slot.radical b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Arad2005.instDecidableEqSlot.decEq (Arad2005.Slot.radical i) Arad2005.Slot.vowel = isFalse ⋯
• Arad2005.instDecidableEqSlot.decEq (Arad2005.Slot.radical i) (Arad2005.Slot.fixed s slot) = isFalse ⋯
• Arad2005.instDecidableEqSlot.decEq Arad2005.Slot.vowel (Arad2005.Slot.radical i) = isFalse ⋯
• Arad2005.instDecidableEqSlot.decEq Arad2005.Slot.vowel Arad2005.Slot.vowel = isTrue ⋯
• Arad2005.instDecidableEqSlot.decEq Arad2005.Slot.vowel (Arad2005.Slot.fixed s slot) = isFalse ⋯
• Arad2005.instDecidableEqSlot.decEq (Arad2005.Slot.fixed s slot) (Arad2005.Slot.radical i) = isFalse ⋯
• Arad2005.instDecidableEqSlot.decEq (Arad2005.Slot.fixed s slot) Arad2005.Slot.vowel = isFalse ⋯
• Arad2005.instDecidableEqSlot.decEq (Arad2005.Slot.fixed a a_1) (Arad2005.Slot.fixed 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.instReprSlot : Repr Slot

Equations

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

def Arad2005.instReprSlot.repr : Slot → ℕ → Std.Format

Equations

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

def Arad2005.Slot.isFixedVowel : Slot → Bool

A fixed vowel of a pattern.

Equations

• (Arad2005.Slot.fixed s Morphology.CVSlot.V).isFixedVowel = true
• x✝.isFixedVowel = false

def Arad2005.Slot.isRadical : Slot → Bool

A radical position.

Equations

• (Arad2005.Slot.radical i).isRadical = true
• x✝.isRadical = false

def Arad2005.Slot.cv : Slot → Morphology.CVSlot

The C or V slot a pattern slot occupies.

Equations

• (Arad2005.Slot.radical a).cv = Morphology.CVSlot.C
• Arad2005.Slot.vowel.cv = Morphology.CVSlot.V
• (Arad2005.Slot.fixed a a_1).cv = a_1

inductive Arad2005.Binyan : Type

The five binyan templates (24b): vowel slots without vowels, the prefixes n-, h-, hit-, and in CVCCVC the geminate slot of the middle radical.

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

def Arad2005.Binyan.skeleton : Binyan → List Slot

The skeletons of (3) and (24b).

Equations

• One or more equations did not get rendered due to their size.
• Arad2005.Binyan.cvcvc.skeleton = [Arad2005.Slot.radical 0, Arad2005.Slot.vowel, Arad2005.Slot.radical 1, Arad2005.Slot.vowel, Arad2005.Slot.radical 2]
• Arad2005.Binyan.cvccvc.skeleton = [Arad2005.Slot.radical 0, Arad2005.Slot.vowel, Arad2005.Slot.radical 1, Arad2005.Slot.radical 1, Arad2005.Slot.vowel, Arad2005.Slot.radical 2]

def Arad2005.Binyan.ofPattern : String → Option (Binyan × Bool)

The binyan and Voice value of a numbered pattern, by (3) and (5): the passives are patterns 4 and 6.

Equations

• Arad2005.Binyan.ofPattern "1" = some (Arad2005.Binyan.cvcvc, true)
• Arad2005.Binyan.ofPattern "2" = some (Arad2005.Binyan.nvccvc, true)
• Arad2005.Binyan.ofPattern "3" = some (Arad2005.Binyan.cvccvc, true)
• Arad2005.Binyan.ofPattern "4" = some (Arad2005.Binyan.cvccvc, false)
• Arad2005.Binyan.ofPattern "5" = some (Arad2005.Binyan.hvccvc, true)
• Arad2005.Binyan.ofPattern "6" = some (Arad2005.Binyan.hvccvc, false)
• Arad2005.Binyan.ofPattern "7" = some (Arad2005.Binyan.hitcvccvc, true)
• Arad2005.Binyan.ofPattern x✝ = none

def Arad2005.mishqalim : List (List Slot)

Nominal patterns carry their vowels (24a).

Equations

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

def Arad2005.Slot.associations : List Slot → ℕ → ℕ → ℕ → List Morphology.Association

The association lines a skeleton dictates: radicals and fixed segments at their positions, vowels left to right into the vowel slots.

Equations

• One or more equations did not get rendered due to their size.
• Arad2005.Slot.associations [] x✝² x✝¹ x✝ = []
• Arad2005.Slot.associations (Arad2005.Slot.radical k :: rest) x✝² x✝¹ x✝ = { melodyIndex := k, slotIndex := x✝² } :: Arad2005.Slot.associations rest (x✝² + 1) x✝¹ x✝

def Arad2005.fill (sk : List Slot) (r : Morphology.ConsonantalRoot String) (voc : List String) : Morphology.TemplateMatch String

Fill a skeleton with a root and a vocalism: association by the subscripts.

Equations

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

inductive Arad2005.VoiceFeature : Type

The features of Voice and of the v exponent it sees.

• active : VoiceFeature
• passive : VoiceFeature
• binyan (b : Binyan) : VoiceFeature

@[instance_reducible]

instance Arad2005.instDecidableEqVoiceFeature : DecidableEq VoiceFeature

Equations

• Arad2005.instDecidableEqVoiceFeature = Arad2005.instDecidableEqVoiceFeature.decEq

def Arad2005.instDecidableEqVoiceFeature.decEq (x✝ x✝¹ : VoiceFeature) : Decidable (x✝ = x✝¹)

Equations

• Arad2005.instDecidableEqVoiceFeature.decEq Arad2005.VoiceFeature.active Arad2005.VoiceFeature.active = isTrue ⋯
• Arad2005.instDecidableEqVoiceFeature.decEq Arad2005.VoiceFeature.active Arad2005.VoiceFeature.passive = isFalse Arad2005.instDecidableEqVoiceFeature.decEq._proof_1
• Arad2005.instDecidableEqVoiceFeature.decEq Arad2005.VoiceFeature.active (Arad2005.VoiceFeature.binyan b) = isFalse ⋯
• Arad2005.instDecidableEqVoiceFeature.decEq Arad2005.VoiceFeature.passive Arad2005.VoiceFeature.active = isFalse Arad2005.instDecidableEqVoiceFeature.decEq._proof_3
• Arad2005.instDecidableEqVoiceFeature.decEq Arad2005.VoiceFeature.passive Arad2005.VoiceFeature.passive = isTrue ⋯
• Arad2005.instDecidableEqVoiceFeature.decEq Arad2005.VoiceFeature.passive (Arad2005.VoiceFeature.binyan b) = isFalse ⋯
• Arad2005.instDecidableEqVoiceFeature.decEq (Arad2005.VoiceFeature.binyan b) Arad2005.VoiceFeature.active = isFalse ⋯
• Arad2005.instDecidableEqVoiceFeature.decEq (Arad2005.VoiceFeature.binyan b) Arad2005.VoiceFeature.passive = isFalse ⋯
• Arad2005.instDecidableEqVoiceFeature.decEq (Arad2005.VoiceFeature.binyan a) (Arad2005.VoiceFeature.binyan b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Arad2005.instReprVoiceFeature.repr : VoiceFeature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Arad2005.instReprVoiceFeature : Repr VoiceFeature

Equations

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

def Arad2005.voiceSpellout : List (DistributedMorphology.VocabularyItem VoiceFeature (List String))

The Voice spell-out (25): a vocalism in the context of the binyan inserted under v.

Equations

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

def Arad2005.voiceNode (b : Binyan) (active : Bool) : DistributedMorphology.Neighborhood (List VoiceFeature)

The Voice node once v has been realized: its feature, with the binyan as the inner neighbor.

Equations

• Arad2005.voiceNode b active = { focus := [if active = true then Arad2005.VoiceFeature.active else Arad2005.VoiceFeature.passive], leftCtx := [[Arad2005.VoiceFeature.binyan b]] }

def Arad2005.surface (m : Morphology.TemplateMatch String) : String

The surface string, with Modern Hebrew degemination.

Equations

• Arad2005.surface m = String.join (List.destutter (fun (x1 x2 : String) => x1 ≠ x2) m.spellout)

def Arad2005.fricative : String → String

The fricative allophone of a stop.

Equations

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

def Arad2005.spirantize (l : List String) : List String

Spirantization of p, b, k after a vowel, blocked in the geminate slot: siper, not sifer.

Equations

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

def Arad2005.verb (r : Morphology.ConsonantalRoot String) (b : Binyan) (active : Bool) : Option String

A root-derived verb: the binyan under v, Voice's vowels by (25) in its context, the root associated by the skeleton (28), spirantization and degemination at the surface. none where Voice has no exponent.

Equations

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

def Arad2005.rootOfLabel : String → Option (Morphology.ConsonantalRoot String)

The roots of (3) and (6), from the fragment.

Equations

• Arad2005.rootOfLabel "lmd" = some Hebrew.lmd
• Arad2005.rootOfLabel "spr" = some Hebrew.spr
• Arad2005.rootOfLabel "qlt" = some Hebrew.qlt
• Arad2005.rootOfLabel "pll" = some Hebrew.pll
• Arad2005.rootOfLabel "npc" = some Hebrew.npc
• Arad2005.rootOfLabel "xlq" = some Hebrew.xlq
• Arad2005.rootOfLabel "str" = some Hebrew.str
• Arad2005.rootOfLabel "pqd" = some Hebrew.pqd
• Arad2005.rootOfLabel x✝ = none

theorem Arad2005.rows_verbs (r : Data.Examples.LinguisticExample) : r ∈ Examples.all → ∀ root ∈ (r.feature? "root" >>= rootOfLabel).toList, ∀ bv ∈ (r.feature? "pattern" >>= Binyan.ofPattern).toList, verb root bv.1 bv.2 = some r.primaryText

The verbs of (3) and (6) are derived: the binyan under v, Voice's vowels in the binyan's context, spirantization and degemination at the surface.

theorem Arad2005.voice_obligatory : (∀ (b : Binyan), (DistributedMorphology.subsetPrinciple voiceSpellout (voiceNode b true)).isSome = true) ∧ ∀ (b : Binyan), (DistributedMorphology.subsetPrinciple voiceSpellout (voiceNode b false)).isSome = true ↔ b = Binyan.cvccvc ∨ b = Binyan.hvccvc

Voice must be spelled out: every binyan has an active vocalism, and a passive one exactly in CVCCVC and hVCCVC (25).

theorem Arad2005.active_many_to_one : (List.map (fun (x : DistributedMorphology.VocabularyItem VoiceFeature (List String)) => x.exponent) (List.filter (fun (x : DistributedMorphology.VocabularyItem VoiceFeature (List String)) => decide (x.site.focus = [VoiceFeature.active])) voiceSpellout)).Nodup ∧ (List.filter (fun (x : DistributedMorphology.VocabularyItem VoiceFeature (List String)) => decide (x.site.focus = [VoiceFeature.active])) voiceSpellout).length = 5

One feature, five exponents: [+active] is realized five ways, the choice fixed by the binyan (25).

theorem Arad2005.binyanim_vowel_slots (b : Binyan) : List.count Slot.vowel b.skeleton = 2 ∧ ∀ p ∈ b.skeleton, p.isFixedVowel = true → b = Binyan.hitcvccvc

Every binyan has two vowel slots and no vowels of its own; the prefix of hitCVCCVC is its only fixed vowel (24b).

theorem Arad2005.mishqalim_no_vowel_slots (p : List Slot) : p ∈ mishqalim → List.count Slot.vowel p = 0

Nominal patterns have no vowel slots: their vowels are their own (24a).

Noun-derived verbs by stem modification (§2.6, §7.5)

def Arad2005.isVowel (c : Char) : Bool

A transliterated vowel.

Equations

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

def Arad2005.stem (base : String) : List Char

The stem of a base word: without a final vowel or the suffix -et, which are not part of the stem (32).

Equations

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

def Arad2005.erase (s : List Char) : List Char

Stray Erasure: only the first and the last vowel of the stem survive resyllabification into the bisyllabic template.

Equations

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

def Arad2005.clusters (s : List Char) : List String

The consonant clusters of a stem, the vowels between them dropped.

Equations

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

def Arad2005.emit : List Slot → List String → List String → Option String

Emit a skeleton whose radical runs have been collapsed, one cluster per run and one Voice vowel per slot.

Equations

• Arad2005.emit [] [] [] = some ""
• Arad2005.emit (Arad2005.Slot.fixed s slot :: rest) x✝¹ x✝ = (fun (x : String) => s ++ x) <$> Arad2005.emit rest x✝¹ x✝
• Arad2005.emit (Arad2005.Slot.vowel :: rest) x✝ (v :: vs) = (fun (x : String) => v ++ x) <$> Arad2005.emit rest x✝ vs
• Arad2005.emit (Arad2005.Slot.radical i :: rest) (c :: cs) x✝ = (fun (x : String) => c ++ x) <$> Arad2005.emit rest cs x✝
• Arad2005.emit x✝² x✝¹ x✝ = none

def Arad2005.denominal (base : String) (b : Binyan) (active : Bool := true) : Option String

A noun-derived verb: the base's stem is modified to the binyan's prosody and its vowels overwritten by Voice's. Clusters are carried into the template whole when they match its runs of consonant slots; otherwise the consonants are resyllabified one per slot.

Equations

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

theorem Arad2005.rows_denominal (r : Data.Examples.LinguisticExample) : r ∈ Examples.all → ∀ base ∈ (r.feature? "base").toList, ∀ bv ∈ (r.feature? "pattern" >>= Binyan.ofPattern).toList, denominal base bv.1 bv.2 = some r.primaryText

The noun-derived verbs of (29), (32), (39), (40), and Ch. 7 (6) are derived from their bases in the stated pattern: misgeret → misger with the nominal m- carried along, transfer → trinsfer with its clusters intact, xrop → xarap resyllabified into CVCVC.

theorem Arad2005.rows_denominal_exists (r : Data.Examples.LinguisticExample) : r ∈ Examples.all → ∀ base ∈ (r.feature? "base").toList, ∃ (b : Binyan) (active : Bool), denominal base b active = some r.primaryText

Every noun-derived verb of the rows is the stem modification of its base into some binyan.

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

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

The words the rows list for 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

The glosses the rows list for 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 as an interpreted realization system over the book's pattern labels.

Equations

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

theorem Arad2005.roots_allosemous {root c c' m m' : String} (h : m ∈ rootMeanings root c) (h' : m' ∈ rootMeanings root c') (hne : m ≠ m') : roots.IsAllosemous root

A root with two glosses in two patterns is allosemous.

theorem Arad2005.sgr_mcm : roots.IsAllosemous "sgr"

√sgr: sagar 'close' against hisgir 'extradite' (Ch. 7 (5)).

theorem Arad2005.qlt_mcm : roots.IsAllosemous "qlt"

√qlt: qelet 'input' against taqlit 'a record' (Ch. 7 (4)).

theorem Arad2005.xsb_mcm : roots.IsAllosemous "xšb"

√xšb: xašav 'to think' against maxšev 'a computer' (Ch. 7 (3)).

theorem Arad2005.smn_mcm : roots.IsAllosemous "šmn"

√šmn: šemen 'oil' against šamenet 'cream' (Ch. 7 (2)).