Documentation

Linglib.Semantics.NaturalLogic

Natural Logic Relations and Entailment Signatures #

[Ica12] [MCM09]

Framework-agnostic infrastructure for the natural logic relation algebra and entailment signatures, following [Ica12] "Inclusion and Exclusion in Natural Language."

Contents #

  1. NLRelation — 7 natural logic relations (≡, ⊑, ⊒, ^, |, ⌣, #)
  2. EntailmentSig — 9 entailment signatures unifying monotonicity/additivity

Key operations #

Algebraic structure #

source
inductive NaturalLogic.NLRelation :
Type

The seven basic set-theoretic relations between denotations ([MCM09], [Ica12] §1).

SymbolNameSet relationExample
≡equivalenceA = Bcouch / sofa
⊑forwardA ⊂ Bdog / animal
⊒reverseA ⊃ Banimal / dog
^negationA ∩ B = ∅, A ∪ B = Uhappy / unhappy
|alternationA ∩ B = ∅cat / dog
⌣coverA ∪ B = Uanimal / nondog
#independentall other caseshungry / tall
Instances For
    source
    @[implicit_reducible]
    instance NaturalLogic.instDecidableEqNLRelation :
    DecidableEq NLRelation
    Equations
    source
    def NaturalLogic.instReprNLRelation.repr :
    NLRelation → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance NaturalLogic.instReprNLRelation :
      Repr NLRelation
      Equations
      source
      def NaturalLogic.NLRelation.Refines :
      NLRelation → NLRelation → Prop

      Informativity ordering on NL relations.

      R ≤ R' means R is at least as informative as R'. The lattice has ≡ at

      at the top (least informative); there is no bottom — the two diamonds #

      (≡ over ⊑/⊒, ^ over |/⌣) meet only at #.

      Refines R R' is the implication ordering ([Ica12] §1): xRy entails xR'y (certified semantically by NLRelation.Holds.of_refines in Semantics/Entailment/Soundness.lean). ≡ refines the inclusion relations but not the exclusion relations (x = y does not make x,y disjoint or exhaustive); ^ refines both | and ⌣.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance NaturalLogic.NLRelation.instDecidableRelRefines :
        DecidableRel Refines
        Equations
        source
        @[implicit_reducible]
        instance NaturalLogic.NLRelation.instLE :
        LE NLRelation
        Equations
        source
        @[implicit_reducible]
        instance NaturalLogic.NLRelation.decidableLE (a b : NLRelation) :
        Decidable (a ≤ b)
        Equations
        source
        @[implicit_reducible]
        instance NaturalLogic.NLRelation.instPreorder :
        Preorder NLRelation
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[implicit_reducible]
        instance NaturalLogic.NLRelation.instPartialOrder :
        PartialOrder NLRelation
        Equations
        source
        @[implicit_reducible]
        instance NaturalLogic.NLRelation.instTop :
        Top NLRelation
        Equations
        source
        @[implicit_reducible]
        instance NaturalLogic.NLRelation.instOrderTop :
        OrderTop NLRelation
        Equations
        source
        def NaturalLogic.NLRelation.join :
        NLRelation → NLRelation → NLRelation

        Join operation ⋈ ([Ica12], Lemma 1.5).

        Given xRy and yR'z, determines the strongest relation x(R⋈R')z. This is the "join" in the relation algebra sense (not lattice join).

        Equations
        Instances For
          source
          theorem NaturalLogic.NLRelation.join_identity_left (r : NLRelation) :
          equiv.join r = r

          ≡ is the identity for join.

          source
          theorem NaturalLogic.NLRelation.join_identity_right (r : NLRelation) :
          r.join equiv = r
          source
          inductive NaturalLogic.EntailmentSig :
          Type

          Entailment signature.

          An entailment signature classifies a function by its algebraic properties with respect to ∨ and ∧. This unifies the separate monotonicity and additivity hierarchies into one 9-element lattice.

          SymbolNameProperties
          •allAny function (no property)
          +monoMonotone (= UE)
          −antiAntitone (= DE)
          ⊕additivef(A∨B)=f(A)∨f(B), f(⊤)=⊤
          ◇antiAddf(A∨B)=f(A)∧f(B)
          ⊞multf(A∧B)=f(A)∧f(B), f(⊥)=⊥
          ⊟antiMultf(A∧B)=f(A)∨f(B), f(⊥)=⊤
          ⊕⊞addMultAdditive + Multiplicative
          ◇⊟antiAddMultAnti-additive + Anti-mult
          Instances For
            source
            @[implicit_reducible]
            instance NaturalLogic.instDecidableEqEntailmentSig :
            DecidableEq EntailmentSig
            Equations
            source
            @[implicit_reducible]
            instance NaturalLogic.instReprEntailmentSig :
            Repr EntailmentSig
            Equations
            source
            def NaturalLogic.instReprEntailmentSig.repr :
            EntailmentSig → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def NaturalLogic.EntailmentSig.Refines :
              EntailmentSig → EntailmentSig → Prop

              Refinement ordering on entailment signatures: σ.Refines τ iff every σ-function is a τ-function ([Ica12]'s ≼, §2.2). addMult/antiAddMult are the most specific elements of their halves; all (•, any function) is the top — every class is contained in it. Certified semantically by EntailmentSig.SoundFor.of_refines in Semantics/Entailment/Soundness.lean.

              Equations
              Instances For
                source
                @[implicit_reducible]
                instance NaturalLogic.EntailmentSig.instDecidableRelRefines :
                DecidableRel Refines
                Equations
                source
                @[implicit_reducible]
                instance NaturalLogic.EntailmentSig.instLE :
                LE EntailmentSig
                Equations
                source
                @[implicit_reducible]
                instance NaturalLogic.EntailmentSig.decidableLE (a b : EntailmentSig) :
                Decidable (a ≤ b)
                Equations
                source
                @[implicit_reducible]
                instance NaturalLogic.EntailmentSig.instPreorder :
                Preorder EntailmentSig
                Equations
                • One or more equations did not get rendered due to their size.
                source
                @[implicit_reducible]
                instance NaturalLogic.EntailmentSig.instPartialOrder :
                PartialOrder EntailmentSig
                Equations
                source
                @[implicit_reducible]
                instance NaturalLogic.EntailmentSig.instTop :
                Top EntailmentSig
                Equations
                source
                @[implicit_reducible]
                instance NaturalLogic.EntailmentSig.instOrderTop :
                OrderTop EntailmentSig
                Equations
                source
                def NaturalLogic.EntailmentSig.project :
                NLRelation → EntailmentSig → NLRelation

                Projection of a NL relation through a function of given signature ([Ica12], Lemma 2.4).

                If xRy and f has signature φ, then f(x) [R]^φ f(y). Returns the ≪-maximal relation guaranteed to hold between f(x) and f(y).

                The table follows from the algebraic definitions:

                • Additive: f(x∨y) = f(x)∨f(y), f(1)=1 → preserves ∨ → [∧]^⊕ = ∼ (cover from x∨y=1)
                • Multiplicative: f(x∧y) = f(x)∧f(y), f(0)=0 → preserves ∧ → [|]^⊞ = | (disjoint from x∧y=0)
                • Anti-additive: f(x∨y) = f(x)∧f(y), f(1)=0 → [∼]^◇ = | (from x∨y=1 ⟹ f(x)∧f(y)=0)
                • Anti-multiplicative: f(x∧y) = f(x)∨f(y), f(0)=1 → [|]^⊟ = ∼ (from x∧y=0 ⟹ f(x)∨f(y)=1)
                • Mono/anti alone: only preserves ⊑/⊒; ^, |, ∼ all weaken to #
                Equations
                Instances For
                  source
                  theorem NaturalLogic.EntailmentSig.project_equiv (φ : EntailmentSig) (h : φ ≠ all) :
                  project NLRelation.equiv φ = NLRelation.equiv

                  Every signature except • preserves equiv (• is the class of arbitrary functions, which need not respect equivalence).

                  source
                  theorem NaturalLogic.EntailmentSig.project_independent (φ : EntailmentSig) :
                  project NLRelation.independent φ = NLRelation.independent

                  Projection preserves independent for all signatures.

                  source
                  def NaturalLogic.EntailmentSig.compose (ψ φ : EntailmentSig) :
                  EntailmentSig

                  Composition of entailment signatures ([Ica12], Lemma 2.7).

                  Derived from project: compose(ψ, φ) is the unique signature whose projection table matches projecting through φ then ψ. This makes projection_composition hold by finite verification rather than requiring two independently maintained tables to agree.

                  The signature is identified by probing with forward and negation, which suffice to distinguish all 9 signatures (• included: its probe pair is (#, #), which makes it absorbing, [Ica12] p. 716).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem NaturalLogic.EntailmentSig.compose_identity_left (s : EntailmentSig) :
                    addMult.compose s = s

                    addMult (⊕⊞, the morphism class) is the identity for composition ([Ica12] Lemma 2.7).

                    source
                    theorem NaturalLogic.EntailmentSig.compose_identity_right (s : EntailmentSig) :
                    s.compose addMult = s
                    source
                    theorem NaturalLogic.EntailmentSig.compose_all_left (s : EntailmentSig) :
                    all.compose s = all

                    • is absorbing: composing with the no-property class yields the no-property class ([Ica12] p. 716: φ ∘ • = • = • ∘ φ).

                    source
                    theorem NaturalLogic.EntailmentSig.compose_all_right (s : EntailmentSig) :
                    s.compose all = all
                    source
                    theorem NaturalLogic.EntailmentSig.compose_assoc (a b c : EntailmentSig) :
                    (a.compose b).compose c = a.compose (b.compose c)

                    Composition is associative.

                    source
                    @[implicit_reducible]
                    instance NaturalLogic.EntailmentSig.instMul :
                    Mul EntailmentSig
                    Equations
                    source
                    @[implicit_reducible]
                    instance NaturalLogic.EntailmentSig.instOne :
                    One EntailmentSig
                    Equations
                    source
                    @[implicit_reducible]
                    instance NaturalLogic.EntailmentSig.instMonoid :
                    Monoid EntailmentSig
                    Equations
                    • One or more equations did not get rendered due to their size.
                    source
                    inductive NaturalLogic.DEStrength :
                    Type

                    Strength of downward entailingness.

                    Names the three levels of the DE hierarchy:

                    • .weak = DE only (licenses weak NPIs: ever, any)
                    • .antiAdditive = DE + ∨→∧ distributive (licenses strong NPIs: lift a finger)
                    • .antiMorphic = AA + ∧→∨ distributive (= negation)
                    Instances For
                      source
                      @[implicit_reducible]
                      instance NaturalLogic.instDecidableEqDEStrength :
                      DecidableEq DEStrength
                      Equations
                      source
                      def NaturalLogic.instReprDEStrength.repr :
                      DEStrength → ℕ → Std.Format
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[implicit_reducible]
                        instance NaturalLogic.instReprDEStrength :
                        Repr DEStrength
                        Equations
                        source
                        def NaturalLogic.DEStrength.toNat :
                        DEStrength → ℕ

                        Rank in the Zwarts chain weak < antiAdditive < antiMorphic.

                        Equations
                        Instances For
                          source
                          theorem NaturalLogic.DEStrength.toNat_injective :
                          Function.Injective toNat
                          source
                          @[implicit_reducible]
                          instance NaturalLogic.instLinearOrderDEStrength :
                          LinearOrder DEStrength

                          The Zwarts DE hierarchy as the linear order weak < antiAdditive < antiMorphic. This is the carrier of the canonical zwartsScale (Semantics/Polarity/Licensing.lean); other theories of NPI strength supply other ordered carriers.

                          Equations
                          source
                          inductive NaturalLogic.UEStrength :
                          Type

                          Strength of upward entailingness (dual of DEStrength).

                          Names the three levels of the UE hierarchy:

                          Instances For
                            source
                            @[implicit_reducible]
                            instance NaturalLogic.instDecidableEqUEStrength :
                            DecidableEq UEStrength
                            Equations
                            source
                            @[implicit_reducible]
                            instance NaturalLogic.instReprUEStrength :
                            Repr UEStrength
                            Equations
                            source
                            def NaturalLogic.instReprUEStrength.repr :
                            UEStrength → ℕ → Std.Format
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def NaturalLogic.strengthSufficient (contextStrength requiredStrength : DEStrength) :
                              Bool

                              Check if a context's DE strength is sufficient for an NPI.

                              strengthSufficient contextStrength requiredStrength returns true when requiredStrength ≤ contextStrength in the Zwarts hierarchy (LinearOrder DEStrength).

                              Equations
                              Instances For
                                source
                                def NaturalLogic.EntailmentSig.toDEStrength (φ : EntailmentSig) :
                                Option DEStrength

                                Map an entailment signature to DE strength, derived from project.

                                A signature is DE iff it reverses forward entailment: [⊑]^φ = ⊒. Within the DE side, anti-additivity is detected by [∼]^φ = | (the ∨→∧ swap: x∨y=1 ⟹ f(x)∧f(y)=0), and anti-morphism additionally requires [|]^φ = ∼ (the ∧→∨ swap).

                                Returns none for UE-side signatures.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  def NaturalLogic.EntailmentSig.toUEStrength (φ : EntailmentSig) :
                                  Option UEStrength

                                  Map an entailment signature to UE strength, derived from project.

                                  A signature is UE iff it preserves forward entailment: [⊑]^φ = ⊑. Additivity is detected by [∼]^φ = ∼ (∨-preservation: x∨y=1 ⟹ f(x)∨f(y)=1), and multiplicativity by [|]^φ = | (∧-preservation: x∧y=0 ⟹ f(x)∧f(y)=0).

                                  Returns none for DE-side signatures.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    inductive NaturalLogic.ContextPolarity :
                                    Type

                                    Whether a context preserves or reverses entailment direction.

                                    This is a coarsening of EntailmentSig: all UE-side signatures collapse to .upward, all DE-side signatures collapse to .downward. Contexts that are neither monotone nor antitone (e.g., "exactly n") are .nonMonotonic.

                                    Used by:

                                    • NeoGricean: determines which alternatives count as "stronger"
                                    • RSA: polarity-sensitive inference
                                    • Any theory computing scalar implicatures
                                    Instances For
                                      source
                                      @[implicit_reducible]
                                      instance NaturalLogic.instDecidableEqContextPolarity :
                                      DecidableEq ContextPolarity
                                      Equations
                                      source
                                      @[implicit_reducible]
                                      instance NaturalLogic.instReprContextPolarity :
                                      Repr ContextPolarity
                                      Equations
                                      source
                                      def NaturalLogic.instReprContextPolarity.repr :
                                      ContextPolarity → ℕ → Std.Format
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        def NaturalLogic.ContextPolarity.compose :
                                        ContextPolarity → ContextPolarity → ContextPolarity

                                        Compose context polarities.

                                        This is the coarse composition table derived from the EntailmentSig monoid: UE ∘ UE = UE, DE ∘ DE = UE (double negation), UE ∘ DE = DE, DE ∘ UE = DE. Any composition involving nonMonotonic yields nonMonotonic.

                                        Equations
                                        Instances For
                                          source
                                          def NaturalLogic.EntailmentSig.toContextPolarity (φ : EntailmentSig) :
                                          ContextPolarity

                                          Map an entailment signature to the coarser ContextPolarity type, derived from project.

                                          A signature is UE iff it preserves forward entailment ([⊑]^φ = ⊑), DE iff it reverses it ([⊑]^φ = ⊒).

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            theorem NaturalLogic.EntailmentSig.toContextPolarity_compose (φ ψ : EntailmentSig) :
                                            (φ * ψ).toContextPolarity = φ.toContextPolarity.compose ψ.toContextPolarity

                                            toContextPolarity is a monoid homomorphism: composing signatures then coarsening gives the same result as coarsening then composing polarities.

                                            This theorem connects the fine-grained EntailmentSig monoid to the coarse ContextPolarity composition, ensuring the two systems can never disagree.

                                            source
                                            def NaturalLogic.EntailmentSig.contextProjectivity (path : List EntailmentSig) :
                                            EntailmentSig

                                            Compute the projectivity signature of a context from the signatures along the path from the target position to the root ([Ica12], Definition 2.9).

                                            Given a parse tree and a target position (e.g., "dangerous" in "Every job that involves a giant squid is dangerous"), the path collects the top signature of each node from the target up to the root. The composed signature is List.prod, using the Monoid instance.

                                            Example from Icard §3.2: path = [⊞, ⊕, ◇] (top(is) ∘ top(involves) ∘ top(every_restrictor)) contextProjectivity path = ◇ (anti-additive)

                                            Equations
                                            Instances For
                                              source
                                              def NaturalLogic.EntailmentSig.projectThrough (R : NLRelation) (path : List EntailmentSig) :
                                              NLRelation

                                              Project a NL relation through a context given by its signature path. Combines contextProjectivity with project.

                                              Equations
                                              Instances For
                                                source
                                                theorem NaturalLogic.projection_composition (R : NLRelation) (φ ψ : EntailmentSig) :
                                                EntailmentSig.project (EntailmentSig.project R φ) ψ = EntailmentSig.project R (ψ.compose φ)

                                                Projection composition ([Ica12], Corollary 2.12).

                                                Projecting through f then g is the same as projecting through g∘f. This is the compositionality principle: nested function application corresponds to signature composition.

                                                Since compose is derived from project (via fromProjectionPair), the only content of this theorem is that the two probe relations (forward, negation) suffice to determine the full projection table.

                                                source
                                                theorem NaturalLogic.de_signature_licenses_weak_npi (σ : EntailmentSig) :
                                                σ.toContextPolarity = ContextPolarity.downward → σ.toDEStrength.isSome = true

                                                Any DE-side signature licenses weak NPIs.

                                                This connects Icard's signature lattice to [Lad80]: a signature on the DE side (anti, antiAdd, antiMult, antiAddMult) creates a DE context, which is sufficient for weak NPI licensing.

                                                source
                                                theorem NaturalLogic.strong_npi_requires_antiadditive (σ : EntailmentSig) :
                                                σ.toDEStrength = some DEStrength.antiAdditive ∨ σ.toDEStrength = some DEStrength.antiMorphic → σ.toContextPolarity = ContextPolarity.downward

                                                Anti-additive or stronger signature licenses strong NPIs.

                                                Strong NPIs (lift a finger, in weeks) require anti-additive contexts. In Icard's system, this corresponds to signatures antiAdd, antiAddMult — but NOT plain anti or antiMult.

                                                source
                                                def NaturalLogic.negationSig :
                                                EntailmentSig

                                                Negation has the anti-morphism signature ◇⊟ (strongest DE signature).

                                                Equations
                                                Instances For