Docs / Syntax / Minimalist / Feature / Interpretability

Interpretable and uninterpretable features

import Linglib.Syntax.Minimalist.Feature.Interpretability · namespace Minimalist

This file defines interpretability and the dual-feature system of Adamson & Anagnostopoulou 2025, together with the operations of that system on coordinations.

A feature is interpretable if it is read at LF and uninterpretable otherwise (Chomsky 1995). In a dual-feature system (Smith 2015) a nominal bears two sets of features of one kind: its interpretable features (iFs), which Transfer sends to LF, and its uninterpretable features (uFs), which Transfer sends to PF. A nominal with no uFs sends its iFs to PF as well, by the redundancy rule.

In a coordination, one feature set of each conjunct percolates to &P, either its iFs or its uFs. Conversion intersects the percolated iF sets, so that &P bears the iFs that every conjunct bears. Percolated uF sets are not intersected. PF realizes each of them, and realization succeeds only if every set receives the same exponent.

Main definitions

Minimalist.Interpretability: interpretable or uninterpretable.
Minimalist.DualFeature.Bundle: a set of iFs and a set of uFs.
Minimalist.DualFeature.Bundle.toPF: the features a bundle sends to PF.
Minimalist.DualFeature.resolve: the iFs two conjuncts share.
Minimalist.DualFeature.realizeAll: the exponent of a family of feature sets.

Implementation notes

A bundle is a function on Interpretability, so bundles are ordered and combined pointwise. The features of a nominal built from two layers are the join ⊔ of the layers' bundles.

References

Chomsky 1995, The Minimalist Program formalized
Smith 2015, Feature Mismatches: Consequences for Syntax, Morphology and Semantics
Adamson & Anagnostopoulou 2025, Gender features and coordination resolution in Greek and other three-gendered languages: Implications for the crosslinguistic representation of gender formalized

Declarations

Whether a feature is read at LF.

inductive Interpretability L48–52

Type

interpretable : Interpretability
uninterpretable : Interpretability

Derives Repr, DecidableEq, Fintype.

Used by DualFeature.Bundle, DualFeature.Bundle.single, DualFeature.Bundle.single_self, DualFeature.Bundle.single_of_ne, DualFeature.resolve_single

Used in Morphology/DistributedMorphology/Gender, Carstens2026

The features of a nominal: a set of iFs and a set of uFs.

@[reducible, inline] abbrev DualFeature.Bundle L58–59

(F : Type u_3) :

Type u_3

DualFeature.Bundle F = (Interpretability → Finset F)

Built from

Used by DualFeature.Bundle.single, DualFeature.Bundle.toPF, DualFeature.resolve, DualFeature.mem_resolve, DualFeature.resolve_comm

Used in AdamsonAnagnostopoulou2025, Carstens2026

L63–64

L66–67

L69–71

The features a bundle sends to PF: its uFs, or its iFs if it has no uFs. The second case is the redundancy rule, (13) of Adamson & Anagnostopoulou 2025.

def DualFeature.Bundle.toPF L73–76

{F : Type u_1} [DecidableEq F] (b : Bundle F) :

Finset F

b.toPF = if b Interpretability.uninterpretable = ∅ then b Interpretability.interpretable else b Interpretability.uninterpretable

Built from

Used by DualFeature.Bundle.toPF_single_interpretable

Used in AdamsonAnagnostopoulou2025

L78–80

The iFs that two conjuncts both bear, the output of conversion, (29) of Adamson & Anagnostopoulou 2025.

def DualFeature.resolve L88–90

{F : Type u_1} [DecidableEq F] (a b : Bundle F) :

Finset F

DualFeature.resolve a b = a Interpretability.interpretable ∩ b Interpretability.interpretable

Built from

Used by DualFeature.mem_resolve, DualFeature.resolve_comm, DualFeature.resolve_single

Used in AdamsonAnagnostopoulou2025, Carstens2026

L92–94

L96–97

L99–102

The exponent that every set in l receives, if l is nonempty and there is one. PF realizes each percolated set separately (p. 25 of Adamson & Anagnostopoulou 2025).

def DualFeature.realizeAll L106–110

{F : Type u_1} {E : Type u_2} [DecidableEq E] (realize : Finset F → Option E) :

List (Finset F) → Option E

DualFeature.realizeAll realize [] = none
DualFeature.realizeAll realize (s :: ss) = if ∀ t ∈ ss, realize t = realize s then realize s else none

Used by DualFeature.realizeAll_eq_some_iff, DualFeature.realizeAll_singleton

Used in AdamsonAnagnostopoulou2025

L112–122

L124–126