Host-dependent interpretability and ordered feature activation

[Cho95] [Hew26]

Two feature utilities that survive the retirement of the 1995 checking lifecycle. The TrackedFeature activate→check→erase state machine and its convergesAtLF/convergesAtSpellOut convergence predicates — Old-Minimalism feature checking — are removed: consistency of feature assignments across substructures is now the MCB Birkhoff renormalization Minimalist.headConsistency (the "single recursive map", Agree/Consistency.lean), a post-syntactic filter over the feature-free core, not a per-feature state machine.

What remains:

• Host-dependent interpretability (isInterpretableOn): whether a feature type is +/−Interpretable on a given host category ([Cho95] Ch. 4 — categorial and nominal φ-features are interpretable; Case and functional-head φ-features are not).
• Ordered activation indices (ActivationIndex, [Hew26] ex. (23)): a feature carries an ordered tuple of category keys; each c-commanding head strips the leftmost matching key, and an exhausted tuple is .active. The formal core of Hewett's Joint Selection via Activate — a [Pre14] "derivational time bomb". (Reformulating [Hew26]'s selection itself in terms of the Birkhoff machinery is future work.)

Host-dependent interpretability

def Minimalist.isInterpretableOn (fv : FeatureVal) (host : Cat) : Interpretability

Whether a feature type is interpretable on a given host category.

[Cho95] Ch 4: Categorial features and φ-features of nouns are +Interpretable. Case features, φ-features on functional heads (T, v, C), and EPP/strong features are –Interpretable.

This encodes the default mapping. Individual languages or analyses may override (e.g., [Zei12] treats embedded tense as uninterpretable in SOT languages).

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.isInterpretableOn fv host = match fv.inherentInterpretability with | some i => i | none => Minimalist.Interpretability.interpretable

theorem Minimalist.phi_on_N_interpretable (pf : PhiFeature) : isInterpretableOn (FeatureVal.phi pf) Cat.N = Interpretability.interpretable

Phi on N is interpretable; phi on T is not.

theorem Minimalist.phi_on_T_uninterpretable (pf : PhiFeature) : isInterpretableOn (FeatureVal.phi pf) Cat.T = Interpretability.uninterpretable

Feature activation status

inductive Minimalist.FeatureStatus : Type

The activation state of a feature: .inactive while its activation tuple is non-empty (a [Pre14] "derivational time bomb"), .active once the tuple is exhausted. The codomain of ActivationIndex.toStatus.

• inactive : FeatureStatus

  Present but dormant: an unexhausted activation tuple, awaiting licensing by the right c-commanding heads ([Hew26] ex. (23)).

• active : FeatureStatus

  Fully activated: the tuple is exhausted and the feature is accessible.

@[implicit_reducible]

instance Minimalist.instReprFeatureStatus : Repr FeatureStatus

Equations

• Minimalist.instReprFeatureStatus = { reprPrec := Minimalist.instReprFeatureStatus.repr }

def Minimalist.instReprFeatureStatus.repr : FeatureStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqFeatureStatus : DecidableEq FeatureStatus

Equations

• Minimalist.instDecidableEqFeatureStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Ordered activation tuples ([Hew26] ex. (23))

[Hew26] ex. (23) (adapted from [Mer15]): a feature can be indexed by an ordered tuple of category keys (c₁, …, cₙ). Each c-commanding head bearing key k strips c₁ from the tuple if k = c₁ (matching activation). When the tuple is exhausted the feature transitions from .inactive to .active.

ActivationIndex α is parametric over the key type α — for Semitic l-selection α combines Cat and SemiticTemplate, but the mechanism generalizes to any domain where features require ordered multi-head activation (e.g., applicatives, serial verbs).

structure Minimalist.ActivationIndex (α : Type) [BEq α] : Type

An ordered tuple of activation keys. Stripping proceeds left-to-right: only the leftmost key can be matched at any derivational step.

• remaining : List α

  Keys remaining to be stripped. Empty = fully activated.

@[implicit_reducible]

instance Minimalist.instReprActivationIndex {α✝ : Type} {inst✝ : BEq α✝} [Repr α✝] : Repr (ActivationIndex α✝)

Equations

• Minimalist.instReprActivationIndex = { reprPrec := Minimalist.instReprActivationIndex.repr }

def Minimalist.instReprActivationIndex.repr {α✝ : Type} {inst✝ : BEq α✝} [Repr α✝] : ActivationIndex α✝ → ℕ → Std.Format

Equations

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

def Minimalist.ActivationIndex.activate {α : Type} [BEq α] (idx : ActivationIndex α) (key : α) : ActivationIndex α

Attempt to strip the leftmost key. Succeeds only if key matches the head of the tuple (matching activation). Non-matching keys and already-empty tuples are no-ops.

Equations

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

def Minimalist.ActivationIndex.isFullyActive {α : Type} [BEq α] (idx : ActivationIndex α) : Bool

Is the tuple fully stripped?

Equations

• idx.isFullyActive = idx.remaining.isEmpty

def Minimalist.ActivationIndex.toStatus {α : Type} [BEq α] (idx : ActivationIndex α) : FeatureStatus

Map activation state to the FeatureStatus: non-empty tuples are .inactive, empty tuples are .active.

Equations

• idx.toStatus = if idx.isFullyActive = true then Minimalist.FeatureStatus.active else Minimalist.FeatureStatus.inactive

theorem Minimalist.activate_matching_strips {α : Type} [BEq α] [LawfulBEq α] (k : α) (rest : List α) : { remaining := k :: rest }.activate k = { remaining := rest }

Matching key strips the head.

theorem Minimalist.activate_nonmatching_noop {α : Type} [BEq α] [LawfulBEq α] (k₁ k₂ : α) (rest : List α) (h : k₁ ≠ k₂) : { remaining := k₁ :: rest }.activate k₂ = { remaining := k₁ :: rest }

Non-matching key is a no-op.

theorem Minimalist.empty_is_active {α : Type} [BEq α] : { remaining := [] }.isFullyActive = true

Empty tuple is fully active.

theorem Minimalist.nonempty_is_inactive {α : Type} [BEq α] (k : α) (rest : List α) : { remaining := k :: rest }.isFullyActive = false

Non-empty tuple is not fully active.

theorem Minimalist.empty_toStatus_active {α : Type} [BEq α] : { remaining := [] }.toStatus = FeatureStatus.active

Empty tuple maps to .active status.

theorem Minimalist.nonempty_toStatus_inactive {α : Type} [BEq α] (k : α) (rest : List α) : { remaining := k :: rest }.toStatus = FeatureStatus.inactive

Non-empty tuple maps to .inactive status.

theorem Minimalist.activate_empty_noop {α : Type} [BEq α] (key : α) : { remaining := [] }.activate key = { remaining := [] }

Activation on an already-empty tuple is a no-op.

theorem Minimalist.full_activation_chain {α : Type} [BEq α] [LawfulBEq α] (k₁ k₂ : α) : have idx := { remaining := [k₁, k₂] }; ((idx.activate k₁).activate k₂).toStatus = FeatureStatus.active

Full activation chain: stripping each key in order yields .active.