Sentential negation as a layer: complementation, anti-morphic.
Used in Homer2021
Docs / Semantics / PolarityItem / Environment
Environments of a polarity item
import Linglib.Semantics.PolarityItem.Environment · namespace PolarityItem
This file defines the environment of a polarity item in a domain, a constituent in which its acceptability is evaluated: the meaning of the domain as a function of the meaning of the item, together with a signature whose function class contains it. A layer of meaning acts on the environment of the domain below it, composing the maps and multiplying the signatures, so along the chain of domains from the item to the sentence each environment is the one below under a layer, and its sign is the product of the signs below it. An environment of negative sign carries weak strength and one of positive sign carries none, so an item licensed in one domain can be anti-licensed in the next, and licensed again in the one after.
Implementation notes
- The licenser of an environment is the classical licenser of a single operator, whose operators
are between lattices in
Type, so carrying and licensing are stated there. - A signature in whose class an environment lies can understate its strength, so showing that a domain does not carry a strength takes meanings of the item on which the environment fails the strength.
References
- Gajewski 2005, Neg-Raising: Polarity and Presupposition
- Homer 2021, Domains of Polarity Items formalized
- Icard 2012, Inclusion and Exclusion in Natural Language formalized
- Zwarts 1998, Three Types of Polarity
Declarations
The environment of a polarity item in a domain: the meaning of the domain as a function of the meaning of the item, with a signature whose function class contains it.
(σ : Type u_1) (P : Type u_2) [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] :
Type (max u_1 u_2)
- toFun : σ → P
The meaning of the domain as a function of the meaning of the item.
- signature : NaturalLogic.ProjectivitySignature
A signature whose function class contains the environment.
Used by Environment.instCoeFunForall, Environment.instMulActionSubtypeProdEndProjectivitySignatureMemSubmonoidClassPairs, Environment.coe_smul, Environment.signature_smul, Environment.monotone_of_sign_eq_one, Environment.antitone_of_sign_eq_neg_one, Environment.Carries, Environment.carries_iff, Environment.not_carries_of_sign_eq_one, Environment.carries_of_le_negationStrength, Environment.carries_weak_of_sign_eq_neg_one, Path, Path.environment
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] :
CoeFun (Environment σ P) fun (x : Environment σ P) => σ → P
- Environment.instCoeFunForall = { coe := Environment.toFun }
Built from
A layer acts on the environment of the domain below it, composing its map with the environment and multiplying its signature with the environment's.
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] :
MulAction (↥(NaturalLogic.ProjectivitySignature.classPairs P)) (Environment σ P)
The definition is too large to print here; read it in the source.
Built from
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (l : ↥(NaturalLogic.ProjectivitySignature.classPairs P)) (e : Environment σ P) :
↑(l • e) = (↑l).1 ∘ ↑e
Built from
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (l : ↥(NaturalLogic.ProjectivitySignature.classPairs P)) (e : Environment σ P) :
Built from
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (e : Environment σ P) (h : e.signature.sign = 1) :
Monotone ↑e
Built from
An environment of negative sign is downward entailing.
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (e : Environment σ P) (h : e.signature.sign = -1) :
Antitone ↑e
Built from
Carrying a strength of negation
An environment carries the strength s of negation when its licenser does.
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (e : Environment σ P) (s : Negation.Strength) :
- e.Carries s = (Licenser.ofOperator ↑e).Carries s
Built from
Used by Environment.carries_iff, Environment.not_carries_of_sign_eq_one, Environment.carries_of_le_negationStrength, Environment.carries_weak_of_sign_eq_neg_one, Path.not_licenses_of_mem_antiLicensor
Used in Homer2021
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (e : Environment σ P) {s : Negation.Strength} :
e.Carries s ↔ s.toProjectivitySignature.HoldsFor ↑e ∧ ¬Monotone ↑e
Built from ,
An environment of positive sign carries no strength of negation.
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (e : Environment σ P) {s : Negation.Strength} (h : e.signature.sign = 1) :
¬e.Carries s
Built from ,
An environment carries the strengths its signature realizes, once it is not constant.
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (e : Environment σ P) {s : Negation.Strength} (hs : ↑s ≤ e.signature.negationStrength) (hne : ↑e ⊥ ≠ ↑e ⊤) :
e.Carries s
Built from ,
An environment of negative sign carries weak strength, once it is not constant.
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (e : Environment σ P) (h : e.signature.sign = -1) (hne : ↑e ⊥ ≠ ↑e ⊤) :
Built from ,
Paths
The path of a polarity item from its minimal domain to the sentence: the environment of the minimal domain and the layers between successive domains, outermost first.
(σ : Type u_1) (P : Type u_2) [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] :
Type (max u_1 u_2)
- minimal : Environment σ P
The environment of the minimal domain.
- layers : List ↥(NaturalLogic.ProjectivitySignature.classPairs P)
The layers between successive domains, outermost first, each in the function class of its signature.
Built from
Used by Path.environment, Path.environment_nil, Path.environment_cons, Path.withAlternatives, Path.ordinary_withAlternatives, Path.withAlternatives_nil, Path.withAlternatives_cons, Path.Licenses, Path.not_licenses_of_mem_licensor, Path.not_licenses_of_mem_antiLicensor
Used in BuccolaCrnic2021, Homer2021
The environment of the domain reached through the layers t, on which they act together.
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (p : Path σ P) (t : List ↥(NaturalLogic.ProjectivitySignature.classPairs P)) :
Environment σ P
- p.environment t = t.prod • p.minimal
Built from ,
Used by Path.environment_nil, Path.environment_cons, Path.ordinary_withAlternatives, Path.Licenses, Path.not_licenses_of_mem_licensor, Path.not_licenses_of_mem_antiLicensor
Used in Homer2021
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (p : Path σ P) :
p.environment [] = p.minimal
Built from ,
The environment of each domain is that of the one below under a layer.
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (p : Path σ P) (l : ↥(NaturalLogic.ProjectivitySignature.classPairs P)) (t : List ↥(NaturalLogic.ProjectivitySignature.classPairs P)) :
p.environment (l :: t) = l • p.environment t
Built from ,
The meaning of the domain reached through the layers t with its alternatives, when A gives
the alternatives of the minimal domain: the layers apply to each alternative.
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (p : Path σ P) (A : σ → Set P) (t : List ↥(NaturalLogic.ProjectivitySignature.classPairs P)) (x : σ) :
- p.withAlternatives A t x = (↑t.prod).1 <$> { ordinary := ↑p.minimal x, alternatives := A x }
Built from
Used by Path.ordinary_withAlternatives, Path.withAlternatives_nil, Path.withAlternatives_cons
Used in BuccolaCrnic2021
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (p : Path σ P) (A : σ → Set P) (t : List ↥(NaturalLogic.ProjectivitySignature.classPairs P)) (x : σ) :
(p.withAlternatives A t x).ordinary = ↑(p.environment t) x
Built from , ,
{σ : Type u_1} {P : Type u_2} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (p : Path σ P) (A : σ → Set P) (l : ↥(NaturalLogic.ProjectivitySignature.classPairs P)) (t : List ↥(NaturalLogic.ProjectivitySignature.classPairs P)) (x : σ) :
p.withAlternatives A (l :: t) x = (↑l).1 <$> p.withAlternatives A t x
Built from ,
Licensing
An item is acceptable under an operator over its position when the operator carries the strength of negation that licenses the item and does not carry the strength that blocks it.
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (π : PolarityItem) (f : σ → P) :
- π.Acceptable f = ((∀ s ∈ π.licensor, (Licenser.ofOperator f).Carries s) ∧ ∀ s ∈ π.antiLicensor, ¬(Licenser.ofOperator f).Carries s)
Used by acceptable_of_licensor, acceptable_of_antiLicensor, Path.Licenses
Used in Homer2021
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] {π : PolarityItem} {f : σ → P} {s : Negation.Strength} (hl : π.licensor = some s) (ha : π.antiLicensor = none) (h : (Licenser.ofOperator f).Carries s) :
π.Acceptable f
Built from
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] {π : PolarityItem} {f : σ → P} {s : Negation.Strength} (hl : π.licensor = none) (ha : π.antiLicensor = some s) (h : ¬(Licenser.ofOperator f).Carries s) :
π.Acceptable f
Built from
The licensing condition: the item is acceptable in some domain.
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (p : Path σ P) (π : PolarityItem) :
- p.Licenses π = ∃ t ∈ p.layers.tails, π.Acceptable ↑(p.environment t)
Built from , ,
Used by Path.not_licenses_of_mem_licensor, Path.not_licenses_of_mem_antiLicensor
Used in Homer2021
An item that a strength licenses is anti-licensed when every domain has positive sign.
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (p : Path σ P) {s : Negation.Strength} {π : PolarityItem} (hs : s ∈ π.licensor) (h : ∀ t ∈ p.layers.tails, (p.environment t).signature.sign = 1) :
¬p.Licenses π
Built from , ,
An item that a strength blocks is anti-licensed when every domain carries it.
{σ P : Type} [Lattice σ] [BoundedOrder σ] [Lattice P] [BoundedOrder P] (p : Path σ P) {s : Negation.Strength} {π : PolarityItem} (hs : s ∈ π.antiLicensor) (h : ∀ t ∈ p.layers.tails, (p.environment t).Carries s) :
¬p.Licenses π
Built from , , ,