Hewett (2026): Verbal templates can influence l-selection in Semitic

This file formalizes [Hew26]'s generalization that the preposition a Semitic root lexically selects can vary with the verbal template, and its analysis by joint selection. A Row records the root, the category, the template where the paper names one, and the selected preposition of an example, and Determines says that the preposition is a function of a coordinate of the data, Function.FactorsThrough on the attested rows. Selection by the root ([Har14b]) or by the categorizing head ([Mer19a]), the structures (12a) and (12b), predicts that the root and its category determine the preposition; the Tunisian roots of (13), the Syrian root of (14) and the Hebrew roots of (17) and (18) refute this (krh_not_categoryDetermined), the category-dependent roots of (5) and (6) refute determination by the root alone, and the roots of (1), (2) and (11) are invariant. Joint selection (23) indexes a selectional feature by an ordered tuple of category features that c-commanding heads strip in order, ActivationIndex; selected runs the derivations (24) and (25), and the lexical entries read off the data select exactly the attested preposition once the categorizing head and then the template have activated them (selected_eq).

Implementation notes

• The prepositions of the four languages are one inductive, each constructor a language's item, the Arabic b- and bi- and ʕala, ʕalej and ʕli- identified; the category of a Semitic verb is V, of the nominals and adjectives of (1), (2), (5) and (6) N and A, and the templates of (2) and (6) are unnamed in the paper.
• The alternations of (15) and (16) and the roots without nonactive forms of (19) and (20) are example rows only; the paper draws from them no claim beyond the template dependence the other examples establish.

TODO

• The locality of joint selection (§4): Activate over spans or within a phase domain.

References

• [Hew26]
• [Har14b]
• [Mer19a]
• [Mer15]
• [Pre14]

Roots, templates and prepositions

inductive Hewett2026.Template : Type

The verbal templates of the data, the Arabic Forms I, II, VII and V and the Hebrew pi'el, pu'al, hif'il and huf'al.

• XaYaZ : Template
• XaYYaZ : Template
• nXaYaZ : Template
• tXaYYaZ : Template
• XiYeZ : Template
• XuYaZ : Template
• hiXYiZ : Template
• huXYaZ : Template

@[instance_reducible]

instance Hewett2026.instDecidableEqTemplate : DecidableEq Template

Equations

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

@[instance_reducible]

instance Hewett2026.instFintypeTemplate : Fintype Template

Equations

• Hewett2026.instFintypeTemplate = { elems := { val := ↑Hewett2026.Template.enumList, nodup := Hewett2026.Template.enumList_nodup }, complete := Hewett2026.instFintypeTemplate._proof_1 }

inductive Hewett2026.Root : Type

The roots of the examples: English √apologi (1) and √prd (5); Syrian Arabic √fxr (2), √brk (6) and √ħkm (14); Tunisian Arabic √xwf (11), √krh and √dwr (13); Hebrew √ṭpl (17) and √špʕ (18).

• apologi : Root
• prd : Root
• fxr : Root
• brk : Root
• Hkm : Root
• xwf : Root
• krh : Root
• dwr : Root
• tpl : Root
• shps : Root

@[instance_reducible]

instance Hewett2026.instDecidableEqRoot : DecidableEq Root

Equations

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

@[instance_reducible]

instance Hewett2026.instFintypeRoot : Fintype Root

Equations

• Hewett2026.instFintypeRoot = { elems := { val := ↑Hewett2026.Root.enumList, nodup := Hewett2026.Root.enumList_nodup }, complete := Hewett2026.instFintypeRoot._proof_1 }

inductive Hewett2026.Prep : Type

The l-selected prepositions: English for, on, in and of; Arabic b-, ʕala, min, la- and fi; Hebrew be- and al.

• for_ : Prep
• on : Prep
• in_ : Prep
• of : Prep
• b : Prep
• Eala : Prep
• min : Prep
• la : Prep
• fi : Prep
• be : Prep
• al : Prep

@[instance_reducible]

instance Hewett2026.instDecidableEqPrep : DecidableEq Prep

Equations

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

@[instance_reducible]

instance Hewett2026.instFintypePrep : Fintype Prep

Equations

• Hewett2026.instFintypePrep = { elems := { val := ↑Hewett2026.Prep.enumList, nodup := Hewett2026.Prep.enumList_nodup }, complete := Hewett2026.instFintypePrep._proof_1 }

inductive Hewett2026.Lang : Type

The languages of the data.

• english : Lang
• syrianArabic : Lang
• tunisianArabic : Lang
• hebrew : Lang

@[instance_reducible]

instance Hewett2026.instDecidableEqLang : DecidableEq Lang

Equations

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

@[instance_reducible]

instance Hewett2026.instFintypeLang : Fintype Lang

Equations

• Hewett2026.instFintypeLang = { elems := { val := ↑Hewett2026.Lang.enumList, nodup := Hewett2026.Lang.enumList_nodup }, complete := Hewett2026.instFintypeLang._proof_1 }

structure Hewett2026.Row : Type

An example's selection: the root, the category of its realization, the verbal template when the paper names one, and the l-selected preposition, none for a bare object or a suppressed preposition.

• root : Root

  The root.

• cat : Minimalist.Cat

  The category of the root's realization.

• template : Option Template

  The verbal template.

• prep : Option Prep

  The l-selected preposition.

• lang : Lang

  The language.

def Hewett2026.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hewett2026.instDecidableEqRow : DecidableEq Row

Equations

• Hewett2026.instDecidableEqRow = Hewett2026.instDecidableEqRow.decEq

def Hewett2026.invariantData : List Row

The category-independent selection of (1) and (2) and the template-independent selection of (11).

Equations

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

def Hewett2026.categoryData : List Row

The category-dependent selection of (5) and (6).

Equations

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

def Hewett2026.templateData : List Row

The template-dependent selection of (13), (14), (17) and (18).

Equations

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

def Hewett2026.data : List Row

All the selection data.

Equations

• Hewett2026.data = Hewett2026.invariantData ++ Hewett2026.categoryData ++ Hewett2026.templateData

def Hewett2026.rows (r : Root) : List Row

The rows of a root.

Equations

• Hewett2026.rows r = List.filter (fun (x : Hewett2026.Row) => decide (x.root = r)) Hewett2026.data

What determines the preposition

def Hewett2026.Determines {K : Type u_1} (π : Row → K) (rows : List Row) : Prop

The preposition is a function of the coordinate π on the rows, that is, Row.prep factors through π there, Function.FactorsThrough restricted to the list.

Equations

• Hewett2026.Determines π rows = ∀ d ∈ rows, ∀ d' ∈ rows, π d = π d' → d.prep = d'.prep

@[instance_reducible]

instance Hewett2026.instDecidableDeterminesOfDecidableEq {K : Type u_1} [DecidableEq K] (π : Row → K) (rows : List Row) : Decidable (Determines π rows)

Equations

• Hewett2026.instDecidableDeterminesOfDecidableEq π rows = Hewett2026.instDecidableDeterminesOfDecidableEq._aux_1 π rows

theorem Hewett2026.Determines.of_factorsThrough {K : Type u_1} {K' : Type u_2} {π : Row → K} {π' : Row → K'} (h : Function.FactorsThrough π π') {rows : List Row} (hπ : Determines π rows) : Determines π' rows

A coordinate that factors through a finer one determines whatever the coarser does.

@[reducible, inline]

abbrev Hewett2026.RootDetermined (rows : List Row) : Prop

Selection by the root (12a), where the root determines the preposition.

Equations

• Hewett2026.RootDetermined rows = Hewett2026.Determines Hewett2026.Row.root rows

@[reducible, inline]

abbrev Hewett2026.CategoryDetermined (rows : List Row) : Prop

Selection by the categorizing head (12b), where the root and its category determine the preposition, the prediction root-based selection makes as well.

Equations

• Hewett2026.CategoryDetermined rows = Hewett2026.Determines (fun (d : Hewett2026.Row) => (d.root, d.cat)) rows

@[reducible, inline]

abbrev Hewett2026.TemplateDetermined (rows : List Row) : Prop

Joint selection, where the root, its category and the template determine the preposition.

Equations

• Hewett2026.TemplateDetermined rows = Hewett2026.Determines (fun (d : Hewett2026.Row) => (d.root, d.cat, d.template)) rows

theorem Hewett2026.CategoryDetermined.of_rootDetermined {rows : List Row} (h : RootDetermined rows) : CategoryDetermined rows

theorem Hewett2026.TemplateDetermined.of_categoryDetermined {rows : List Row} (h : CategoryDetermined rows) : TemplateDetermined rows

theorem Hewett2026.apologi_rootDetermined : RootDetermined (rows Root.apologi)

√apologi selects for in every category (1).

theorem Hewett2026.fxr_rootDetermined : RootDetermined (rows Root.fxr)

√fxr selects b- in every category (2).

theorem Hewett2026.xwf_rootDetermined : RootDetermined (rows Root.xwf)

√xwf selects min in both templates (11), a template-independent l-selection.

theorem Hewett2026.prd_not_rootDetermined : ¬RootDetermined (rows Root.prd)

√prd selects on, in and of by category (5), so the root alone does not determine the preposition, though the root with its category does.

theorem Hewett2026.prd_categoryDetermined : CategoryDetermined (rows Root.prd)

theorem Hewett2026.brk_not_rootDetermined : ¬RootDetermined (rows Root.brk)

√brk selects b- as a verb and ʕala as a noun (6).

theorem Hewett2026.brk_categoryDetermined : CategoryDetermined (rows Root.brk)

theorem Hewett2026.krh_not_categoryDetermined : ¬CategoryDetermined (rows Root.krh)

√krh takes a bare object in XaYaZ and fi in XaYYaZ (13a), so the root and its category do not determine the preposition and selection at or below the categorizer is too early.

theorem Hewett2026.dwr_not_categoryDetermined : ¬CategoryDetermined (rows Root.dwr)

√dwr selects b- in XaYaZ and ʕala in XaYYaZ (13b).

theorem Hewett2026.Hkm_not_categoryDetermined : ¬CategoryDetermined (rows Root.Hkm)

√ħkm selects ʕala in XaYaZ and no preposition in XaYYaZ (14).

theorem Hewett2026.tpl_not_categoryDetermined : ¬CategoryDetermined (rows Root.tpl)

√tpl selects be- in XiYeZ and suppresses it in the passive XuYaZ (17).

theorem Hewett2026.shps_not_categoryDetermined : ¬CategoryDetermined (rows Root.shps)

√ʃpʕ selects al in hiXYiZ and suppresses it in the passive huXYaZ (18).

theorem Hewett2026.data_templateDetermined : TemplateDetermined data

The root, its category and the template together determine the preposition throughout the data, which is the fixing point of l-selection.

theorem Hewett2026.data_not_categoryDetermined : ¬CategoryDetermined data

The data are not determined below the template.

Joint selection via Activate (23)

@[reducible, inline]

abbrev Hewett2026.Key : Type

An activation key is a category feature, stripped by the categorizing head, or a template, stripped by the template-defining head.

Equations

• Hewett2026.Key = (Minimalist.Cat ⊕ Hewett2026.Template)

structure Hewett2026.ActivationIndex : Type

An ordered tuple of activation keys ((23), after [Mer15]). Each c-commanding head bearing the leftmost key strips it, and the feature is active once the tuple is exhausted, a derivational time bomb in the sense of [Pre14].

• remaining : List Key

  The keys remaining to be stripped.

def Hewett2026.instDecidableEqActivationIndex.decEq (x✝ x✝¹ : ActivationIndex) : Decidable (x✝ = x✝¹)

Equations

• Hewett2026.instDecidableEqActivationIndex.decEq { remaining := a } { remaining := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hewett2026.instDecidableEqActivationIndex : DecidableEq ActivationIndex

Equations

• Hewett2026.instDecidableEqActivationIndex = Hewett2026.instDecidableEqActivationIndex.decEq

def Hewett2026.ActivationIndex.activate (idx : ActivationIndex) (key : Key) : ActivationIndex

The tuple after a head bearing key, which strips the leftmost key when it matches and leaves the tuple as it is otherwise.

Equations

• idx.activate key = match idx.remaining with | k :: rest => if k = key then { remaining := rest } else idx | [] => idx

def Hewett2026.ActivationIndex.IsActive (idx : ActivationIndex) : Prop

The tuple is exhausted and the feature it indexes is active.

Equations

• idx.IsActive = (idx.remaining = [])

@[instance_reducible]

instance Hewett2026.ActivationIndex.instDecidablePredIsActive : DecidablePred IsActive

Equations

• idx.instDecidablePredIsActive = Hewett2026.ActivationIndex.instDecidablePredIsActive._aux_1 idx

structure Hewett2026.SelectionalFeature : Type

A selectional feature [SEL: p^C] (23), the preposition it selects, visible to selection only once its activation tuple C is exhausted.

• prep : Prep

  The selected preposition.

• activation : ActivationIndex

  The ordered activation tuple.

def Hewett2026.SelectionalFeature.dormant (p : Prep) (t : Template) : SelectionalFeature

The feature [SEL: p⟨V, t⟩], dormant until the categorizing head and then the template t have activated it.

Equations

• Hewett2026.SelectionalFeature.dormant p t = { prep := p, activation := { remaining := [Sum.inl Minimalist.Cat.V, Sum.inr t] } }

def Hewett2026.SelectionalFeature.activate (f : SelectionalFeature) (k : Key) : SelectionalFeature

Activate (23) by a c-commanding head bearing the key.

Equations

• f.activate k = { prep := f.prep, activation := f.activation.activate k }

def Hewett2026.SelectionalFeature.IsActive (f : SelectionalFeature) : Prop

The feature is active once its tuple is exhausted.

Equations

• f.IsActive = f.activation.IsActive

@[instance_reducible]

instance Hewett2026.SelectionalFeature.instDecidablePredIsActive : DecidablePred IsActive

Equations

• f.instDecidablePredIsActive = Hewett2026.SelectionalFeature.instDecidablePredIsActive._aux_1 f

theorem Hewett2026.SelectionalFeature.not_isActive_dormant (p : Prep) (t : Template) : ¬(dormant p t).IsActive

A dormant feature is inactive, a derivational time bomb ([Pre14]).

theorem Hewett2026.SelectionalFeature.not_isActive_activate_V (p : Prep) (t : Template) : ¬((dormant p t).activate (Sum.inl Minimalist.Cat.V)).IsActive

The categorizing head alone leaves the template key.

theorem Hewett2026.SelectionalFeature.activate_template_first (p : Prep) (t : Template) : ((dormant p t).activate (Sum.inr t)).activation.remaining = [Sum.inl Minimalist.Cat.V, Sum.inr t]

The template before the categorizing head strips nothing, since only the leftmost key can be matched.

theorem Hewett2026.SelectionalFeature.isActive_activate_V_template (p : Prep) (t : Template) : (((dormant p t).activate (Sum.inl Minimalist.Cat.V)).activate (Sum.inr t)).IsActive

The categorizing head and then the matching template activate the feature.

theorem Hewett2026.SelectionalFeature.not_isActive_activate_V_other (p : Prep) (t : Template) {t' : Template} (h : t' ≠ t) : ¬(((dormant p t).activate (Sum.inl Minimalist.Cat.V)).activate (Sum.inr t')).IsActive

Another template leaves the feature inactive, so the features of one root for different templates are mutually exclusive.

def Hewett2026.entry (r : Root) : List SelectionalFeature

The lexical entry of a root (§4), one dormant feature per attested template in which it selects a preposition, [SEL: {b⟨V, XaYaZ⟩, ʕala⟨V, XaYYaZ⟩}] for √dwr.

Equations

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

def Hewett2026.derive (r : Root) (t : Template) : List SelectionalFeature

The derivations (24) and (25), in which the categorizing head activates the root's features and the template-defining head follows.

Equations

• Hewett2026.derive r t = List.map (fun (f : Hewett2026.SelectionalFeature) => (f.activate (Sum.inl Minimalist.Cat.V)).activate (Sum.inr t)) (Hewett2026.entry r)

def Hewett2026.selected (r : Root) (t : Template) : List Prep

The prepositions the active features select after the derivation.

Equations

• Hewett2026.selected r t = List.filterMap (fun (f : Hewett2026.SelectionalFeature) => if f.IsActive then some f.prep else none) (Hewett2026.derive r t)

theorem Hewett2026.dwr_XaYaZ : selected Root.dwr Template.XaYaZ = [Prep.b]

In XaYaZ the root √dwr's feature for b- is activated and the one for ʕala is not (24).

theorem Hewett2026.dwr_XaYYaZ : selected Root.dwr Template.XaYYaZ = [Prep.Eala]

In XaYYaZ it is the feature for ʕala that is activated (25).

theorem Hewett2026.selected_eq (d : Row) : d ∈ data → ∀ (t : Template), d.template = some t → selected d.root t = d.prep.toList

Joint selection reproduces the data. In every attested root–template pairing the active features select exactly the attested preposition, and none where none is selected.