Documentation

Linglib.Theories.Semantics.Lexical.Roots.Closure

Entailment Closure on Roots #

@cite{beavers-koontz-garboden-2020}

Root.entailments is the base entailment set: atoms asserted directly by the lexicographer. But @cite{beavers-koontz-garboden-2020}'s typology treats roots as networks of entailments, where some atoms entail others. The closure of the base under such network rules is the root's full entailment set.

This file provides:

  1. EntailmentRules: a function LexEntailment → List LexEntailment giving the atoms each premise atom directly entails.
  2. closeOnce: one closure step (single inference round).
  3. closure: alias for closeOnce — kept as the public API. For the currently-codified rules a single step is a fixpoint (closure_bkgRules_idempotent); if a chaining rule is added later, redefine closure as Nat.iterate closeOnce n and re-prove idempotence at the new bound.
  4. bkgRules: the documented B&K-G rules. Currently a single rule: becomesState s ⇒ hasState s (a change-of-state to s entails the resulting state attribution s).
  5. Root.closedEntailments and Root.closedFeatureSignature: the closure-derived counterparts of entailments/featureSignature.

The infrastructure is designed so that adding a new B&K-G inference (e.g., volitional ⇒ sentient, contact ⇒ motion) is a one-line extension to bkgRules.

source
@[reducible, inline]
abbrev Semantics.Lexical.Roots.EntailmentRules :
Type

A rule set: each atom maps to the atoms it directly entails.

Equations
Instances For
    source
    def Semantics.Lexical.Roots.closeOnce (rules : EntailmentRules) (atoms : List LexEntailment) :
    List LexEntailment

    One closure step: adjoin to atoms everything any rule fires from an atom in atoms. Result is atoms followed by all derived atoms. Duplicates are not removed (they are inert under List.any / List.contains queries used downstream).

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Semantics.Lexical.Roots.closure :
      EntailmentRules → List LexEntailment → List LexEntailment

      Backwards-compatible alias for closeOnce. The currently-codified bkgRules reach a fixpoint after one step (closure_bkgRules_idempotent). If a chaining rule is added, redefine via Nat.iterate closeOnce.

      Equations
      Instances For
        source
        def Semantics.Lexical.Roots.bkgRules :
        EntailmentRules

        The documented B&K-G entailment rules. Currently:

        • becomesState s ⇒ hasState s: a change of state to s entails that s holds at the post-state, so the root attributes s.

        Other candidate rules (volitional ⇒ sentient, contact ⇒ motion) are debated in the literature and intentionally omitted until they can be argued for from primary sources.

        Equations
        Instances For
          source
          theorem Semantics.Lexical.Roots.bkgRules_only_state (a b : LexEntailment) (h : a ∈ bkgRules b) :
          a.isState

          Every atom produced by bkgRules is a state-attribution.

          source
          def Semantics.Lexical.Roots.Root.closedEntailments (r : Root) :
          List LexEntailment

          The B&K-G closure of the root's base entailments.

          Equations
          Instances For
            source
            def Semantics.Lexical.Roots.Root.closedFeatureSignature (r : Root) :
            FeatureSignature

            The feature signature computed over the closure of the root's entailments. For the current bkgRules, this differs from featureSignature only in the state field: any root with a becomesState atom in its base set acquires state = true.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Semantics.Lexical.Roots.closure_includes (rules : EntailmentRules) (atoms : List LexEntailment) (a : LexEntailment) (h : a ∈ atoms) :
              a ∈ closure rules atoms

              Closure preserves all base atoms: the base list is a prefix of the closure.

              source
              theorem Semantics.Lexical.Roots.closure_any_of_any (rules : EntailmentRules) (atoms : List LexEntailment) (p : LexEntailment → Bool) (h : atoms.any p = true) :
              (closure rules atoms).any p = true

              Adding the closure step never makes any p go from true to false — closure is monotone for List.any.

              source
              @[simp]
              theorem Semantics.Lexical.Roots.closedFeatureSignature_manner (r : Root) :
              r.closedFeatureSignature.manner = r.featureSignature.manner

              Closed and base signatures agree on manner.

              source
              @[simp]
              theorem Semantics.Lexical.Roots.closedFeatureSignature_result (r : Root) :
              r.closedFeatureSignature.result = r.featureSignature.result

              Closed and base signatures agree on result.

              source
              @[simp]
              theorem Semantics.Lexical.Roots.closedFeatureSignature_cause (r : Root) :
              r.closedFeatureSignature.cause = r.featureSignature.cause

              Closed and base signatures agree on cause.

              source
              theorem Semantics.Lexical.Roots.closedFeatureSignature_state_of_base (r : Root) (h : r.featureSignature.state = true) :
              r.closedFeatureSignature.state = true

              Closure can only add state: if the base says state = true, the closure agrees; if base says false, closure may say true.

              source
              theorem Semantics.Lexical.Roots.closedFeatureSignature_state_of_becomes (r : Root) (s : String) (h : LexEntailment.becomesState s ∈ r.entailments) :
              r.closedFeatureSignature.state = true

              The principal closure consequence: every becomesState s in the base entailment set forces state = true in the closed signature.

              source
              theorem Semantics.Lexical.Roots.closedFeatureSignature_state_eq (r : Root) :
              r.closedFeatureSignature.state = (r.featureSignature.state || r.featureSignature.result)

              Closure adds state atoms exactly when the base set has a becomesState atom. So the closed state field is the disjunction of base state and base result.

              source
              theorem Semantics.Lexical.Roots.bkgRules_eq_nil_of_isState (a : LexEntailment) (h : a.isState) :
              bkgRules a = []

              bkgRules produces nothing from a hasState atom (and similarly nothing from any non-becomesState atom).

              source
              theorem Semantics.Lexical.Roots.flatMap_bkgRules_eq_nil_of_all_isState (atoms : List LexEntailment) (h : ∀ (a : LexEntailment), a ∈ atoms → a.isState) :
              List.flatMap bkgRules atoms = []

              If every atom in atoms is a hasState, flatMap bkgRules is empty.

              source
              theorem Semantics.Lexical.Roots.flatMap_bkgRules_flatMap_bkgRules_eq_nil (atoms : List LexEntailment) :
              List.flatMap bkgRules (List.flatMap bkgRules atoms) = []

              After one flatMap bkgRules, every atom is a state-attribution, so a further flatMap bkgRules produces nothing.

              source
              theorem Semantics.Lexical.Roots.closure_bkgRules_any_idempotent (atoms : List LexEntailment) (p : LexEntailment → Bool) :
              (closure bkgRules (closure bkgRules atoms)).any p = (closure bkgRules atoms).any p

              closeOnce bkgRules is idempotent up to List.any queries — a second application adds duplicate copies of state atoms, but no new distinct atoms. This is the precise sense in which closure := closeOnce suffices for the downstream Root.closedFeatureSignature API.