Documentation

Linglib.Fragments.Hungarian.Focus

Hungarian Focus and the Identificational/Information Distinction #

@cite{kiss-1998}

@cite{kiss-1998} argues that two structurally distinct focus types must be distinguished in Hungarian:

Identificational focus moves to the specifier of a left-peripheral functional projection (Spec,FP), surfacing in the immediately preverbal position. It expresses exhaustive identification — selecting the maximal subset of contextually-given alternatives for which the predicate holds.
Information focus stays VP-internal in the postverbal domain, marked only by pitch accent. It conveys nonpresupposed information without exhaustivity.

The two are not interpretational variants of one operator: they occupy distinct structural positions and trigger distinct semantic operations. This is the structural basis for the Hungarian–English parallel @cite{kiss-1998} draws (English clefts realise identificational focus) and the typological pivot for the @cite{hartmann-zimmermann-2007} debate (Hausa is the negative counterpart: in-situ position does not block focus interpretation).

Distributional restrictions (paper §3): identificational focus is barred from universal quantifiers (minden 'every'), additive also-phrases (X+is) and even-phrases (még…is), and the existential valami/valaki 'somebody/something'. Csak 'only'-phrases are obligatorily realised as identificational foci. The minimal class encoding here lets us state and prove these restrictions as theorems rather than stipulate them inline.

FocusConfig.Licensed is propositional (Prop with Decidable). The structure carries a position, a focus type, and a constituent class; licensing combines the position–type pairing with the §3 class-based distributional facts. Smart constructors mkIdentificational and mkInformation package the position–type pairing automatically; ill-licensed combinations are constructed directly to demonstrate the predicate has bite.

inductive Fragments.Hungarian.Focus.Position :

The two structural positions for focused constituents in Hungarian. preverbal = Spec,FP (the immediately preverbal identificational focus slot, see @cite{kiss-1998} eq. 5a); postverbal = VP-internal in situ (the information focus position, see eq. 5b).

preverbal : Position
postverbal : Position

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instDecidableEqPosition :

DecidableEq Position

Equations

Fragments.Hungarian.Focus.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instReprPosition :

Equations

Fragments.Hungarian.Focus.instReprPosition = { reprPrec := Fragments.Hungarian.Focus.instReprPosition.repr }

def Fragments.Hungarian.Focus.instReprPosition.repr :

Position → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instInhabitedPosition :

Inhabited Position

Equations

Fragments.Hungarian.Focus.instInhabitedPosition = { default := Fragments.Hungarian.Focus.instInhabitedPosition.default }

def Fragments.Hungarian.Focus.instInhabitedPosition.default :

Equations

Fragments.Hungarian.Focus.instInhabitedPosition.default = Fragments.Hungarian.Focus.Position.preverbal

Instances For

inductive Fragments.Hungarian.Focus.FocusType :

The two focus types @cite{kiss-1998} distinguishes. The identificational type carries an exhaustivity entailment; information focus does not. The eq. 5a vs 5b minimal pair is the empirical pivot.

identificational : FocusType
information : FocusType

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instDecidableEqFocusType :

DecidableEq FocusType

Equations

Fragments.Hungarian.Focus.instDecidableEqFocusType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instReprFocusType :

Equations

Fragments.Hungarian.Focus.instReprFocusType = { reprPrec := Fragments.Hungarian.Focus.instReprFocusType.repr }

def Fragments.Hungarian.Focus.instReprFocusType.repr :

FocusType → Nat → Std.Format

Equations

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

Instances For

def Fragments.Hungarian.Focus.instInhabitedFocusType.default :

Equations

Fragments.Hungarian.Focus.instInhabitedFocusType.default = Fragments.Hungarian.Focus.FocusType.identificational

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instInhabitedFocusType :

Inhabited FocusType

Equations

Fragments.Hungarian.Focus.instInhabitedFocusType = { default := Fragments.Hungarian.Focus.instInhabitedFocusType.default }

def Fragments.Hungarian.Focus.FocusType.IsExhaustive :

FocusType → Prop

Whether the focus type carries an exhaustivity entailment. Direct consequence of @cite{kiss-1998} §2 (the Szabolcsi–Farkas test). Stated at the FocusType level — exhaustivity is intrinsic to the type, independent of any particular configuration.

Equations

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instDecidableIsExhaustive (t : FocusType) :

Decidable t.IsExhaustive

Equations

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

inductive Fragments.Hungarian.Focus.ConstituentClass :

Coarse classification of the focused constituent for the §3 distributional facts. regular covers ordinary DPs that can occur as either focus type; universal is the minden 'every' / X+is 'also' / még…is 'even' class barred from identificational focus (paper eq. 17b–d); onlyPhrase is csak X 'only X', obligatorily identificational; someIndef is valami/valaki 'somebody/something', barred from both focus positions (paper eq. 17e).

regular : ConstituentClass
universal : ConstituentClass
onlyPhrase : ConstituentClass
someIndef : ConstituentClass

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instDecidableEqConstituentClass :

DecidableEq ConstituentClass

Equations

Fragments.Hungarian.Focus.instDecidableEqConstituentClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instReprConstituentClass :

Repr ConstituentClass

Equations

Fragments.Hungarian.Focus.instReprConstituentClass = { reprPrec := Fragments.Hungarian.Focus.instReprConstituentClass.repr }

def Fragments.Hungarian.Focus.instReprConstituentClass.repr :

ConstituentClass → Nat → Std.Format

Equations

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

Instances For

def Fragments.Hungarian.Focus.instInhabitedConstituentClass.default :

ConstituentClass

Equations

Fragments.Hungarian.Focus.instInhabitedConstituentClass.default = Fragments.Hungarian.Focus.ConstituentClass.regular

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instInhabitedConstituentClass :

Inhabited ConstituentClass

Equations

Fragments.Hungarian.Focus.instInhabitedConstituentClass = { default := Fragments.Hungarian.Focus.instInhabitedConstituentClass.default }

structure Fragments.Hungarian.Focus.FocusConfig :

A Hungarian focused-clause configuration. Position, focus type, and constituent class are independent fields at the structure level; Licensed enforces the @cite{kiss-1998} pairings.

position : Position
The structural position of the focused constituent.
focusType : FocusType
The focus type (identificational vs information).
cclass : ConstituentClass
The lexical class of the focused constituent.

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instDecidableEqFocusConfig :

DecidableEq FocusConfig

Equations

Fragments.Hungarian.Focus.instDecidableEqFocusConfig = Fragments.Hungarian.Focus.instDecidableEqFocusConfig.decEq

def Fragments.Hungarian.Focus.instDecidableEqFocusConfig.decEq (x✝ x✝¹ : FocusConfig) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instReprFocusConfig :

Repr FocusConfig

Equations

Fragments.Hungarian.Focus.instReprFocusConfig = { reprPrec := Fragments.Hungarian.Focus.instReprFocusConfig.repr }

def Fragments.Hungarian.Focus.instReprFocusConfig.repr :

FocusConfig → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instInhabitedFocusConfig :

Inhabited FocusConfig

Equations

Fragments.Hungarian.Focus.instInhabitedFocusConfig = { default := Fragments.Hungarian.Focus.instInhabitedFocusConfig.default }

def Fragments.Hungarian.Focus.instInhabitedFocusConfig.default :

Equations

Fragments.Hungarian.Focus.instInhabitedFocusConfig.default = { position := default, focusType := default, cclass := default }

Instances For

def Fragments.Hungarian.Focus.positionFor :

FocusType → Position

The canonical position for a given focus type. Paper §2: in Hungarian, identificational focus moves to Spec,FP (preverbal); information focus stays VP-internal (postverbal).

Equations

Instances For

def Fragments.Hungarian.Focus.ConstituentClass.compatibleWith :

ConstituentClass → FocusType → Prop

A constituent class is compatible with a focus type per @cite{kiss-1998} §3:

regular works as either type;
universal is barred from identificational (eq. 17b–d) but can be information focus (eq. 19b);
onlyPhrase is obligatorily identificational (paper §3 last ¶);
someIndef is barred from both focus positions (eq. 17e and surrounding prose: "Some-phrases … cannot function as information foci, either").

Equations

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instDecidableCompatibleWith (c : ConstituentClass) (t : FocusType) :

Decidable (c.compatibleWith t)

Equations

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

def Fragments.Hungarian.Focus.FocusConfig.Licensed (c : FocusConfig) :

A FocusConfig is licensed iff (i) its position is the canonical position for its focus type (paper §2) and (ii) its constituent class is compatible with that focus type (paper §3).

Equations

c.Licensed = (c.position = Fragments.Hungarian.Focus.positionFor c.focusType ∧ c.cclass.compatibleWith c.focusType)

Instances For

@[implicit_reducible]

instance Fragments.Hungarian.Focus.instDecidableLicensed (c : FocusConfig) :

Decidable c.Licensed

Equations

Fragments.Hungarian.Focus.instDecidableLicensed c = Fragments.Hungarian.Focus.instDecidableLicensed._aux_1 c

def Fragments.Hungarian.Focus.mkIdentificational (cc : ConstituentClass) (_h : cc.compatibleWith FocusType.identificational) :

Smart constructor for a preverbal identificational focus. The position–type pairing is automatic; the caller supplies the constituent class and a proof of compatibility.

Equations

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

Instances For

def Fragments.Hungarian.Focus.mkInformation (cc : ConstituentClass) (_h : cc.compatibleWith FocusType.information) :

Smart constructor for a postverbal information focus. The position–type pairing is automatic; the caller supplies the constituent class and a proof of compatibility.

Equations

Fragments.Hungarian.Focus.mkInformation cc _h = { position := Fragments.Hungarian.Focus.Position.postverbal, focusType := Fragments.Hungarian.Focus.FocusType.information, cclass := cc }

Instances For

theorem Fragments.Hungarian.Focus.mkIdentificational_licensed (cc : ConstituentClass) (h : cc.compatibleWith FocusType.identificational) :

(mkIdentificational cc h).Licensed

Configurations built by mkIdentificational are licensed.

theorem Fragments.Hungarian.Focus.mkInformation_licensed (cc : ConstituentClass) (h : cc.compatibleWith FocusType.information) :

(mkInformation cc h).Licensed

Configurations built by mkInformation are licensed.

theorem Fragments.Hungarian.Focus.licensed_position_determines_type (c : FocusConfig) (h : c.Licensed) :

c.position = Position.preverbal ↔ c.focusType = FocusType.identificational

Position determines focus type for licensed configurations. The structural pairing in FocusConfig.Licensed makes the focus type a function of the position. This is the load-bearing biconditional that lets the Meaning-Structure Mapping Hypothesis be proved for Hungarian (vs refuted for Hausa).

theorem Fragments.Hungarian.Focus.onlyPhrase_forces_identificational (c : FocusConfig) (h : c.Licensed) (hcc : c.cclass = ConstituentClass.onlyPhrase) :

c.focusType = FocusType.identificational

csak-phrases must be identificational foci (paper §3 last paragraph, eq. 51–53). Any licensed configuration with an onlyPhrase constituent has identificational focus type.

theorem Fragments.Hungarian.Focus.someIndef_never_licensed (c : FocusConfig) (h : c.Licensed) :

c.cclass ≠ ConstituentClass.someIndef

valami/valaki can never be focused (paper eq. 17e and surrounding prose). No licensed configuration has an someIndef constituent — neither focus type accepts it.