Composing layers of signatures

import Linglib.Logic.Natural.Composition · namespace NaturalLogic.ProjectivitySignature

The maps in the function class of a signature, each paired with that signature, form a submonoid of Function.End α × ProjectivitySignature (ProjectivitySignature.classPairs), since function classes compose along ProjectivitySignature.compose and the identity is a morphism. A path of such layers is therefore in the class of the product of its signatures, the projectivity of a position, and the sign of that product is the product of the signs of the layers. The sign fixes the direction of the composite: it is monotone under a positive sign and antitone under a negative one, so composing with a layer of negative sign reverses the direction (antitone_list_prod).

References

Icard 2012, Inclusion and Exclusion in Natural Language formalized

Declarations

The maps paired with a signature whose function class contains them, a submonoid of Function.End α × ProjectivitySignature: function classes compose along ProjectivitySignature.compose, and the identity is a morphism.

def classPairs L36–43

(α : Type u_1) [Lattice α] [BoundedOrder α] :

Submonoid (Function.End α × ProjectivitySignature)

classPairs α = { carrier := {p : Function.End α × NaturalLogic.ProjectivitySignature | p.2.HoldsFor p.1}, mul_mem' := ⋯, one_mem' := ⋯ }

Used by mem_classPairs

Used in Semantics/PolarityItem/Environment, Homer2021

A path of layers whose signs multiply to the negative sign composes to an antitone map.

theorem antitone_list_prod L66–71

{α : Type u_1} [Lattice α] [BoundedOrder α] {l : List (Function.End α × ProjectivitySignature)} (h : ∀ p ∈ l, p.2.HoldsFor p.1) (hs : (List.map (fun (p : Function.End α × ProjectivitySignature) => p.2.sign) l).prod = -1) :

Antitone l.prod.1