Documentation

Studies.PaapeVasishth2026

Paape and Vasishth (2026): Context Ameliorates but Does Not Eliminate Garden-Pathing #

This file formalizes the multinomial processing tree of Paape and Vasishth. A trial follows a route through a tree of Bernoulli decisions, and the route fixes the reading-time costs, whether the reader regresses, and the acceptability judgment. The paper fits the tree to a replication of Altmann, Garnham, and Dennis's study, which crosses referential context with complement- and relative-clause disambiguation. Its case for the tree is that condition means cannot tell an effect of context on attachment from an effect on reanalysis cost.

Main definitions #

Main results #

Implementation notes #

Which cells match is derived from when each analysis's definite refers: with two women the bare definite fails its uniqueness presupposition, as Altmann and Steedman argue. Costs are added above non-decision time. The mixture's component distributions, the predictor structure across conditions, and the baseline regression probability of the text are not modeled, and the inattentive reader's bias is a free parameter rather than the estimate from Paape and Vasishth's earlier model. The fitted estimates and the model comparisons are not formalized.

References #

The design #

source
inductive PaapeVasishth2026.Disambiguation :
Type

The string the woman that he'd risked his life for is disambiguated in three ways, after a verb that takes a clausal complement or, in the control condition, after one that does not.

  • complementClause : Disambiguation

    He told the woman that he'd risked his life for many people in similar fires.

  • relativeClause : Disambiguation

    He told the woman that he'd risked his life for to install a smoke detector.

  • unambiguousRelativeClause : Disambiguation

    He asked the woman that he'd risked his life for to install a smoke detector ...

Instances For
    source
    @[instance_reducible]
    instance PaapeVasishth2026.instDecidableEqDisambiguation :
    DecidableEq Disambiguation
    Equations
    source
    def PaapeVasishth2026.Disambiguation.IsRelative :
    Disambiguation → Prop

    A disambiguation is relative when it resolves the string to a relative clause.

    Equations
    Instances For
      source
      inductive PaapeVasishth2026.Referent :
      Type

      Besides the fireman, the discourses of Table 1 introduce the woman he rescued and either a man or a second woman.

      • rescued : Referent

        The woman the fireman rescued.

      • man : Referent

        The man of the one-woman discourse.

      • otherWoman : Referent

        The second woman of the two-woman discourse.

      Instances For
        source
        @[instance_reducible]
        instance PaapeVasishth2026.instDecidableEqReferent :
        DecidableEq Referent
        Equations
        source
        @[instance_reducible]
        instance PaapeVasishth2026.instFintypeReferent :
        Fintype Referent
        Equations
        • One or more equations did not get rendered due to their size.
        source
        inductive PaapeVasishth2026.ReferentialContext :
        Type

        A discourse introduces one woman, with a man, or two women.

        Instances For
          source
          @[instance_reducible]
          instance PaapeVasishth2026.instDecidableEqReferentialContext :
          DecidableEq ReferentialContext
          Equations
          source
          def PaapeVasishth2026.ReferentialContext.Woman :
          ReferentialContext → Referent → Prop

          c.Woman r holds when r is one of the women the context c introduces.

          Equations
          Instances For
            source
            def PaapeVasishth2026.ReferentialContext.restrictor (c : ReferentialContext) :
            Disambiguation → Referent → Prop

            The restrictor of the definite is woman under the complement-clause analysis and woman that he'd risked his life for under a relative-clause analysis.

            Equations
            Instances For
              source
              @[simp]
              theorem PaapeVasishth2026.ReferentialContext.restrictor_complementClause (c : ReferentialContext) :
              c.restrictor Disambiguation.complementClause = c.Woman
              source
              def PaapeVasishth2026.ReferentialContext.Supports (c : ReferentialContext) (d : Disambiguation) :
              Prop

              A context supports an analysis when the analysis's definite refers and, for a relative clause, the bare definite does not.

              Equations
              Instances For
                source
                theorem PaapeVasishth2026.ReferentialContext.iota_woman_isSome_iff (c : ReferentialContext) :
                (Reference.iota c.Woman).isSome = true ↔ c = uniqueReferent

                The woman refers exactly when the context has one woman.

                source
                theorem PaapeVasishth2026.ReferentialContext.iota_woman_eq_none_iff (c : ReferentialContext) :
                Reference.iota c.Woman = none ↔ c = nonUniqueReferents

                The woman fails to refer exactly when the context has two women.

                source
                theorem PaapeVasishth2026.ReferentialContext.iota_restrictor_isSome (c : ReferentialContext) {d : Disambiguation} (hd : d.IsRelative) :
                (Reference.iota (c.restrictor d)).isSome = true

                The woman that he'd risked his life for refers in either context.

                source
                structure PaapeVasishth2026.Condition :
                Type

                A condition is a cell of the three-by-two design.

                Instances For
                  source
                  def PaapeVasishth2026.instDecidableEqCondition.decEq (x✝ x✝¹ : Condition) :
                  Decidable (x✝ = x✝¹)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[instance_reducible]
                    instance PaapeVasishth2026.instDecidableEqCondition :
                    DecidableEq Condition
                    Equations
                    source
                    def PaapeVasishth2026.Condition.IsMatch (c : Condition) :
                    Prop

                    A condition matches when its context supports its disambiguation.

                    Equations
                    Instances For
                      source
                      theorem PaapeVasishth2026.Condition.isMatch_iff (c : Condition) :
                      c.IsMatch ↔ (c.context = ReferentialContext.nonUniqueReferents ↔ c.disambiguation.IsRelative)

                      A condition matches exactly when its context has two women and its disambiguation is a relative clause, or one woman and a complement clause.

                      The processing tree #

                      source
                      inductive PaapeVasishth2026.Reanalysis :
                      Type

                      A garden-pathed reader reanalyzes overtly, by a regression, or covertly, either in situ at the disambiguating region or postponed to the spillover region.

                      • overt : Reanalysis

                        Overt reanalysis rereads earlier material.

                      • covertImmediate : Reanalysis

                        Covert reanalysis happens in situ at the disambiguating region.

                      • covertPostponed : Reanalysis

                        Covert reanalysis is postponed to the spillover region.

                      Instances For
                        source
                        @[instance_reducible]
                        instance PaapeVasishth2026.instDecidableEqReanalysis :
                        DecidableEq Reanalysis
                        Equations
                        source
                        @[instance_reducible]
                        instance PaapeVasishth2026.instFintypeReanalysis :
                        Fintype Reanalysis
                        Equations
                        • One or more equations did not get rendered due to their size.
                        source
                        inductive PaapeVasishth2026.Route :
                        Type

                        A route runs from the root of the tree of Fig. 1 to a leaf.

                        • guess (accept : Bool) : Route

                          The reader is inattentive and guesses the judgment.

                        • correct : Route

                          The reader adopts the correct analysis on the first pass.

                        • triage : Route

                          The reader is garden-pathed and rejects the sentence without reanalysis.

                        • reanalysis (kind : Reanalysis) (success : Bool) : Route

                          The reader is garden-pathed and reanalyzes, succeeding or failing.

                        Instances For
                          source
                          def PaapeVasishth2026.instDecidableEqRoute.decEq (x✝ x✝¹ : Route) :
                          Decidable (x✝ = x✝¹)
                          Equations
                          Instances For
                            source
                            @[instance_reducible]
                            instance PaapeVasishth2026.instDecidableEqRoute :
                            DecidableEq Route
                            Equations
                            source
                            @[instance_reducible]
                            instance PaapeVasishth2026.instFintypeRoute :
                            Fintype Route
                            Equations
                            source
                            @[instance_reducible]
                            instance PaapeVasishth2026.instMeasurableSpaceRoute :
                            MeasurableSpace Route
                            Equations
                            source
                            instance PaapeVasishth2026.instDiscreteMeasurableSpaceRoute :
                            DiscreteMeasurableSpace Route
                            source
                            def PaapeVasishth2026.Route.GardenPathed :
                            Route → Prop

                            o.GardenPathed holds when the reader on route o is garden-pathed.

                            Equations
                            Instances For
                              source
                              def PaapeVasishth2026.Route.Regresses :
                              Route → Prop

                              o.Regresses holds when route o shows a first-pass regression, which in the tree only overt reanalysis does.

                              Equations
                              Instances For
                                source
                                def PaapeVasishth2026.Route.Accepts :
                                Route → Prop

                                o.Accepts holds when route o ends in acceptance of the sentence.

                                Equations
                                Instances For
                                  source
                                  structure PaapeVasishth2026.Params :
                                  Type

                                  The parameters of the tree are the branching probabilities of Fig. 1.

                                  • attentive : ↑unitInterval

                                    The probability of attentive reading.

                                  • bias : ↑unitInterval

                                    The inattentive reader's probability of accepting.

                                  • gardenPath : ↑unitInterval

                                    The probability of garden-pathing.

                                  • triage : ↑unitInterval

                                    The probability of triage rather than reanalysis.

                                  • covert : ↑unitInterval

                                    The probability of covert rather than overt reanalysis.

                                  • postpone : ↑unitInterval

                                    The probability of postponing covert reanalysis.

                                  • overtSuccess : ↑unitInterval

                                    The probability that overt reanalysis succeeds.

                                  • covertSuccess : ↑unitInterval

                                    The probability that covert reanalysis succeeds.

                                  Instances For
                                    source
                                    noncomputable def PaapeVasishth2026.node (p : ↑unitInterval) (yes no : MeasureTheory.Measure Route) :
                                    MeasureTheory.Measure Route

                                    A decision node draws a Bernoulli variable with success probability p and continues the route as yes on success and as no otherwise.

                                    Equations
                                    • PaapeVasishth2026.node p yes no = (ProbabilityTheory.bernoulliMeasure true false p).bind fun (b : Bool) => bif b then yes else no
                                    Instances For
                                      source
                                      theorem PaapeVasishth2026.node_eq (p : ↑unitInterval) (yes no : MeasureTheory.Measure Route) :
                                      node p yes no = unitInterval.toNNReal p • yes + unitInterval.toNNReal (unitInterval.symm p) • no
                                      source
                                      @[simp]
                                      theorem PaapeVasishth2026.node_zero (yes no : MeasureTheory.Measure Route) :
                                      node 0 yes no = no
                                      source
                                      @[simp]
                                      theorem PaapeVasishth2026.node_one (yes no : MeasureTheory.Measure Route) :
                                      node 1 yes no = yes
                                      source
                                      @[simp]
                                      theorem PaapeVasishth2026.node_dirac (p : ↑unitInterval) (x y : Route) :
                                      node p (MeasureTheory.Measure.dirac x) (MeasureTheory.Measure.dirac y) = ProbabilityTheory.bernoulliMeasure x y p
                                      source
                                      instance PaapeVasishth2026.instIsProbabilityMeasureRouteNode (p : ↑unitInterval) (yes no : MeasureTheory.Measure Route) [MeasureTheory.IsProbabilityMeasure yes] [MeasureTheory.IsProbabilityMeasure no] :
                                      MeasureTheory.IsProbabilityMeasure (node p yes no)
                                      source
                                      theorem PaapeVasishth2026.node_real_apply (p : ↑unitInterval) (yes no : MeasureTheory.Measure Route) [MeasureTheory.IsFiniteMeasure yes] [MeasureTheory.IsFiniteMeasure no] (s : Set Route) :
                                      (node p yes no).real s = ↑p * yes.real s + (1 - ↑p) * no.real s
                                      source
                                      theorem PaapeVasishth2026.integral_node (p : ↑unitInterval) (yes no : MeasureTheory.Measure Route) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure yes] [MeasureTheory.IsFiniteMeasure no] (f : Route → E) :
                                      ∫ (o : Route), f o ∂node p yes no = ↑p • ∫ (o : Route), f o ∂yes + (1 - ↑p) • ∫ (o : Route), f o ∂no
                                      source
                                      @[reducible, inline]
                                      noncomputable abbrev PaapeVasishth2026.reanalyze (r : Reanalysis) (s : ↑unitInterval) :
                                      MeasureTheory.Measure Route

                                      Reanalysis of kind r succeeds with probability s.

                                      Equations
                                      Instances For
                                        source
                                        noncomputable def PaapeVasishth2026.tree (p : Params) :
                                        MeasureTheory.Measure Route

                                        The tree of Fig. 1 is the distribution of routes its decision nodes generate.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          instance PaapeVasishth2026.instIsProbabilityMeasureRouteTree (p : Params) :
                                          MeasureTheory.IsProbabilityMeasure (tree p)
                                          source
                                          theorem PaapeVasishth2026.tree_real_gardenPathed (p : Params) :
                                          (tree p).real {o : Route | o.GardenPathed} = ↑p.attentive * ↑p.gardenPath

                                          Garden-pathing has the probability of attentive reading times that of garden-pathing.

                                          source
                                          theorem PaapeVasishth2026.tree_real_regresses (p : Params) :
                                          (tree p).real {o : Route | o.Regresses} = ↑p.attentive * ↑p.gardenPath * (1 - ↑p.triage) * (1 - ↑p.covert)

                                          A regression has the probability of overt reanalysis.

                                          source
                                          theorem PaapeVasishth2026.tree_real_accepts (p : Params) :
                                          (tree p).real {o : Route | o.Accepts} = (1 - ↑p.attentive) * ↑p.bias + ↑p.attentive * (1 - ↑p.gardenPath + ↑p.gardenPath * (1 - ↑p.triage) * ((1 - ↑p.covert) * ↑p.overtSuccess + ↑p.covert * ↑p.covertSuccess))

                                          Acceptance collects the accepting guess, the correct first pass, and the successful reanalyses, and its probability does not depend on postponement.

                                          Reading times as a mixture #

                                          source
                                          structure PaapeVasishth2026.Costs :
                                          Type

                                          The costs of Fig. 1 are reading time added above non-decision time.

                                          • attention : NNReal

                                            The cost of attending.

                                          • gardenPath : NNReal

                                            The cost of being garden-pathed.

                                          • regression : NNReal

                                            The cost of launching a regression.

                                          • covert : NNReal

                                            The cost of covert reanalysis.

                                          Instances For
                                            source
                                            def PaapeVasishth2026.Costs.disambiguating (k : Costs) :
                                            Route → ℝ

                                            k.disambiguating o is the cost route o pays at the disambiguating region.

                                            Equations
                                            Instances For
                                              source
                                              def PaapeVasishth2026.Costs.spillover (k : Costs) :
                                              Route → ℝ

                                              k.spillover o is the cost route o pays at the spillover region, which only postponed covert reanalysis incurs.

                                              Equations
                                              Instances For
                                                source
                                                theorem PaapeVasishth2026.integral_disambiguating_tree (p : Params) (k : Costs) :
                                                ∫ (o : Route), k.disambiguating o ∂tree p = ↑p.attentive * (↑k.attention + ↑p.gardenPath * (↑k.gardenPath + (1 - ↑p.triage) * ((1 - ↑p.covert) * ↑k.regression + ↑p.covert * (1 - ↑p.postpone) * ↑k.covert)))

                                                The mean cost at the disambiguating region adds the attention cost of attentive reading to the garden-path probability times the expected cost of a garden-pathed trial.

                                                source
                                                theorem PaapeVasishth2026.integral_spillover_tree (p : Params) (k : Costs) :
                                                ∫ (o : Route), k.spillover o ∂tree p = ↑p.attentive * ↑p.gardenPath * (1 - ↑p.triage) * ↑p.covert * ↑p.postpone * ↑k.covert

                                                The mean cost at the spillover region is the covert reanalysis cost on postponed trials.

                                                source
                                                theorem PaapeVasishth2026.monotone_integral_gardenPath (p : Params) (k : Costs) :
                                                Monotone fun (g : ↑unitInterval) => ∫ (o : Route), k.disambiguating o ∂tree { attentive := p.attentive, bias := p.bias, gardenPath := g, triage := p.triage, covert := p.covert, postpone := p.postpone, overtSuccess := p.overtSuccess, covertSuccess := p.covertSuccess }

                                                A lower garden-path probability never raises the mean cost at the disambiguating region.

                                                source
                                                theorem PaapeVasishth2026.monotone_integral_covert (p : Params) (k : Costs) :
                                                Monotone fun (c : NNReal) => ∫ (o : Route), { attention := k.attention, gardenPath := k.gardenPath, regression := k.regression, covert := c }.disambiguating o ∂tree p

                                                A lower covert reanalysis cost never raises the mean cost at the disambiguating region.

                                                source
                                                theorem PaapeVasishth2026.means_not_identifiable :
                                                ∃ (p : Params) (k : Costs) (g : ↑unitInterval) (c : NNReal), g < p.gardenPath ∧ c < k.covert ∧ ∫ (o : Route), k.disambiguating o ∂tree { attentive := p.attentive, bias := p.bias, gardenPath := g, triage := p.triage, covert := p.covert, postpone := p.postpone, overtSuccess := p.overtSuccess, covertSuccess := p.covertSuccess } = ∫ (o : Route), { attention := k.attention, gardenPath := k.gardenPath, regression := k.regression, covert := c }.disambiguating o ∂tree p ∧ ∫ (o : Route), k.spillover o ∂tree { attentive := p.attentive, bias := p.bias, gardenPath := g, triage := p.triage, covert := p.covert, postpone := p.postpone, overtSuccess := p.overtSuccess, covertSuccess := p.covertSuccess } = ∫ (o : Route), { attention := k.attention, gardenPath := k.gardenPath, regression := k.regression, covert := c }.spillover o ∂tree p ∧ (tree { attentive := p.attentive, bias := p.bias, gardenPath := g, triage := p.triage, covert := p.covert, postpone := p.postpone, overtSuccess := p.overtSuccess, covertSuccess := p.covertSuccess }).real {o : Route | o.Regresses} = (tree p).real {o : Route | o.Regresses} ∧ (tree { attentive := p.attentive, bias := p.bias, gardenPath := g, triage := p.triage, covert := p.covert, postpone := p.postpone, overtSuccess := p.overtSuccess, covertSuccess := p.covertSuccess }).real {o : Route | o.Accepts} = (tree p).real {o : Route | o.Accepts} ∧ MeasureTheory.Measure.map k.disambiguating (tree { attentive := p.attentive, bias := p.bias, gardenPath := g, triage := p.triage, covert := p.covert, postpone := p.postpone, overtSuccess := p.overtSuccess, covertSuccess := p.covertSuccess }) ≠ MeasureTheory.Measure.map { attention := k.attention, gardenPath := k.gardenPath, regression := k.regression, covert := c }.disambiguating (tree p)

                                                Condition means cannot locate an effect of context. From garden-path probability 1 / 2 and covert reanalysis cost 800, illustrative values, an effect on attachment that halves the probability and an effect on reanalysis that halves the cost leave the same mean cost at both regions and the same rates of regression and acceptance, but different mixtures over route costs, 800 on a quarter of the trials against 400 on half of them.