NeSyCat: A Monad-Based Categorical Semantics of the Neurosymbolic ULLER Framework Daniel Romero Schellhorn1 and Till Mossakowski2 1
arXiv:2604.24612v1 [cs.AI] 27 Apr 2026
University of Osnabrück, Osnabrück, Germany. [email protected] 2 University of Osnabrück, Osnabrück, Germany. [email protected]
Abstract ULLER (Unified Language for LEarning and Reasoning) offers a unified first-order logic (FOL) syntax, enabling its knowledge bases to be used directly across a wide range of neurosymbolic systems. The original specification endows this syntax with three pairwise independent semantics: classical, fuzzy, and probabilistic, each accompanied by dedicated semantic rules. We show that these seemingly disparate semantics are all instances of one categorical framework based on monads, the very construct that models side effects in functional programming. This enables the modular addition of new semantics and systematic translations between them. As example, we outline the addition of generalised quantification in Logic Tensor Networks (LTN) to arbitrary (also infinite) domains by extending the Giry monad to probability spaces. In particular, our approach allows a modular implementation of ULLER in Python and Haskell, of which we have published initial versions on GitHub.
Keywords: Neurosymbolic AI, Category Theory, Monads, Probability Theory, Fuzzy Logic, Categorical Logic
1
Introduction
Neurosymbolic integration is a rapidly developing branch of AI. In the past, numerous heterogeneous approaches have emerged, each with its own code base. Van Krieken et al. [2024] introduces ULLER, a unified neurosymbolic library that aspires to play for neurosymbolic systems the role that TensorFlow and PyTorch play for deep-learning workflows. Their theoretical core is the concept of a NeSy system: standard first-order logic enriched with neural components. In particular, formulas of the form x := m(T1 , . . . , Tn )F
(Ti terms, F a formula involving variable x, m a neural model)
are used to integrate neural models m into logical formulas. These formulas go beyond classical first-order logic. Instead, they perform computations that may return multiple values and typically involve non-determinism or probability distributions as illustrated in the following toy example in [Van Krieken et al., 2024]: Example 1 (MNIST digit classification). ∀x ∈ ImageData (n1 := classify(x.im1 ) (n2 := classify(x.im2 ) (n1 + n2 = x.sum) )) 1
This classifies two images of digits and checks whether the sum of the resulting numbers is as specified in the dataset. The resulting (e.g. fuzzy or probabilistic) truth value can be used in a loss function. A shorthand notation for this is: ∀x ∈ ImageData n1 := classify(x.im1 ), n2 := classify(x.im2 ) (n1 + n2 = x.sum)
To simplify notation and to stress the relation to dynamic logic [Harel et al., 2001, Mossakowski et al., 2010], we henceforth use the notation ∀x ∈ ImageData n1 := classify(x.im1 ) n2 := classify(x.im2 ) n1 + n2 = x.sum
or shorthand ∀x ∈ ImageData n1 := classify(x.im1 ), n2 := classify(x.im2 ) n1 + n2 = x.sum
While the notion of NeSy system in Van Krieken et al. [2024] is very powerful, it also has several shortcomings: • There is no uniform inductive definition of truth, i.e. of the truth value of a sentence in an interpretation. Rather, the notion of NeSy system has the inductive interpretation function as a component, meaning that classical, probabilistic and fuzzy NeSy systems employ three different inductive definitions of truth. Parts of these definitions of truth are copied verbatim from one NeSy system to another, other parts need to be replaced. This duplication of semantic rules is not modular. By contrast, we aim at a truly uniform inductive definition of truth value that is independent of the NeSy system and hence can be reused for different NeSy systems, such that the NeSy system itself is a parameter of the inductive definition of truth. • The case of continuous probability distributions (involving probability kernels or Markov kernels) is not covered faithfully, because in this case, measurable spaces are required to properly define the mentioned Markov kernels. However, measurable spaces are not considered in Van Krieken et al. [2024] and probability measures are confused with density functions in the monadic formula of the probabilistic semantics. • The treatment of logical connectives is not uniform across NeSy systems, i.e. the different sets of connectives are not considered as instances of a common abstract (algebraic) notion. Also, quantifiers in probabilistic semantics are defined using possibly infinite products, without requiring a suitable order structure on domains and without discussing convergence. • The high-level concepts of semantics and computation are not properly separated. Computation (namely sampling) is mixed into the semantics at least in two places. The first one in the classical semantics, where the possibly multi-valued arg max can only be properly evaluated using sampling. We conceptualise the arg max differently as a transition between semantics. The second time is in "Sampling Semantics", which is not really semantics but computation (sampling). We argue that ULLER is conceptually robust and show that a monadic formulation resolves all of the foregoing issues. In particular, ULLER formulas of the form [x := m(T1 , . . . , Tn )]F
(Ti terms, F a formula involving variable x, m a neural model)
can be modelled using Moggi’s notion of computational monad [Moggi, 1991], which has been introduced to model side effects in (functional) programming. Although monads originate in category theory, we first present them using a set-theoretic approach that does not involve any 2
category theory. The generalisation to an arbitrary category, which is needed for continuous probabilities and some aspects of infinite domains, comes only in later sections. We call our categorical approach simply NeSyCat, standing for Neurosymbolic Category-theory framework. This paper is organised as follows. Section 2 introduces NeSy frameworks and their algebraic prerequisites without use of category theory. Based on that, section 3 introduces the syntax and semantics of NeSyCat. Section 4 discusses several examples of set-based NeSy frameworks, including classical, fuzzy, and probabilistic ones. Section 5 discusses translations between NeSy systems. Section 6 generalises set-based NeSy frameworks to categorical NeSy frameworks, which is needed for continuous probability distributions and infinite domains. Section 7 defines the categorical semantics of NeSyCat and provides examples of categorical NeSy systems. Section 8 discusses related work, and section 9 outlines our implementation of NeSyCat in Python and Haskell. Section 10 concludes the paper and outlines future work. Appendix A contains a brief introduction to the needed concepts of category theory. This paper is an extended an revised version of Schellhorn and Mossakowski [2025]. Finally, while this paper focuses on the theoretical foundation, questions of differentiability, computability, and computational complexity are left for future work in a subsequent paper dedicated to the implementation and practical evaluation of NeSyCat.
2
Set-Based NeSy Frameworks
Background: key concepts from ULLER. We briefly recall the main concepts from Van Krieken et al. [2024] that our framework builds upon. ULLER is a first-order logic extended with statements x := f (T1 , . . . , Tn )(F ), which bind a variable x to the result of applying a (possibly neural) function f to terms Ti , then evaluate the formula F in the extended context. An interpretation I assigns meanings to the non-logical symbols: domains I(D) to domain symbols, functions I(f ) to function symbols (as conditional probability distributions), predicates I(P ) to predicate symbols, and constants I(c) to constant symbols. A NeSy system (I, η, B, J·K) in ULLER bundles an interpretation I, a variable assignment η, a set of outputs B (e.g., {0, 1} for classical, [0, 1] for fuzzy/probabilistic), and a semantic function J·K that inductively assigns a value in B to each formula. ULLER provides three example semantics – classical, probabilistic, and fuzzy – each defining J·K separately, which leads to the duplication of semantic rules that we address below. A neurosymbolic framework (NeSy framework) is a general framework for NeSy systems combining neural models with symbolic logic, and it provides the semantic background for the specific logic involved. Examples are the logics behind DeepProbLog [Manhaeve et al., 2021] or Logic Tensor Networks [Badreddine et al., 2022]. The notion of NeSy framework is not defined in Van Krieken et al. [2024]. Rather, they define a notion of NeSy system, which is quite ad-hoc, because it simultaneously makes two choices: (1) a choice of a particular interpretation with functions, predicates and neural models (e.g., probabilities for traffic lights, or neural networks learning addition of digit images), and (2) a choice of semantic rules for interpreting terms (which also involves a choice of the logic, e.g. classical or probabilistic or fuzzy). This causes semantic rule duplication. Our notion of NeSy framework provides a means to disentangle these two choices. Moreover, our approach makes semantic rules independent not only of particular interpretations, but also of the choice of logic (classical, probabilistic, or fuzzy). In the sequel, we first introduce the algebraic structure needed to model the space of truth values (section 2.1), generalising the standard two-valued truth value space {T, F } used in classical logic. Neural, probabilistic and/or non-deterministic aspects are incorporated into logics using monads, which are the key concept of our approach and which we introduce in section 2.2. Being such prepared, we can define a NeSy framework as consisting of a monad and a truth algebra in setion 2.3. 3
2.1
Double Monoid Bounded Lattices (2Mon-BLat)
We need an algebraic structure to model the space of truth values. We weaken the notion of BL algebra of Hájek [1998] from fuzzy logic as follows: Definition 1. A double monoid bounded lattice (2Mon-BLat) R is a tuple S, ≤, ⊥, ⊤, ⊗, 0, 1, ⊕, →, ¬
in which S is a set, L := (S, ≤) a bounded lattice (see App. A for this and other standard algebraic and categorical terms), while ⊥ ∈ S and ⊤ ∈ S are its bottom and top elements.1 Also (S, ⊗, 1) and (S, ⊕, 0) are monoids (App. A), → is a map S × S → S, and ¬ is a map S → S. Our monoid requirement on (⊗, 1) and (⊕, 0) – i.e. associativity and the existence of neutral elements – is stronger than what the original ULLER paper [Van Krieken et al., 2024] explicitly requires. ULLER instead requires that its semantics be classical in the limit: when the truth space is restricted to {0, 1} (which actually are the implicit unit elements), the semantics should agree with classical first-order logic (see [Van Krieken et al., 2024, Appendix C]). This classicalin-the-limit property follows from the monoid axioms together with the standard boundary conditions of t-norms and t-conorms (e.g., 1 ⊗ x = x and 0 ⊕ x = x), but is strictly weaker: one could have classical-in-the-limit behaviour without full associativity. We adopt the stronger monoid requirement because it provides a cleaner algebraic structure and associativity ensures that the order of evaluation of iterated conjunctions and disjunctions does not matter. All concrete algebras used in this paper (Table 3) satisfy these requirements; whether there are useful NeSy-relevant algebras that are classical in the limit but not monoids is an open question. Note that we do not require commutativity of ⊗ or ⊕ in general, although all concrete instances in Table 3 happen to be commutative. Also, we want to allow different aggregation operations other than infinite meet and join to cover the quantifiers of Logic Tensor Networks [Badreddine et al., 2022], motivating the following definition:2 Definition 2. An aggregated 2Mon-BLat (aggr-2Mon-BLat) has for each set X two order-preserving maps: aggr∀X , aggr∃X : LX −→ L. In case of a complete lattice, aggr∀X can be chosen as meet
2.2
V
W ∃ X and aggrX as join X.
Set-Based Monads
We interpret formulas [x := m(T1 , . . . , Tn )]F involving neural models m (= certain computations) using Moggi’s notion of computational monad [Moggi, 1991]. Moggi’s central idea is to use monads to abstract from various computational effects by providing an abstract framework covering many different types of effects such as state, input, output or non-determinism. We here use monads in a similar way, but rather focus on neural and probabilistic computations. This use of moands has been widely adopted for probabilistic programming [Ramsey and Pfeffer, 2002, Staton et al., 2016]; we discuss this connection in detail in Section 8.3. Note that the monadic approach does not focus on mere effectful computation only, it also captures values that are returned by such computations. E.g. think of a stateful function that alters the state 1
In many cases we have ⊥ is neutral element for ⊕ and ⊤ is neutral element for ⊗, for example inside of the unit interval [0, 1]. In some cases, like Gödel or Boolean logic, we even have ⊕ = ∨ and ⊗ = ∧. Also, → is normally chosen as right adjoint to ⊗ (App. A) or as x → y := ¬x ⊕ y. In the first case ¬ can be defined as implication to zero, in the second one it is defined a priori. Check Table 3 for details. 2 This is inspired by the notion of aggregated functions in [Badreddine and Spranger, 2021].
4
but also returns a value, or, in our case, a probability distribution over a set of values. A monad provides three ingredients: (1) given a set (type) of values, a set of computations over such values, (2) an embedding of values into computations, and (3) a notion of sequential composition of computations that allows for passing values through the composition. Definition 3. A (set-based) monad3 (T , η, (−)∗ ) consists of: • A mapping T , mapping sets X to sets T X (of computations with values from X), • A family of functions: ηX : X → T X for each set X (construing a value a ∈ X as stateless computation ηX (a) ∈ T X), • A function that assigns to each function f : X → T Y a function f ∗ : T X → T Y (called the Kleisli extension), needed for sequential composition of computations, such that the following axioms hold: 1. (ηX )∗ = idT X , the identity function on T X, 2. f ∗ ◦ ηX = f for all f : X → T Y , 3. (g ∗ ◦ f )∗ = g ∗ ◦ f ∗ for all f : X → T Y and g : Y → T Z. We now explain how the third ingredient of a monad can be used for sequential composition. Assume that we have a computation ma : T A and a computation f (x) : T B parameterised over x : A, i.e. f : A → T B. We can compose them to (λx : A.f (x))∗ (ma)4 , or short f ∗ (ma), of type T B. In Haskell’s do-notation, (λx : A.f (x))∗ (ma) is written as do x ← ma; f (x). For the sake of readability, we will use do-notation henceforth. f ∗ (ma) is also written as ma >>= f in fish notation.5 Example 2. Non-empty Powerset monad P̸=∅ For a set X: P̸=∅ X := {A ⊆ X | A ̸= ∅} ηX (x) := {x},
f ∗ (A) :=
[
(non-empty subsets of X),
f (a)
f : X → P̸=∅ Y, A ∈ P̸=∅ X .
a∈A
This monad models non-deterministic computation returning one or more possible values. The S Kleisli extension f ∗ (A) = a∈A f (a) applies f to each element and collects all results – a “flatMap” over sets. In a NeSy setting, this captures situations such as an ambiguous image classifier that returns multiple plausible labels (e.g., a poorly written digit classified as both 7 and 1). Example 3. Probability distribution monad D.6 DX :=
n
ρ : X → [0, 1] finitely supported
X
o
ρ(x) = 1
(prob. distributions on X),
x∈X
(
ηX (x) := δx , δx (y) =
1, x = y 0, x ̸= y
f ∗ (ρ)(y) :=
X
f (x)(y) · ρ(x)
f : X → DY, ρ ∈ DX .
x∈X
3
In category theory, a monad on a category C can be equivalently presented in two ways: (1) as an endofunctor T with natural transformations η : Id ⇒ T (unit) and µ : T 2 ⇒ T (multiplication) satisfying associativity and unit laws; (2) as an extension system (also called Kleisli triple), which is the presentation we adopt here because it directly captures sequential composition of computations and is therefore most natural for computer science applications [Moggi, 1991]. 4 In this lambda notation the variable x of type A is sent to f (x) of type T B. 5 See https://ncatlab.org/nlab/show/monad+%28in+computer+science%29#DoNotation for a comprehensive comparison of all different notations. 6 Note that the sums below are only finite if one excludes all the zero addenda.
5
δx is the probability distribution that assigns all probability mass to x. f ∗ (ρ) corresponds to a two-level random process: first x is drawn from ρ, then y is drawn from f (x). This results in a marginal distribution of Y for the joint distribution ρ̂(x, y) := f (x)(y) · ρ(x). do x ← ma; f (x) can be interpreted as “sample x from ma and then proceed with f (x)”. When the formula F := [x := m(T )]P (x) evaluates to a numerical truth value, f ∗ (ρ), with f (a) := JP (a)K and ρ := m(T ), computes the expected truth value under ρ – this is how probabilistic NeSy semantics yields expected-value loss functions (cf. Example 1).
2.3
Definition of Set-Based NeSy Framework
Given some basic set of truth values Ω, our NeSy systems work on the monadic space of truth values T Ω, which is required to be an aggregated 2Mon-BLat. If T is the identity monad, T {0, 1} is just the two-element set {0, 1} of classical truth values. If T is the distribution monad, T {0, 1} is isomorphic to the unit interval [0, 1], regarded as the space of probabilistic or fuzzy truth values. Definition 4. A NeSy framework F = (T , R) consists of 1. a monad T , 2. an aggr-2Mon-BLat R on T Ω for some set Ω. Here, Ω is a set acting as truth basis,7 and T Ω is the monadic space of truth values. Examples are given in Table 1 and discussed in more detail in section 4. Note that further examples arise by varying the 2Mon-BLat R on [0, 1]. Examples requiring category theory are given in Table 4. Table 1: NeSy Framework Examples (set-based) Logic/Theory
T
Ω
TΩ
R
Subsection
Classical Three-valued LP Distributional Finitary LTNp Classical Fuzzy
Identity Powerset P̸=∅ Distribution D Distribution D Identity
{0, 1} {0, 1} {0, 1} {0, 1} [0, 1]
{0, 1} {0, B, 1} [0, 1] [0, 1] [0, 1]
Boolean Alg. Kleene/Priest Alg. Product BL–Alg. Product SBL-Alg. Classical BL–Alg.
4.1 4.1 4.2 4.3 –
Proposition 1. Assume that we can lift lattices along T , i.e. for a lattice structure on X, we can construct a lattice on T X such that η preservers ⊥ and ⊤. If R = (Ω, ≤, ⊥, ⊤, ⊗, 0, 1, ⊕, →, ¬) is a 2Mon-BLat, then T Ω is so, too, in a canonical way. Proof. We define (T Ω, ≤′ , ⊥′ , ⊤′ , ⊗′ , 0, 1, ⊕′ , →′ , ¬′ ) as follows: • ≤′ is the lifting of ≤, • ⊥′ := η(⊥),
⊤′ := η(⊤),
• 0′ := η(0), • 1′ := η(1), • a ⊗′ b := do x ← a; y ← b; η(x ⊗ y), • a ⊕′ b := do x ← a; y ← b; η(x ⊕ y), 7
Similar to the basis of a vector space.
6
• a →′ b := do x ← a; y ← b; η(x → y), • ¬′ a := do x ← a; η(¬x). Associativity and unit laws of ⊗′ and ⊕′ follows from the corresponding properties of the monoids for ⊗ and ⊕ and those of the monad.
3
Syntax and Semantics of NeSyCat
3.1
Syntax of First-Order Logic
The ULLER language of Van Krieken et al. [2024] features computational function symbols that can be realised e.g. by neural networks. In a similar spirit, we here add computational predicate symbols, which are also realised by neural networks, for example in Logic Tensor Networks [Badreddine et al., 2022]. Definition 5. A NeSy signature Σ consists of • a set S of sorts of Σ, • two disjoint sets Pred, mPred of predicate symbols and computational predicate symbols of form p : s1 , . . . , sn , where p is a name and each si ∈ S a sort, • two disjoint sets Func, mFunc of function symbols and computational function symbols of form f : s1 , . . . , sn → s, , where f is a name and s, si ∈ S are sorts. (Computational) predicate symbols with no arguments are called (computational) propositional symbols (Prps and mPrps respectively). Function symbols with one argument are called properties (Prop), those with none are called constants (Const).
3.2
Tarskian Semantics
Definition 6. A NeSy interpretation I on Σ of (T , R), for a NeSy signature Σ and a NeSy framework (T , R), is given by • a set I(s) for every sort s, • a function I(f ) : I(s1 ) × . . . × I(sn ) → I(s) for every (normal) function symbol f : s1 , . . . , sn → s ∈ Func, • a function I(m) : I(s1 ) × . . . × I(sn ) → T (I(s)) for every computational function symbol m : s1 , . . . , sn → s ∈ mFunc, • a function I(P ) : I(s1 ) × . . . × I(sn ) → Ω for every predicate symbol P : s1 , . . . , sn ∈ Pred, • and a function I(M ) : I(s1 ) × . . . × I(sn ) → T Ω for every computational predicate symbol M : s1 , . . . , sn ∈ mPred. Definition 7. A NeSy system can be defined as a triple (T , R, I), where (T , R) is a NeSy framework and I a NeSy interpretation over that same NeSy framework. Note that in this notation the underlying set of basic truth values Ω, with which the aggr2Mon-BLat R is defined, and the signature Σ on which the interpretation I is defined, are suppressed since they are implicit.
7
Example 4. The MNIST addition formula from the introduction (Example 1, slightly adapted), ∀x ∈ ImageData n1 := classify(x1 ), n2 := classify(x2 ) n1 + n2 = sum(x1 , x2 )
illustrates why the signature requires both computational and non-computational symbols. Here, classify : Image → Digit is a computational function symbol (∈ mFunc): it is realised by a neural network and its interpretation maps into D(I(Digit)), i.e. it returns a distribution over digits rather than a single digit. By contrast, + : Digit2 → Digit (∈ Func), and the projection symbols π1 , π2 : ImageData → Image : x 7→ x1 , x 7→ x2 and sum : ImageData → Digit are likewise normal function symbols. Similarly, = : Digit2 → Bool is the built-in equality predicate symbol interpreted in the usual way as diagonal. The distinction between computational and non-computational symbols matters because the monadic machinery of a NeSy framework acts only on computational symbols: the monad T wraps their output, and the dynamic logic brackets [·] bind the resulting values. Non-computational symbols, by contrast, are interpreted as ordinary functions or predicates and are independent of the choice of monad. Compared to Van Krieken et al. [2024], we have added computational predicate symbols, because LTN and other NeSy frameworks use these. However note that for probabilistic logic and weighted model counting, ULLER makes (probabilistic) independence assumptions due to the nature of its notion of interpretation.8 While computational function symbols enable the use of conditional probabilities, computational predicate symbols are not available in ULLER.9 Hence, ULLER supports a certain combination of probabilistic and fuzzy logic, and so do LTNs. For details, see section 7.1 Also, we have dropped uniformity of the notion of interpretation—it now becomes dependent on the monad at hand. This is necessary for faithfully distinguishing finitely supported and continuous probability distributions and for dealing with LTN-style quantification on infinite domains. Still, computational symbols can be realised by neural networks in all of these cases. However, the details of the mapping from neural networks to interpretations of computational symbols differ. In Van Krieken et al. [2024], based on an interpretation, the notion of NeSy system provides a Tarskian inductive definition J·K of the semantics of formulas and thus it implicitly also defines the semantics of the logical symbols. The drawback of this approach is that the Tarskian semantics J·K is inherently tied to the specific NeSy system. We can modularise matters here, because we first give a semantics of the logical symbols via a NeSy framework, and based on that, the interpretation provides the semantics of the non-logical symbols. Hence, the inductive definition of the Tarskian semantics J·K needs to be given only once, and this definition holds across all NeSy frameworks and systems. The Tarskian semantics uses variable valuations. As a preparation, we collect variables occurring freely in terms and formulas. Given a term T , let ΓT = {x1 : s1 , . . . , xn : sn } be its context (of variables) and sT be its sort. Then, we define the space of variable valuations Q compatible with T as VT := x:s∈ΓT I(s) = I(s1 ) × · · · × I(sn ). Given a variable valuation ν ∈ VT , note that is maps variables x : s to values in I(s). Q Analogously, for a formula F , VF := x:s∈ΓF I(s). Sentences, i.e. formulas without free variables, can be interpreted over the unique empty variable valuation (in this case, VF = {()} is a singleton set containing just the empty tuple). Hence, as usual in first-order logic, for interpreting sentences, we do not need a variable valuation. 8
As already hinted at in the original ULLER paper [Van Krieken et al., 2024] and looked at in more detail by van Krieken et al. [2024] and van Krieken et al. [2025], the independence assumption can prevent NeSy predictors from correctly modelling uncertainty. 9 Note that the predicate True(x), used in some ULLER examples to convert values {0, 1} (delivered by computational funnctions) into truth values, can also be used in NeSyCat. However, in NeSyCat, we can directly use computational predicates instead.
8
Definition 8. The Tarskian semantics J·K of formulas and terms in a NeSy system (T , R, I) is given by two functions defined in Table 2: Formulas: JF KI,ν : VF → T Ω,
Terms: JT KI,ν : VT → I(sT ).
Table 2: Inductive definition of the Tarskian semantics Syntax
Set Semantics J·KI,ν
Terms Jx : sK JcK, JT.propK, Jf (T⃗ )K
ν(x) I(c), I(prop)(JT K), I(f ) JT⃗ K
Atomic formulas JRK, JP (T⃗ )K JN K, JM (T⃗ )K
ηΩ (I(R)), ηΩ I(P )(JT⃗ K) I(N ), I(M ) JT⃗ K
Compound formulas J⊥K, J⊤K JF → GK, J¬F K JF ∥GK, JF &GK
J∃x:s F K, J∀x:s F K J[x := m(T⃗ )]F K
⊥R , ⊤R JF K →R JGK, ¬R JF K
JF K ⊕R JGK, JF K ⊗R JGK
aggr∃I(s) (λa.JF Kν[x7→a] ), aggr∀I(s) (λa.JF Kν[x7→a] ) do a ← I(m)(JT⃗ K); JF Kν[x7→a]
T⃗ stands for T1 , . . . , Tn . We write JT KI,ν = JT KI (ν) and JF KI,ν = JF KI (ν). That said, we mostly omit I and ν if clear from the context. The computational formula rule. The last row of Table 2 is the key rule connecting neural models to logic. It reads: “to evaluate [x := m(T⃗ )]F , first evaluate the terms T⃗ , then apply the computational function m to obtain a computation I(m)(JT⃗ K) ∈ T (I(s)). The do-notation do a ← ·; · then ‘extracts’ a value a from this computation and evaluates F with x bound to a.” What “extract” means concretely depends on the monad: for the distribution monad D (Ex. 3), it means averaging JF Kν[x7→a] over all possible values a, weighted by their probabilities; for the non-empty powerset monad (Ex. 2), it means collecting the truth values of F for every possible value a returned by m. This is precisely the Kleisli extension JF K∗ν[x7→a] of the monad applied to I(m)(JT⃗ K). Quantifier aggregation. The quantifiers ∀x:s and ∃x:s evaluate F for every element a of the domain I(s), producing a family of truth values JF Kν[x7→a] a∈I(s) . The aggregation functions
aggr∀I(s) and aggr∃I(s) then combine this family into a single truth value. Unlike in classical firstorder logic, where the quantifiers are hardcoded as infimum and supremum, the aggregation in NeSyCat is parametrised by the NeSy framework: for classical logic, it is min/max; for probabilistic semantics, a product and probabilistic sum; for LTN, a p-norm. Section 4 spells out each of these instantiations. The Tarskian semantics of Definition 8 is deliberately inductive, i.e. defined by recursion on the structure of formulas. In ULLER [Van Krieken et al., 2024], the broader notion of “neurosymbolic system” also permits non-inductive evaluation strategies—for instance, first compiling a 9
formula into a circuit representation and then evaluating that circuit. NeSyCat does not incorporate such strategies into its semantics. This is by design: we cleanly separate the meaning of a formula (given inductively by the Tarskian semantics) from the method of evaluation (which may involve compilation, circuit construction, or sampling). Non-inductive evaluation strategies are thus implementation concerns that operate on top of the inductively defined semantics, rather than alternatives to it. This mirrors the classical separation in programming language theory between denotational semantics and compilation, and aligns with the analogous separation of semantics and sampling discussed in Section 4.4.
4
Examples of Set-Based Semantics
In the sequel, we will discuss some NeSy frameworks in more detail and spell out how the semantic rules look when instantiated. Each subsection specifies a monad T and a 2Mon-BLat algebra R; the full definitions of all algebras used in this paper are collected in Table 3 (Sec. 6.2). Note that the semantic rule for computational formulas [x := m(T⃗ )]F is always determined by the monad’s Kleisli extension f ∗ , while the rules for connectives and quantifiers are determined by the 2Mon-BLat. We often implicitly define parts of the 2Mon-BLat through the semantic rules. E.g. the aggr∃ and aggr∀ functions are implicitly defined by listing semantic rules for the quantifiers.
4.1
Classical and Three-valued Semantics
Classical semantics is simply given by the identity monad (Ex. 5) and the Boolean algebra (Table 3, row “Boolean”) on Ω = {0, 1}, which results in classical first-order logic. Our classical semantics is deterministic, while Van Krieken et al. [2024] use probability distributions, causing the need for selection of values with highest probability, done via argmax. We will model this as NeSy transformation in section 5 and need a non-deterministic NeSy framework as target of this transformation. The (non-empty) powerset monad models nondeterministic computations, cf. multialgebras [Walicki and Meldal, 1994]. These result in nondeterministic truth values as in: Logic of Paradox Semantics For the Logic of Paradox [Priest, 2008], we use the non-empty powerset monad P̸=∅ (Ex. 2) with the Kleene/Priest algebra (Table 3, row “Priest”). We have T = P̸=∅ , Ω = {0, 1} (equivalently {F, T }), and T Ω = P̸=∅ ({0, 1}) = {{0}, {1}, {0, 1}}. The three truth values correspond to: {0} ≡ F (false only), {1} ≡ T (true only), and {0, 1} ≡ B (both true and false). Following the uniform Tarskian semantics (where the union in the computational formula rule arises from the Kleisli extension of P̸=∅ , cf. Ex. 2): J[x := m(T⃗ )]F K :=
[
(1)
JF Kν[x7→a]
a∈I(m)(JT⃗ K)
J∃x:s F K := sup JF Kν[x7→a] ,
J∀x:s F K := inf JF Kν[x7→a]
(2)
JF ∥GK := max(JF K, JGK),
JF &GK := min(JF K, JGK)
(3)
a∈I(s)
a∈I(s)
{0, 1} if JF K = {0, 1} ({0, 1} \ JF K) else
(
JF → GK := max(J¬F K, JGK), J⊥K := {0},
J¬F K :=
J⊤K := {1}
(4) (5)
where the operations implement Priest’s Logic of Paradox with the lattice ordering {0} <LP {0, 1} <LP {1} (i.e., F < B < T). 10
4.2
Distributional Semantics
The distributional semantics corresponds to the third row in Table 1, where we use the distribution monad D (Ex. 3) over the classical truth basis {0, 1}, yielding the truth space [0, 1] equipped with the Product algebra (Table 3, row “Product”): x ⊗ y = xy (product t-norm), x ⊕ y = x + y − xy (probabilistic sum), x → y = max(1, y/x) (R-implication), and ¬x = 1 − x. This framework provides the semantic foundation for probabilistic logic programming systems and neural-symbolic approaches that work with probability distributions over truth values. The weighted sum in the computational formula rule below arises from the Kleisli extension of D (cf. Ex. 3). In this setting, computational predicates and function symbols return probability distributions rather than deterministic values. We need to restrict interpretations to finite domains. Finite quantification just iterates conjunction or disjunction. For infinite quantifiers, check section 7.1. J[x := m(T⃗ )]F K :=
X a∈I(sm )
J∃x:s F K := 1 −
JF Kν[x7→a] · ρm (a | T⃗ ),
Y a∈I(s)
(1 − JF Kν[x7→a] ),
JF ∥GK := JF K + JGK − JF K · JGK,
JF → GK := max 1, JGK/JF K ,
J⊥K := 0,
4.3
J⊤K := 1.
where ρm (a | T⃗ ) := I(m)(JT⃗ K)(a)
J∀x:s F K :=
Y a∈I(s)
JF Kν[x7→a]
JF &GK := JF K · JGK
(6) (7) (8)
J¬F K := 1 − JF K
(9) (10)
Finitary LTNp Semantics
The finitary Logic Tensor Networks (LTN) semantics corresponds to the fourth row in Table 1, employing the distribution monad D (Ex. 3) over the classical truth basis {0, 1} with the truth space [0, 1] equipped with the S-Product algebra (Table 3, row “S-Prod.”). This algebra has the same t-norm (x ⊗ y = xy) and t-conorm (x ⊕ y = x + y − xy) as the Product algebra used in the distributional semantics (Sec. 4.2), but uses S-implication x → y = 1 − x + xy (strong implication) instead of R-implication max(1, y/x) (residual implication). Moreover, aggregation differs as well: following Badreddine et al. [2022], quantification is performed using p-norms, where the parameter p controls the "softness" of the logical operations. For existential quantification, we compute the p-norm of truth values, while for universal quantification, we use the dual formulation 1 − ∥1 − ·∥p : J∃x:s F K :=
1
X
|Is | a∈I
J∀x:s F K := 1 −
s
1
p JF Kν[x7 →a]
X
|Is | a∈I
s
1/p
(1 − JF Kν[x7→a] ) p
JF → GK := 1 − JF K + JF K · JGK.
(11)
, 1/p
,
(12) (13)
This is however only possible for finite domains. For the infinite case and additional quantifier variants, we refer to section 7.2.
4.4
Sampling "Semantics"
While Van Krieken et al. [2024] have introduced a sampling semantics, we think that the semantics should define probabilities, while an implementation can work with e.g. Monte Carlo sampling in order to obtain an approximation that is easier to implement (and, in the case of 11
quantification over infinite domains, unavoidable). Hence, we do not discuss sampling semantics here. But we expect that a Monte Carlo convergence theorem can be stated and proved.
5
NeSy Transformations Crossing x
argmax[light(x)] = {•, •, •}
l=•
l=•
l=•
argmax[drive(x, •)] = ×
argmax[drive(x, •)] = {×, ✓}
argmax[drive(x, •)] = ✓
d=× Formula TRUE
d=× Formula FALSE
d=✓ Formula TRUE
d=✓ Formula TRUE
Union of Branches = BOTH
Figure 1: Argmax transformation flowchart for the traffic light example from [Van Krieken et al., 2024], shown for a fixed crossing x. The diagram instantiates only the local non-deterministic evaluation of [l := light(x), d := drive(x, l)](d ̸= ✓, l = •) after the arg max transformation; it does not yet apply the universal quantifier. Since the traffic lights are uniformly distributed, arg max[light(x)] returns all three colours, and in the amber case arg max[drive(x, l)] returns both × and ✓. The LP truth values generated along these branches are collected by the local monadic evaluation, yielding BOTH. If one evaluates the full formula ∀x:Crossing [l := light(x), d := drive(x, l)](d ̸= ✓, l = •), the quantifier only afterwards aggregates these percrossing results over the domain of crossings. The original ULLER paper [Van Krieken et al., 2024] uses a uniform notion of interpretation. This leads to the problem that classical semantics needs to extract values with maximal probability (using arg max) from a distribution, which is not possible if there is a tie10 . Here, we propose an alternative way of dealing with this problem: namely, using a NeSy transformation, we can move e.g. from an interpretation in a probabilistic NeSy framework to one in a classical framework. Dealing with ties can be done using a non-deterministic semantics. Definition 9. A NeSy transformation α : F → F ′ between two NeSy frameworks is a family of functions11 αΣ : IntpF (Σ) → IntpF ′ (Σ). Here, the interpretation function IntpF : Σ 7→ Intp(F , Σ) sends a signature to the set of interpretations on F for that signature. We write α for αΣ if Σ is clear from context. Argmax transformation: From distributional to non-deterministic semantics For a given distributional interpretation I(m) of a computational function symbol m, we can define 10 11
Or in case of an infinite distribution (see section 7.1) For those interested in category theory; this is in fact a natural transformation (App. A), hence the name.
12
a non-deterministic interpretation α(I)(m) of m by defining, where sm is the sort of m, and likewise, M is a computational predicate symbol: α(I)(m) := arg max I(m)(a) ,
α(I)(M ) := arg max I(M )(b) ,
a∈I(sm )
b∈Ω={0,1}
and for all other symbols set α(I) := I. This definition is not possible in the general probabilistic case, because probability measures often return zero on all single values. It is also a non-deterministic interpretation since it returns a set of values instead of a single value. The resulting semantics is three-valued, as in section 4.1, and we apply it to the traffic light example from [Van Krieken et al., 2024] in Fig. 1. There we fix a single crossing x and evaluate the computational part [l := light(x), d := drive(x, l)](d ̸= ✓, l = •): the uniform distribution on light(x) makes the first arg max return all three colours, and the amber branch remains non-deterministic because arg max[drive(x, •)] returns both × and ✓. The local monadic evaluation, via the Kleisli extension for the non-empty powerset monad, then collects both truth values, giving the LP value BOTH. The universal quantifier in the full formula is not used inside the diagram; it would only aggregate these already computed per-crossing values over the domain of crossings. This arg max transformation is just one example of many possible NeSy transformations. Then, in the practical implementation of NeSyCat, one can use random sampling (see section 4.4) over a uniform distribution to obtain a single value from the set of values α(I)(m). This gives a precise foundation for the use of arg max in the classical semantics in Van Krieken et al. [2024].
6
Categorical NeSy Frameworks
So far, in this paper, we have not made use of category theory. Indeed, we have introduced setbased notions of monad and of Double monoid bounded lattice. They do not rely on category theory, nor do the central definitions of NeSyCat, in particular, the notions of NeSy framework, of signature, interpretation and formula, nor the rules of the Tarskian semantics. By contrast, in this and the next section, we will heavily make use of category theory. (The subsequent Sections 8 and 9 implicitly use the results of this section, but do not directly make uses of category theory. Reader not interested in category theory may skip to Section 8.) The main purpose of our use of category theory is the possibility to work with continuous probability distributions.12 Another motivation is the need for quantification structures for infinite domains, which are common in first-order logic. In these cases, we need to work with structured objects and structure-preserving maps, like measurable spaces and measurable functions. Without organising such spaces and maps into a category, we still can use most of the set-theoretic rules of the semantics. However, we would need to restrict to structure-preserving maps in places like the definition of interpretation (Def. 6), and, more severely, would need to prove that the semantic rules in Def. 8 again yield structure-preserving maps. When using category theory, we can avoid such proofs and base our theory on a certain structure that is required for the involved categories. That said, we still can use the set-theoretic semantics rules for convenience, also for categories of sets with structure13 , just because the categorical version of the rules tells us that the resulting maps will be structure-preserving. The only set-theoretic rules of the semantics that we cannot simply re-use are the rules for quantifiers. Here, the aggregation functions aggr∃ and aggr∀ generally need to make use of the extra structure that the “sets with structure” have, see e.g. 12
The lack of which is described as a major shortcoming of traditional NeSy systems by Smet et al. [2023]. Technically, these set-based categories C are constructs in the sense of Adámek et al. [1990], which means they come with a faithful functor U : C → Set. U maps objects of C to their underlying sets. 13
13
the aggregation functions for probabilistic semantics defined in section 7.1 below need to make use of the probability distribution coming with the universe. A brief introduction to category theory is given in Appendix A.
6.1
More (on) Monads
Definition 10. A monad on a category C (in extension system form, cf. the footnote in Def. 3) involves a mapping of objects T : Ob(C) → Ob(C), a family of morphisms ηX : X → T X for each object X in C (called the unit), and a function that assigns to each morphism f : X → T Y a morphism f ∗ : T X → T Y such that the axioms hold as in Def. 3. Note that a set-based monad is then a monad on the category Set. Definition 11 (Strong monad). A monad (T , η, (−)∗ ) on a category C with finite products is called strong if there is a natural transformation SA,B : A × T B −→ T (A × B) satisfying the naturality condition: for any morphisms f : A → A′ and g : B → B ′ , T (f × g) ◦ SA,B = SA′ ,B ′ ◦ (f × T g), and such that SA,B ◦ (idA × ηB ) = ηA×B ,
SA,B ◦ (idA × f ∗ ) = (id × f )∗ ◦ SA,C .
Example 5. Identity monad Id on Set (category of sets and functions). For a set X: Id(X) := X
(identity functor),
f ∗ (x) := f (x)
ηX (x) := x,
f : X → Y, x ∈ X .
The identity monad models deterministic computation with no effects – the baseline case. The Kleisli extension f ∗ (x) = f (x) is just ordinary function application; composition in the Kleisli category reduces to ordinary function composition. In a NeSy setting, this corresponds to classical two-valued logic where neural models return crisp values (e.g., a thresholded classifier emitting exactly one label). Example 6. Powerset monad P on Set (category of sets and functions). For a set X: PX := {A ⊆ X} (powerset of X), ηX (x) := {x},
f ∗ (A) :=
[
f (a)
f : X → PY, A ⊆ X .
a∈A
Unlike the non-empty variant (Ex. 2), the full powerset monad allows the empty set as a valid outcome, representing failure or unsatisfiability. The Kleisli extension works identically – union over mapped elements – but if f returns ∅ for some input, that branch contributes nothing. In a NeSy setting, this models a reasoning system where queries may have no satisfying assignment. Example 7 (Sub-Distribution Monad S). The sub-distribution monad S is similar to the distribution monad D but it allows for finitely supported measures that do not sum up to 1, that means: SX :=
n
ρ : X → [0, 1]
X
o
ρ(x) ≤ 1, ρ countably additive and has finite support ,
x∈X
(
ηX (x) := δx , δx (y) =
1, x = y 0, x ̸= y
f ∗ (ρ)(y) :=
X x∈X
14
ρ(x)f (x)(y)
f : X → SY, ρ ∈ SX .
The sub-distribution monad models probabilistic computation where probability mass can be “lost” (total ≤ 1). The Kleisli extension works like that of D, but the resulting probabilities may sum to less than 1, representing partial failure or absorption. In a NeSy setting, this captures a probabilistic classifier with a rejection option – if no class exceeds a confidence threshold, some probability mass is discarded rather than assigned. Example 8. Giry monad G on Meas, the category of measurable spaces and measurable maps (see Appendix A). For a measurable space (X, ΣX ) and Dirac measure δx on X for x ∈ X: G(X, ΣX ) := ρ : X → [0, 1] ρ(X) = 1, ρ countably additive
(
η(X,ΣX ) (x) := δx , f ∗ (ρ)(A) :=
Z
f (x)(A)dρ(x)
δx (A) =
(prob. measures on X),
1, x ∈ A 0, x ̸∈ A
f : X → GY, A ⊆ Y measurable .
X
δx is the probability distribution that assigns all probability mass to x. Note that the Kleisli category (App. A) Kℓ G is isomorphic to the category Stoch of measurable spaces and Markov kernels, which is a Markov category in the sense of Fritz [2020]; see Section 8.3 for further discussion. The Kleisli extension f ∗ (ρ)(A) = X f (x)(A) dρ(x) computes the probability of the outcome landing in A, averaged over all inputs x weighted by ρ – the continuous analogue of D’s “twolevel random process.” In a NeSy setting, this models e.g. a sensor where the input (temperature, position) is a continuous random variable and the neural model maps it to a probability distribution over outcomes. R
Example 9. Infinite Giry monad G∞ on Meas. For a measurable space (X, ΣX ): G∞ (X, ΣX ) := µ : ΣX → [−∞, ∞] | µ(∅) = 0, µ countably additive ,
1 0
(
η(X,ΣX ) (x) := δx , ∗
f (µ)(A) :=
Z X
f (x)(A) dµ(x)
δx (A) =
x∈A , x∈ /A
f : X → SY, A ⊆ Y measurable .
Here the integral is the Lebesgue–Stieltjes integral with respect to the extended signed measure µ. Writing the Jordan decomposition µ = µ+ − µ− and using linearity of the integral, one checks that the monad laws hold; thus S extends the Giry monad by allowing negative and (possibly) infinite total mass. This monad generalises G by allowing signed and infinite measures, which is primarily a theoretical extension. It is needed for certain mathematical constructions (e.g., characteristic functions, reward/penalty signals in reinforcement-learning-style objectives) and as an intermediate step in proofs involving measure-theoretic arguments. Proposition 2 (and definition of the measure-space monad M). We can define a measure monad M as a monad (T , η, µ)14 on the category Measr of measure spaces (see Appendix A for the distinction between Meas and Measr) with η, µ being the unit and multiplication of the Giry monad G on Meas. For ρ being probability measures, we can define a probability-space 14
Here we use the multiplication form of a monad (T , η, µ), where µ is monad multiplication; see the footnote in Def. 3 for the equivalence of presentations.
15
monad O on the category Prob of probability spaces (Appendix A). The same construction can be applied to obtain an infinite measure-space monad M∞ on Measr. M((X, ρ)) := (G(X), ρη ), ρη := B 7−→ ρ(η −1 (B)), for B ⊆ G(X) measurable, η M := η,
µM := µ.
Proof. If ρ is a probability measure, we know that ρη (G(X)) = ρ(η −1 (G(X))) = ρ(X) = 1, countable additivity follows alike. The measure-space monad M models probability on spaces that already carry their own measure – this is needed when quantifiers use sort-dependent measures (cf. Table 6, column +DQ). In a NeSy setting, this arises when the domain of discourse (e.g., images, sensor readings) comes equipped with a data distribution, and universal or existential quantification integrates against that distribution.
6.2
The 2Mon-BLat Algebra: A Comprehensive Overview
In this subsection, we provide a comprehensive overview of the different algebraic structures that can serve as algebras on the truth space T Ω in our neurosymbolic framework, along with their associated operations types and logical properties. Table 3 provides a comprehensive comparison of the fundamental operations across different algebraic structures, showing how each algebra defines its basic operations. Table 3: Overview of aggregated 2Mon-BLat Algebra Boolean LTNp LTNq Product S-Prod. Priest
Set {0, 1} [0, 1] [0, 1] [0, 1] [0, 1] {F, B, T }
⊥ 0 0 0 0 0 F
⊤ 1 1 1 1 1 T
⊕ max SP SP SP SP max
⊗ min TP TP TP TP min
→ IB ISP ISP IP ISP IKD
t-conorms and t-norms (⊕ and ⊗, App. A): • SP (Probabilistic sum): xSP y = x + y − xy • TP (Product): xTP y = xy Implications (→): (
• IP (Product/Goguen): IP (x, y) = (
• IB (Boolean): IB (x, y) =
0 1
1 y/x
if x ≤ y otherwise
if x = 1, y = 0 otherwise
• IS (General S-implication): IS (x, y) = ¬x ⊕ y • IKD (Kleene-Dienes/Material): IKD (x, y) = max(1 − x, y) • ISP (S-Product): ISP (x, y) = 1 − x + xy 16
¬ ¬R ¬C ¬C ¬R ¬C ¬C
aggr∃ sup ∥·∥p P ∃q P∃ P∃ sup
Negations (¬): • ¬R (Residual): ¬R x = x → 0 (includes Heyting/intuitionistic negation) • ¬C (Classical/1-Involutive): ¬C x = 1 − x • ¬V (0-Involutive): ¬V x = 0 − x = −x Aggregations (aggr∃ ): h
i
• P ∃ (Infinitary Probabilistic Sum): P ∃(x) = 1 − exp Ea∼µ ln(1 − JF Kν[x7→a] )
h
q i 1q
• P ∃q ((µ, q)-approximated P ∃): P ∃q (x) = 1 − exp Ea∼µ ln 1 − JF Kν[x7→a] for 1/2 ≤ q ≤ 1, with P ∃q → P ∃ as q → 1. Here µ can be any measure and it depends on the context, in LTNq it depends on the measure space of the sort of the quantified variable at hand. The quantification aggregations employ logarithmic and exponential transforms because they provide the natural generalisation of the product (or probabilistic sum) to infinitary domains. While finite probabilistic sums can be computed directly using products, extending to infinite domains requires the use of expectations, and the logarithmic and exponential transforms enable this generalisation while preserving the essential structure of probabilistic aggregation.
6.3
Definition of Categorical NeSy Frameworks
Definition 12. Definition 13. An aggr-2Mon-BLat internal to a category with finite products C on an object A in C consists of a lattice on A internal15 to C, morphisms ⊕, ⊗, →: A × A → A; ⊥, ⊤, 0, 1 : 1C → A and for any objects B and C maps aggr∀B,C , aggr∃B,C : C(B×C, A) → C(B, A), such that the axioms of Def. 1 hold when appropriately interpreted in C 16 . Note that our categorical handling of aggregation differs from that in the set-theoretic setting. A full analogy to the set-theoretic case would require aggregation morphisms AX → A, which would need a Cartesian closed category. This requirement seems too strong for our purposes, since it is not met in many examples and only is required for interpreting higher-order logics. However, given a Cartesian closed category (like Set) with aggregation aggr : AX → A, Λ(f )
aggr
we can define aggregation in the sense of Def. 12 as mapping f : B ×C → A to B → AC → A. Here, Λ(f ) is currying, defined as follows in Set: Λ(f )(x)(y) = f (x, y). In the sequel, we will rely on this definition also for Set-based categories (constructs [Adámek et al., 1990]) that are not Cartesian closed, noting that the definition works even if AC is just a set and not an object in the category. Hence, in examples, we will define aggregation mostly as in Def. 1, but in some cases, we make use of the structure of the object C. Definition 14. A NeSy framework (T , R) consists of 1. a strong monad T with strength S on a category with finite products C,17 2. an aggr-2Mon-BLat R in C on T Ω for some object Ω. Here, Ω is a set acting as truth basis,18 and T Ω is the monadic space of truth values.
17
Table 4: NeSy Framework Examples (categorical) Logic/Theory
C
T
Ω
TΩ
R
Sem.
Simple Prob. Standard Borel Probabilistic Infinitary LTNp STLr
Meas BorelMeas Measr Prob Measr
Giry G Giry G|BorelMeas Measr-space M Prob-space O ∞-Measr-space M∞
{0, 1} {0, 1} {0, 1} {0, 1} {1}
[0, 1] [0, 1] [0, 1] [0, 1] R
Product BL–Alg. Product BL–Alg. Product BL–Alg. Product SBL-Alg. approx. R
§7.1 §7.1 §7.1 §7.2 §7.3
Examples are given in Table 4 and their semantics are discussed in section 7. Note that further examples arise by varying the 2Mon-BLat R on [0, 1].
7
Categorical Semantics
The categorical notion of interpretation differs from the set-theoretic definition (Definition 6) only in that sets are replaced by objects in the category C and functions are replaced by morphisms in C. This generalisation allows the framework to work in any category with suitable structure, not just the category of sets and functions. In particular, I(s) is now an object in C, and consequently idI(s) is the identity morphism on that object in C (not in Set). In the set-theoretic case, C = Set, so the two notions coincide; in the categorical case, e.g. C = Meas, I(s) is a measurable space and idI(s) is the identity measurable function. Definition 15 (Tarskian semantics J·K of formulas). Given a NeSy framework (T , R) and a NeSy interpretation I we can determine the interpretation morphisms: Formulas: JF KI : VF → T Ω,
Terms: JT KI : VT → I(sT ) :
Remark 1. We define VT := x:t∈ΓT I(t). Here ΓT is the context of T and sT is the (unique) Q sort of the term T . Analogously VF := x:t∈ΓF I(t). Note that if T1 is a subterm of T2 , there is a projection πT1 ,T2 : VT2 → VT1 , and analogously for formulas. T⃗ stands for T1 , . . . , Tn . Moreover, ⟨JT⃗ Ki ◦ πi ⟩i = ⟨JT1 K ◦ π1 , . . . , JTn K ◦ πn ⟩ and JT⃗ K = (JT1 K, . . . , JTn K). The categorical semantics ensures that all involved and resulting functions are morphisms in C, i.e. are measurable in case that C = Meas, etc. With a purely set-theoretic semantics, we would need to prove measurability (or other properties) separately for each NeSy framework. That said, besides the general categorical case, 19 for better understandability, we also translate the equations to their meaning in the category of sets. We work with variable valuations ν ∈ VT Q (and ν ∈ VF ), noting that elements of x:t∈ΓT I(t) map variables x : t to values in I(t). We write JT KI,ν = JT KI (ν) and JF KI,ν = JF KI (ν). That said, we mostly omit I and ν if clear from the context. Q
7.1
Probabilistic Semantics
Definition 16. A probabilistic NeSy framework is a tuple (T , R) with T = M the Giry monad (Ex. 8) on the category Measr of measure spaces and R a suitable 2Mon-BLat, typically 15
For an explanation check https://ncatlab.org/nlab/show/internalization and https://ncatlab.org/ nlab/show/monoid+in+a+monoidal+category, since this is out of scope for this paper. 16 1C is a terminal object. 17 Note that Set is a Cartesian closed category (App. A), and every monad on Set is strong. 18 Similar to the basis of a vector space. 19 Logician’s note: We don’t differentiate properly between additive and multiplicative connectives/units/quantifiers for an easier presentation coherent with the NeSy literature. However, this could easily be adapted to obtain something like Girard’s linear logic [Girard, 1995], following the Zeitgeist of his transcendental syntax.
18
Table 5: Inductive definition of the Tarskian semantics Syntax
Categorical Semantics J·KI
Set Semantics J·KI,ν
idI(s) I(c) I(prop) ◦ JT K I(f ) ◦ ⟨JT⃗ Ki ◦πi ⟩i
νs (x) I(c) I(prop)(JT K) I(f ) JT⃗ K
Terms Jx : sK JcK JT.propK Jf (T⃗ )K
Atomic formulas JP K JN K JR(T⃗ )K JM (T⃗ )K
ηΩ ◦ I(P ) I(N ) ηΩ ◦ I(R) ◦ ⟨JT⃗ Ki ◦πi ⟩i I(M ) ◦ ⟨JT⃗ Ki ◦πi ⟩i
ηΩ (I(P )) I(N ) ηΩ I(R)(JT⃗ K) I(M ) JT⃗ K
Compound formulas 1R , 0R
1R , 0R
J¬F K
¬R ◦ JF K
¬R (JF K)
JF ∥GK
⊕R ◦⟨JF K◦πF , JGK◦πG ⟩
JF K ⊕R JGK
J⊤K, J⊥K JF → GK JF &GK J∃x:s F K J∀x:s F K
J[x := m(T⃗ )]F K
→R ◦⟨JF K◦πF , JGK◦πG ⟩
JF K →R JGK
⊗R ◦⟨JF K◦πF , JGK◦πG ⟩
JF K ⊗R JGK
aggr∃VF \x:s ,I(s)(JF K)
aggr∃I(s) (λa.JF Kν[x7→a] )
JF K∗ ◦S ◦ πVF \x:s , I(m) ◦ ⟨JT⃗ Ki ◦πi ⟩i
do a ← I(m)(JT⃗ K); JF Kν[x7→a]
aggr∀VF \x:s ,I(s)(JF K)
aggr∀I(s) (λa.JF Kν[x7→a] )
the Product algebra on [0, 1] (Table 3, row “Product”; see Sec. 6.2 for the full overview of algebras). The integral in the computational formula rule below is the continuous analogue of the weighted sum in the distributional semantics (Sec. 4.2) and arises from the Kleisli extension of M. The interpretation of a function f of arity n is a Markov kernel (App. A), which is a measurable q map X → − M(Y ) where M denotes the measure monad on the category Measr of measure spaces (Appendix A). Our definition of a probabilistic semantics largely follows that in the original ULLER paper [Van Krieken et al., 2024]. A central design decision of ULLER is the use of first-order interpretations and the use of probability distributions to interpret computational function symbols. This means that ULLER (and therefore also NeSyCat) is (like Logic Tensor Networks) not built on weighted model counting, i.e. on probability distributions over the set of interpretations. That said, it is still possible to capture certain aspects of weighted model counting in ULLER and NeSyCat, as we will see in section 7.4 below. Connectives in the probabilistic semantics of ULLER are interpreted assuming independence of probabilities for atomic formulas. Hence, our distributional semantics can be seen as a special case of a fuzzy semantics, where the t-norm is the probabilistic product and the t-conorm is the probabilistic sum. This means that we can use the same equations as in the fuzzy semantics (and as in LTNs), but with a different motivation. Moreover, this explains why there is no 19
essential difference between these probabilistic and fuzzy semantics. Let us derive from our general semantic in definition 8 the interpretation of monadic formulas in probabilistic semantics. For the probabilistic NeSy framework, we define the aggregation morphisms aggr∀B,C , aggr∃B,C required by Def. 12 as follows: for any measure spaces B and C, aggr∀B,C (f ) := exp ◦ Ec∼µC [ln ◦f (·, c)] aggr∃B,C (f ) := 1 − exp ◦ Ec∼µC [1 − ln ◦f (·, c)] where f : B × C → [0, 1] and µC is the measure on C. In the following examples, we provide implicit definitions of these aggregation operations through their concrete realisations. In settheoretic notation, the semantics of computational formulas can be written as, where we use the notation ρm (·|T⃗ ) := I(m)(JT⃗ K): J[x := m(T⃗ )]F K = do a ← I(m)(JT⃗ K); JF Kν[x7→a] =
Z
=
Z
a∈I(sm )
a∈I(sm )
JF Kν[x7→a] dI(m)(JT⃗ K)(a)
JF Kν[x7→a] dρm (a|T⃗ )
= Ea∼ρm (·|T⃗ ) JF Kν[x7→a]
=
X
a∈I(sm )
JF Kν[x7→a] · ρm (a|T⃗ )
(if I(sm ) is finite)
We evaluate in the Product Algebra to obtain, where µs is the measure given by the measure space of I(s) J[x := m(T⃗ )]F K = Ea∼ρm (·|T⃗ ) JF Kν[x7→a]
(14)
J∃x:s F K = 1 − exp Ea∼µs ln 1 − JF Kν[x7→a]
J∀x:s F K = exp Ea∼µs lnJF Kν[x7→a]
JF &GK = JF K · JGK,
(17)
J¬F K = 1 − JF K
J⊥K = 0,
(16)
JF ∥GK = JF K + JGK − JF K · JGK,
JF → GK = max 1, JGK/JF K ,
(15)
J⊤K = 1.
(18) (19)
∀ as weighted products (finite case). Let I(s) be finite and define the random variable X(a) := JF Kν[x7→a] . The infinitary probabilistic ∀ (Eq. (16)) evaluated on F with a weighted counting measure on X yields X
J∀x:s F K = exp
wa ln X(a)
=
Y
a∈I(s)
exp(ln(X(a)wa ))
a∈I(s)
=
Y
X(a)wa .
a∈I(s)
By contrast, the finite product aggregator of the original ULLER semantics is obtained by setting wa = 1 for all a ∈ I(s): J∀x:s F K =
Y
X(a)1 .
a∈I(s)
However, our definition of the ∀ quantifier is more general even in the finite case, as it allows for meaningful examples like the weighted counting measure on I(s) yielding the geometric mean with n := #I(s), the number of elements in I(s), yielding J∀x:s F K =
n Y i=1
20
X(ai )1/n .
In the case above of the geometric mean and also in many other (continuous) cases, one actually does choose only one universal quantifier to be constant on all sorts, as for the existential quantifier. In this case one can actually work within a simpler framework using the normal Giry monad on the category Meas of measurable spaces: Definition 17. A simple probabilistic NeSy framework is a tuple (T , R) with T = M the Giry monad on the category Meas of measurable spaces and Ω the truth basis, normally Ω = {0, 1}. Now, if one works in standard Borel spaces20 (as one most often does in practice), one obtains an even more practical version of this simple probabilistic NeSy framework. This is very useful in practice since one can see an uncountable standard Borel space just as a set that is canonically equipped with the Borel sigma-algebra and Lebesgue measure. Also a finite or countable standard Borel space can be seen as a set that is canonically equipped with the discrete sigma-algebra and counting measure. Definition 18. A simple standard Borel NeSy framework is a tuple (T , R) with T = M the Giry monad on the category BorelMeas of standard Borel spaces and Ω the truth basis, normally Ω = {0, 1}. Additionally, if one chooses the measures for universal and existential quantification to be given by a density functions f (most often the case in practice), one obtains an implementationfriendly Lebesgue-probabilistic NeSy semantics for the quantifiers ∀ and ∃: J∀x:s F K = exp
Z a∈I(s)
J∃x:s F K = 1 − exp
lnJF Kν[x7→a] f (a) da
Z a∈I(s)
ln(1 − JF Kν[x7→a] ) f (a) da
(20) (21)
In the same spirit, if the semantics of the monadic formula 14 should only use probability measures admitting a density w.r.t. the Lebesgue measure21 , one can work with a simplified Giry monad on the category BorelMeas, sending a standard Borel space to the standard Borel space of probability measures on that space admitting a density w.r.t. the Lebesgue measure. Combined with the quantifiers defined w.r.t Lebesgue densities from eq. (20) and eq. (21), this makes the implementation simpler and more efficient and is the default choice in practice anyway. Actually, depending on the use case, one might want to use a probability monad on one of the following categories22 , listed in increasing complexity in Table 6 summarising typical suitability. The symbols ✓, ◦, and × indicate whether a given category is the simplest adequate choice (✓), technically compatible but unnecessarily complex or not the canonical setting (◦), or incompatible (×) for probability measures of the kind indicated by the column. For example, finitely supported distributions can be defined on Meas, but the measurable structure adds nothing over plain Set, hence the ◦; conversely, sort-dependent quantifiers require a measure on each sort, which is only available in Measr or Prob (not in Meas or Set), hence the × in those 20
Standard Borel spaces are measurable spaces where the underlying set is isomorphic to R or is finite or countable. All finite powers of the real line and all intervals, as measurable spaces, are isomorphic to the real line, as explained at https://ncatlab.org/nlab/show/standard+Borel+space. Also a measure space (or probability space) is called a standard Borel measure space (BorelMeas) (standard Borel probability space (BorelProb)) if and only if its underlying measurable space is standard Borel as above. 21 This is hidden in the notation of the semantics of the monadic formula in the original ULLER semantics in [Van Krieken et al., 2024], Eq. 20; although there the density is mistakenly confused with the corresponding measure. 22 Which are by far not all, see https://ncatlab.org/nlab/show/monads+of+probability,+measures,+and+ valuations for more examples.
21
Table 6: Suitability of base categories and their probability monads (see Appendix A for definitions of these categories and the distinction between them) Category
Monad
FS
Finite
∼ =Z
∼R =
+DQ
+DPQ
+HO
Set BorelMeas BorelMeasr BorelProb Meas Measr Prob QBS
D (Ex. 3) G|Borel M|Borel O|Borel G (Ex. 8) M (Prop. 2) O (Prop. 2) P (Def. 21)
✓ ◦ ◦ ◦ ◦ ◦ ◦ ◦
✓ ◦ ◦ ◦ ◦ ◦ ◦ ◦
✓ ✓ ◦ ◦ ✓ ◦ ◦ ✓
✓ ✓ ◦ ◦ ✓ ◦ ◦ ✓
× × ✓ ◦ × ✓ ◦ ×
× × ◦ ✓ × ◦ ✓ ×
✓ × × × × × × ✓
cells. The Borel variants restrict to standard Borel spaces, which simplifies measure theory at the cost of excluding exotic spaces. The column abbreviations are: “FS” = finitely supported probability measures, “Finite” = probability measures on finite spaces, “∼ = Z” = on countable (discrete) spaces, “∼ = R” = on uncountable (continuous) spaces, “+DQ” = sort-dependent quantifiers via measures, “+DPQ” = sort-dependent quantifiers via probability measures, and “+HO” = higher-order logic (requires a Cartesian closed category). Notably, QBS (quasi-Borel spaces, Def. 21) [Heunen et al., 2017] is the only category in the table that supports both continuous distributions and higherorder logic, since it is Cartesian closed and carries a probability monad that agrees with the Giry monad on standard Borel spaces. This has made QBS the preferred semantic foundation for higher-order probabilistic programming languages [Staton et al., 2016, Vakar et al., 2019, Ścibior et al., 2018]; see Section 8.3 for details.
7.2
Infinitary LTNp Semantics
Definition 19. A LTN-like NeSy framework is a tuple (T , R) with T = O the probability monad on the category Prob of probability spaces and Ω the truth basis, normally Ω = {0, 1}, and R a suitable 2Mon-BLat, typically the S-Product algebra (Table 3, row “S-Prod.”) as in [Badreddine et al., 2022]. This is the infinitary generalisation of the finitary LTN semantics from Sec. 4.3. Setting Stable product real logic of Logic Tensor Networks [Badreddine et al., 2022] uses p-means for finite quantification. However, since domains are generally infinite, we also need to aggregate infinite many truth–scores (xi )i∈I ⊆ [0, 1]. The power–mean extends from the finite case to an integral form that is well defined whenever the data are Lp -integrable. Let (X, A, ρ) Z
be a probability space and f : X → [0, 1] ⊆ R a measurable map with
X
f dρ ≤ 1. Because
0 ≤ f ≤ 1, one automatically has f ∈ Lp (ρ) for every real p, so p-means are always defined. This bounded–by–one assumption reflects the fact that in our logical reading a truth-score never exceeds 1. Integral p-Mean Quantifiers The idea behind p-mean aggregation is that the hyperparameter p acts as a strictness dial: for small p the quantifier behaves like an average, tolerating a few low truth-scores among many high ones, while for p → ∞ it converges to the supremum (for ∃) or infimum (for ∀), enforcing a strictly logical reading. In a learning setting one typically anneals p upward during training, starting with a smooth, gradient-friendly landscape and gradually tightening toward classical logic. The infinitary LTNp semantics is a modification of the probabilistic semantics, which is motivated by replacing the quantifiers in equation (15) and (16). We generalise this: by working 22
in the category Prob, for any sort s we have to provide a probability measure ρs on I(s). This enables us to obtain p-means for infinite23 domains: Mp (a1 , . . . , an ) :=
n 1 X
n i=1
aip
1/p
Z
Mp (f ; ρs ) :=
,
x∈X
f (x)p dρs (x)
1
Q
n
1/p
,
(22)
n and these extend to M0 (a1 , . . . , an ) := and M0 (f ; ρs ) := exp ln f dρs . For p → ∞ i=1 ai we recover the supremum. Take X = {1, . . . , N } with counting measure 1/N , then Mp (f ; ρs ) reduces to Mp (a1 , . . . , an ) or choose weights wi summing up to 1 for i = 1, . . . , N to obtain the weighted p-mean. The aggregated 2Mon-BLat is similar to the probabilistic one, except for the Reichenbach implication as implication and the following aggregation functions. For a hyperparameter 1 ≤ p < ∞ of LTNp , let aggr∃I(s) (f ) := Mp (f ; ρs ) and aggr∀I(s) (f ) := 1 − Mp (λx.f (1 − x); ρs ). As a result, equation (22) now becomes:
J∃x:s F K =
R
Z a∈I(s)
JF Kν[x7→a]
p
dρs (a)
1/p
.
As in Badreddine et al. [2022], this is for 1 ≤ p < ∞, where for p → ∞ we recover the supremum. Log-Power q-Mean Quantifiers The p-mean quantifiers above are tied to the Łukasiewicz or Reichenbach style of combining truth values additively. A different, arguably more natural, choice for a product-based real logic is to aggregate multiplicatively: universal quantification should behave like an infinite conjunction under the (Goguen) product t-norm, i.e. like a (possibly weighted) geometric mean. The logarithm converts this product into a sum, so the natural “p-mean in log-space” is a power mean applied to lnJF K rather than to JF K itself. This motivates the following alternative pair of quantifiers with 1/2 ≤ q ≤ 1, where for q → 1 the universal quantifier converges to the product mean (geometric mean), while the existential quantifier converges to the probabilistic sum: J∀x:s F K := exp
Z a∈I(s)
lnJF Kν[x7→a]
q
dρs (a)
1/q
,
J∃x:s F K := J¬∀x:s ¬F K.
A subtle but important design choice concerns the probability measure used inside the integrals: should it be attached to the sort s (i.e. to the domain of quantification) or to the individual variable x? We opt for the former. Hence, our probability measure ρs depend on the sort s of the variable x in the quantifier, since it is given by the probability measure of the probability space of I(s). This stands in contrast to Ślusarz et al. [2023], where the probability measure depends directly on the variable x. Lebesgue-Density Variants In many practical settings the domain I(s) is a subset of Rn and the probability measure ρs admits a density with respect to the Lebesgue measure. Working with a density function f directly is often more convenient for implementation: one replaces dρs by f (a) da and can leverage standard numerical integration or Monte-Carlo sampling. Just as in the case of the simple probabilistic NeSy framework, one can also work with a simple Lebesgue 23
Logic Tensor Networks [Badreddine et al., 2022] were originally designed for finite domains only: all variables are mapped to finite sequences of real numbers, bypassing the notion of random variables and probability distributions entirely. Ślusarz et al. [2023] criticise this limitation, arguing that a differentiable logic must account for the unknown probability distribution from which the training data is sampled (see [Ślusarz et al., 2023, Sec. 4]). While this criticism is justified for the original LTN formulation, the infinitary LTNp semantics we define here shows that LTN’s p-norm quantifiers can be extended to infinite (and continuous) domains by replacing finite sums with integrals against a probability measure ρs . This extension is our contribution, not part of the original LTN.
23
NeSy framework, and choose the measures for universal and existential quantification to be given by a Lebesgue-density function f to obtain. for the case of log-power q-mean quantifiers: J∀x:s F K := exp
Z
q
a∈I(s)
lnJF Kν[x7→a] f (a) da
1/q
,
J∃x:s F K := J¬∀x:s ¬F K,
or in the case of the integral p-mean quantifiers originally used by LTNs: J∃x:s F K =
7.3
Z
p
a∈I(s)
JF Kν[x7→a] f (a) da
1/p
,
J∀x:s F K := J¬∃x:s ¬F K.
Infinitary STL Semantics
Signal Temporal Logic (STL) is a temporal logic for expressing properties of signals. STL is particularly useful for modelling and analysing the temporal aspects of real-time systems, such as the timing and sequencing of events. In the semantics of the original STL, we do not have any implication connective, nor neutral elements. We still need to interpret the syntactic implication connective as some form of semantical implication and the syntactic ⊥ and ⊤ as −∞ and ∞, the latter as in Ślusarz et al. [2023]. Also keep in mind, that this does not touch the truth designations of −∞ as absolute falsity and ∞ as absolute truth. That is, STL works with these degrees of truth and falsity, which could be taken together to form one single degree (of probability), and which the absolute degrees are infinite. Therefore we model STL with a truth basis containing only one element: {1}, a basis element which is then scaled by to form the extended real numbers as truth space. A consequence of this that there are no meaningful non-computational predicates in STL. What also can not be ignored is that STL does not directly uses a 2Mon-BLat, but only approximates one. It works within the normal extended real numbers algebra (R̃, max, min, +, ∗) and then goes on to approximate the min and max operations. The are many different ways to do this, but one of the most recent ones is to use the Ar and Or operators as defined in Varnai and Dimarogonas [2020]. Additionally, STL is not concerned with the operations ⊗ and ⊕ of the 2Mon-BLat, these are not used in the semantics of STL, and are just kept to be the standard operations +, ∗ of the extended real numbers algebra. For these reasons, in order to faithfully model STL, in a way that makes it comparable to other semantics, we would need to extend our syntax and semantics, and we would also need to allow to approximate 2Mon-BLats. This however, is out of scope for this paper, and will be discussed in a future work, and yet we still give a first sketch: J[x := m(T⃗ )]F K := Ea∼µm (·|T⃗ ) JF Kν[x7→a]
J∃x:s F K := Ora∈I(s) JF Kν[x7→a] ,
JF ∥GK := Or (JF K, JGK),
(23)
J∀x:s F K := Ara∈I(s) JF Kν[x7→a] ,
JF &GK := Ar (JF K, JGK)
JF → GK := J¬F ∥GK = O(−JF K, JGK), J⊥K := −∞,
J⊤K := ∞.
J¬F K := −JF K
(24) (25) (26) (27)
The STL robustness metrics are defined as in Ślusarz et al. [2023] and originally in Varnai and Dimarogonas [2020]: P amin eã erã aP rã P a e −rã Ara∈M (a) = Pa ae e−rã a
0
24
if amin < 0 if amin > 0 if amin = 0
r min where r ∈ R+ (constant), amin = mina∈M (a), and ã = a−a amin . A is an approximation of the min operation, and for r → ∞ it converges to it. Therefore, its notation is similar to the notation of the min operation, with Arb∈N (f (b)) := Ar (im(f )) := Ara∈im(f ) (a). The operator Ora∈M is defined as −Ara∈M (−a).24 For infinite domains, the minimum is replaced by the infimum R P inf a∈M (a), and the summations a∈M are replaced by integrals a∈M dµs (a), where µs is the measure given by the measure space of I(s).
7.4
Weighted Model Counting and Weighted Model Integration
The purpose of this subsection is not to introduce new semantics, but to demonstrate that NeSyCat’s monadic do-notation is expressive enough to recover weighted model counting (WMC) and weighted model integration (WMI) as special cases. This shows that the move to monadic semantics does not lose any expressiveness compared to the original ULLER formulation; rather, the do-notation provides a uniform syntax for iterated monadic binding that naturally captures the nested summations (or integrations) characteristic of WMC/WMI. ULLER can model certain aspects of WMC in a probabilistic semantics. However, instead of summing up literal or model weights, one needs to sum up weights of variable valuations. In the case of ULLER [Van Krieken et al., 2024], we have the following definition. Given an interpretation I and a formula F that is classical (i.e. without computational symbols) with context ΓF := {x1 : s1 , . . . , xn : sn }, the domains of the variables are given by I(s1 ), . . . , I(sn )25 . This yields the weighted model count (WMC) as follows: WMC(F, w) =
X ⃗a∈I(s1 )×···×I(sn )
=
X
X
···
a1 ∈I(s1 )
w(⃗a)JF Kν[x1 7→a1 , ..., xn 7→an ]
an ∈I(sn )
w(a1 , . . . , an ) JF Kν[x1 7→a1 , ..., xn 7→an ]
If the weight function factorises, i.e. the random variables x1 , . . . , xn are assumed independent26 —then for every assignment (a1 , . . . , an ) ∈ I(s1 ) × · · · × I(sn ): w(a1 , . . . , an ) =
n Y
ρfi (ai ).
i=1
Consequently, the weighted model count becomes WMC(F, f1 , . . . , fn ) =
X
X
···
a1 ∈I(s1 )
Y n
an ∈I(sn ) i=1
ρfi (ai ) JF Kν[x1 7→a1 ,...,xn 7→an ] .
This WMC can be expressed in the language of NeSy systems as follows [Van Krieken et al., 2024, p. 234]: [x1 := f1 (), . . . , xn := fn ()]F In the linearly dependent case, rewrite it via the chain rule, w(a1 , . . . , an ) =
n Y
ρfi ai | a1 , . . . , ai−1 ,
i=1
to make the conditional dependencies explicit. In this case, the WMC becomes X a1 ∈I(s1 )
···
X
Y n
ρfi ai | a1 , . . . , ai−1
an ∈I(sn ) i=1
JF Kν[x1 7→a1 ,...,xn 7→an ] .
In the continuous case we obtain weighted model integration27 (WMI) as follows: 24
See Varnai and Dimarogonas [2020] for details. In the original ULLER paper these were written as Ω1 := I(s1 ), . . . , Ωn := I(sn ). 26 As in [Van Krieken et al., 2024, p. 16]. 27 Compare with [Morettin et al., 2017].
25
25
Z
···
a1 ∈I(s1 )
Z
JF Kν[x1 7→a1 ,...,xn 7→an ] dρfn an | a1 , . . . , an−1 · · · dρf1 a1
an ∈I(sn )
Finally, we can also express even more general dependencies than linear ones. Given any Bayesian network with a set of variables x1 , . . . , xn , we can express this in ULLER as follows: X a1 ∈I(s1 )
···
X
Y n
ρfi ai | parents(ai )
an ∈I(sn ) i=1
JF Kν[x1 7→a1 ,...,xn 7→an ] .
and in ULLER, this is expressed as (assuming that the xi are topologically ordered, i.e. xi can only a parent of xj if i < j): [x1 := f1 (), x2 := f2 (parents(x2 )), . . . , xn := fn (parents(xn ))]F. In each of the above cases – independent, linearly dependent, Bayesian, and continuous – the nested sums or integrals arise from iterating the monadic do-notation [xi := fi (·)], which unfolds via the Kleisli extension of the distribution or Giry monad. The contribution of NeSyCat here is not a new derivation of WMC/WMI, but rather the demonstration that the monadic framework subsumes these constructions: the do-notation provides a single, compositional syntax from which WMC, WMI, and Bayesian factorisations all emerge as instances of iterated monadic binding.
8
Related Work and Their Examples
Monad-based dynamic logic [Mossakowski et al., 2010] is similar to our approach, but differs in some important aspects. In Mossakowski et al. [2010], not the whole of T Ω is used as the space of truth values, but only a subset of it, namely the pure computations p with truth-valued result. These are discardible, i.e. they can be left out in a sequence of computations, and copyable, i.e. deterministic. The latter means that [x := p, y := p]x = y holds. In the non-empty powerset monad, the distribution and the Giry monads, all computations are discardible, but only those in the image of η are copyable. That is, only T and F (in the non-empty non-determinism monad) and δT and δF (in the distribution and Giry monads) are copyable. However, in the nondeterminism monad, we clearly want B ≡ {T, F } as a truth value, and in the distribution and the Giry monads, we want all probabilities [0, 1] as a truth values (and this space is isomorphic to probability distributions over {T, F }). Hence, we do not want a copyability assumption in our semantics. It seems that this is common in monads used for knowledge representation, as opposed to monads used for programming language semantics as in Mossakowski et al. [2010]. Note that both views may even be useful for one and the same monad (e.g. the non-empty powerset monad), depending on its use.
8.1
Example: Weather Prediction of DeepSeaProbLog
As an illustration of how existing neurosymbolic systems using continuous probability distributions28 can be expressed in NeSyCat, using the Giry monad on Borel measurable spaces with probailstic semantics (see section 7.1). Consider the following weather prediction example from DeepSeaProbLog [Smet et al., 2023]. The original DeepSeaProbLog program uses neural distributional facts to model humidity detection and temperature prediction: humid(Data) ~ bernoulli(humid_detector(Data)). temp(Data, T) ~ normal(temperature_predictor(Data)). 28
Note that a proper treatment of these requires category theory, see sections 6.1 and 6.
26
good_weather(Data) :- humid(Data) =:= 1, temp(Data) < 0. good_weather(Data) :- humid(Data) =:= 0, temp(Data) > 15. query(good_weather(world)). Here, humid_detector and temperature_predictor output distribution parameters, while world represents a specific dataset. In NeSyCat syntax, this last query becomes the following formula (later denoted by F ) with world := I(data1 ): [h := bernoulli(humid_detector(data1 ))] [t := normal(temperature_predictor(data1 ))] (h = 1 ∧ t < 0) ∨ (h = 0 ∧ t > 15) where humid_detector is a function returning parameters for a Bernoulli distribution, and temperature_predictor returns parameters (µ, σ) for a normal distribution.29 The nested monadic assignments capture the same probabilistic dependencies as the original program, demonstrating how NeSyCat’s uniform syntax can express diverse neurosymbolic paradigms. The semantic evaluation JF KI,ν of this formula yields the probability distribution over truth values, corresponding to the query result in DeepSeaProbLog. DeepSeaProbLog semantics vs NeSyCat (same query).
Given the signature
W orlds, U nit_Interval, Reals2 , Reals ∈ Σ, data1 ∈ Const humid_detector, temperature_predictor ∈ Func Bernoulli, N ormal ∈ mFunc, define the interpretation function world := I(data1 ) ∈ W orlds := I(W orlds) I(temperature_predictor) : W orlds → R2 ,
I(humid_detector) : W orlds → [0, 1];
N := I(N ormal) : R → G(R),
B := I(Bernoulli) : [0, 1] → G({0, 1}).
2
and label (µ, σ) = I(temperature_predictor)(world),
p = I(humid_detector)(world);
T ∼ N (µ, σ 2 ),
H ∼ B(p).
Then define events A := {H = 1, T < 0} and B := {H = 0, T > 15} (disjoint). DeepSeaProbLog assigns the query probability as an expectation of an indicator under the joint measure (here product measure by independence of PCFs): PDSP (good_weather) = E[1A + 1B ] = p
Z R
Z
1(t < 0) φµ,σ (t) dt + (1 − p)
R
1(t > 15) φµ,σ (t) dt,
29 In Smet et al. [2023] the humid_detector returns a probability distribution over [0, 1] and temperature_predictor returns a probability distribution over R2 , that is that they are also monadic functions, that are composed in the Kleisli category with the monadic functions Bernoulli and Normal, respectively. For simplicity of presentation, we do not explicitly mention this in the syntax and assume they are just deterministic functions.
27
1 (t − µ)2 where φµ,σ (t) := √ exp − is the normal density. In NeSyCat, the monadic rule 2σ 2 2π σ for [x := m(·)]F evaluates to an expectation (Eq. (14)), hence for F above !
h
h
JF K = EH ET 1{H=1,T <0} + 1{H=0,T >15} H
ii
h
i
= EH 1{H=1} ET [1{T <0} ] + 1{H=0} ET [1{T >15} ] Z 0
= EH [1{H=1} ]
Z ∞
Z 0
=p
−∞
Z ∞
φµ,σ (t) dt + EH [1{H=0} ]
−∞
φµ,σ (t) dt + (1 − p)
15
15
φµ,σ (t) dt
φµ,σ (t) dt
0−µ 15 − µ = pΦ + (1 − p) 1 − Φ σ σ = PDSP (good_weather).
Here, Φ denotes the standard normal cumulative distribution function. Thus, for this program our semantics coincides with DeepSeaProbLog’s possible-world semantics while avoiding world enumeration. Beyond single-instance queries, the distributional quantifiers from Table 2 are meaningful in this setting. Three typical use cases are: • All stations (universal aggregation). Probability that all weather stations have good weather: ∀s ∈ WeatherStations [h := bernoulli(humid_detector(Worlds ))] [t := normal(temperature_predictor(Worlds ))] (h = 1 ∧ t < 0) ∨ (h = 0 ∧ t > 15) which evaluates via
s (·) in the Product algebra.
Q
• Exists a region (existential aggregation). Probability that at least one region has good weather: ∃r ∈ Regions [h := bernoulli(humid_detector(Worldr ))] [t := normal(temperature_predictor(Worldr ))] (h = 1 ∧ t < 0) ∨ (h = 0 ∧ t > 15) which evaluates via 1 −
r (1 − ·) (probabilistic sum).
Q
• Always over time (universal over time). Probability that the weather is good for all time slots: ∀τ ∈ TimeSlots [h := bernoulli(humid_detector(Worldτ ))] [t := normal(temperature_predictor(Worldτ ))] (h = 1 ∧ t < 0) ∨ (h = 0 ∧ t > 15) again aggregating with a product over τ . On ∀-aggregation: product vs. infimum vs. LTN. For distributional semantics there are several meaningful choices for aggregating universal quantification: • Product (probabilistic ∀) as in (16): J∀x : s F K = a∈I(s) JF Kν[x7→a] . This reads as "probability that all independent30 events hold". It is however extremely sensitive: a Q
30
See paragraph 7.1 for a critical discussion of independence.
28
single zero (e.g., one faulty station reporting bad weather) collapses the product to 0 and, even without zeros, the value decays exponentially with the number of stations, at least for continuous values. • Infimum/min (classical fuzzy ∀): inf a JF Kν[x7→a] . This captures a strict worst-case reading and does not shrink when many stations are near 1, but it is still killed by a single zero and ignores the distribution of the other values.
• LTN-style p-mean of complements (Sec. 4.3, App. 7.2): J∀x : s F K = 1−
1 X (1− |I(s)| a
1/p
(or its measure-theoretic analogue). This provides a tunable continuum JF Kν[x7→a] )p between averaging (p small) and the infimum (p → ∞), and is typically more robust to P P isolated outliers. A weighted variant a wa (1−JF Ka )p with a wa = 1 can encode station reliability. In sensor networks with occasional false alarms (one station outputs 0 while thousands report values near 1), product and infimum both collapse to 0. A moderate-p LTN aggregator (optionally weighted) avoids single-sensor catastrophic failure while still converging to the strict infimum as p → ∞. When a strict “all must hold” interpretation is intended and measurements are trusted as independent, the product is appropriate. Infinite (time) domains. For countably or uncountably infinite sets of (time) points T , instead of the finite set of TimeSlots from the previous example, we use the measure-theoretic aggregations from Sec. 7.1 (Eqs. (15)–(16)) or the infinitary LTN aggregations from Sec. 7.2. Given a (probability) measure ρT on T and writing ϕ(τ ) := JF Kν[τ 7→τ ] ∈ [0, 1]:
J∀τ :T F K = exp Eτ ∼ρT [ln ϕ(τ )] ,
J∃τ :T F K = 1 − exp Eτ ∼ρT [ln(1 − ϕ(τ ))] .
These reduce to certain (depending on the measure ρT ) finite products/probabilistic sums when T is finite with the counting measure. Zeros at isolated times yield ln 0 = −∞ and therefore a value 0 for ∀ (consistent with the convention 0 · ∞ = 0). Alternatively, the infinitary LTN scheme provides a robust family of aggregators: J∀τ :T F K = 1 −
Z T
(1 − ϕ(τ )) dρT (τ ) p
1/p
,
J∃τ :T F K =
Z T
ϕ(τ )p dρT (τ )
1/p
.
For rare glitches (bad weather reported at a few time instants), these aggregators with moderate p (or with ρT down-weighting unlikely times) avoid collapse to 0, while p → ∞ recovers the strict infimum. When a “almost everywhere” reading is desired, one may also use the essential infimum/supremum w.r.t. ρT to ignore measure-zero anomalies.
8.2
Comparison to LDL (Logic of Differentiable Logics)
The Logic of Differentiable Logics (LDL) approach [Ślusarz et al., 2023] differs from our framework in several fundamental aspects. First, LDL incorporates comparison operators directly into their syntax, whereas our approach treats them as part of the non-logical signature, providing greater flexibility in language design. Second, LDL restricts their type system to Bool, Real, Vector, and Index types, while our framework maintains a more general type-theoretic foundation. Third, LDL’s syntax includes constructs such as lambda-terms, let-terms, repetitions of expressions, vector constructors, and vector look-ups, which introduces complexity that our approach avoids through a more streamlined logical structure. While both approaches employ typed languages, LDL does not utilise an abstract signature to achieve language generality. Furthermore, LDL lacks the algebraic structure provided by 29
our 2Mon-BLat framework, which endows our semantics with a clearly defined mathematical structure while maintaining sufficient flexibility to accommodate different logical semantics (STL as an approximation). Additionally, LDL makes the restrictive assumption that all distinct random variables are independent, limiting its applicability to scenarios where this independence assumption holds. A key distinction lies in the quantification mechanisms: LDL employs variable-dependent quantification, whereas our framework utilises sort-dependent quantification, which furthermore reduces complexity by providing all the (sort-dependent) information necessary for quantification by defining the interpretation function. Finally, LDL does not require associativity of the logical operators, enabling the use of non-associative and/or operators characteristic of Signal Temporal Logic (STL). This nonassociativity requirement constitutes another reason why STL does not naturally fit into our 2Mon-BLat model and should instead be modelled as approximating a 2Mon-BLat structure, a topic to be addressed in subsequent work. Actually, it is not absolutely necessary to require associativity, as we did in Def. 1 of our 2Mon-BLat. However unifying nearly all semantics under this algebraic umbrella and seeing STL (and potentially others) as approximations of the 2Mon-BLat algebra, gives us a richer structure of our semantics and reveals otherwise suppressed algebraic laws. LDL quantifiers Recall Defs. 2 and 12 and this discussion following the latter: an aggregated 2Mon-BLat provides maps aggr∀X , aggr∃X : LX → L, where additionally, a structure on X may be used. In LDL, the context Q maps a bound variable x:s to a random variable Q[x] on I(s) with density pX . For a measurable g : I(s) → R write xmin := arg min g(a),
xmax := arg max g(a).
a∈I(s)
a∈I(s)
For a random variable X with density pX , LDL defines in [Ślusarz et al., 2023, p. 9] (and we adopt) the quantifier aggregations exactly as Emin [g(X)] := lim
Z
γ→0 x∈Bγxmin
pX (x) g(x) dx,
Emax [g(X)] := lim
Z
γ→0 x∈Bγxmax
pX (x) g(x) dx.
Hence we set aggr∀I(s),Q[x] (g) := Emin g Q[x] ,
aggr∃I(s),Q[x] (g) := Emax g Q[x] .
Consequently, for any F and valuation ν, this is coherent with the definition of the quantifiers from Table 2: J∀x:s F Kν = aggr∀I(s),Q[x] λa.JF Kν[x7→a] ,
J∃x:s F Kν = aggr∃I(s),Q[x] λa.JF Kν[x7→a] .
Variable–dependent vs. sort–dependent quantification. In our probabilistic semantics (Sec. 7.1), each sort s comes with a fixed measure µs and quantification integrates with respect to µs (independent of the variable name). LDL instead equips each bound variable x:s with its own random variable Q[x] (which has a density and may differ between variables of the same sort). This design choice serves two purposes: • It allows simultaneous use of different distributions on the same sort in one formula, e.g. x:s drawn from a data distribution Q[x] and y:s drawn from an adversarial or reweighted distribution Q[y]. • It enables contextual or conditional sampling: Q[x] can depend on the surrounding bound context Γ or external parameters, effectively acting as a Markov kernel ρx (· | Γ). 30
By contrast, our sort–based variant fixes a measure µs and uses the same aggregator for every variable x:s: for the chosen aggregation operators (product/infimum/LTN, etc.). This is much simpler, since it avoids the complexity of managing multiple distributions for different variables of the same sort. Moreover, it seems natural to associate the carrier sets of an interpretation with probability distributions. However, NeSyCat still fulfils all 3 goals stated in Sec. 1 of Ślusarz et al. [2023] and is even more modular and well-separated: 1. NeSyCat formally covers a sufficient fragment of first-order logic to express key properties in machine learning verification, such as robustness. 2. The syntax, semantics and pragmatics of NeSyCat are well-separated. And even more so than in LDL, since we clearly disentangle the concepts of signature, syntax as context-free grammar, interpretation of a NeSy framework, and Tarskian semantics of a NeSy system in an 2Mon-BLat algebra. 3. NeSyCat has a unified, general syntax and semantics able to express multiple different DLs and is modular on the choice of DL, by introducing the modularity of choosing the monad, the truth space, and the 2Mon-BLat algebra by choosing a NeSy framework. NeSyCat encoding of the LDL robustness example. Following [Ślusarz et al., 2023, Ex. 3.1], we consider an image-classification setting where inputs are 28 × 28 grayscale images flattened to vectors in R784 . Hence our input sort is Vec784 with I(Vec784 ) = R784 . A classifier typically outputs a vector of class scores/logits in Rm (e.g., m = 10 for MNIST). Accordingly, we take the network as a function f : R784 −→ Rm
(m ≥ 1 fixed).
The robustness property we encode states ℓ∞ -robustness around a reference image x̂: whenever an input x lies in the ℓ∞ -ball B∞ (x̂, ε), the output f (x) must lie in the ℓ∞ -ball B∞ (f (x̂), δ). This is exactly what our predicate bounded(·, ·, ·) and the formula Φε,δ,x̂ capture below. Regarding the first goal mentioned above, we can encode the LDL robustness example as follows: Fix sorts Vec784 , Index784 , Vecm , Indexm , Real with interpretations I(Vec784 ) = R784 , I(Index784 ) = {0, . . . , 783}, I(Vecm ) = Rm , I(Indexm ) = {0, . . . , m − 1}, I(Real) = R. Let normal function symbols at784 : Vec784 × Index784 → Real,
atm : Vecm × Indexm → Real,
abs : Real → Real,
leq : Real × Real → Ω,
be given, where at784 (v, i) and atm (w, j) read components, abs is absolute value, and leq(a, b) is the crisp predicate [a ≤ b]. Let f :Vec784 → Vecm be a computational function symbol (the network). Define the derived predicates bounded_in(v, u, a) := ∀i:Index784 leq abs(at784 (v, i) − at784 (u, i)), a ,
bounded_out(w, z, a) := ∀j:Indexm leq abs(atm (w, j) − atm (z, j)), a .
For parameters ε, δ ∈ R and a fixed input x̂ ∈ R784 , the LDL robustness property of f is encoded in NeSyCat as the family of formulas
Φε,δ,x̂ := ∀x:Vec784 bounded_in(x, x̂, ε) → bounded_out f (x), f (x̂), δ
.
Under the LDL quantifier aggregator (par. 8.2) for the bound variable x, its semantics is JΦε,δ,x̂ Kν = aggr∀I(Vec784 ), Q[x] λa.Jbounded_in(x, x̂, ε) → bounded_out(f (x), f (x̂), δ)Kν[x7→a] = Emin g(Q[x])
31
where the semantics of g(a) := λa.Jbounded_in(x, x̂, ε) → bounded_out(f (x), f (x̂), δ)Kν[x7→a] is given by the semantics of the implication operator in a certain 2Mon-BLat. In conclusion we have modelled our example to coincide with the LDL semantics.
8.3
Monadic Semantics and Probabilistic Programming
Our use of monads for structuring neurosymbolic semantics draws on a rich tradition of monadic approaches to probabilistic programming. Moggi [1991] established monads as the uniform abstraction for computational effects; the application to probability was pioneered by Giry [1982], who introduced the probability monad on measurable spaces, and by Jones and Plotkin [1989], who developed the analogous probabilistic powerdomain in domain theory. Ramsey and Pfeffer [2002] made the connection to programming languages explicit via a stochastic lambda calculus in which probability distributions form a monad with unit given by the Dirac delta and bind given by marginalisation. On the semantic side, Staton et al. [2016] gave the first adequate measure-theoretic denotational semantics for a probabilistic programming metalanguage supporting higher-order functions, continuous distributions, and soft constraints (conditioning), using Kleisli morphisms of a measure monad as the central semantic objects—the same kind of compositional, Kleisli-based semantics that NeSyCat employs. Staton [2017] further showed that the semantics based on sfinite kernels is commutative, meaning that independent computations can be reordered freely; this property is directly relevant to NeSyCat, where independent parts of a neurosymbolic system may be evaluated in any order. A tutorial exposition of the “programs as measures” viewpoint is given in [Staton, 2020]. On the categorical side, Fritz [2020] developed the theory of Markov categories, showing that the Kleisli category of any affine commutative monad (including the Giry monad) is a Markov category. In particular, Kℓ G ∼ = Stoch is a Markov category, and fundamental results of probability theory—conditional independence, disintegration, sufficient statistics—can be stated and proved at this abstract level, applying uniformly to all NeSyCat instantiations. Fritz and Perrone [2018] complements this with a bimonoidal treatment of joints, marginals, and independence for probability monads. Cho and Jacobs [2019] developed disintegration and Bayesian inversion categorically via string diagrams, and Jacobs [2018] systematically connected probability monads to commutative effectuses—a categorical framework for probabilistic reasoning supporting predicates, conditioning, and Bayesian inversion. A central limitation of the category Meas is that it is not Cartesian closed, preventing a straightforward higher-order probabilistic semantics. Heunen et al. [2017] resolved this by introducing quasi-Borel spaces (QBS), which carry a probability monad P that, when restricted to standard Borel spaces, agrees with the Giry monad. Since NeSyCat currently works within standard Borel spaces (or measure spaces) for its probabilistic frameworks, our semantics embeds conservatively into the QBS setting, which would become necessary for higher-order extensions (e.g., neural networks as first-class probabilistic objects). Vakar et al. [2019] extended this to quasi-Borel predomains supporting recursion and conditioning, and Ścibior et al. [2018] used the QBS semantics to formally validate inference algorithms in the monad-bayes library [Ścibior et al., 2015]. In summary, NeSyCat sits at a previously unexplored intersection: it applies the same categorical and monadic foundations developed for probabilistic programming (Giry monad, Kleisli categories, Markov categories) to the problem of unifying neurosymbolic systems, rather than to probabilistic languages per se. This connection suggests that results from categorical probability—such as Fritz’s abstract conditional independence or Cho–Jacobs disintegration— may be directly applicable to structured reasoning about neurosymbolic systems.
32
8.4
Categorical Logic and Categories for AI
The use of category-theoretic structure in logic long predates current neurosymbolic and machinelearning applications. Makkai and Reyes [1977] provide a classical account of first-order categorical logic, and Johnstone’s later exposition Johnstone [2002] develops the same tradition in a form that has informed our NeSyCat semantics. NeSyCat does not aim to replace this line of work; rather, it keeps the surface syntax of first-order logic while extending the semantic side through monads and algebraically parametrised truth-value aggregation through the 2Mon-BLat. Within categories for AI, categorical NLP provides another important point of contact. In standard DisCoCat, grammatical types are mapped to vector spaces and grammatical reductions to linear maps, yielding a compositional model of meaning based on string diagrams [Coecke et al., 2010]. Especially relevant for our purposes is higher-order DisCoCat [Toumi and de Felice, 2025], which reconnects categorical compositional semantics with Montague-style first-order logic by treating word meanings as diagram-valued higher-order functions and recovering negation and quantification in a string-diagrammatic setting. This is close in spirit to NeSyCat because it shows how categorical structure can recover genuinely logical operations, although its primary focus is natural-language semantics rather than monadic semantics for neurosymbolic systems. A more recent line applies category theory directly to AI and machine learning. Fong et al. [2019] show that supervised learning and backpropagation admit a compositional functorial formulation, and Spivak’s broader applied-category-theory perspective [Spivak, 2014] helped make such compositional methods accessible well beyond pure category theory. This is close in spirit to NeSyCat, since both emphasise compositional structure and parametrisation, but the focus is different: their work formalises learning dynamics, whereas our concern here is the interpretation of logical formulas in monadic and algebraic neurosymbolic semantics. Likewise, Gavranović et al. [2024] argue that categorical deep learning offers a unifying algebraic account of neural network architectures and parametric maps. This complements rather than competes with NeSyCat: they focus on architecture and learnable composition, whereas we focus on signatures, interpretations, and semantic evaluation. In this sense, NeSyCat can be read as a bridge between categorical logic and categories for AI, importing categorical and monadic structure into neurosymbolic semantics rather than only into architecture design.
9
Implementation of NeSy Frameworks
We have implemented NeSy frameworks in 2 NeSyCat libraries, which are available at https:// github.com/NeSyCat/PyTorch for the PyTorch version and at https://github.com/NeSyCat/ HaskTorch for the HaskTorch version. The library comes with predefined NeSy frameworks, but also allows users to define their own frameworks, by providing a monad, a truth value space and a double monoid bounded lattice. The library also supports the definition of interpretations. A parser transforms formulas into an abstract syntax tree. There is a function implementing Tarskian semantics, i.e. the evaluation of formulas in a given interpretation. The library also includes a module for NeSy transformations, allowing users to apply transformations between different NeSy frameworks. For simplicity, we have not implemented a sort system, which means that the implementation is untyped.31 Also, the integration of neural networks into interpretations has not been implemented yet, but we plan to do so in the future. The rich Haskell type system allows us to express the semantics of NeSy frameworks in a type-safe way. The Python implementation takes this as a role model, but less type-safe, because Python is dynamically typed. We start with describing the Haskell implementation. 31
In Haskell, we could use type families and heterogeneous lists to implement sorted interpretations.
33
We first introduce a type class for double monoid bounded lattices. Note that for simplicity, we have not implemented the lattice structure, because it is not used in the semantics.32 class TwoMonBLat a where top, bot :: a neg :: a -> a conj, disj, implies :: a -> a -> a Note that conj and disj are typed as plain binary operations a -> a -> a, without an explicit Monoid constraint. This is intentional: the monoid laws (associativity and neutral elements, cf. Def. 1 and Remark 2.1) are mathematical requirements on the algebra not enforced by Haskell’s type system. The implementation trusts that concrete instances satisfy these laws by construction – the predefined algebras in our library do so, and users designing custom algebras should verify the laws mathematically. Enforcing algebraic laws at the type level (e.g., via property-based testing or dependent types) is left for future work. Based on this, we define a type class for aggregated double monoid bounded lattices: class TwoMonBLat a => Aggr2MonBLat s a where -- for a structure on b and a predicate on b, aggregate truth values a aggrE, aggrA :: s b -> (b -> a) -> a Note that aggregation takes into account the structure of our category C of sets with structure, represented as s b here. Usually, we use finite lists, and then aggregation is just iteration of disjunction or conjunction: -- the mainly used Aggr2MonBLat: no additional structure (just lists) + Booleans instance Monad t => Aggr2MonBLat [] (t Bool) where aggrE s f = foldr disj bot $ map f s aggrA s f = foldr conj top $ map f s For infinite aggregation, we need s b to be some (probability) measure. For example, for implementing the Giry monad, we can use the Integrator monad [Tobin, 2018] from the monad-bayes package, which represents measure spaces in a very faithful way. the Giry monad can be defined as a submonad. Values of this monad can be constructed from values of the Integrator monad by normalising them: newtype Giry a = Giry { runGiry :: Integrator a } fromIntegrator :: Integrator a -> Giry a fromIntegrator m = Giry $ normalize $ lift m Then, aggregation can be defined as in equation 15 and 16. Note that we need a double integral (runIntegrator) here, because the integrand is itself an element of T Bool, and we need to employ the isomorphism Giry Bool ∼ = [0, 1] for the Giry monad. instance Aggr2MonBLat Integrator (Giry Bool) where aggrA meas f = Giry $ integrator $ \meas_fun -> exp $ runIntegrator (runIntegrator (log . meas_fun) . runGiry . f) meas aggrE meas f = neg (aggrA meas (neg . f)) 32
In the future, this needs to be added. LDL quantifiers use the lattice structure. Also, to use ULLER for neuro-symbolic learning and reasoning, we need the lattice structure, because we need to be able maximise and minimise over the truth values as described in [Van Krieken et al., 2024].
34
However, the Integrator monad is not very efficient and does not provide sampling. Therefore, we also provide an instance for the SamplerIO monad from the same package, which implements the Giry monad using sampling. Here, using Monte Carlo integration, we can compute the infinite aggregation up to any given precision by increasing the number of samples. Note that first a value in the domain is sampled, then the computational predicate is applied to the value, resulting in an element of T Bool, and finally a Boolean value is sampled from that. In the case of universal quantification, we aggregate the sampled Boolean values using logical conjunction. The probability of obtaining True in all cases is the product of the probabilities of obtaining True for each case. This finite product approximates the infinite product (expressed using exp and ln) in equation 15. A similar reasoning holds for existential quantification. -- Expectation-style aggregation over a distribution -- Here we approximate via Monte Carlo with no_samples samples no_samples = 1000 aggregation :: Monad m => ([a] -> a) -> m b -> (b -> m a) -> m a aggregation connective dist f = do samples <- sequence (replicate no_samples dist) vals <- mapM f samples return (connective vals) instance Aggr2MonBLat SamplerIO (SamplerIO Bool) where aggrE = aggregation or aggrA = aggregation and Based on this type class and the predefined type constructor class for monads, we define a type class for NeSy frameworks, as well as various instances. The instances do not to define any methods, because these have already been defined in the superclasses. class (Monad t, Aggr2MonBLat s (t omega)) => NeSyFramework t s omega -- Classical instance using identity monad, Omega is Bool instance NeSyFramework Identity [] Bool -- Distribution instance, Omega is Bool instance Num prob => NeSyFramework (Dist.T prob) [] Bool -- Non-empty powerset instance (non-determinism) instance NeSyFramework SM.Set [] Bool -- Giry monad instance, using SamplerIO for both aggregation and the monad instance NeSyFramework SamplerIO SamplerIO Bool -- Giry monad instance, using Integrator for aggregation and Giry for the monad instance NeSyFramework Giry Integrator Bool Next, we show the type definition for NeSy interpretations, which is parameterised by the monad t, the structure s of the category C, the truth value space omega and a type a for the universe of discourse. data Interpretation t s omega a = Interpretation { universe :: s a, funcs :: Map.Map Ident ([a] -> a), mFuncs :: Map.Map Ident ([a] -> t a), preds :: Map.Map Ident ([a] -> omega), mPreds :: Map.Map Ident ([a] -> t omega) } We refrain from showing the same number of details of the Python implementation here, because it is much more verbose than the Haskell implementation. The Python implementation follows a structure similar to that of the Haskell implementation, but uses Python’s dynamic typing and built-in data structures, building on the pymonad package. Here is the Python code snippet for the NeSy framework type class: 35
class NeSyFramework[_T: ParametrizedMonad, _O, _R: Aggr2MonBLat]: """ Class to represent a monadic NeSy framework consisting of a monad (T), a set Omega acting as truth basis (O), and an aggregated double monoid bounded lattice (R). This class ensures the following runtime constraint which is not representable in Pythons type system: - _R: Aggr2MonBLat[_T[_O]] """ _monad: Type[_T] _logic: _R ... As in the case of Haskell, also for Python, we provide two versions of the Giry monad, one based on integration and one based on sampling. Again, the integration version is more faithful to the mathematical definition of the Giry monad, but the sampling version is more efficient. The sampling version is based on the numpy library. An idea for a more abstract version would be to use the PyMC library, such that Bayesian inference becomes possible. However, a principal problem arises. For PyMC, only an internal monad can be defined, providing monadic lifting for functions depending on TensorVariables. However, in order to obtain a monad in Python, we would need to lift functions depending on normal Python variables. This is a topic for future work. Once the code base of the original ULLER paper [Van Krieken et al., 2024] is available, our code base could be used to enhance the ULLER implementation with our modular abstractions.
10
Conclusion
The ULLER language Van Krieken et al. [2024] aims at a unifying foundation for neurosymbolic systems. In this paper, we have developed a new semantics for ULLER, based on Moggi’s formalisation of computational effects as monads. In contrast to the original semantics, our semantics is truly modular. It is based on a notion of NeSy framework that provides the structure of the computational effects and the space of truth values. This modularity will enable a cleaner, more modular implementation of ULLER in Python and an easier integration of new frameworks, as well as a structured method of translating between different frameworks. First implementations of our NeSyCat framework are available in Python and Haskell, see https://github.com/cherryfunk/NeSyCat. Note that the distributional and probabilistic NeSy frameworks will make parameterized interpretations in the sense of Van Krieken et al. [2024] differentiable and that this can be integrated by using a category of differentiable manifolds and functions. However, a detailed investigation of differentiability, computability, and computational complexity of our approach is left for future work in a subsequent paper dedicated to NeSyCat’s implementation. Our work suggests an analogy between ULLER’s formulas [x := m(T1 , . . . , Tn )]F and Haskell’s do-notation do x ← m(T1 , . . . , Tn ); F for computational effects. Inspired by this analogy, one could extend ULLER to a language with computational terms and formulas that may be nested.
Acknowledgments We thank Rick Adamy for the idea to use monads in the context of ULLER, Kai-Uwe Kühnberger for initiating our collaboration, Emile van Krieken for useful discussions and Björn Gehrke for helping us with the implementation in Python. From Daniel: Big thanks to my father and family Bircks for providing me the space-time to work on this paper, Alice for reminding me to eat, and to my mother and Leilani H. Gilpin for mental support. 36
References J. Adámek, H. Herrlich, and G. Strecker. Abstract and Concrete Categories. Wiley, New York, 1990. S. Awodey. Category Theory. Number 52 in Oxford Logic Guides. Oxford Univ. Press, Oxford, 2. ed edition, 2010. ISBN 978-0-19-958736-0 978-0-19-923718-0. S. Badreddine and M. Spranger. Extending real logic with aggregate functions. In A. S. d’Avila Garcez and E. Jiménez-Ruiz, editors, Proceedings of the 15th International Workshop on Neural-Symbolic Learning and Reasoning as part of the 1st International Joint Conference on Learning & Reasoning (IJCLR 2021), Virtual conference, October 25-27, 2021, volume 2986 of CEUR Workshop Proceedings, pages 115–125. CEUR-WS.org, 2021. URL https: //ceur-ws.org/Vol-2986/paper9.pdf. S. Badreddine, A. S. d’Avila Garcez, L. Serafini, and M. Spranger. Logic tensor networks. Artif. Intell., 303:103649, 2022. doi: 10.1016/J.ARTINT.2021.103649. URL https://doi.org/10. 1016/j.artint.2021.103649. K. Cho and B. Jacobs. Disintegration and Bayesian inversion via string diagrams. Mathematical Structures in Computer Science, 29(7):938–971, 2019. doi: 10.1017/S0960129518000488. B. Coecke, M. Sadrzadeh, and S. Clark. (DisCoCat) Mathematical Foundations for a Compositional Distributional Model of Meaning, Mar. 2010. B. Fong, D. I. Spivak, and R. Tuyéras. Backprop as functor: A compositional perspective on supervised learning. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13. IEEE, 2019. doi: 10.1109/LICS.2019.8785665. T. Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239, 2020. doi: 10.1016/j.aim.2020. 107239. T. Fritz and P. Perrone. Bimonoidal structure of probability monads. Electronic Notes in Theoretical Computer Science, 341:121–149, 2018. doi: 10.1016/j.entcs.2018.11.007. B. Gavranović, P. Lessard, A. Dudzik, T. von Glehn, J. G. M. Araújo, and P. Veličković. Position: Categorical Deep Learning is an Algebraic Theory of All Architectures, June 2024. J.-Y. Girard. Linear Logic: Its syntax and semantics. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 1–42. Cambridge University Press, 1 edition, June 1995. ISBN 978-0-521-55961-4 978-0-511-62915-0. doi: 10.1017/CBO9780511629150.002. M. Giry. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, volume 915 of Lecture Notes in Mathematics, pages 68–85, Berlin, Heidelberg, 1982. Springer. P. Hájek. Metamathematics of Fuzzy Logic. Trends in Logic. Springer Netherlands, Dordrecht, 1998. ISBN 978-1-4020-0370-7 978-94-011-5300-3. doi: 10.1007/978-94-011-5300-3. D. Harel, D. Kozen, and J. Tiuryn. Dynamic logic. ACM SIGACT News, 32(1):66–69, 2001. C. Heunen, O. Kammar, S. Staton, and H. Yang. A Convenient Category for Higher-Order Probability Theory. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, June 2017. doi: 10.1109/LICS.2017.8005137.
37
P. Hájek. Metamathematics of Fuzzy Logic. Trends in Logic. Springer Netherlands, Dordrecht, 1998. ISBN 978-1-4020-0370-7 978-94-011-5300-3. doi: 10.1007/978-94-011-5300-3. URL http://link.springer.com/10.1007/978-94-011-5300-3. B. Jacobs. From probability monads to commutative effectuses. Journal of Logical and Algebraic Methods in Programming, 94:200–237, 2018. doi: 10.1016/j.jlamp.2016.11.006. P. T. Johnstone. Sketches of an Elephant A Topos Theory Compendium. Oxford University PressOxford, Sept. 2002. ISBN 978-0-19-851598-2 978-1-383-02287-2. doi: 10.1093/oso/ 9780198515982.001.0001. C. Jones and G. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS), pages 186–195, 1989. doi: 10.1109/LICS.1989.39173. S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer New York, New York, NY, 1978. ISBN 978-1-4419-3123-8 978-1-4757-4721-8. doi: 10.1007/978-1-4757-4721-8. M. Makkai and G. E. Reyes. First Order Categorical Logic: Model-Theoretical Methods in the Theory of Topoi and Related Categories, volume 611 of Lecture Notes in Mathematics. Springer, Berlin, Heidelberg, 1977. doi: 10.1007/BFb0066201. R. Manhaeve, S. Dumancic, A. Kimmig, T. Demeester, and L. D. Raedt. Neural probabilistic logic programming in DeepProbLog. Artif. Intell., 298:103504, 2021. doi: 10.1016/J.ARTINT. 2021.103504. URL https://doi.org/10.1016/j.artint.2021.103504. E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991. ISSN 08905401. doi: 10.1016/0890-5401(91)90052-4. P. Morettin, A. Passerini, and R. Sebastiani. Efficient Weighted Model Integration via SMTBased Predicate Abstraction. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, pages 720–728, Melbourne, Australia, Aug. 2017. International Joint Conferences on Artificial Intelligence Organization. doi: 10.24963/ijcai.2017/100. T. Mossakowski, L. Schröder, and S. Goncharov. A generic complete dynamic logic for reasoning about purity and effects. Formal Aspects Comput., 22(3-4):363–384, 2010. doi: 10.1007/ S00165-010-0153-4. URL https://doi.org/10.1007/s00165-010-0153-4. G. Priest. An introduction to non-classical logic: From if to is. Cambridge University Press, 2008. N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 154–165, 2002. doi: 10.1145/503272.503288. D. R. Schellhorn and T. Mossakowski. muller: A modular monad-based semantics of the neurosymbolic uller framework. In L. H. Gilpin, E. Giunchiglia, P. Hitzler, and E. van Krieken, editors, Proceedings of The 19th International Conference on Neurosymbolic Learning and Reasoning, volume 284 of Proceedings of Machine Learning Research, pages 494–518. PMLR, 08–10 Sep 2025. URL https://proceedings.mlr.press/v284/schellhorn25a.html. A. Ścibior, Z. Ghahramani, and A. D. Gordon. Practical probabilistic programming with monads. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, pages 165–176, 2015.
38
A. Ścibior, O. Kammar, M. Vakar, S. Staton, H. Yang, Y. Cai, K. Ostermann, S. K. Moss, C. Heunen, and Z. Ghahramani. Denotational validation of higher-order Bayesian inference. volume 2, 2018. doi: 10.1145/3158148. N. Ślusarz, E. Komendantskaya, M. L. Daggitt, R. Stewart, and K. Stark. Logic of Differentiable Logics: Towards a Uniform Semantics of DL, Oct. 2023. L. D. Smet, P. Z. D. Martires, R. Manhaeve, G. Marra, A. Kimmig, and L. D. Raedt. Neural Probabilistic Logic Programming in Discrete-Continuous Domains, Mar. 2023. D. I. Spivak. Category Theory for the Sciences. The MIT Press, Cambridge, Massachusetts, 2014. ISBN 978-0-262-02813-4. S. Staton. Commutative semantics for probabilistic programming. In Programming Languages and Systems (ESOP 2017), volume 10201 of LNCS, pages 855–879. Springer, 2017. doi: 10.1007/978-3-662-54434-1_32. S. Staton. Probabilistic programs as measures. In G. Barthe, J.-P. Katoen, and A. Silva, editors, Foundations of Probabilistic Programming, pages 43–74. Cambridge University Press, 2020. doi: 10.1017/9781108770750.003. S. Staton, H. Yang, F. Wood, C. Heunen, and O. Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 525–534, 2016. doi: 10.1145/2933575.2935313. J. Tobin. Embedded Domain-Specific Languages for Bayesian Modelling and Inference. PhD thesis, University of Auckland, 2018. A. Toumi and G. de Felice. Higher-Order DisCoCat (Peirce-Lambek-Montague semantics). Electronic Proceedings in Theoretical Computer Science, 429:130–145, Sept. 2025. ISSN 20752180. doi: 10.4204/EPTCS.429.7. M. Vakar, O. Kammar, and S. Staton. A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages, 3(POPL), 2019. doi: 10.1145/3290349. E. Van Krieken, S. Badreddine, R. Manhaeve, and E. Giunchiglia. ULLER: A Unified Language for Learning and Reasoning. In T. R. Besold, A. d’Avila Garcez, E. Jimenez-Ruiz, R. Confalonieri, P. Madhyastha, and B. Wagner, editors, Neural-Symbolic Learning and Reasoning, volume 14979, pages 219–239. Springer Nature Switzerland, Cham, 2024. ISBN 978-3-03171166-4 978-3-031-71167-1. doi: 10.1007/978-3-031-71167-1_12. E. van Krieken, P. Minervini, E. M. Ponti, and A. Vergari. On the Independence Assumption in Neurosymbolic Learning, June 2024. E. van Krieken, P. Minervini, E. Ponti, and A. Vergari. Neurosymbolic Reasoning Shortcuts under the Independence Assumption, July 2025. P. Varnai and D. V. Dimarogonas. On Robustness Metrics for Learning STL Tasks. In 2020 American Control Conference (ACC), pages 5394–5399, July 2020. doi: 10.23919/ACC45564. 2020.9147692. M. Walicki and S. Meldal. Multialgebras, power algebras and complete calculi of identities and inclusions. In Workshop on the Specification of Abstract Data Types, pages 453–468. Springer, 1994. 39
A
Brief Introduction to Category Theory
We recall some basic notions of category theory. See Spivak [2014] for an introduction with a focus on application in database theory, Awodey [2010] for a logical and type-theoretic overview, and Mac Lane [1978] as a general reference. Definition 20. A Category C consists of • a class |C| of objects, • for any two objects A, B ∈ |C| a set C(A, B) of morphisms from A to B. f ∈ C(A, B) is written as f : A → B (not necessarily a function), • for any object A ∈ |C| an identity morphism idA ∈ C(A, A), i.e. idA : A → A, • for any A, B, C ∈ |C| a composition operation ◦ : C(B, C) × C(A, B) → C(A, C), i.e. for f : A → B, g : B → C, we have g ◦ f : A → C, such that • identities are neutral elements for composition, i.e. f ◦ idA = f = idB ◦ f , and • composition is associative, i.e. (f ◦ g) ◦ h = f ◦ (g ◦ h). Examples of categories are: • Set: Sets and functions. – |Set| = {M | M is a set} – Set(A, B) = {f | f : A → B is a function} – Compositions and identities of functions. • Meas: measurable spaces and measurable functions.33 – |Meas| = {(X, ΣX ) | ΣX is a σ-algebra on X} – Meas((X, ΣX ), (Y, ΣY )) = {f : X → Y | f −1 (B) ∈ ΣX for all B ∈ ΣY } – Compositions and identities of measurable functions. • Measr: measure spaces and measurable functions.34 – |Measr| = {(X, ΣX , µX ) | µX is a measure on (ΣX , X)} – Measr((X, ΣX , µX ), (Y, ΣY , µY )) = {f : X → Y | f measurable} – Compositions and identities of measurable functions. • Prob: probability spaces and measurable functions.35 – |Prob| = {(X, ΣX , ρX ) | ρX is a probability measure on (ΣX , X)} – Prob((X, ΣX , ρX ), (Y, ΣY , ρY )) = {f : X → Y | f is measurable} – Compositions and identities of measurable functions. 33
More details at https://ncatlab.org/nlab/show/measurable+space. More details at https://ncatlab.org/nlab/show/measure+space. 35 More details at https://ncatlab.org/nlab/show/Prob. 34
40
The key distinction between Meas and Measr is that objects of Meas are measurable spaces (X, ΣX ) carrying only a σ-algebra, while objects of Measr are measure spaces (X, ΣX , µX ) additionally equipped with a measure. This extra structure is needed when quantifiers require sort-dependent measures (see Table 6). In both categories, morphisms are measurable functions—in particular, morphisms in Measr are not required to preserve the measure. Definition 21. A quasi-Borel space [Heunen et al., 2017] is a set X together with a set MX ⊆ (R → X) of admissible random elements satisfying: (1) all constant functions are in MX ; (2) MX is closed under precomposition with measurable functions R → R; and (3) MX is closed under countable case-splitting along measurable partitions of R. A morphism f : (X, MX ) → (Y, MY ) is a function f : X → Y such that f ◦ α ∈ MY for all α ∈ MX . The category QBS of quasi-Borel spaces is Cartesian closed and carries a probability monad that, when restricted to standard Borel spaces, agrees with the Giry monad on Meas. This makes QBS the natural setting for higher-order probabilistic programming and, by extension, for higher-order extensions of NeSyCat; see Section 8.3 for further discussion. Commutative diagrams are often used to visualise equalities between (compositions of) morphisms in categories. For example, the following diagram shows the composition of morphisms f : A → B and g : B → C: f
A
B g◦f
g
C
Definition 22. An object 1 ∈ |C| is called terminal, if for each A ∈ |C| there exists a unique morphism !A : A → 1C . Definition 23 (Products). Let C be a category and let A, B be objects in C. A product of A and B is an object A × B together with two morphisms (called projections) πA : A × B → A and πB : A × B → B such that for any object X with morphisms f : X → A and g : X → B, there exists a unique morphism u : X → A × B such that πA ◦ u = f and πB ◦ u = g. This unique u is noted as ⟨f, g⟩ and is called the pairing of f and g. This universal property can be depicted by the following commutative diagram: X
f
g
u=⟨f,g⟩
A
πA
A×B
πB
B
This easily generalises to products of finitely many objects. A category having a terminal object and binary products is called category with finite products, which can also be considered as a cartesian monoidal category up to the choice of the product.36
Glossary of Algebraic and Categorical Terms We collect here brief definitions of standard algebraic and categorical notions used in the main text. For further background, see Awodey [2010], Mac Lane [1978], Hájek [1998], Giry [1982]. Monoid. A monoid (M, ·, e) is a set M equipped with an associative binary operation · : M ×M → M and a neutral element e ∈ M satisfying e · x = x = x · e for all x ∈ M . The monoids (S, ⊗, 1) and (S, ⊕, 0) in the 2Mon-BLat (Def. 1) model conjunction and disjunction, respectively. 36
For more information on cartesian monoidal categories, see https://ncatlab.org/nlab/show/cartesian+ monoidal+category.
41
Bounded lattice. A bounded lattice (S, ≤, ⊥, ⊤) is a partially ordered set in which every pair of elements a, b ∈ S has a greatest lower bound (meet) a ∧ b and a least upper bound (join) a ∨ b, and in which there exist elements ⊥ (bottom) and ⊤ (top) satisfying ⊥ ≤ x ≤ ⊤ for all x ∈ S. σ-algebra and measurable space. A σ-algebra on a set X is a collection ΣX ⊆ P(X) containing X, closed under complements and countable unions. The pair (X, ΣX ) is called a measurable space. A function f : X → Y between measurable spaces is measurable if f −1 (B) ∈ ΣX for every B ∈ ΣY . Measure and probability measure. A measure on a measurable space (X, ΣX ) is a countably additive function µ : ΣX → [0, ∞] with µ(∅) = 0. If µ(X) = 1, then µ is a probability measure and (X, ΣX , µ) is a probability space. Markov kernel. A Markov kernel from a measurable space (X, ΣX ) to (Y, ΣY ) is a function k : X×ΣY → [0, 1] such that k(x, ·) is a probability measure on Y for each x ∈ X, and k(·, B) is a measurable function on X for each B ∈ ΣY . Equivalently, it is a measurable map X → G(Y ), i.e. a Kleisli morphism for the Giry monad. Functor. A functor F : C → D between categories maps objects to objects and morphisms to morphisms, preserving identities (F (idA ) = idF (A) ) and composition (F (g ◦ f ) = F (g) ◦ F (f )). Natural transformation. Given functors F, G : C → D, a natural transformation α : F ⇒ G is a family of morphisms αA : F (A) → G(A) indexed by objects A of C, such that αB ◦ F (f ) = G(f ) ◦ αA for every morphism f : A → B. Kleisli category. For a monad (T , η, (−)∗ ) on a category C, the Kleisli category Kℓ T has the same objects as C, but a morphism A → B in Kℓ T is a morphism A → T B in C. Composition is given by Kleisli composition: g ◦Kl f := g ∗ ◦ f . Adjunction and right adjoint. An adjunction F ⊣ G between categories C and D consists of functors F : C → D (the left adjoint) and G : D → C (the right adjoint) together with a natural bijection D(F (A), B) ∼ = C(A, G(B)). In the 2Mon-BLat (Def. 1), when → is the right adjoint of ⊗, this means a ⊗ b ≤ c if and only if a ≤ b → c (the residuation or deduction property). Cartesian closed category. A category is Cartesian closed if it has finite products and, for every object B, the functor (−) × B has a right adjoint (−)B (the exponential or internal hom). This provides currying: morphisms A × B → C correspond bijectively to morphisms A → C B . The category Set is Cartesian closed; Meas is not (which motivates QBS, Def. 21). t-norm and t-conorm. A t-norm ⊗ : [0, 1]2 → [0, 1] is a commutative, associative, monotone operation with neutral element 1. A t-conorm ⊕ : [0, 1]2 → [0, 1] is dual: commutative, associative, monotone with neutral element 0. These provide the algebraic operations for fuzzy and probabilistic logics in the 2Mon-BLat framework (Sec. 6.2).
42