Documentation

Linglib.Semantics.Composition.Ty

Semantic types and denotation domains #

The semantic types of the composition engine and their denotation domains. Ty is the type grammar — e, t, ⟨a,b⟩, ⟨s,a⟩, and the degree, cardinality and eventuality sorts of later work — and Denot E W ty computes the domain of possible denotations of each type from an entity type E and an index type W: functions denote in function spaces and intensions in W-indexed families, so a denotation is an ordinary Lean term and composition is function application.

Denot is reducible: a denotation of type ⟨e,t⟩ is an E → Prop to every tactic and instance, and the pointwise Boolean algebra of a type that ends in t is mathlib's Pi instance. Denot.booleanAlgebra? computes that algebra by recursion on the type, for the composition engine's runtime type dispatch.

Main definitions #

References #

source
inductive Semantics.Composition.Ty :
Type

Semantic types: Montague's e, t, fn a b (⟨a,b⟩) and intens a (⟨s,a⟩), the degree sort d ([heim-2001], [wellwood-2015]), the cardinality sort n ([sudo-2016], [scontras-2014], [little-moroney-royer-2022]), and the eventuality sorts v (events) and s (states) ([davidson-1967], [parsons-1990], [yu-ausensi-smith-2023]).

  • e : Ty
  • t : Ty
  • d : Ty

    Degrees, denoting in the model's scale.

  • n : Ty

    Cardinalities, denoting in ℕ.

  • v : Ty

    Events.

  • s : Ty

    States (not the index sort, which is intens).

  • fn : Ty → Ty → Ty

    Functions ⟨a,b⟩.

  • intens : Ty → Ty

    Intensions ⟨s,a⟩.

Instances For
    source
    def Semantics.Composition.instReprTy.repr :
    Ty → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Semantics.Composition.instReprTy :
      Repr Ty
      Equations
      source
      def Semantics.Composition.instDecidableEqTy.decEq (x✝ x✝¹ : Ty) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        @[instance_reducible]
        instance Semantics.Composition.instDecidableEqTy :
        DecidableEq Ty
        Equations
        source
        def Semantics.Composition.«term_⇒_» :
        Lean.TrailingParserDescr

        Functions ⟨a,b⟩.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[reducible, inline]
          abbrev Semantics.Composition.Ty.et :
          Ty

          ⟨e,t⟩, properties of individuals.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Semantics.Composition.Ty.eet :
            Ty

            ⟨e,⟨e,t⟩⟩, relations between individuals.

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev Semantics.Composition.Ty.ett :
              Ty

              ⟨⟨e,t⟩,t⟩, generalized quantifiers.

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev Semantics.Composition.Denot (E W : Type) (ty : Ty) (D : Type := ℝ) :
                Type

                Denotation domains: e denotes in E, t in Prop, d in the scale D, n in ℕ, ⟨a,b⟩ in Denot a → Denot b and ⟨s,a⟩ in W → Denot a. The eventuality sorts have the empty domain: nothing here constructs event-typed denotations.

                Equations
                Instances For
                  source
                  def Semantics.Composition.Denot.booleanAlgebra? (E W : Type) (ty : Ty) (D : Type := ℝ) :
                  Option (BooleanAlgebra (Denot E W ty D))

                  The pointwise Boolean algebra of a conjoinable type ([PR83]), computed by recursion on the type: none exactly when the type does not end in t. At a concrete type this is the instance Pi.instBooleanAlgebra finds statically.

                  Equations
                  Instances For