Documentation

Linglib.Theories.Semantics.Dynamic.Core.Accessibility

DRS Interpretation and Accessibility #

@cite{muskens-1996}

Semantic interpretation bridge: maps DRSExpr syntax (from Core.DRSExpr) to DRS (Assignment E) semantics, connecting the pure syntactic representation to the dynamic semantic algebra.

Key Results #

source
@[reducible, inline]
abbrev Semantics.Dynamic.Core.Accessibility.RelInterp (E : Type u_1) :
Type u_1

Interpretation of relation symbols.

Equations
Instances For
    source
    def Semantics.Dynamic.Core.Accessibility.interp {E : Type u_1} (rels : RelInterp E) :
    DRSExpr → DynProp.DRS (Assignment E)

    Semantic interpretation: maps DRS syntax to DRS semantics.

    Each syntactic DRS expression denotes a binary relation on assignments (type DRS (Assignment E)), following the abbreviation clauses ABB1–ABB4 (@cite{muskens-1996}, p. 157).

    Equations
    Instances For
      source
      def Semantics.Dynamic.Core.Accessibility.interp.interpConds {E : Type u_1} (rels : RelInterp E) :
      List DRSExpr → DynProp.DRS (Assignment E)
      Equations
      Instances For
        source
        def Semantics.Dynamic.Core.Accessibility.projDref {E : Type u_1} (n : ℕ) :
        DynamicTy2.Dref (Assignment E) E

        Projection dref: the n-th register value.

        In @cite{muskens-1996}'s terminology, projDref n is the variable register uₙ — the function that reads the n-th slot of an assignment.

        Equations
        Instances For
          source
          theorem Semantics.Dynamic.Core.Accessibility.update_projDref_eq {E : Type u_1} (g : Assignment E) (n : ℕ) (e : E) :
          projDref n (g.update n e) = e

          Updating at index n assigns the new value to the n-th projection dref.

          This is the concrete version of AssignmentStructure.extend_at for Assignment E: uₙ(g[n ↦ e]) = e.

          source
          theorem Semantics.Dynamic.Core.Accessibility.update_projDref_ne {E : Type u_1} (g : Assignment E) (n m : ℕ) (e : E) (h : n ≠ m) :
          projDref m (g.update n e) = projDref m g

          Updating at index n preserves other projection drefs.

          Concrete version of AssignmentStructure.extend_other: uₘ(g[n ↦ e]) = uₘ(g) when n ≠ m.

          source
          theorem Semantics.Dynamic.Core.Accessibility.interpConds_append {E : Type u_1} (rels : RelInterp E) (cs1 cs2 : List DRSExpr) :
          interp.interpConds rels (cs1 ++ cs2) = interp.interpConds rels cs1 ⨟ interp.interpConds rels cs2

          interpConds distributes over list concatenation.

          source
          theorem Semantics.Dynamic.Core.Accessibility.foldl_append_introduce {E : Type u_1} (drefs1 drefs2 : List ℕ) :
          List.foldl (fun (D : DynProp.DRS (Assignment E)) (n : ℕ) => D ⨟ fun (i j : Assignment E) => ∃ (e : E), j = i.update n e) (fun (i j : Assignment E) => i = j) (drefs1 ++ drefs2) = List.foldl (fun (D : DynProp.DRS (Assignment E)) (n : ℕ) => D ⨟ fun (i j : Assignment E) => ∃ (e : E), j = i.update n e) (fun (i j : Assignment E) => i = j) drefs1 ⨟ List.foldl (fun (D : DynProp.DRS (Assignment E)) (n : ℕ) => D ⨟ fun (i j : Assignment E) => ∃ (e : E), j = i.update n e) (fun (i j : Assignment E) => i = j) drefs2

          Dref introduction over concatenation = sequencing of introductions.

          When dref n does not occur in expression K, the DRS interp rels K is semantically invariant under Assignment.update at slot n: updating slot n in both input and output preserves the relation (FreshFwd), and any output from an updated input factors through an un-updated intermediate (FreshBack).

          source
          theorem Semantics.Dynamic.Core.Accessibility.mergingLemma {E : Type u_1} (rels : RelInterp E) (drefs1 drefs2 : List ℕ) (conds1 conds2 : List DRSExpr) (hfresh : ∀ (n : ℕ), n ∈ drefs2 → ∀ (c : DRSExpr), c ∈ conds1 → occurs n c = false) :
          interp rels ((DRSExpr.DRSExpr.box drefs1 conds1).seq (DRSExpr.DRSExpr.box drefs2 conds2)) = interp rels (DRSExpr.DRSExpr.box (drefs1 ++ drefs2) (conds1 ++ conds2))

          Merging Lemma (@cite{muskens-1996}, p. 150).

          If drefs x'₁,...,x'ₖ do not occur in any condition γ₁,...,γₘ, then sequencing two boxes equals a single merged box:

          ⟦[x₁...xₙ|γ₁,...,γₘ]; [x'₁...x'ₖ|δ₁,...,δq]⟧ = ⟦[x₁...xₙx'₁...x'ₖ|γ₁,...,γₘ,δ₁,...,δq]⟧

          This is used throughout §III.4 to simplify compositional derivations.

          The proof reduces (via foldl_append_introduce, interpConds_append, and dseq_assoc) to showing that condition tests commute with fresh dref introductions. This commuting step requires a mutual induction on DRSExpr proving that interp rels c is semantically invariant under Assignment.update at slots not mentioned in c.

          Kamp & Reyle's DRS reduction — the operation that collapses compositional .seq (.box …) (.box …) derivations into canonical single-box form. This is Muskens's T₅ rule applied iteratively.

          reduce K walks the .seq spine bottom-up: whenever two adjacent boxes satisfy the freshness precondition of the merging lemma, they are fused into one box. The soundness theorem says interpretation is invariant: interp rels (reduce K) = interp rels K.

          source
          def Semantics.Dynamic.Core.Accessibility.reduce :
          DRSExpr → DRSExpr

          Reduce a DRS expression by iteratively merging sequential boxes.

          Only reduces .seq chains (the discourse-composition spine). Conditions inside boxes are left structurally intact — they don't contain .seq in well-formed DRT derivations.

          Equations
          Instances For
            source
            theorem Semantics.Dynamic.Core.Accessibility.reduce_sound {E : Type u_1} (rels : RelInterp E) (K : DRSExpr) :
            interp rels (reduce K) = interp rels K

            DRS reduction preserves interpretation.

            Contextual properness #

            The syntactic isProper function (from DRSExpr.lean) has a soundness gap: it conflates accessibility across disjunction branches, allowing expressions like [u₁|P(u₁)] ∨ [|Q(u₁)] to pass even though u₁ is free in the second disjunct. The allBound check defined here tracks bound drefs contextually and requires each disjunct to be independently well-bound.

            source
            def Semantics.Dynamic.Core.Accessibility.allBound :
            List ℕ → DRSExpr → Bool

            Context-sensitive properness: every dref used in K must appear in the bound set B.

            Equations
            Instances For
              source
              def Semantics.Dynamic.Core.Accessibility.allBound.allBoundConds :
              List ℕ → List DRSExpr → Bool
              Equations
              Instances For
                source
                theorem Semantics.Dynamic.Core.Accessibility.proposition_1 {E : Type u_1} [Nonempty E] (rels : RelInterp E) (K : DRSExpr) (hproper : allBound [] K = true) :
                WeakestPrecondition.isProper (interp rels K)

                Proposition 1 (@cite{muskens-1996}, p. 174).

                A syntactically proper DRS (no free discourse referents) has state-independent truth conditions: wp(⟦K⟧, ⊤) doesn't depend on the input assignment.

                This bridges syntactic properness (allBound) with semantic properness (WeakestPrecondition.isProper). The proof uses a rebase lemma: if all drefs in K are bound, then satisfaction can be transferred between any two assignments.

                Connection to cylindric algebras #

                The algebraic definitions (cylindrify, invariantOn, cylClosed, diagonal, axioms C1–C7, substitution, derived theorems) live in CylindricAlgebra.lean. This section re-exports them and adds the DRT-specific bridge theorems that depend on interp/closure.

                source
                theorem Semantics.Dynamic.Core.Accessibility.allBound_invariantOn {E : Type u_1} [Nonempty E] (rels : RelInterp E) (K : DRSExpr) (B : List ℕ) (hB : allBound B K = true) :
                Core.CylindricAlgebra.invariantOn (DynProp.closure (interp rels K)) B

                The truth condition of a DRS with allBound B K is invariant on B: it only depends on the registers that K is allowed to read.

                This is the support theorem: syntactic bound-checking (allBound) correctly over-approximates semantic support.

                source
                theorem Semantics.Dynamic.Core.Accessibility.cylClosed_of_not_occurs {E : Type u_1} [Nonempty E] (rels : RelInterp E) (K : DRSExpr) (n : ℕ) (h : occurs n K = false) :
                Core.CylindricAlgebra.cylClosed n (DynProp.closure (interp rels K))

                Per-register support theorem: if dref n does not occur in K, then the truth condition of K is cylindrification-closed at n.

                This connects freshInv (§3b) to the cylindric algebra vocabulary. occurs is the per-register support checker, and allBound is the global version.

                source
                theorem Semantics.Dynamic.Core.Accessibility.interp_is_eq_diagonal {E : Type u_1} (rels : RelInterp E) (u v : ℕ) :
                DynProp.closure (interp rels (DRSExpr.DRSExpr.is u v)) = Core.CylindricAlgebra.diagonal u v

                The DRS identity condition is u v denotes the diagonal element.

                source
                theorem Semantics.Dynamic.Core.Accessibility.closure_introReg_seq {E : Type u_1} (n : ℕ) (D : DynProp.DRS (Assignment E)) :
                DynProp.closure ((fun (g h : Assignment E) => ∃ (e : E), h = g.update n e) ⨟ D) = Core.CylindricAlgebra.cylindrify n (DynProp.closure D)

                Register introduction + D under closure = cylindrification.

                The DRS [n]; D (introduce dref n then continue with D), under closure, equals cₙ(closure(D)): cylindrification at n.

                This is the DRS-level analog of the DPL theorem closure(∃x.φ) = cₓ(closure(φ)).

                source
                theorem Semantics.Dynamic.Core.Accessibility.closure_introReg {E : Type u_1} [Nonempty E] (n : ℕ) :
                (DynProp.closure fun (g h : Assignment E) => ∃ (e : E), h = g.update n e) = fun (x : Assignment E) => True

                Register introduction alone under closure is trivially true (given a nonempty entity type). closure([n]) = ⊤.