Relativization

These theory-neutral types describe relativization across languages. The relativizable positions of Keenan and Comrie's Accessibility Hierarchy form a bounded linear order; a relative clause has a placement relative to its head; something occupies the relativized position (NP_rel); and the fragments record each language's relativizers.

Main declarations

• Relativization.Position — the relativizable positions, linearly ordered by accessibility with the subject on top: the Accessibility Hierarchy.
• Relativization.Placement — the clause's placement relative to the head noun.
• Relativization.NPRel — what occupies the relativized position.
• Relativizer — a relativizer with its placement and what occupies NP_rel at each position.

Implementation notes

A relativizer's realization is a finite relation between positions and NP_rel types, given as a Finset-valued function so that fragments enter it by cases and every check decides. A fragment records one entry per relativizer, as a grammar describes it, with free variation where the grammar reports it (Hebrew she- with a gap or a resumptive at the direct object). A classification of relative clauses is a predicate on NPRel pulled back along the realization, and lives with the paper that draws it: Keenan and Comrie's ±case and their "RC-forming strategies" are derived in Studies/KeenanComrie1977.lean.

A restrictive relative clause needs no semantic rule of its own: the composition engine of Semantics/Composition/Tree.lean interprets it by Predicate Abstraction over the gap and Predicate Modification with the head, as Studies/HeimKratzer1998.lean computes.

References

• [KC77]
• [Ryd05]
• [Sco21]
• [Sic14]

The Accessibility Hierarchy

inductive Relativization.Position : Type

The relativizable positions of [KC77]'s Accessibility Hierarchy, subject > direct object > indirect object > oblique > genitive > object of comparison. A higher position is relativizable in more languages and by lighter strategies.

• subject : Position
• directObject : Position
• indirectObject : Position
• oblique : Position
• genitive : Position
• objComparison : Position

  The object of comparison, "the person [that I am taller than _]".

@[instance_reducible]

instance Relativization.instDecidableEqPosition : DecidableEq Position

Equations

• Relativization.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Relativization.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Relativization.instReprPosition : Repr Position

Equations

• Relativization.instReprPosition = { reprPrec := Relativization.instReprPosition.repr }

@[instance_reducible]

instance Relativization.instFintypePosition : Fintype Position

Equations

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

def Relativization.Position.rank : Position → ℕ

The rank of a position, higher for the more accessible.

Equations

• Relativization.Position.subject.rank = 5
• Relativization.Position.directObject.rank = 4
• Relativization.Position.indirectObject.rank = 3
• Relativization.Position.oblique.rank = 2
• Relativization.Position.genitive.rank = 1
• Relativization.Position.objComparison.rank = 0

theorem Relativization.Position.rank_injective : Function.Injective rank

@[instance_reducible]

instance Relativization.Position.instLinearOrder : LinearOrder Position

In the accessibility order p ≤ q iff p is no more accessible than q.

Equations

• Relativization.Position.instLinearOrder = LinearOrder.lift' Relativization.Position.rank Relativization.Position.rank_injective

@[instance_reducible]

instance Relativization.Position.instBoundedOrder : BoundedOrder Position

The subject is the top of the hierarchy, the object of comparison its bottom.

Equations

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

@[instance_reducible]

instance Relativization.Position.instLocallyFiniteOrder : LocallyFiniteOrder Position

Equations

• Relativization.Position.instLocallyFiniteOrder = Fintype.toLocallyFiniteOrder

Placement of the clause

inductive Relativization.Placement : Type

The placement of the relative clause relative to its head noun.

• postNominal : Placement

  The clause follows the head, English "the man [who left]".

• preNominal : Placement

  The clause precedes the head, Japanese "[ _ kaetta] hito".

• internallyHeaded : Placement

  The head sits inside the clause, as in Washo ([Han21]).

• correlative : Placement

  The clause, with the head inside it, stands outside the main clause and is linked anaphorically to a noun phrase there ([Dry13]), as Hindi-Urdu jo … vo and Bambara relatives are.

@[instance_reducible]

instance Relativization.instDecidableEqPlacement : DecidableEq Placement

Equations

• Relativization.instDecidableEqPlacement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Relativization.instReprPlacement : Repr Placement

Equations

• Relativization.instReprPlacement = { reprPrec := Relativization.instReprPlacement.repr }

def Relativization.instReprPlacement.repr : Placement → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Relativization.instFintypePlacement : Fintype Placement

Equations

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

What occupies the relativized position

inductive Relativization.NPRel : Type

What occupies the relativized position NP_rel inside the clause. A relativizer that does not vary with the relativized position, such as a complementizer or a relative pronoun agreeing with the head, leaves NP_rel a gap.

• gap : NPRel

  Nothing overt at the relativized position, English "the man [that _ left]".

• resumptive : NPRel

  A personal pronoun, Modern Standard Arabic al-kitaab-u lladhii qaraʾ-naa-hu 'the book that we read (it)' ([Ryd05]).

• resumptiveMovement : NPRel

  A resumptive that is a partially pronounced lower copy of an Ā-movement chain, diagnosed by parasitic gaps ([Sco21]).

• resumptiveBound : NPRel

  A base-generated resumptive bound by the head, obligatory inside adjunct islands ([Sco21]).

• relPronoun : NPRel

  A relative pronoun marked for the relativized position, by its case or an accompanying adposition, German "der Mann [den ich sah]".

• nonReduction : NPRel

  The head noun repeated in full inside the clause, as in Bambara.

@[instance_reducible]

instance Relativization.instDecidableEqNPRel : DecidableEq NPRel

Equations

• Relativization.instDecidableEqNPRel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Relativization.instReprNPRel : Repr NPRel

Equations

• Relativization.instReprNPRel = { reprPrec := Relativization.instReprNPRel.repr }

def Relativization.instReprNPRel.repr : NPRel → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Relativization.instFintypeNPRel : Fintype NPRel

Equations

• Relativization.instFintypeNPRel = { elems := { val := ↑Relativization.NPRel.enumList, nodup := Relativization.NPRel.enumList_nodup }, complete := Relativization.instFintypeNPRel._proof_1 }

Relativizers

structure Relativizer : Type

A relativizer of a language, the particle, pronoun or affix introducing a relative clause or the zero relativizer, with the placement of its clause and what occupies NP_rel at each position of the hierarchy: empty where it does not relativize the position, several values where they alternate.

• form : String

  The form, "∅" for the zero relativizer.

• placement : Relativization.Placement

  The clause's placement relative to the head.

• realize : Relativization.Position → Finset Relativization.NPRel

  What may occupy NP_rel at each position.