Documentation

Linglib.Semantics.Presupposition.Accommodation

Accommodation #

[Lew79b] [Bea01] [vdS92]

Accommodation is the process by which a context is adjusted to satisfy a presupposition that is not already entailed. [Lew79b] introduced the concept: "If at time t something is said that requires presupposition P to be acceptable, and if P is not presupposed just before t, then — ceteris paribus — presupposition P comes into existence at t."

Three Levels ([Bea01] Ch. 5) #

Three Strategies #

  1. Heim/Lewis preference: prefer global > intermediate > local. Global preference + consistency constraint ≈ Gazdar's cancellation ([Bea01] Ch. 5.8.1).
  2. Van der Sandt structural: DRT-based move-α; presupposition DRS is moved to the highest accessible position ([vdS92]).
  3. Fauconnier flotation: presupposition floats upward through mental spaces, leaving a shadow at each level ([Bea01] Ch. 5.8.3).

Constraints ([Bea01] Ch. 5.3) #

Accommodation levels #

source
inductive Semantics.Presupposition.Accommodation.AccommodationLevel :
Type

The level at which accommodation occurs. [Bea01] Ch. 5, [Lew79b], [Hei83].

  • global : AccommodationLevel

    Add presupposition to the global common ground.

  • local : AccommodationLevel

    Satisfy presupposition within the local embedded context.

  • intermediate (depth : ℕ) : AccommodationLevel

    Add presupposition at an intermediate level (e.g., restrictor of a quantifier, antecedent of a conditional). [Bea01] Ch. 5.5 argues this is heavily restricted.

Instances For
    source
    @[instance_reducible]
    instance Semantics.Presupposition.Accommodation.instDecidableEqAccommodationLevel :
    DecidableEq AccommodationLevel
    Equations
    source
    def Semantics.Presupposition.Accommodation.instDecidableEqAccommodationLevel.decEq (x✝ x✝¹ : AccommodationLevel) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Semantics.Presupposition.Accommodation.instReprAccommodationLevel.repr :
      AccommodationLevel → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance Semantics.Presupposition.Accommodation.instReprAccommodationLevel :
        Repr AccommodationLevel
        Equations

        Global accommodation #

        source
        @[reducible, inline]
        abbrev Semantics.Presupposition.Accommodation.globalAccommodate {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) :
        CommonGround.ContextSet W

        Global accommodation: update the context to include the presupposition. [Lew79b]: "presupposition P comes into existence."

        Delegates to Semantics.Presupposition.Context.accommodate.

        Equations
        Instances For

          Accommodation constraints #

          source
          def Semantics.Presupposition.Accommodation.isTrapped (bindingDepth : ℕ) :
          AccommodationLevel → Prop

          Trapping: a presupposition with a bound variable cannot be accommodated above its binder. [Bea01] Ch. 5.3.

          Modeled as a predicate on the accommodation level and a binding depth: accommodation at level l is trapped if the presupposition is bound at depth d and l would place it above d.

          Equations
          Instances For
            source
            @[instance_reducible]
            instance Semantics.Presupposition.Accommodation.instDecidablePredAccommodationLevelIsTrapped (bindingDepth : ℕ) :
            DecidablePred (isTrapped bindingDepth)
            Equations
            • One or more equations did not get rendered due to their size.
            source
            structure Semantics.Presupposition.Accommodation.AccommodationOK {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) :
            Prop

            All constraints bundled together. Uses canonical operations from Semantics.Presupposition.Context.

            Instances For

              The Heim/Lewis strategy #

              source
              noncomputable def Semantics.Presupposition.Accommodation.heimSelect {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) :
              AccommodationLevel

              Select accommodation level based on the Heim/Lewis strategy.

              Try global first; if inconsistent, fall back to local.

              [Hei83]: "by stipulating a ceteris paribus preference for global over local accommodation, we recapture the effect of Gazdar's assumption that presupposition cancellation occurs only under the threat of inconsistency."

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

                Key theorems #

                source
                theorem Semantics.Presupposition.Accommodation.heim_cancellation_equivalence {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) (h_inconsistent : ¬Set.Nonempty (globalAccommodate c presup)) :
                heimSelect c presup = AccommodationLevel.local

                Heim's observation: global accommodation preference is equivalent to Gazdar's cancellation under threat of inconsistency.

                When global accommodation would be inconsistent, we fall back to local accommodation — which has the same effect as Gazdar's presupposition cancellation.

                [Bea01] Ch. 5.8.1: "with one short remark buried in a terse paper, Heim offers a simple synthesis between the two antitheses of 1970s presupposition theory."

                source
                theorem Semantics.Presupposition.Accommodation.heim_projection_when_consistent {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) (h_consistent : Set.Nonempty (globalAccommodate c presup)) :
                heimSelect c presup = AccommodationLevel.global

                When global accommodation IS consistent, Heim's strategy projects the presupposition globally — matching Karttunen's projection.

                source
                theorem Semantics.Presupposition.Accommodation.heim_never_intermediate {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) (d : ℕ) :
                heimSelect c presup ≠ AccommodationLevel.intermediate d

                Intermediate accommodation is problematic.

                [Bea01] Ch. 5.5 argues that intermediate accommodation (accommodation into the restrictor of a quantifier or antecedent of a conditional) is heavily restricted and only occurs with generic/habitual statements. Without intermediate accommodation, both Heim's CCP and van der Sandt's DRT make better predictions.

                This is formalized as: the Heim preference strategy never selects intermediate accommodation.