Documentation

Studies.Hanink2021

Hanink (2021): DP Structure and Internally Headed Relatives in Washo #

Hanink argues that an index is a syntactic head of its own, idx below D, which Washo pronounces gi ~ ge in third-person pronouns (1), in demonstratives (2), and at the edge of internally headed relative clauses (3), DPs over a nominalized CP (40). The index has two meanings (80). As a variable it restricts D's ι to its antecedent (15), with the deixis of hádi and wídi a presupposition on D (34). As a binder it turns the embedded clause, whose semantic head is a restricted variable (69), into a property without movement, so the relative denotes what an externally headed relative denotes by raising and Predicate Modification, (72) and (60). The Prohibition against Vacuous Binding (86) leaves the binder meaning to complements with a free variable, and the Vocabulary for idx (119) and D (130), with contextual specificity ranked above the Elsewhere Principle (118), derives where gi is overt. The examples are the rows of Data.Examples.Hanink2021, among them section 4's island-insensitivity and stacking and the absence of the head's φ-features on idx (91), which makes its relation to the head binding rather than Agree.

Main results #

Implementation notes #

The index is the substrate's assignment index, so the variable meaning is idxVar and the binder meaning lambdaAbsG; D's ι is iota, whose ∃! presupposition is (34a)'s. The R head of demonstratives (35) is the identity relation, so it is not represented. Ellipsis of a pronoun's NP is recorded as the complement lacking the feature that makes an NP overt (section 6.3). The quantified heads of section 5.1 and the German relative-clause parallel of section 4.4 are recorded as data and prose only. Hanink calls wídi proximal and hádi distal; their deictic content is read as the two cells of Harbour's author bipartition, the participant sets containing the speaker and the others.

TODO #

References #

The two meanings of the index, (80) #

source
def Hanink2021.idxVar {E : Type} (n : ℕ) :
Assignment E → E → Prop

The index as a variable, (80a) and (14), denotes the property of being its value.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Hanink2021.idxBind {E : Type} (n : ℕ) (φ : Assignment E → Prop) :
    Assignment E → E → Prop

    The index as a binder, (80b), takes the open proposition of its complement to the property of the values of the variable that verify it. It is the substrate's abstraction over n, achieved without movement.

    Equations
    Instances For
      source
      theorem Hanink2021.denote_anaphoric_eq_iota {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) (g : Assignment E) (s : W) :
      Semantics.Denotes.denote (Reference.Description.anaphoric R d) g s = Reference.iota fun (x : E) => R g s x ∧ idxVar d g x

      A familiar DP, D's ι over the restriction modified by the index as a variable ((15), (35b), (97) and (106)), is the substrate's anaphoric description, which denotes the antecedent if it satisfies the restriction.

      source
      theorem Hanink2021.denote_demonstrative_eq_iota {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) (g : Assignment E) (s : W) :
      Semantics.Denotes.denote (Reference.Description.demonstrative R d) g s = Reference.iota fun (x : E) => R g s x ∧ idxVar d g x

      The demonstrative D heads hádi and wídi of (34b) and (34c) add a deictic presupposition and otherwise contribute ι, so a demonstrative refers as the anaphoric DP does.

      Internally headed relatives, section 4 #

      source
      def Hanink2021.openClause {E : Type} (n : ℕ) (P : E → Prop) (ψ : Assignment E → Prop) :
      Assignment E → Prop

      The embedded clause of an internally headed relative, (69) and (70), is an open proposition whose semantic head is the restricted variable n. The restriction P holds of the variable's value, and the clause ψ says the rest of it.

      Equations
      Instances For
        source
        theorem Hanink2021.idxBind_openClause {E : Type} (n : ℕ) (P : E → Prop) (ψ : Assignment E → Prop) (g : Assignment E) :
        idxBind n (openClause n P ψ) g = Modifier.intersective P (HeimKratzer.lambdaAbsG n ψ g)

        The property (71) that the index yields by binding the restricted variable in situ is the property (59) that an externally headed relative builds by abstracting over the trace and intersecting with the head noun.

        source
        theorem Hanink2021.iota_idxBind {E : Type} (n : ℕ) (P : E → Prop) (ψ : Assignment E → Prop) (g : Assignment E) :
        Reference.iota (idxBind n (openClause n P ψ) g) = Reference.iota (Modifier.intersective P (HeimKratzer.lambdaAbsG n ψ g))

        The silent D over the bound clause, (72), refers to what the definite over the externally headed relative, (60), refers to, the same meaning reached by different steps.

        source
        theorem Hanink2021.idxBind_eq_const {E : Type} {n : ℕ} {φ : Assignment E → Prop} (h : DependsOn φ {n}ᶜ) (g : Assignment E) :
        idxBind n φ g = fun (x : E) => φ g

        Without a free occurrence of the index, when φ depends only on the other indices, the binder meaning is constant and binds nothing. The Prohibition against Vacuous Binding (86) then leaves only the variable meaning, which is why a perception nominalization (106), a property of events with no open variable, is a familiar DP.

        The exponence of idx and D, section 6 #

        source
        inductive Hanink2021.Feat :
        Type

        The features Vocabulary Insertion reads at idx and D and on their complements are the index head, dependent (accusative) case, the D head with its deixis, and the complement's category. The complement is an overt NP, a CP, an RP, or a nominal under ellipsis, which lacks the phonological features that make an NP overt (section 6.3).

        Instances For
          source
          def Hanink2021.instDecidableEqFeat.decEq (x✝ x✝¹ : Feat) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            @[instance_reducible]
            instance Hanink2021.instDecidableEqFeat :
            DecidableEq Feat
            Equations
            source
            def Hanink2021.idxItems :
            Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem Feat String)

            The Vocabulary entries for idx, (119) and (131), are gi elsewhere, ge under dependent case, and null before an overt NP.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Hanink2021.dItems :
              Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem Feat String)

              The Vocabulary entries for D, (130), are null elsewhere, hádi distal and wídi proximal, the speaker's space.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Hanink2021.contextualSpecificity (i : DistributedMorphology.VocabularyItem Feat String) :
                Lex (ℕ × ℕ)

                Under (118), contextual specificity takes precedence over the Elsewhere Principle, the ordering of [AN12]. An item is ranked first by the features it demands of the context and then by those it spells out.

                Equations
                Instances For
                  source
                  def Hanink2021.idxExponent (n : DistributedMorphology.Neighborhood (List Feat)) :
                  Option String

                  idxExponent n is the exponent of idx in the neighborhood n.

                  Equations
                  Instances For
                    source
                    def Hanink2021.dExponent (n : DistributedMorphology.Neighborhood (List Feat)) :
                    Option String

                    dExponent n is the exponent of D in the neighborhood n.

                    Equations
                    Instances For
                      source
                      theorem Hanink2021.idxExponent_distribution :
                      idxExponent { focus := [Feat.idx], rightCtx := [[Feat.elided]] } = some "gi" ∧ idxExponent { focus := [Feat.idx, Feat.dep], rightCtx := [[Feat.elided]] } = some "ge" ∧ idxExponent { focus := [Feat.idx], rightCtx := [[Feat.cp]] } = some "gi" ∧ idxExponent { focus := [Feat.idx, Feat.dep], rightCtx := [[Feat.cp]] } = some "ge" ∧ idxExponent { focus := [Feat.idx], leftCtx := [[Feat.d, Feat.deixis Person.first.participantSetsᶜ]], rightCtx := [[Feat.rp]] } = some "gi" ∧ idxExponent { focus := [Feat.idx], rightCtx := [[Feat.np]] } = some "" ∧ idxExponent { focus := [Feat.idx, Feat.dep], rightCtx := [[Feat.np]] } = some ""

                      The exponent gi ~ ge is distributed as in (108) to (115) and (127) to (129). It is overt in pronouns, whose NP is elided (113), at the edge of clausal nominalizations (114), and in demonstratives, whose complement is RP (129), each alternating for case ((44), (45)). It is null before the overt NP of an anaphoric bare definite (115), and still null under dependent case (22), where the contextual entry outranks the case entry.

                      source
                      theorem Hanink2021.subsetPrinciple_accusative_bare :
                      DistributedMorphology.subsetPrinciple idxItems { focus := [Feat.idx, Feat.dep], rightCtx := [[Feat.np]] } = some "ge"

                      Under the Elsewhere score alone the case entry and the contextual entry tie on the accusative bare definite and vocabulary order decides for ge; the paper's ordering (118) is what makes the null entry win.

                      source
                      theorem Hanink2021.demonstrative_forms :
                      ((dExponent { focus := [Feat.d, Feat.deixis Person.first.participantSetsᶜ], rightCtx := [[Feat.idx]] }).bind fun (a : String) => Option.map (fun (x : String) => a ++ x) (idxExponent { focus := [Feat.idx], leftCtx := [[Feat.d, Feat.deixis Person.first.participantSetsᶜ]], rightCtx := [[Feat.rp]] })) = some "hádigi" ∧ ((dExponent { focus := [Feat.d, Feat.deixis Person.first.participantSets], rightCtx := [[Feat.idx]] }).bind fun (a : String) => Option.map (fun (x : String) => a ++ x) (idxExponent { focus := [Feat.idx], leftCtx := [[Feat.d, Feat.deixis Person.first.participantSets]], rightCtx := [[Feat.rp]] })) = some "wídigi"

                      The demonstratives hádigi and wídigi of (25) and (127) decompose as the D exponent followed by the idx exponent.