Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras

TL;DR

This paper explores convolution operations in mathematical logic and computing, introducing relational convolution for quantale-valued functions, leading to new modal operators and applications in various logical and quantitative models.

Contribution

It develops a unified framework for relational convolution in logic, generalizing modal operators and applying to categorial, linear, and interval logics with quantitative examples.

Findings

Relational convolution leads to new modal operators for qualitative and quantitative models.

Convolution-based semantics are provided for fragments of various logics.

Applications include algebras of durations and mean values in duration calculus.

Abstract

Convolution is a ubiquitous operation in mathematics and computing. The Kripke semantics for substructural and interval logics motivates its study for quantale-valued functions relative to ternary relations. The resulting notion of relational convolution leads to generalised binary and unary modal operators for qualitative and quantitative models, and to more conventional variants, when ternary relations arise from identities over partial semigroups. Convolution-based semantics for fragments of categorial, linear and incidence (segment or interval) logics are provided as qualitative applications. Quantitative examples include algebras of durations and mean values in the duration calculus.

Figures

Equations

$$(f\ast g)x=\sum _{y,z\in {\Sigma }^{\ast }}^{x=yz}fy\cdot gz.$$

$$\underset{x\in X}{\overset{Px}{⨆}}fx=⨆\{fx\mid x\in X\wedge Px\}$$

$$\mathop{\big{|}R\big{\rangle}}g\,x=\bigsqcup_{y\in Y}^{R\,x\,y}g\,y\qquad\text{ and }\qquad\mathop{\big{\langle}R\,\big{|}}f\,y=\bigsqcup_{x\in X}^{R\,x\,y}f\,x.$$

$$\mathop{\big{|}R\,\big{]}}g\,x=\bigsqcap_{y\in Y}^{R\,x\,y}g\,y\qquad\text{ and }\qquad\mathop{\big{[}R\,\big{|}}f\,y=\bigsqcap_{x\in X}^{R\,x\,y}f\,x.$$

$$\displaystyle\textstyle\mathop{\big{|}\bigcup_{i\in I}R_{i}\big{\rangle}}g$$

$$\displaystyle\textstyle\mathop{\big{|}R\big{\rangle}}(\bigsqcup_{i\in I}g_{i})$$

$$\displaystyle\mathop{\big{|}R\mathbin{;}S\big{\rangle}}h$$

$$\displaystyle\mathop{\big{|}\mathsf{Id}_{X}\big{\rangle}}g$$

$$\mathop{\big{|}R\big{\rangle}}g\leq f\Leftrightarrow g\leq\mathop{\big{[}R\,\big{|}}f\qquad\text{ and }\qquad\mathop{\big{\langle}R\,\big{|}}f\leq g\Leftrightarrow f\leq\mathop{\big{|}R\,\big{]}}g.$$

$$\mathop{\big{|}R\big{\rangle}}g\sqcap f=0\Leftrightarrow g\sqcap\mathop{\big{\langle}R\,\big{|}}f=0\qquad\text{ and }\qquad\mathop{\big{|}R\,\big{]}}f\sqcup g=\top\Leftrightarrow f\sqcup\mathop{\big{[}R\,\big{|}}g=\top.$$

$$(⨆X)\cdot y=\underset{x\in X}{⨆}x\cdot y\text{ and }x\cdot ⨆Y=\underset{y\in Y}{⨆}x\cdot y$$

$$(f{\ast }_{R}g)x=\underset{y\in Y,z\in Z}{\overset{Rxyz}{⨆}}fy\cdot gz.$$

$$f{\ast }_{S}g$$

$$({⨆}_{i\in I}{f}_i){\ast }_{R}g$$

$$f{\ast }_R({⨆}_{i\in I}{g}_i)$$

$$\mathop{\big{|}R\big{\rangle}}f=f\ast_{S}c_{1}\qquad\text{ and }\qquad\mathop{\big{\langle}R\,\big{|}}f=f\ast_{T}c_{1}.$$

$$f\ast_{R}g=\mathop{\big{|}S\big{\rangle}}(\lambda(y,z).\ (f\,y\cdot g\,z)).$$

$$\cdot \text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$(\exists y\in X.Ryuv\wedge Rxyw)\iff (\exists z\in X.Rzvw\wedge Rxuz).$$

$$(f\ast g)\ast h=f\ast (g\ast h).$$

$$(f\ast g)x=\underset{y,z}{\overset{Rxyz}{⨆}}fy\cdot gz=fx\text{mbox}or(g\ast f)x=\underset{y,z}{\overset{Rxyz}{⨆}}gy\cdot fz=fx$$

$$\exists e\in \xi .Ryey\text{mbox}and\exists e\in \xi .Ryye,$$

$$Rxey\Rightarrow x=y\text{mbox}andRxye\Rightarrow x=y.$$

$$\delta xy=\{\begin{array}{ll}1,& \text{if }x=y,\\ 0,& \text{otherwise},\end{array}$$

$$u\cdot v\le w\iff v\le u\backslash w\iff u\le w/v.$$

$$(f\backslash g)x={\text{bigsqcap}}_{y,z}^{Rzyx}fy\backslash gz\text{ and }(g/f)x={\text{bigsqcap}}_{y,z}^{Rzxy}gz/fy,$$

$$f\ast g\le h\iff g\le f\backslash h\iff f\le h/g.$$

$$(f\backslash c_{0})\,x=\bigsqcap_{y,z}^{R\,z\,y\,x}f\,y\to 0=\bigsqcap_{y,z}^{R\,z\,y\,x}\overline{f}\,y\sqcup 0=\bigsqcap_{y}^{S\,x\,y}\overline{f}\,y=\mathop{\big{|}S\,\big{]}}\overline{f}\,x.$$

$$Dxy\wedge D(x\cdot y)z$$

$$\exists e\in E.Dex\wedge e\cdot x=x,$$

$$\exists e\in E.Dxe\wedge x\cdot e=x,$$

$$e_1,e_2\in E\wedge D{e}_1{e}_2\Rightarrow e_1=e_2.$$

$$(f\ast g)x=\underset{y,z}{\overset{x=y\cdot z}{⨆}}fy\cdot gz.$$

Full text

The research reported here was supported in part by Australian Research Council (ARC) Grant DP190102142. Dongol is supported by EPSRC grants EP/R019045/2, EP/R032556/1 and EP/R025134/2.

1. Introduction

Convolution is a ubiquitous operation in mathematics, and computing. Schützenberger and Eilenberg’s approach to formal languages, for instance, uses convolution of formal power series (which are functions from free monoids into semirings) to generalise the standard language product to the context of weighted automata [BR84]. If $\Sigma^{\ast}$ is the free monoid over the alphabet $\Sigma$ and $f,g:\Sigma^{\ast}\to S$ are functions mapping words in $\Sigma^{\ast}$ to values or weights in the semiring $S$, then the convolution of $f$ and $g$ is defined, for all $x\in\Sigma^{\ast}$, as

[TABLE]

Word $x$ is thus split into all possible prefix/suffix pairs $(y,z)$, the functions $f$ and $g$ are applied separately to $y$ and $z$, respectively, the weights of $f\,y$ and $g\,z$ are then multiplied in $S$ and finally the sum of weights for all possible pairs $(y,z)$ is taken. We study convolution algebras with operations of similar shape in this article, yet replace $\Sigma^{\ast}$ and $S$ with different data.

Other examples relevant to us come from Rota’s famous work on the foundations of combinatorics [Rot64], where convolution is one of the operations of the incidence algebra of segments in locally finite posets, and Goguen’s classical work on fuzzy logic, which uses a category with quantale-valued sets as objects and quantale-valued relations as morphisms that are composed by convolution [Gog67]. Before that, Heisenberg’s matrix approach to quantum mechanics was originally presented as a convolution algebra of functions from the groupoid of ordered pairs into the field of complex numbers [Hei25], as pointed out by Connes [Con95]. The Dirichlet convolution of arithmetic functions and the convolution operation in group algebras used in the representation theory of finite groups provide even earlier examples. Notions of convolution in analysis date back at least to work by Cauchy, but are less relevant for us.

More recently, further computationally interesting applications of convolution of functions from partial semigroups or monoids into quantales have been discussed [DHS16]. Separating conjunction, for instance, is a convolution on a partial abelian resource monoid within the assertion quantale of separation logic. The chop modality, a widely used binary modality in interval temporal logics, arises as convolution on a partial semigroup of intervals and yields a similar quantale.

It is well known that the logic of bunched implication—the logical counterpart of the assertion quantale of separation logic—is a substructural logic similar to relevance and linear logics, which have Kripke semantics based on ternary frames. This raises the question whether convolution generalises similarly to ternary relations, and hence to generic semantics for substructural logics. This generalisation seems interesting for several reasons. Using functions instead of predicates with modalities supports quantitative applications. An emphasis on simple uniform constructions on algebras and mappings between them leads to equally concise formalisations in proof assistants, and further to simple generic verification components for separation or interval logics.

The main contribution of this article lies in an answer to that question: in a novel approach to relational convolution, the investigation of the generalised binary and unary modalities that arise from it, in its specialisation to a previous approach based on quantale-valued functions from partial semigroups [DHS16], in further instantiations with a focus on incidence algebras and interval temporal logics, and, last but not least, in its formalisation in the Isabelle/HOL proof assistant [DGHS17].

More specifically, we generalise the standard Kripke semantics for unary multimodal operators from predicates to lattice-valued functions and show how quantale modules [AV93] and various kinds of function transformers arise in this setting (Section 2). More general notions of binary modalities and relational convolution over ternary relations are introduced next (Section 3). These generalise from predicates to quantale-valued functions. Jónsson and Tarski’s famous duality between $(n+1)$-ary relational structures and boolean algebras with $n$-ary operators [JT51] generalises these results in the arity of relations and modal operators, but for the special case of powerset algebras. Yet duality theory is not the subject of this article; see [HWW18] for subsequent results in the lattice-valued case. A correspondence theory for relational convolution is outlined next (Section 4), with emphasis on relational conditions inducing monoidal laws in the convolution algebras of quantale-valued functions. Using these, previous lifting results to convolution algebras [DHS16] are generalised: quantale-valued functions with relational convolution as composition form quantales in the presence of suitable conditions on relations (Theorem 11).

Theorem 11 specialises to a convolution-based semantics for variants of the Lambek calculus, and hence for fragments of other substructural logics including categorical and linear ones (Section 5). It also subsumes previous lifting results based on partial semigroups and monoids (Section 6), and specialises to various incidence algebras for segments and intervals in partial orders with different kinds of compositions (Section 7). Convolution algebras with semi-infinite intervals (those without upper bounds) are based on functions from semidirect products of two partial semigroups—one for finite behaviours, another one for infinite ones—into quantale modules (Section 8 and Section 9). They form quantales (Theorem 23) in which certain distributivity and unit laws are weakened. A glossary of the main algebraic structures used is provided in Appendix A.

After these general mathematical investigations, the second part of this article is devoted to applications. First, a convolution-based algebraic semantics for Halpern-Shoham and Venema style temporal logics [HS91, Ven91] with unary and binary modalities is presented, but generalised to incidence algebras of segments over abstract time domains given by arbitrary posets (Section 10). Within this framework, different kinds of segments, with or without point segments and with different kinds of bounds or compositions, can be included in a uniform and modular way by setting up different kinds of partial semigroups or monoids. From that basis, a substantial part of the interval temporal logic ITL [Mos12] can be obtained, using a semigroup construction for stream functions that abstract from the dynamics of state spaces or program stores (Section 11), and by instantiating to a time domain of natural numbers. This semantics extends seamlessly to the duration calculus [ZH04] (Section 12) and one of its variants, the mean-value calculus [PR98] (Section 13), by instantiating to a real-time domain. For these last two logics, we provide examples that illustrate the relevance of convolution in quantitative modelling, by showing that the algebras of durations and mean values over intervals form quantales, too.

A convolution-based semantics of separation logic has been investigated in a previous article [DGS15]. It provides further evidence for the universality of the convolution-based approach to modal and substructural logics outlined. For all applications considered, it suffices to specify an appropriate ternary relation on the fundamental objects considered. These could be intervals, resources as in separation logic, linear logic or biological modelling [PRS09], threads of concurrent programs [HMSW11] or even operators representing measurements on quantum systems [FB94]. Often, these relations arise from equations over partial semigroups or monoids, and from constructions over these. The lifting to convolution algebras is then generic, and it may yield qualitative assertion algebras corresponding to substructural or modal logics, or else quantitative algebras, for instance of weights or probabilities—for separation logics, interval temporal logics, duration calculi and beyond. A series of additional examples can be found in [DHS16].

The main results of this article have been formalised and verified with the Isabelle/HOL proof assistant. Section 14 contains a brief overview of this implementation. The complete Isabelle code and a corresponding proof document can be found online [DGHS17] in the Archive of Formal Proofs [AFP]. Due to this, we show only a few proofs in the article; cross references between the theorems in the article and Isabelle proofs in the Archive of Formal Proofs can be found in Appendix B. A typical lifting result based on convolution, similar to Theorems 11 and 23, can be found in [DHS16]. The generalised proofs in this article are similar and provide little further insight.

2. Generalised Unary Modalities over Binary Relations

This section introduces generalised unary modalities, parametrised by binary relations, that are defined in terms of lattice-valued functions. These are related to Halpern-Shoham style interval modalities [Ven90, HS91, Ven91] in Section 10. More general notions of binary modalities, parametrised by ternary relations, are introduced and related with unary modalities in Section 3. Modalities over binary relations arise in the context of standard Kripke frames [BdRV01].

According to the standard Kripke semantics, if $R\subseteq X\times X$ is a relation and $P\subseteq X$ a predicate, then \mathop{\big{|}R\big{\rangle}}P\,x holds if and only if $R\,x\,y$ and $P\,y$ hold for some $y\in X$.111We freely use set and predicate notation for relations, we write either $X\to Y$ or $Y^{X}$ for types and sets of functions. Similarly, swapping the order of arguments in $R$, \mathop{\big{\langle}R\,\big{|}}P\,y holds if and only if $R\,x\,y$ and $P\,x$ hold for some $x\in X$. The forward diamond operator \mathop{\big{|}\underline{\phantom{x}}\big{\rangle}} is thus a relational preimage operation; \mathop{\big{|}R\big{\rangle}}P yields the set of pre-states that $R$ relates to any post-state where $P$ holds. The backward diamond \mathop{\big{\langle}\underline{\phantom{x}}\,\big{|}} corresponds to a relational image; \mathop{\big{\langle}R\,\big{|}}P yields the set of post-states to which $R$ relates any pre-state where $P$ holds. In a Kripke frame, $R$ is usually interpreted in terms of accessibility or transitions between possible worlds. Yet some modal logics, such as interval logics, require other interpretations.

More generally, we assume that $R\subseteq X\times Y$, $f:X\to{\mathcal{L}}$ and $g:Y\to{\mathcal{L}}$, where ${\mathcal{L}}=(L,\leq)$ is a complete lattice. We write $\sqcup$ for the join and $\sqcap$ for the meet operation in ${\mathcal{L}}$; we write [math] for the least and $\top$ for the greatest element in this lattice. Finally, we write

[TABLE]

for the supremum of the set $\{f\,x\mid x\in X\wedge P\,x\}$. Then, for all $x\in X$ and $y\in Y$,

[TABLE]

Forward and backward diamonds are related by opposition duality, which is modelled by conversion: \mathop{\big{\langle}R\,\big{|}}=\mathop{\big{|}{R}^{\smallsmile}\big{\rangle}}, where ${R}^{\smallsmile}\,x\,y\Leftrightarrow R\,y\,x$. Forward and backward box modalities can be obtained with infima in place of suprema:

[TABLE]

Whenever the complete lattice is boolean, boxes and diamonds are related by De Morgan duality. Using $\overline{\varphi}=\lambda x.\ \overline{\varphi\,x}$ then yields \mathop{\big{|}R\,\big{]}}g=\overline{\mathop{\big{|}R\big{\rangle}}\overline{g}} and \mathop{\big{[}R\,\big{|}}f=\overline{\mathop{\big{\langle}R\,\big{|}}\overline{f}}.

The standard modalities [BdRV01] can be recovered by restricting types and using ${\mathcal{L}}=\mathbb{B}$, the two-element lattice of booleans. The generalisation to lattice-valued functions allows the transition from qualitative to quantitative reasoning, using, for instance, the complete lattice of extended reals or the unit interval with respect to $\min$ and $\max$ (cf. Example 3 and Sections 12 and 13).

The following statement shows that generalised modalities satisfy module-like laws, more precisely the laws of quantale modules [AV93], which are introduced formally in Section 9. In this lemma, $R\mathbin{;}S$ denotes the relational composition of $R$ and $S$ and $\mathsf{Id}_{X}=\{(x,x)\mid x\in X\}$ the identity relation over $X$.

Lemma 1**.**

For an index set $I$ and $i\in I$, let $R,R_{i}\subseteq X\times Y$, $S\subseteq Y\times Z$, $g,g_{i}:Y\to{\mathcal{L}}$, and $h:Z\to{\mathcal{L}}$. Then

[TABLE]

The proofs have been formalised with Isabelle. The diamond operator \mathop{\big{|}\underline{\phantom{x}}\big{\rangle}}:\mathbb{P}(X\times Y)\to{\mathcal{L}}^{Y}\to{\mathcal{L}}^{X} corresponds to a generalised (module) action of a binary relation of type $\mathbb{P}(X\times Y)$ between the complete join (semi)lattices of functions ${\mathcal{L}}^{Y}$ and ${\mathcal{L}}^{X}$ obtained by pointwise lifting from $Y$ and $X$. Identity (3) can be written as \mathop{\big{|}R\mathbin{;}S\big{\rangle}}=\mathop{\big{|}R\big{\rangle}}\circ\mathop{\big{|}S\big{\rangle}}, where \mathop{\big{|}R\mathbin{;}S\big{\rangle}}:{\mathcal{L}}^{Z}\to{\mathcal{L}}^{X}, \mathop{\big{|}R\big{\rangle}}:{\mathcal{L}}^{Y}\to{\mathcal{L}}^{X} and \mathop{\big{|}S\big{\rangle}}:{\mathcal{L}}^{Z}\to{\mathcal{L}}^{Y}. Identity (4) can be written as \mathop{\big{|}\mathsf{Id}_{X}\big{\rangle}}=\mathsf{id}_{{\mathcal{L}}^{X}}, where $\mathsf{id}_{{\mathcal{L}}^{X}}$ is the identity function of type ${\mathcal{L}}^{X}\to{\mathcal{L}}^{X}$. Thus \mathop{\big{|}\underline{\phantom{x}}\big{\rangle}} is indeed a covariant functor between the category of relations and the category with lattice-valued functions as objects and higher-order functions—or function transformers—between these functions as morphisms. Identity (1) can be written as \mathop{\big{|}\bigcup_{i\in I}R_{i}\big{\rangle}}=\bigsqcup_{i\in I}\mathop{\big{|}R_{i}\big{\rangle}}, hence \mathop{\big{|}\underline{\phantom{x}}\big{\rangle}} sends unions in the category of relations of type $\mathbb{P}(X\times Y)$ to suprema in the complete semilattice of function transformers. Finally, by (2), \mathop{\big{|}R\big{\rangle}} is (completely) additive and hence an operator on the lattice of functions ${\mathcal{L}}^{Y}$ in the sense of boolean algebras with operators [JT51]. This justifies the status of diamond operators as modalities.

Analogous facts for the other kinds of modalities arise by duality. The operator \mathop{\big{\langle}\underline{\phantom{x}}\,\big{|}} is contravariant: \mathop{\big{\langle}R\mathbin{;}S\,\big{|}}=\mathop{\big{\langle}S\,\big{|}}\circ\mathop{\big{\langle}R\,\big{|}} because ${(R\mathbin{;}S)}^{\smallsmile}={S}^{\smallsmile}\mathbin{;}{R}^{\smallsmile}$. Similarly, identities (1), (2) and (4) in Lemma 1 are dualised by replacing \mathop{\big{|}\underline{\phantom{x}}\big{\rangle}} by \mathop{\big{\langle}\underline{\phantom{x}}\,\big{|}}. The operator \mathop{\big{|}\underline{\phantom{x}}\,\big{]}} acts covariantly on the space of functions of type ${\mathcal{L}}^{Y}\to{\mathcal{L}}^{X}$ under lattice duality like \mathop{\big{|}\underline{\phantom{x}}\big{\rangle}}, that is, \mathop{\big{|}R\mathbin{;}S\,\big{]}}=\mathop{\big{|}R\,\big{]}}\circ\mathop{\big{|}S\,\big{]}} and \mathop{\big{|}\mathsf{Id}_{X}\,\big{]}}=\mathsf{id}_{{\mathcal{L}}^{X}}. However it maps relational unions to infima in the space of function transformers, i.e., \mathop{\big{|}\bigcup_{i\in I}R_{i}\,\big{]}}=\bigsqcap_{i\in I}\mathop{\big{|}R_{i}\,\big{]}}, and it is (completely) multiplicative, that is, \mathop{\big{|}R\,\big{]}}(\bigsqcap_{i\in I}g_{i})=\bigsqcap_{i\in I}\mathop{\big{|}R\,\big{]}}g_{i}. Once again, \mathop{\big{[}\underline{\phantom{x}}\,\big{|}} is contravariant, \mathop{\big{[}R\mathbin{;}S\,\big{|}}=\mathop{\big{[}S\,\big{|}}\circ\mathop{\big{[}R\,\big{|}}, and the properties corresponding to (1), (2) and (4) in Lemma 1 arise from the forward box laws by replacing \mathop{\big{|}\underline{\phantom{x}}\,\big{]}} by \mathop{\big{[}\underline{\phantom{x}}\,\big{|}}.

A study of these relationships in the context of (Sup-)enriched categories or quantaloids [Ros91] seems worthwhile. Pragmatically, however, the functional programming style used in this section seems general enough to cover various applications while simple enough for a straightforward formalisation in an interactive theorem prover like Isabelle.

The final statements of this section show, in the tradition of boolean algebras with operators, that generalised unary modalities are related by adjunctions or Galois connections and conjugations. This yields additional theorems for free. All four proofs have been verified with Isabelle.

Lemma 2**.**

Let $R\subseteq X\times Y$, $f:X\to{\mathcal{L}}$ and $g:Y\to{\mathcal{L}}$. Then

[TABLE]

Lemma 3**.**

Let $R\subseteq X\times Y$, $f:X\to{\mathcal{L}}$ and $g:Y\to{\mathcal{L}}$, where ${\mathcal{L}}$ is a complete boolean algebra. Then

[TABLE]

3. Generalised Binary Modalities over Ternary Relations

Kripke frames based on ternary relations yield semantics for substructural logics such as relevance logics [DR02], the Lambek calculus [Lam58], categorial logics [MR12] or linear logic [AD93]; the general theory is once again due to Jónsson and Tarski [JT51]. We generalise the approach from Section 2 to ternary relations and binary modalities. These are closely related to the concatenation or product of the Lambek calculus, the tensor of linear logic or the chop operators of interval logics. In particular, they yield relational convolution operators similar to those that appear widely across mathematics and computing [DHS16]. Binary modalities require enrichment of the complete lattices of the previous section by an operation of composition.

{defi}

A quantale [Con71, Ros90] is a structure ${\mathcal{Q}}=(Q,\leq,\cdot)$ such that $(Q,\leq)$ is a complete lattice, $(Q,\cdot)$ is a semigroup with composition operator $\cdot$ and the distributivity axioms

[TABLE]

hold for any $X,Y\subseteq Q$. We write [math] for its least and $\top$ for its greatest element with respect to $\leq$.

• •

A quantale is unital if $(Q,\cdot,1)$ is a monoid with unit $1$.

• •

A quantale is distributive if the underlying lattice is.

• •

A distributive quantale is boolean if every element $x$ is complemented, that is, $x\sqcap\overline{x}=0$ and $x\sqcup\overline{x}=\top$ hold.

The annihilation laws $x\cdot 0=0=0\cdot x$ hold in any quantale because $\bigsqcup\emptyset=0$. Our lifting results from quantales to convolution algebras in the forthcoming sections preserve distributivity and complementation properties of the quantale. For the sake of simplicity, however, we present our results for quantales only and leave the extensions to distributive or boolean quantales implicit. They can be found in our Isabelle theories.

We present some well known examples of quantales that are useful for our purposes.

{exa}

1. (a)

The Booleans form the boolean unital quantale $(\mathbb{B},\leq,\sqcap,1)$ in which composition is the lattice meet $\sqcap$. It allows us to treat predicates as boolean-valued functions. 2. (b)

The Lawvere quantale $(\mathbb{R}_{+}^{\infty},\geq,+,0)$ consists of the extended nonnegative reals $\mathbb{R}_{+}^{\infty}$ with reversed order on the reals $\geq$, $\bigsqcap$ as supremum, $+$ as composition extended by $x+\infty=\infty=\infty+x$, and [math] as its unit. 3. (c)

Similarly to (a), $(\mathbb{R}_{+}^{\infty},\geq,\max,0)$ forms a unital quantale with $\bigsqcap$ as supremum. 4. (d)

The structure $(\mathbb{R}_{+}^{\infty},\leq,\cdot,1)$ forms a unital quantale with $\bigsqcup$ as supremum. 5. (e)

The unit interval $([0,1],\leq,\cdot,1)$ forms a unital quantale with $\bigsqcup$ as supremum. It is isomorphic to the Lawvere quantale via the function $(\lambda x\cdot-\ln x)$. 6. (f)

The structures $([0,1],\leq,\min,1)$ and $([0,1],\geq,\max,0)$ form unital quantales.

The quantales in (b)-(f) are distributive, but not boolean. ∎

{defi}

Let $R\subseteq X\times Y\times Z$ be a ternary relation, and let $f:Y\to{\mathcal{Q}}$ and $g:Z\to{\mathcal{Q}}$ be functions into the quantale ${\mathcal{Q}}$. We define, for all $x\in X$, the generalised binary modality of relational convolution $\ast_{R}$ by

[TABLE]

In applications, $R$ is often fixed. It is then convenient to simply write $f\ast g$.

Sections 10 and 11 show how relational convolution specialises to chop modalities in various interval logics. Its relationship to the (non-associative) Lambek calculus and similar substructural logics is explained in Section 5. Its relationship with more conventional notions of convolution [DHS16] is discussed further in Section 6. A similar convolution function into lattices has been studied independently by Harding, Walker and Walker [HWW18].

The following binary counterpart of Lemma 1 has been verified with Isabelle.

Lemma 4**.**

For an index set $I$ and $i\in I$, let $R\subseteq X\times Y\times Z$, $f,f_{i}:Y\to{\mathcal{Q}}$ and $g,g_{i}:Z\to{\mathcal{Q}}$. Then, with $S=(\bigcup_{i\in I}R_{i})$,

[TABLE]

The laws (3) and (4) from Lemma 1 make no sense in this context.

Next we relate unary and binary modalities. Both of the following statements have been verified with Isabelle.

Lemma 5**.**

Let $R\subseteq X\times Y$ and ${\mathcal{Q}}$ be a unital quantale. Let $f:Y\to{\mathcal{Q}}$ and let the constant function $c_{1}:Z\to{\mathcal{Q}}$ be defined by $c_{1}\,z=1$ for all $z\in Z$. Then, with $S=\lambda x,y,z.\ R\,x\,y$ and $T=\lambda y,x,z.\ R\,x\,y$,

[TABLE]

Lemma 6**.**

Let $R\subseteq X\times Y\times Z$, $f:Y\to{\mathcal{Q}}$ and $g:Z\to{\mathcal{Q}}$. Then, with $S\,x\,(y,z)=R\,x\,y\,z$,

[TABLE]

With $(\cdot)=\lambda(y,z).\ y\cdot z$ one can write f\ast_{R}g=\mathop{\big{|}S\big{\rangle}}((\cdot)\circ(f,g)) in functional programming style.

Convolutions $f\ast g$ have been introduced in Schützenberger and Eilenberg’s approach to formal language theory [BR84]. In this case, $x$, $y$ and $z$ are words from some free monoid $X^{\ast}$ and $R\,x\,y\,z$ corresponds to $x=y\cdot z$. Similar forms of convolution have been considered widely in mathematics. Many well-known constructions from computer science can be represented this way [DHS16].

4. Relational Semigroups and Convolution Algebras

We now fix a ternary relation $R\subseteq X\times X\times X$ and write $f\ast g$ instead of $f\ast_{R}g$. The main result of this section (Theorem 11) is also one of the main theorems of this article. It characterises the convolution algebras that arise from lifting to function spaces ${\mathcal{Q}}^{X}$ of quantale-valued functions of type $X\to{\mathcal{Q}}$, with relational convolution as the operation of composition on function spaces and other operations such as suprema and the order relation lifted pointwise from $Q$. Convolution algebras are usually quantale-like, but we also encounter situations where they form semirings. But before that, in the tradition of modal correspondence theory, we impose conditions on $R$ that are reflected by algebraic laws in convolution algebras.

We first consider associativity $(f\ast g)\ast h=f\ast(g\ast h)$ of convolution for quantale-valued functions $f,g,h:X\to{\mathcal{Q}}$. We present two counterexamples. The first one is computationally interesting, the second one purely syntactic.

Lemma 7**.**

There exists a ternary relation over $X$ such that $(f\ast f)\ast f\neq f\ast(f\ast f)$ for some $f:X\to\mathbb{B}$.

Proof 4.1**.**

1. (a)

Let $X$ be the set of binary trees with leaves labelled by $a$. Let $R\,x\,y\,z$ hold if $y$ is an immediate left subtree of $x$ and $z$ an immediate right subtree of tree $x$. Let $f=\lambda v.\ (v=a)$. Then $f\ast(f\ast f)$ holds of the tree below, whereas $(f\ast f)\ast f$ does not.

[TABLE] 2. (b)

Let $X=\{a,b\}$, $R=\{(a,b,b),(b,b,a)\}$ and consider $f:X\to\mathbb{B}$ defined by $f\,a=0$ and $f\,b=1$. Then $((f\ast f)\ast f)\,b=0\neq 1=(f\ast(f\ast f))\,b$ holds by unfolding definitions and performing some simple calculations.

In order to force associativity of convolution, we impose the following condition on $R$.

{defi}

A relational semigroup is a structure ${\mathcal{X}}=(X,R)$ such that $X$ is a set and $R$ a ternary relation over $X$ that satisfies the relational associativity law for any $x,u,v,w\in X$:

[TABLE]

The next result has been verified with Isabelle.

Lemma 8**.**

If ${\mathcal{X}}$ is a relational semigroup and ${\mathcal{Q}}$ is a quantale, then for all $f,g,h:{\mathcal{X}}\to{\mathcal{Q}}$,

[TABLE]

Next we consider the unit laws $f\ast\mathsf{id}=f=\mathsf{id}\ast f$ for a suitable function $\mathsf{id}$. Again we provide a counterexample first.

Lemma 9**.**

There is a relational semigroup ${\mathcal{X}}$ for which there is no function $g:{\mathcal{X}}\to\mathbb{B}$ such that $f\ast g=f$ and $g\ast f=f$ hold for all $f:{\mathcal{X}}\to\mathbb{B}$.

Proof 4.2**.**

Consider the closed strict intervals $[i,j]$ with $i<j$ within $[0,1]$ (see Section 7 for formal definitions) and let $R\,x\,y\,z$ hold if $y,z\subseteq[0,1]$ are intervals such that $x=y\cup z$ whenever the maximal point in $y$ equals the minimal point in $z$. As point intervals of $[i,i]$ have been excluded by strictness $i<j$, all strict intervals $x$ and $y$ satisfy $\neg R\,x\,x\,y$ and $\neg R\,x\,y\,x$ and therefore it cannot be the case that either

[TABLE]

for any function $g$, because this would require $R\,x\,x\,y$ for some $y$ in the first case and $R\,x\,y\,x$ for some $y$ in the second one in order to “filter out” $f\,x$.

This proof additionally shows that the candidate identity function $g$ would have to yield $1$ on all intervals $y$ satisfying $R\,x\,x\,y$ or $R\,x\,y\,x$, assuming those existed, and it would have to yield [math] on all other intervals. This motivates the following definitions.

{defi}

A relational monoid is a structure ${\mathcal{Y}}=(Y,R,\xi)$ such that $(Y,R)$ is a relational semigroup and $\xi\subseteq Y$ such that for all $y\in Y$,

[TABLE]

and for all $x,y\in Y$ and $e\in\xi$,

[TABLE]

Using the Kronecker delta function $\delta:Y\to Y\to{\mathcal{Q}}$ into a unital quantale ${\mathcal{Q}}$ defined by

[TABLE]

we can verify the following fact with Isabelle.

Lemma 10**.**

Let ${\mathcal{Y}}$ be a relational monoid and let ${\mathcal{Q}}$ be a unital quantale. Then $\mathsf{id}=\bigsqcup_{e\in\xi}\delta\,e$ is a left and right unit of relational convolution in ${\mathcal{Q}}^{\mathcal{Y}}$.

Relational encodings of partial algebras date back at least to Skolem [Sko20]. The correspondence between relational semigroups and monoids and (partial) algebras is explained in Section 6. In a monoidal context, a relation $R\,x\,y\,z$ denotes an identity $x=y\cdot z$, and a relational specification of an algebraic identity is obtained by flattening the parse trees of algebraic expressions while memoising subexpressions. The unit axioms are more general than those of monoids in that the order of quantifiers is swapped. This allows multiple units in a partial algebra, and different left and right units for each element, for instance, like in (small) categories. The precise relationship to categories, and equivalent axiomatisations of relational monoids with unit axioms more similar to those of arrows-only categories [ML98], are discussed in [CDS20b]. Similar axioms have also been used by Rosenthal [Ros97] who has proved a special case of the following lifting result.

Theorem 11(a) below does not hold for quantales but does for proto-quantales. {defi} A proto-quantale is a quantale in which composition need not be associative.

Within this theorem, which has once more been verified by Isabelle, and beyond we refer to algebraic structures ${\mathcal{Q}}^{\mathcal{A}}$ that arise from the quantale liftings of suitable relational structures $\mathcal{A}$ as convolution algebras.

Theorem 11**.**

In each ${\mathcal{Q}}^{\mathcal{A}}$ below, take composition as convolution $\ast_{R}$ and suprema and infima to be the pointwise liftings of those in ${\mathcal{Q}}$.

1. (a)

Let $X$ be a set and $R\subseteq X\times X\times X$. If ${\mathcal{Q}}$ is a proto-quantale, then so is ${\mathcal{Q}}^{X}$. 2. (b)

Let ${\mathcal{X}}$ be a relational semigroup. If ${\mathcal{Q}}$ is a quantale, then so is ${\mathcal{Q}}^{\mathcal{X}}$. 3. (c)

Let ${\mathcal{Y}}$ be a relational monoid. If ${\mathcal{Q}}$ is a unital quantale, then so is ${\mathcal{Q}}^{\mathcal{Y}}$ with unit $\mathsf{id}$.

These lifting results extend to distributive and boolean quantales. Proofs can be found in our Isabelle theories.

Finally, it is natural to consider the law $\forall x,y,z.\ R\,x\,y\,z\Rightarrow R\,x\,z\,y$, although it plays no further role in this study. A relational semigroup is abelian if this relational commutativity law holds; we call a quantale abelian if the underlying semigroup is. We have verified with Isabelle that, if ${\mathcal{S}}$ is an abelian relational semigroup, then ${\mathcal{Q}}^{\mathcal{S}}$ is an abelian quantale whenever ${\mathcal{Q}}$ is. In particular, the convolution of quantale-valued functions from an abelian relational semigroup is commutative. In addition, we have proved lifting results to abelian quantales similar to those in Theorem 11. These are relevant to separation logic [DGS15].

Quantales guarantee that infinite sums or suprema exist. In other situations, a restriction to finite sums is possible.

{defi}

A relation $R\subseteq X\times Y\times Z$ is finitely decomposable if for all $x$ there are finitely many $y$ and $z$ such that $R\,x\,y\,z$ holds. A relational semigroup or monoid is finitely decomposable whenever its relation is.

This notion adapts the notions of the same name for semigroups and monoids as well as the topological concept of locally finite collections, and local finiteness of incidence algebras in order theory [Rot64]. Theorem 11 then specialises to semirings. On the one hand, these are essentially rings without additive inverses, that is, the additive reducts of semirings are abelian monoids, but not necessarily abelian groups. On the other hand, they can be seen as quantales in which finite suprema are replaced by (non-idempotent) sums, whereas infinite sums or infima need not exist.

Corollary 12**.**

Let ${\mathcal{S}}$ be a finitely decomposable semigroup (monoid). If ${\mathcal{R}}$ is a (unital) semiring, then so is ${\mathcal{R}}^{\mathcal{S}}$.

By finite decomposability, all sums in convolutions $(f\ast g)\,x$ are finite and can thus be taken over semirings without convergence issues. Alternatively one could require that $f$ and $g$ have finite support. For an extension of this lifting result to Kleene algebras see [CDS20a].

Finally, the relation $R\subseteq X\times X\times X$ can be recovered in ${\mathcal{Q}}^{X}$. The following lemma has not been formalised with Isabelle. We therefore provide a proof.

Lemma 13**.**

A relational monoid ${\mathcal{Y}}$ can be embedded into ${\mathcal{Q}}^{\mathcal{Y}}$ for any unital quantale ${\mathcal{Q}}$.

Proof 4.3**.**

With $\delta$ as defined above, we have $(\delta\,y\ast\delta\,z)\,x=\bigsqcup_{v,w}^{R\,x\,v\,w}\delta\,y\,v\cdot\delta\,z\,w$ and it follows that $((\delta\,y\ast\delta\,z)\,x=\delta\,x\,x)\Leftrightarrow R\,x\,y\,z$, which implies $((\delta\,y\ast\delta\,z)=\delta\,x)\Leftrightarrow R\,x\,y\,z$. Hence consider the relation $S\subseteq{\mathcal{Q}}^{\mathcal{Y}}\times{\mathcal{Q}}^{\mathcal{Y}}\times{\mathcal{Q}}^{\mathcal{Y}}$ defined by $S\,f\,g\,h\Leftrightarrow f=g\ast h$. Then $\delta:{\mathcal{Y}}\to{\mathcal{Q}}^{\mathcal{Y}}$ is the desired (relational) embedding, because, by definition, $R\,x\,y\,z\Leftrightarrow S\,(\delta\,x)\,(\delta\,y)\,(\delta\,z)$. The function $\delta$ is injective because if $\delta\,x\,z=\delta\,y\,z$ holds for all $z$, then $x=y$. The embedding extends to relational monoids because $\delta$ maps every $e\in\xi$ to the identity of the convolution, $\mathsf{id}:{\mathcal{Y}}\to{\mathcal{Q}}$.

5. Non-Associative Lambek Calculus and Residuation

Non-associative binary modalities are well known from substructural logics such as the non-associative Lambek calculus [MR12], which forms a precursor to and fragment of more expressive categorical and linear logics. In this case, binary modalities are interpreted over ternary Kripke frames $R\subseteq X\times X\times X$. These are sometimes presented as multi-operations or hyper-operations of type $X\to X\to\mathcal{P}\,X$, which are isomorphic to ternary relations [GL06]. In any quantale ${\mathcal{Q}}$, two residuation operations, $\backslash$ and $/$ can be defined for all $u,v,w\in{\mathcal{Q}}$, by the Galois connections

[TABLE]

In addition to a binary product modality similar to $f\ast g$, where $f$ and $g$ are predicates, hence functions of type $X\to\mathbb{B}$, two residual modalities $f\backslash g$ and $f/g$ can be defined. In our setting, conflating syntax and semantics, these generalise to

[TABLE]

In the non-associative Lambek calculus, these lift from the propositional logic to the modal level. We obtain a more general result for convolution algebras in our Isabelle theories.

Proposition 14**.**

Let $R\subseteq X\times Y\times Z$ and let $f:X\to{\mathcal{Q}}$, $g:Y\to{\mathcal{Q}}$ and $h:Z\to{\mathcal{Q}}$ be functions into a quantale ${\mathcal{Q}}$. Then,

[TABLE]

In the correspondence theory of the non-associative Lambek calculus, relational associativity laws have already been studied [MR12]. In fact, these can be split into two implications and they are reflected at the modal level. Similarly, one obtains $(f\ast g)\ast h\leq f\ast(g\ast h)$ and its order dual in the convolution algebra [CDS20a].

We also recover the expected relationship between the binary modalities $f\backslash g$ and $f/g$ and unary modal box operators. If the target quantale forms a complete distributive lattice and multiplication coincides with meet, then $f\backslash g$ and $f/g$ correspond to Heyting implications $f\to g$ and $f\leftarrow g$. The two cases are distinguished only by the order of arguments in $R$; they coincide if $R$ is relationally commutative. If in addition the lattice is complemented and $c_{0}:Z\to{\mathcal{Q}}$ defined by $c_{0}\,z=0$ for all $z\in Z$, then with $S\,x\,y\Leftrightarrow\exists z.\ R\,z\,y\,x$,

[TABLE]

The backward box can be obtained from $c_{0}/f$ by conversion duality. Deeper investigations of convolution algebras with relational residuations in other substructural logics, in particular linear ones, are left for future work.

Modal correspondence theory also studies relational properties induced by modal ones (conversely to the completeness-like properties in Section 4). To show that associativity of relational convolution implies relational associativity, for instance, one can assume that the latter fails and show that this makes the former fail as well. To this end it suffices to check that the relation $R$ in the proof of Lemma 7(b) violates the relational associativity law, which is routine. Proofs related to commutativity and units are similar. Full soundness and completeness proofs for the Lambek calculus with respect to a relational semantics have been given by MacCaull [Mac98], see also [AM94]. For our convolution algebras, there are two additional correspondences: properties of ${\mathcal{Q}}^{X}$ and ${\mathcal{Q}}$ lead to properties of $X$; those of ${\mathcal{Q}}^{X}$ and $X$ lead to properties of ${\mathcal{Q}}$, under certain nondegeneracy assumptions on elements of ${\mathcal{Q}}$ and $X$, respectively [CDS20a]. These results are not needed for this article.

6. Partial Semigroups as Relational Semigroups

This section links relational convolution with more conventional notions, as investigated in  [DHS16]. Algebraic semantics for categorical and linear logics are well known (see [AD93, Dos92, AM94] for early examples). We generalise in two ways by considering partial algebras and quantale-valued functions instead of boolean-values ones. Lifting results for functions from partial semigroups and monoids into convolution algebras formed by quantales are not new [DHS16]. Thus it remains to explain how partial algebras correspond to their relational counterparts. All results in this section have been verified with Isabelle.

{defi}

A partial semigroup is a structure ${\mathcal{S}}=(X,\cdot,D)$ such that $X$ is a set, $D\subseteq X\times X$ the domain of composition and $\cdot:D\to X$ a partial operation of composition. Composition is associative, $x\cdot(y\cdot z)=(x\cdot y)\cdot z$, with respect to Kleene equality in the sense that if either side of the equation is defined then so is the other and, in that case, both sides are equal. Formally,

[TABLE]

{defi}

A partial monoid is a structure ${\mathcal{M}}=(X,\cdot,D,E)$ such that $(X,\cdot,D)$ is a partial semigroup and $E\subseteq X$ a set of (generalised) units that satisfy

[TABLE]

Every monoid $(X,\cdot,1)$ is a partial monoid with $D=X\times X$ and $E=\{1\}$. Partial monoids are also related to categories. More specifically, an object-free category [ML98] is a partial monoid in which $(x\cdot y)\cdot z$ is defined if and only if $x\cdot y$ and $y\cdot z$ are both defined. More generally, partial semigroups are relational semigroups that are functional in the sense that for each $y$ and $z$ there is at most one $x$ such that $R\,x\,y\,z$; see [CDS20a] for further information. This is the case because the result of the associated multi-operation is either a singleton set or empty.

Lemma 15**.**

Let $R=\lambda x,y,z.\ D\,y\,z\wedge x=y\cdot z$.

1. (a)

If $(X,\cdot,D)$ is a partial semigroup, then $(X,R)$ is a relational semigroup. 2. (b)

If $(X,\cdot,D,E)$ is a partial monoid, then $(X,R,E)$ is a relational monoid.

This immediately yields a previous lifting construction to a convolution algebra for functions from partial semigroups into quantales [DHS16] as a corollary to Theorem 11.

Corollary 16**.**

1. (a)

Let ${\mathcal{S}}$ be a partial semigroup. If ${\mathcal{Q}}$ is a quantale, then so is ${\mathcal{Q}}^{\mathcal{S}}$. 2. (b)

Let ${\mathcal{M}}$ be a partial monoid. If ${\mathcal{Q}}$ is a unital quantale, then so is ${\mathcal{Q}}^{\mathcal{M}}$.

Again, our Isabelle theories show that these results extend to distributive or boolean quantales. Relational convolution now specialises to the more conventional convolution operation. Using $x=y\cdot z$ to indicate that $y\cdot z$ is both defined and equal to $x$, we obtain:

[TABLE]

For the free semigroup $X^{+}$ or the free monoid $X^{\ast}$ over a finite set $X$, the associated relation $\lambda x,y,z.\ x=y\cdot z$ is finitely decomposable. As in Corollary 12, the sum in the convolution can then be taken over an arbitrary semiring ${\mathcal{R}}$. In formal language theory, functions ${\mathcal{R}}^{X^{+}}$ or ${\mathcal{R}}^{X^{\ast}}$ are known as formal power series [BR84]. These are to weighted automata, what languages are to ordinary finite state machines. Languages, in particular, correspond to functions from $X^{+}$ or $X^{\ast}$ into the semiring of booleans. In this special case, convolution reduces to language product.

Finally we present three example constructions that are needed in the sequel.

{exa}

[Ordered Pairs] If $X$ is a set, then $(X\times X,\cdot,D,E)$ is a partial monoid with

[TABLE]

where $\pi_{1}$ and $\pi_{2}$ are the standard projections. The cartesian fusion product $(x_{1},x_{2})\cdot(y_{1},y_{2})$ thus composes two ordered pairs whenever $x_{2}=y_{1}$. This algebra on ordered pairs is known as pair groupoid. It has been used by Heisenberg in his original presentation of matrix mechanics [Con95]. In particular, $\mathbb{B}^{X\times X}$ is the quantale of binary relations with convolution as relational composition, $\mathbb{Q}^{X\times X}$ is the quantale of $Q$-valued relations which Goguen introduced to fuzzy logic [Gog67]. ∎

{exa}

[Partial Monoid Product]

If $(X,\odot,D_{\odot},E_{\odot})$ and $(Y,\otimes,D_{\otimes},E_{\otimes})$ are partial monoids, then $(X\times Y,\cdot,D,E)$ is a partial monoid with

[TABLE]

{exa}

[Monoid-Set Product]

If $(X,\cdot,D,E)$ is a partial monoid and $Y$ a set, then $(X\times Y,\odot,D^{\prime},E^{\prime})$ is a partial monoid with

[TABLE]

7. Convolution Algebras of Finite Segments and Intervals

Following the general mathematical considerations thus far, we prepare for applications to interval logics. Our starting point is Rota’s incidence algebras of order theory [Rot64], though we do not restrict our attention to locally finite posets, which are finitely decomposable. Instead we focus on quantale-valued functions from partial algebras of segments and intervals, in line with Section 6. In that sense, incidence algebras are convolution algebras that arise from lifting quantale-valued functions from partial semigroups and monoids of segments and intervals.

Rota attributes the idea of interval functions to Dedekind and E. T. Bell. As before, the most important facts in this section have been verified with Isabelle. We have so far restricted our Isabelle formalisation to non-strict closed segments and intervals, that is, segments or intervals of the form $[i,j]$, with point intervals $[i,i]$ included. Formalisations of strict and (semi-)open intervals are routine and would not yield additional insights.

{defi}

A segment of a poset ${\mathcal{P}}$ is an ordered pair $(i,j)$ on ${\mathcal{P}}$ in which $i\leq j$; the segment is strict if $i\neq j$. We write $S({\mathcal{P}})$ for the set of all segments and $S_{s}({\mathcal{P}})$ for the set of all strict segments over ${\mathcal{P}}$. We write $[i,j]$ for the segment $(i,j)$ and write $[i,j]_{s}$ to indicate strictness.

{defi}

A li-poset is a poset $({\mathcal{P}},\leq)$ that satisfies Halpern and Shoham’s linear interval property [HS91]:

[TABLE]

Intuitively, li-posets generalise linear posets in that all intervals over li-posets are linear.

{defi}

A (strict) interval is a (strict) segment of a li-poset.

Example 16 extends immediately to segments.

Lemma 17**.**

Let ${\mathcal{P}}$ be a poset.

1. (a)

$(S_{s}({\mathcal{P}}),\cdot,D)$* forms a partial semigroup of ordered pairs.* 2. (b)

$(S({\mathcal{P}}),\cdot,D,E)$* forms a partial monoid of ordered pairs.*

By segment fusion, therefore, $[i,j]\cdot[j^{\prime},k]=[i,k]$ whenever $j=j^{\prime}$. This is exactly cartesian fusion of ordered pairs. Note that in each pair, the second component must not be smaller than the first one.

The proof of Lemma 9 shows that partial semigroups $S_{s}({\mathcal{P}})$ do not have units. It is now straightforward to lift from $S_{s}({\mathcal{P}})$ and $S({\mathcal{P}})$ to ${\mathcal{Q}}^{S_{s}({\mathcal{P}})}$ and ${\mathcal{Q}}^{S({\mathcal{P}})}$ by virtue of Corollary 16.

Corollary 18**.**

Let ${\mathcal{P}}$ be a poset.

1. (a)

If ${\mathcal{Q}}$ is a quantale, then so is ${\mathcal{Q}}^{S_{s}({\mathcal{P}})}$. 2. (b)

If ${\mathcal{Q}}$ is a unital quantale, then so is ${\mathcal{Q}}^{S({\mathcal{P}})}$.

Relational convolution can now be written, as usual in texts on incidence algebras, as

[TABLE]

Finally, using again a Kronecker delta function, the unit of composition on the incidence algebra is $\delta\,(\pi_{1}\,x)\,(\pi_{2}\,x)$ or, more simply, $\delta\,i\,j$, if $x=[i,j]$. In the case of locally finite posets, and in particular intervals formed over $\mathbb{N}$, Corollary 18 generalises to semirings instead of quantales, as in Corollary 12.

Segments and intervals are often defined as sets instead of pairs. For intervals, the associated partial semigroups or monoids are isomorphic. For each segment $[i,j]$, the function $\sigma\,[i,j]=\{k\in{\mathcal{P}}\mid i\leq k\leq j\}$ is a bijective morphism from the partial semigroup (monoid) of ordered pairs under interval fusion onto that of set-based intervals under the partial composition $x\cup y$, whenever $\mathit{max}\,x=\mathit{min}\,y$. For general segments, however, only $\sigma\,(x\cdot y)\supseteq\sigma\,x\cup\sigma\,y$ always holds, and right-hand sides do not generally form segments. For example, if $x=[i,j]$ and $y=[j,k]$, one may have:

[TABLE]

Using segments as sets is therefore not an option.

Open or semi-open bounded intervals seem less popular in interval logics. It then seems appropriate to compose not by fusion, but by unions provided segments or intervals are adjacent, but non-overlapping. Such more general segments can be modelled by a direct product construction like in Example 16. We outline this construction below; an Isabelle formalisation is left as future work.

Using the constants $o$ and $c$ to indicate whether boundaries of segments are open or closed, an open segment $(i,j)$ can be represented by the pair $([i,j],(o,o))$, a semi-open segment $(i,j]$ by $([i,j],(o,c))$, a semi-open segment $[i,j)$ by $([i,j],(c,o))$ and a closed segment $[i,j]$ by $([i,j],(c,c))$.

Partial semigroups for strict segments can be constructed from these. Elements $([i,i],(c,o))$ and $([i,i],(o,c))$ correspond to the empty segment, which is the unit of composition in the product monoid; for instance, $[1,3)\cdot[3,3)=[1,3)$ and $[1,3]\cdot(3,3]=[1,3]$.

Lemma 19**.**

1. (a)

Let $C=\{o,c\}$. Then ${\mathcal{C}}=(C\times C,\bullet,D_{\bullet},E_{\bullet})$ is a partial monoid of ordered pairs with

[TABLE] 2. (b)

$S({\mathcal{P}})\times{\mathcal{C}}$* is a partial product monoid with composition, domain of definition and set of units defined as in Example 16.*

Elements $([i,i],(o,o))$, however, shrink segments—$[1,3]\cdot(3,3)=[1,3)$ by definition—and therefore seem undesirable in the algebra. Fortunately, no element $([i,i],(o,o))$ can be decomposed into a product of other elements of the product algebra, and these elements can therefore be neglected.

Lemma 20**.**

$(S({\mathcal{P}})\times{\mathcal{C}})-\{([i,i],(o,o))\mid i\in{\mathcal{P}}\}$* forms a partial submonoid of $S({\mathcal{P}})\times{\mathcal{C}}$.*

The lifting to convolution algebras then proceeds as usual by Corollary 16.

8. Partial Semigroups of Closed and Semi-Open Segments

Convolution can be adapted to infinite objects such as infinite words or streams and, consequently, to semi-infinite intervals $[i,\infty]$ without upper bounds [DHS16]. This extension supports applications in interval temporal logics and duration calculi. The following two sections present an alternative to our previous approach that is based on well known semigroup constructions.

The notion of an action of a semigroup or monoid on a set, or on another semigroup or monoid, is standard. First we adapt it to partiality.

{defi}

A (left) action of a partial semigroup ${\mathcal{S}}=(S,\odot,D_{\odot})$ on a partial semigroup ${\mathcal{T}}=(T,\oplus,D_{\oplus})$ is a partial operation $\circ:D_{\circ}\to T$, where $D_{\circ}\subseteq S\times T$, that satisfies

[TABLE]

If $(S,\odot,D_{\odot},E_{\odot})$ is a partial monoid, then the left action also satisfies the left unit axiom

[TABLE]

If $(T,\oplus,D_{\oplus},E_{\oplus})$ is a partial monoid, then the following right annihilation axiom also holds:

[TABLE]

In our intended applications, ${\mathcal{S}}$ and ${\mathcal{T}}$ represent different behaviours of a system encoded in terms of pairs $(s,t)\in{\mathcal{S}}\times{\mathcal{T}}$. These could be finite or infinite behaviours, non-faulting or faulting ones or, as in our context, closed or semi-open intervals or segments, including those with infinite chains.

More concretely, we consider ${\mathcal{S}}$ to be a partial monoid of closed finite segments and ${\mathcal{T}}$ a (partial) monoid of semi-open segments $[i,j)$. For convenience, we may include segments $[i,\infty)$ and $[i,\infty]$, which are obtained by adding an element $\infty$ that is greater than any element of the underlying poset whenever such an element does not exist. A typical example is formed by the extended non-negative reals $\mathbb{R}_{+}^{\infty}$. General intervals, as in Section 7, would require a more tedious nested product construction.

In this setting, multiplication $\odot$ models fusion of closed segments, as usual. Action $s\circ t$ represents the fusion of a closed segment $s$ with a semi-open segment $t$. The use of partial semigroup actions and the clear typing of closed and semi-open segments rule out that semi-open segments are fused with closed or other semi-open ones.

A similar construction on the free monoid $X^{\ast}$ and the set $X^{\omega}$ models the compositions of finite and infinite words, albeit in a simpler total setting.

Next, in order to construct convolution algebras for such mixed behaviours, we need to encode their algebras, and in particular those of closed and semi segments, as partial semigroups. To this end, we adapt the well known semidirect product construction of two semigroups or monoids [CP61].

{defi}

For every action of a partial semigroup or partial monoid ${\mathcal{S}}$ on a partial semigroup ${\mathcal{T}}$, the semidirect product ${\mathcal{S}}\ltimes{\mathcal{T}}=(S\times T,\ltimes,D_{\ltimes})$ of ${\mathcal{S}}$ and ${\mathcal{T}}$ with $\ltimes:D_{\ltimes}\to S\times T$ and $D_{\ltimes}\subseteq(S\times T)\times(S\times T)$ is defined by

[TABLE]

If ${\mathcal{S}}$ and ${\mathcal{T}}$ are both partial monoids with sets of units $E_{\odot}$ and $E_{\oplus}$, respectively, then ${\mathcal{S}}\ltimes{\mathcal{T}}=(S\times T,\ltimes,D_{\ltimes},E_{\ltimes})$ with $E_{\ltimes}=E_{\odot}\times E_{\oplus}$.

The following fact has been verified with Isabelle.

Proposition 21**.**

If ${\mathcal{S}}$ and ${\mathcal{T}}$ are partial semigroups (monoids), then so is ${\mathcal{S}}\ltimes{\mathcal{T}}$.

Since we are mainly interested in purely closed segments $(s,0)$ and purely semi-open segments $(0,t)$, we add an element [math] as an annihilator to ${\mathcal{S}}$ that denotes the empty closed segment. By definition it satisfies

[TABLE]

The use of $\oplus$ in semidirect products requires that we explain this operation on ${\mathcal{T}}$ in the instance of semi-open segments. In the context of convolution, where semi-open segments $(0,t)$ are split with respect to $\ltimes$, into all combinations $(0,t)=(0,t_{1}\oplus s_{1}\circ t_{2})=(s_{1},t_{1})\ltimes(0,t_{2})$, it seems reasonable to assume that a split produces either $(0,t_{1})$ or $(0,s_{1}\circ t_{2})$. For this we assume that $\oplus$ is not only associative, but (also commutative and) selective: $t_{1}\oplus t_{2}\in\{t_{1},t_{2}\}$ for all $t_{1},t_{2}\in{\mathcal{T}}$. The unit [math] in ${\mathcal{T}}$ then represents the empty semi-open segment. Consequently, $s\circ 0=0$ holds by definition of partial monoid actions.

The following example checks that semidirect products of pure closed and semi-open segments yield the intended behaviour.

{exa}

1. (a)

$(s_{1},0)\ltimes(s_{2},0)=(s_{1}\odot s_{2},0)$, whenever fusion $s_{1}\odot s_{2}$ is defined. Hence, the semidirect product of two closed segments is their fusion, as expected. 2. (b)

$(0,t_{1})\ltimes(0,t_{2})=(0,t_{1})$, which is always defined, Hence, the fusion of a first semi-open segment with a second one simply yields the first segment. This is reasonable because one cannot fuse a semi-open segment with any other one. 3. (c)

$(s,0)\ltimes(0,t)=(0,s\circ t)$, whenever $s\circ t$ is defined. In this case, the closed segment is fused with the semi-open segment, as expected. 4. (d)

$(0,t)\ltimes(s,0)=(0,t)$, for the same reason as in (b). 5. (e)

Finally, $(s_{1},t_{1})\ltimes(s_{2},t_{2})$ equals either $(s_{1}\odot s_{2},t_{1})$ or $(s_{1}\odot s_{2},s_{1}\circ t_{2})$ by selectivity.∎

Based on these calculations, it is even simpler to check that semidirect products of finite and infinite words in $X^{\ast}$ and $X^{\omega}$ model their compositions as expected.

9. Convolution Algebras of Closed and Semi-Open Segments

We now construct convolution algebras over partial semigroups of closed and semi-open segments. A simplistic approach might attempt using the partial semigroups and monoids from Proposition 21 together with Corollary 16. However, this would misrepresent the most suitable splitting of semi-open segments, intervals or words in convolutions and therefore the most natural convolution algebra.

{exa}

Let $f\,x$ state that word $x\in X^{\ast}\cup X^{\omega}$ is an element of language $f:X^{\ast}\cup X^{\omega}\to\mathbb{B}$. Then $(f\ast g)\,x=1$ if and only if $x$ is in the language product of $f$ and $g$. For infinite $x$ this holds if either $f\,x=1$ or $x$ can be split into some finite $y$ and infinite $z$ such that $f\,y=1$ and $g\,z=1$. This generalises to segments and intervals.∎

In [DHS16] we have redefined convolution in order to handle this situation. The convolution algebra then becomes a weak quantale. {defi} A quantale is weak if the left distributivity law $x\cdot\bigsqcup Y=\bigsqcup_{y\in Y}x\cdot y$ holds only for $Y\neq\emptyset$ and hence [math] is no longer a right annihilator.

{exa}

In the language algebra $\mathbb{B}^{X^{\ast}\cup X^{\omega}}$, products $f\ast 0$ with the empty language [math] yield the set of all infinite words in $f$ by definition, but not necessarily [math]. Once more this generalises to segments and intervals.∎

Here, instead of redefining convolution, we adjust the target algebra $\mathcal{A}$ of functions ${\mathcal{S}}\ltimes{\mathcal{T}}\to\mathcal{A}$ in such a way that the splitting of segments according to $\ltimes$ is reflected in $\mathcal{A}$. In addition, it seems reasonable to assume that elements of ${\mathcal{S}}$ are evaluated by a quantalic structure in $\mathcal{A}$ and a complete lattice structure ${\mathcal{T}}$. Elements in ${\mathcal{T}}$ thus cannot be composed intrinsically by a multiplication. However, suprema are needed for convolution. This leads to the following definition. {defi} A quantale module [AV93] of a quantale ${\mathcal{Q}}=(Q,\leq_{\mathcal{Q}},\cdot)$ and a complete lattice ${\mathcal{L}}=(L,\leq_{\mathcal{L}})$ is an action $\circ:{\mathcal{Q}}\to{\mathcal{L}}\to{\mathcal{L}}$ that satisfies, for all $u,v\in Q$, $x\in L$, $V\subseteq Q$ and $X\subseteq L$,

[TABLE]

If ${\mathcal{Q}}$ is unital, then, in addition, $1\circ x=x$.

Obviously, every quantale defines a quantale module on itself with multiplication as action. A semidirect product can be defined on ${\mathcal{Q}}$ and ${\mathcal{L}}$ as usual as

[TABLE]

We can then verify the following counterpart of Proposition 21 with Isabelle.

Proposition 22**.**

Let ${\mathcal{Q}}$ be a (unital) quantale and ${\mathcal{L}}$ a complete lattice. Then ${\mathcal{Q}}\ltimes{\mathcal{L}}$ forms a weak (unital) quantale in which the left distributivity law is weakened to

[TABLE]

and where the lattice order and operations are defined as for ${\mathcal{Q}}\times{\mathcal{L}}$.

The multiplicative unit of ${\mathcal{Q}}\ltimes{\mathcal{L}}$ is $(1,0)$, where $1$ is the unit of ${\mathcal{Q}}$ and [math] the least element in ${\mathcal{L}}$. {exa} As a counterexample to full left distributivity, hence right annihilation, let the unital quantale defined by $0\leq\top$ with $1=\top$ act on itself. Note that multiplication is fixed. Then, $(0,\top)\ltimes\bigsqcup\emptyset=(0,\top)\ltimes(0,0)=(0\cdot 0,1\sqcup 1\circ 0)=(0,1\sqcup 0)=(0,1)\neq(0,0).$∎

Before completing the construction of the convolution algebra we check that our constructions are consistent with Example 9.

{exa}

Let $S_{\rm c}({\mathcal{P}})$ and $S_{\rm so}({\mathcal{P}})$ denote the closed and semi-open segments for poset ${\mathcal{P}}$ respectively. Assume that functions $f:S_{\rm c}({\mathcal{P}})\ltimes S_{\rm so}({\mathcal{P}})\to{\mathcal{Q}}\ltimes{\mathcal{L}}$ are given by pairs $f=(f_{\rm c},f_{\rm so})$ such that $f\,(s,t)=(f_{\rm c}\,s,f_{\rm so}\,t)$ and that $f_{\rm c}\,0=0$ and $f_{\rm so}\,0=0$. For the sake of simplicity, we further assume that ${\mathcal{Q}}={\mathcal{L}}$, in which case the action is quantale multiplication.

• •

Convolutions over closed segments split only on $S_{\rm c}({\mathcal{P}})$:

[TABLE]

This recovers the standard convolution of closed segments restricted to $f_{\rm c}$ and $g_{\rm c}$.

• •

A semi-open segment $(0,y)$ is split by convolution into pairs $(x_{1},y_{1})$ and $(0,y_{2})$, and hence, $y=y_{1}\sqcup x_{1}\circ y_{2}$. Therefore either $y=y_{1}$ or $y=x_{1}\circ y_{2}$ by selectivity and therefore

[TABLE]

This is consistent with our previous treatment of convolution [DHS16].∎ The following generalisations of Corollary 16, which we have verified with Isabelle, characterise the convolution algebras of finite and infinite segments and intervals. The first statement is generic for partial semigroups and weak quantales.

Theorem 23**.**

Let ${\mathcal{Q}}$ be a weak quantale.

1. (a)

If ${\mathcal{S}}$ is a partial semigroup, then ${\mathcal{Q}}^{\mathcal{S}}$ is a weak proto-quantale. 2. (b)

If ${\mathcal{M}}$ is a partial monoid, then ${\mathcal{Q}}^{\mathcal{M}}$ is a weak quantale. 3. (c)

If ${\mathcal{Q}}$ is unital, then $\mathsf{id}$ is a left unit in ${\mathcal{Q}}^{\mathcal{S}}$, but not necessarily a right unit.

{exa}

Consider the weak unital quantale defined by $0\leq 1\leq\top$ and by multiplication $0\cdot u=0$, $\top\cdot u=\top$.

1. (a)

As a counterexample to associativity, consider this quantale with the partial semigroup $\{a,b\}$ where $a^{2}=b$ is the only composition defined, and let $f\ a=f\,b=\top$. With $f^{2}=(f\ast f)$, thus $(f\ast f^{2})\,b=f\,a\cdot f^{2}\,a=\top\cdot 0=\top\neq 0=0\cdot\top=f^{2}\,a\cdot f\,a=(f^{2}\ast f)\,b.$ 2. (b)

As a counterexample to the right unit law, consider this quantale with the (total) monoid $\{a,1\}$, where multiplication is defined by $a^{2}=a$. Let $f\,a=\top$ and $f\,1=1$. Then $(f\ast\mathsf{id})\,1=f\,1\cdot\mathsf{id}\,1\sqcup f\,a\cdot\mathsf{id}\,a=1\cdot 1\sqcup\top\cdot 0=1\sqcup\top=\top\neq 1=f\,1.$ ∎

Intuitively, associativity may fail for partial semigroups because not all elements can be split in such structures. Suprema in convolutions may thus become empty and associativity fails due to the lack of right annihilation. By contrast, the units in partial monoids guarantee that all elements can be split.

The second statement considers semidirect products, but is still general.

Proposition 24**.**

Let ${\mathcal{Q}}$ be a quantale and ${\mathcal{L}}$ a complete lattice.

1. (a)

If ${\mathcal{S}}$ and ${\mathcal{T}}$ are partial semigroups, then $({\mathcal{Q}}\ltimes{\mathcal{L}})^{{\mathcal{S}}\ltimes{\mathcal{T}}}$ is a weak proto-quantale. 2. (b)

If ${\mathcal{S}}$ and ${\mathcal{T}}$ are partial monoids, then $({\mathcal{Q}}\ltimes{\mathcal{L}})^{{\mathcal{S}}\ltimes{\mathcal{T}}}$ is a weak quantale. 3. (c)

If, in addition, ${\mathcal{Q}}$ is unital, then so is $({\mathcal{Q}}\ltimes{\mathcal{L}})^{{\mathcal{S}}\ltimes{\mathcal{T}}}$. 4. (d)

In each case, the subquantale ${\mathcal{Q}}^{\mathcal{S}}\simeq({\mathcal{Q}}\ltimes\{0\})^{{\mathcal{S}}\ltimes\{0\}}$ is embedded into $({\mathcal{Q}}\ltimes{\mathcal{L}})^{{\mathcal{S}}\ltimes{\mathcal{T}}}$.

Proof 9.1**.**

Apart from the right unit law, all properties follow immediately from Theorem 23 with Propositions 21 and 22.

The right unit law has not been checked with Isabelle (this would be rather tedious), so we provide a proof. Because the unit in ${\mathcal{Q}}\times{\mathcal{L}}$ is $(1,0)$, the unit $\mathsf{id}$ on $({\mathcal{Q}}\ltimes{\mathcal{L}})^{{\mathcal{S}}\ltimes{\mathcal{T}}}$ must map each pair $(s,t)$ to $(1,0)$ if $s$ is a monoidal unit segment and $t=0$, and to $(0,0)$ otherwise, hence $\mathsf{id}=(\mathsf{id},\lambda x.\ 0)$. We calculate

[TABLE]

Finally, it is routine to verify (d) in all cases considered.

{exa}

The failure of right annihilation with the function $0=(\lambda x.\ 0,\lambda x.\ 0)$ can be checked by using the calculation in Example 9(b):

[TABLE]

whenever $f_{\rm so}\,t\neq 0$. ∎

Do Theorem 23(a) or Proposition 24(a) rule out associativity of composition in convolution algebras over partial semigroups of strict segments and intervals? The pragmatic answer is no. By construction, only splittings of semi-open segments or intervals can affect associativity (otherwise Corollary 16 would already fail). Yet even unbounded intervals $[i,\infty)$ over $\mathbb{N}$ can always be split finitely many times into finite prefixes and infinite suffixes. A formalisation of such results with Isabelle is left for future work.

10. Modalities over Segments

The remaining technical sections relate the abstract approach to segments and their incidence or convolution algebras with well known interval logics. Binary relationships between intervals were first proposed by Allen [All83]; a binary modality based on chopping intervals has been introduced by Moszkowski [MM83]. The modal logics that arise from such relationships have been studied by Halpern and Shoham [HS91] (who consider unary modalities only) and [Ven90, Ven91] (who considers binary modalities including chop as well). Decidability, undecidability and completeness of various fragments including neighbourhood logic (see Section 12) have been studied extensively [ZH04, MM11, MGMS11]. We refer to some excellent surveys [MGMS11, GMS04, Kon13] for more information.

This section outlines how semantics for the interval logics of Halpern and Shoham [HS91], and Venema [Ven90] arise as instances of the convolution algebras developed in previous sections. Our constructions start from partial monoids of strict closed segments over arbitrary partial orders, yet the approach is modular with respect to adaptations to partial semigroups of non-strict segments and to instantiations to algebras of strict or non-strict intervals, as in Section 7. It is also generic with respect to discrete, dense or Dedekind-complete orders.

The unary and binary interval modalities that form our convolution algebras are more general as well. As in Sections 2 and 3, they are based on lattice-valued or quantale-valued functions that admit quantitative interpretations beyond the standard qualitative ones. As we disregard concrete syntax in this and the following sections, our algebraic semantics are loose: they are not generated by homomorphic extensions of semantic maps from (finite) sets of atomic functions or predicates and restricted sets of operations. Instead they are given by full convolution algebras formed by all functions or predicates of a certain type. More precise semantics usually arise as subalgebras induced by homomorphic images. Typical examples are subalgebras that are closed under the semiring operations, but not with respect to arbitrary infima and suprema.

We first describe relations for segments analogous to those in Allen’s interval calculus [All83]. These in turn lead to algebraic companions of Halpern and Shoham’s and Venema’s interval logics [HS91, Ven90] (for segments). Allen’s relations can be based on a single ternary relation.

Possible relationships between segments $x$ and $y$ are illustrated in Figures 2 and 2, recalling that relation ${R}^{\smallsmile}$ is the converse of $R$. Like Goranko et al. [GMS04], we write ${\sf B}$, ${\sf E}$ and ${\sf A}$ for the beginning, end and after relationships, and ${\sf D}$, ${\sf O}$ and ${\sf L}$ for the during, overlapping and later relationships. Figure 2 provides an informal semantics for these. As ${\sf D}$, ${\sf O}$ and ${\sf L}$ can be defined in terms of ${\sf B}$, ${\sf E}$ and ${\sf A}$ (see below), we discuss the latter three first.

Lemma 25**.**

Consider the partial semigroup $(S({\mathcal{P}}),\cdot,D)$ of segments (strict or non-strict) over the poset ${\mathcal{P}}$ as a relational semigroup $({\mathcal{P}},{\sf C})$ with

[TABLE]

like in Lemma 15. Then

[TABLE]

Proof 10.1**.**

From the definition of ${\sf C}$, ${\sf B}\,x\,y\Leftrightarrow\exists z.\ D\,y\,z\land x=y\cdot z$, that is, $y$ is indeed a beginning segment within $x$. Similarly, ${\sf E}\,x\,y\Leftrightarrow\exists z.\ D\,z\,y\land x=z\cdot y$, that is, $y$ is indeed an ending segment within $x$. Finally, ${\sf A}\,x\,y\Leftrightarrow\exists z.\ D\,x\,y\land z=x\cdot y$, that is, segment $y$ comes immediately after segment $x$, hence can be composed into a segment $z$. More formally, these definitions are faithful with respect to those in [GMS04] when specialised to intervals.

Further, following [MGMS11, GMS04], we (re)define

[TABLE]

Next we show how the partial and relational semigroups and the Allen-style segment relations introduced above yield a semantics for generalised unary Halpern-Shoham modalities over segment functions in the context of incidence or convolution algebras. Because forward and backward modalities are both available, modalities corresponding to the relations in Fig. 2 can be defined by using only ${\sf B}$, ${\sf E}$ and ${\sf A}$.

For a segment $x\in S({\mathcal{P}})$ and quantale-valued function $f:S({\mathcal{P}})\to{\mathcal{Q}}$, the intended semantics is as follows:

• •

\mathop{\big{|}{\sf B}\big{\rangle}}f\,x means that $f$ is applied to some beginning segment $y$ of $x$:

[TABLE]

• •

\mathop{\big{|}{\sf E}\big{\rangle}}f\,x means that $f$ is applied to some ending segment $y$ of $x$:

[TABLE]

• •

\mathop{\big{|}{\sf A}\big{\rangle}}f\,x means that $f$ is applied to some segment $y$ that starts precisely where $x$ ends:

[TABLE]

These equations expand the definitions of unary modalities in Section 2.

By opposition duality, \mathop{\big{\langle}{\sf B}\,\big{|}}\,f\,x means that $f$ is applied to some segment of which $x$ is a beginning, \mathop{\big{\langle}E\,\big{|}}\,f\,x that $f$ is applied to some segment of which $x$ is an ending, and \mathop{\big{\langle}{\sf A}\,\big{|}}\,f\,x that $f$ is applied to some segment that ends precisely where $x$ begins. The standard interval semantics can be obtained as before by instantiating $S({\mathcal{P}})$ to li-posets (Definition 7) and ${\mathcal{Q}}$ to $\mathbb{B}$. Once again this is consistent with Section 2.

Next we show how Venema’s binary interval modalities $\textrm{V\!}_{C}$, $\textrm{V\!}_{D}$ and $\textrm{V\!}_{T}$ [Ven91] arise in convolution algebras222We use non-standard notation in order to avoid conflicts within this article.. These are needed in interval logics because no finite set of unary interval operators can be functionally complete over over dense orders [Ven90]. The modality $\textrm{V\!}_{C}$, in particular, corresponds to ITL’s chop operator. Like in Lemma 5, we then show how Halpern and Shoham’s unary interval modalities can be obtained from Venema’s binary ones by restricting relational convolution.

For predicates $f$ and $g$, the semantics of $\textrm{V\!}_{C}$, $\textrm{V\!}_{D}$ and $\textrm{V\!}_{T}$ can be described as follows:

• •

$\textrm{V\!}_{C}\,f\,g\,x=1$ iff there are segments $y$ and $z$ such that $x=y\cdot z$ and $f\,y=g\,z=1$;

• •

$\textrm{V\!}_{D}\,f\,g\,x=1$ iff there are segments $y$ and $z$ such that $z=y\cdot x$ and $f\,y=g\,z=1$;

• •

$\textrm{V\!}_{T}\,f\,g\,x=1$ iff there are segments $y$ and $z$ such that $z=x\cdot y$ and $f\,y=g\,z=1$.

The standard interval semantics is obtained as before by instantiating $S({\mathcal{P}})$ to li-posets and ${\mathcal{Q}}$ to $\mathbb{B}$.

Linking this semi-formal semantics with convolution requires ternary relations in the context of a partial semigroup $(S({\mathcal{P}}),\cdot,D)$. These relations are depicted in Fig. 3. Apart from ${\sf C}=\lambda x,y,z.\ D\,y\,z\land x=y\cdot z$, they are defined as

[TABLE]

and they capture permutations of splittings within and in the neighbourhood of a given segment. A convolution-based semantics for generalised Venema modalities is then straightforward.

Lemma 26**.**

For the partial semigroup $(S({\mathcal{P}}),\cdot,D)$ of strict closed segments and functions $f,g:S({\mathcal{P}})\to{\mathcal{Q}}$,

[TABLE]

Proof 10.2**.**

Firstly, $\textrm{V\!}_{C}\,f\,g=\lambda x.\ \bigsqcup_{y,z}^{x=y\cdot z}f\,y\cdot g\,z=f\ast_{\sf C}g$. Secondly, $\textrm{V\!}_{D}\,f\,g=\lambda x.\ \bigsqcup_{y,z}^{z=y\cdot x}f\,y\cdot g\,z=f\ast_{{\sf D}_{\rm v}}g$. Thirdly, $\textrm{V\!}_{T}\,f\,g=\lambda x.\ \bigsqcup_{y,z}^{z=x\cdot y}f\,y\cdot g\,z=f\ast_{{\sf T}_{\rm v}}g$. In each case, the first step is justified by the semi-formal semantics above. Formally, it is easy to show that it is faithful with Venema’s semantics [Ven91] when functions are specialised to predicates and segments to intervals.

It can be shown that none of the three modalities can be defined in terms of permutations and combinations of the other two, and that all other possible permutations of indices are captured by these three. It can also be checked that $({\mathcal{P}},{\sf C})$ forms a relational semigroup, whereas the structures $({\mathcal{P}},\textrm{V\!}_{D})$ and $({\mathcal{P}},\textrm{V\!}_{T})$ do not; and hence the convolutions $\ast_{{\sf D}_{\rm v}}$ and $\ast_{{\sf T}_{\rm v}}$ need not be associative.

Lemma 27**.**

The relations ${\sf C}$, ${\sf D}_{\rm v}$ and ${\sf T}_{\rm v}$ are definable in terms of Allen’s relations (Fig. 2).

[TABLE]

The correspondence between binary and unary modalities captured in Lemma 5 allows us to relate Halpern and Shoham’s modalities with relational convolution.

Lemma 28**.**

For the partial semigroup $(S({\mathcal{P}}),\cdot,D)$ of strict closed segments, $f:S({\mathcal{P}})\to{\mathcal{Q}}$ and $c_{1}=\lambda x.\ 1$, where 1 is the unit in ${\mathcal{Q}}$,

[TABLE]

Proof 10.3**.**

Spelling out the semi-formal semantics above, \mathop{\big{|}{\sf B}\big{\rangle}}f\,x=\bigsqcup_{y,z}^{x=y\cdot z}f\,y\cdot c_{1}\,z, \mathop{\big{|}{\sf E}\big{\rangle}}f\,x=\bigsqcup_{y,z}^{x=y\cdot z}c_{1}\,y\cdot f\,z and \mathop{\big{|}{\sf A}\big{\rangle}}f\,x=\bigsqcup_{y,z}^{z=x\cdot y}f\,y\cdot c_{1}\,z.

Finally, Lemmas 26 and 28 in combination relate Venema’s binary segment modalities with Halpern and Shoham’s unary ones:

[TABLE]

11. Interval Temporal Logic

The generalised segment modalities from Section 10 can be adapted to an algebraic semantics for the interval temporal logic ITL [Mos12, CM16]. We ignore the next-step operator in our considerations, and our semantics is once again loose: it is not generated by a morphism from the ITL syntax. A tighter semantics would require forming a subalgebra in which arbitrary suprema and infima need not exist. This would be more akin to a Kleene algebra without a right annihilator (a.k.a. a weak quantale) than a quantale. Our loose semantics, however, allows for more expressive higher-order variants of ITL with quantification over predicates. We do not elaborate this in detail and focus on the role of convolution instead.

ITL and the duration calculus, which subsumes it (see Section 12), use notions of iteration. These can be defined as fixpoints on every quantale, including weak ones, due to the underlying complete lattice structure and monotonicity of the functions needed. In particular, $x\leq y\Rightarrow z\cdot x\leq z\cdot y$ holds even in weak quantales. Hence least and greatest fixpoints of $\varphi=\lambda x.\ f\cdot x$ and $\psi=\lambda x.\ 1\sqcup f\cdot x$ exist and $f^{\omega}=\nu\varphi$, $f^{\ast}=\mu\psi$, and $f^{\infty}=\nu\psi$ can be used for modelling infinite, finite and potentially infinite iteration on convolution algebras formed by weak quantales in our loose semantics.

ITL uses a notion of program store (or state space) that changes over time within an interval. We model the store dynamics abstractly by streams of type ${\mathcal{P}}\to X$ that map a time domain given by a poset ${\mathcal{P}}$ onto a set $X$, which may be a set of functions from program variables to values. How the variables and values change over time, e.g. by assignment, is not our concern. In our ITL semantics, a predicate $p$ evaluates a stream $\sigma$ over an interval $x$, written as $p\,x\,\sigma$. Only the intervals carry algebraic structure, $X^{\mathcal{P}}$ is merely a set. The global relationship between streams, convolution algebras and ITL is captured as follows.

Proposition 29**.**

Let ${\sf Cl}=S_{\rm c}({\mathcal{P}})$ be a partial monoid of (non-strict) closed segments under fusion and ${\sf Sop}=S_{\rm so}({\mathcal{P}})$ a monoid of semi-open segments. Let $X^{\mathcal{P}}$ be a set of streams, let ${\mathcal{Q}}$ be a unital quantale and ${\mathcal{L}}$ a complete lattice.

1. (a)

${\sf Cl}\times X^{\mathcal{P}}$* is a partial monoid and ${\mathcal{Q}}^{{\sf Cl}\times X^{\mathcal{P}}}$ a unital quantale with convolution as composition.* 2. (b)

$({\sf Cl}\ltimes{\sf Sop})\times X^{\mathcal{P}}$* is a partial monoid and $({\mathcal{Q}}\ltimes{\mathcal{L}})^{({\sf Cl}\ltimes{\sf Sop})\times X^{\mathcal{P}}}$ a weak unital quantale, within which the unital quantale ${\mathcal{Q}}^{{\sf Cl}\times X^{\mathcal{P}}}$ is embedded.*

Proof 11.1**.**

Part (a) is immediate by the product construction in Example 16 and Corollary 16; part (b) follows from Proposition 21 and Proposition 24.

We call the elements of the function spaces segment stream functions. For ${\mathcal{Q}}={\mathcal{L}}=\mathbb{B}$ we obtain (weak) quantales of segment stream predicates as special cases. These describe the logic of ITL in terms of convolution algebras. In the more concrete case of ${\mathcal{P}}=\mathbb{N}$, we may associate ${\sf Cl}$ and ${\sf Sop}$ with finite and semi-infinite intervals $[i,j]$ and $[i,\infty)$ in $\mathbb{N}$. Moreover, the order is locally finite with respect to finite intervals. By Corollary 12, the convolution algebra of finite intervals then forms an idempotent semiring (with respect to addition). Similar observations on the algebra of ITL predicates have been made by Höfner and Möller [HM09, HM08].

We now explain some of the ITL operations in light of Proposition 29 and sketch the most important features of the loose algebraic semantics. It is based on interval stream predicates of type $S_{\rm c}({\rm Nature})\times X^{\rm Nature}\to\mathbb{B}$ over closed, non-strict and finite intervals. With this approach, the ITL semantics of terms or expressions is abstracted into stream functions.

The semantics of boolean operations on predicates is given in Proposition 29(a) by the pointwise liftings in Theorem 11 and Corollary 16, owing to the fact that segment stream functions form partial monoids (Example 16). The semantics of the chop $p\mathbin{\fatsemi}q$ of two predicates $p$ and $q$ is more interesting. According to the ITL semantics, it holds on some interval $x$ if $x$ can be split into some prefix-suffix pair $y$ and $z$ such that $x=y\cdot z$, predicate $p$ holds on the prefix $y$ and $q$ holds on the suffix $z$ [Mos12, CM16]. Hence chop is indeed convolution and it coincides with $\textrm{V\!}_{C}$. Thus,

[TABLE]

where the stream $\sigma:{\rm Nature}\to X$ supplies the store as a function of time within the intervals $y$ and $z$, over which the predicates $p$ and $q$ are evaluated. To obtain the middle expression from $p\ast q$, the convolution is computed over intervals $x$; the product and supremum have been extended pointwise with respect to streams $\sigma$.

The unit predicate is given by $\mathsf{id}\ [i,j]=\delta\,i\,j$, as in Section 7. Intuitively it holds precisely of any point interval. Finally, the ITL semantics of the iteration $p^{*}$, according to which $p^{*}$ holds on interval $x$ if $p$ holds on each interval that results from a finite decomposition of $x$, can be derived from iteration in the target quantale. As the incidence algebra of finite intervals over $\mathbb{N}$ is locally finite, the idempotent semiring, which forms a tight ITL semantics as well as a subalgebra of the quantale described by Proposition 29(a), can be extended to a Kleene algebra to model iteration of ITL predicates. In sum, the convolution algebras of a tight convolution-based semantics for ITL predicates over finite intervals are therefore Kleene algebras.

In the presence of semi-open intervals $S_{\rm so}({\rm Nature})$, the boolean operations are interpreted as outlined, but chop $p\fatsemi q$ is interpreted differently, and the incidence algebra is no longer locally finite. Now, by the standard ITL semantics, either $p$ is evaluated over the entire infinite interval $x$, or the infinite interval $x$ is split into a finite prefix $y$ and an infinite suffix $z$, as in Section 8, and predicate $p$ is evaluated over $y$, and predicate $q$ over $z$. This corresponds precisely to the treatment of infinite segments in Example 9(• ‣ 9). Hence, also for infinite intervals, $p\mathbin{\fatsemi}q=p\ast q$—chop is convolution, as desired. In this case, for Proposition 29(b), the loose algebraic ITL semantics is provided by a weak quantale. Tighter semantics in terms of weak semirings and Kleene algebras, which may arise as subalgebras, require further work. Finally, the restriction to finite intervals of the form $(x,0)$ as in Example 9(• ‣ 9) displays the embedding $\lambda x.\ (x,0)$ into the subquantale ${\mathcal{Q}}^{{\sf Cl}\ltimes X^{\mathcal{P}}}$.

12. Duration calculus

Duration Calculus (DC) [ZH04, BRZ00] is an extension of ITL with continuous time domain $\mathbb{R}$. This makes DC interesting for verifying hybrid and cyberphysical systems. In [ZH04], intervals are assumed to be finite, non-strict and closed; incidence algebras are therefore fusion-based. Additionally, DC includes operators for reasoning about properties in the neighbourhood of an interval, and it offers the capability of measuring and reasoning about durations, that is, the amount of time during which a state formula holds in an interval [ZH04, HM08, BRZ00]. Extensions of DC admit reasoning with semi-infinite intervals [ZHL95]. Our approach supports their uniform treatment via different kinds of partial semigroups and monoids, as before, and generalisations to segments. Hence, we need not make any particular assumptions about the type of intervals.

Algebraic reconstructions of (fragments of) DC were given previously by Höfner and Möller [HM08, HM09], using a trajectory-based approach. This included embeddings of the neighbourhood logics into modal semirings [DMS06], and the use of weak semirings to cope with infinite intervals. Beyond that, their approach is unrelated to ours.

We first discuss the duration component, which distinguishes DC from ITL. As with ITL, we use stream predicates to abstract from the store dynamics. In DC, these have type $\real\to\mathbb{B}$, but could easily be generalised to stream interval predicates of type $S(\real)\to X\to\mathbb{B}$, similar to the previous section. We keep the former for the sake of simplicity.

Intuitively, a duration measures the amount of time for which a predicate is true in an interval. Formally, the duration of stream predicate $b$ in interval $x$ is given by

[TABLE]

Hence $\textstyle{\int}:\mathbb{B}\to S(\real)\to{}_{+}^{o}$, where ${}_{+}^{o}$ for $o\in\{+\infty,-\infty\}$ is an appropriate extension of the non-negative reals by either $\infty$ or $-\infty$ to indicate that integrals do not exist, e.g., due to divergence or due to non-integrable functions. Note that finitely supported predicates can be integrable over semi-infinite intervals, and that integrals over point intervals are zero.

Next we outline a convolution-based semantics for predicates, which we model as interval stream predicates of type $S(\real)\times\mathbb{B}\to\mathbb{B}$. As in ITL, the meaning of boolean operators is obtained by pointwise lifting, that of chop $p\mathbin{\fatsemi}q$ is modelled by convolution over finite or semi-infinite intervals. Beyond that, the semantics of neighbourhood modalities $\Diamond_{r}\,p$ (i.e., $p$ holds for some immediately following interval) and $\Diamond_{l}\,p$ (i.e., $p$ holds for some immediately preceding interval) can be obtained from that of the Halpern-Shoham modalities \mathop{\big{\langle}A\,\big{|}} and \mathop{\big{|}A\big{\rangle}} from Section 10 as \Diamond_{r}=\mathop{\big{|}{\sf A}\big{\rangle}} and \Diamond_{l}\,=\mathop{\big{\langle}{\sf A}\,\big{|}}. Since suprema correspond to existential quantification, this yields $\Diamond_{r}\,p\,x\,\sigma=\exists y.\ {\sf A}\,x\,y\land p\,y\,\sigma$ and $\Diamond_{l}\,p\,x\,\sigma=\exists y.\ {\sf A}\,y\,x\land p\,y\,\sigma$. Finally, the semantics of iteration of predicates again follows ITL.

In light of our mathematical development so far, it is no surprise that the duration component of DC carries an interesting algebraic structure too. However, this seems to have been overlooked in the literature so far. It turns out that DC yields, in fact, an interesting application of Proposition 29 and relatives beyond the booleans in a quantitative setting.

We now study durations as functions from partial monoids of type $S(\real)$ into the Lawvere quantale $({}_{+}^{\infty},\geq,+,0)$ from Example 3. The following characterisation of the associated convolution algebra then follows immediately from our general lifting results, in particular Corollary 16.

Proposition 30**.**

$(({}_{+}^{\infty})^{S(\real)},\geq,\ast,\mathsf{id})$* is a weak distributive unital quantale with*

[TABLE]

The unit is given, as in Lemma 10, by $\mathsf{id}\ x=\bigsqcap_{e\in E}\delta\,e\,x$, where $E$ is the set of all point intervals. As always, the delta function yields the unit of composition of the target quantale when it encounters a point interval $x$ and the minimal element of the quantale otherwise. For the Lawvere quantale these are [math] and $\infty$, since the order is reversed.

Proposition 30 specialises to durations of predicates $\textstyle{\int}b$, which have type $S(\real)\to{}_{+}^{\infty}$, as follows, writing ${\it Int}\subseteq\mathbb{B}$ for the set of all stream predicates that are integrable over any strict interval.

Corollary 31**.**

1. (a)

$\{\textstyle{\int}b\mid b\in{\it Int}\}$* forms a weak distributive quantale.* 2. (b)

$\{\textstyle{\int}b\mid b\in\mathbb{B}^{\mathbb{R}}\}$* forms a weak distributive unital quantale.*

In this instance, we obtain the convolution

[TABLE]

and any non-integrable predicate $b$ (for any interval) yields the same unit $\textstyle{\int}b$, since $\textstyle{\int}b\,x$ is equal to [math] if $x$ is a point interval and $\infty$ otherwise.

Alternatively, one can use any other of the $\mathbb{R}^{\infty}_{+}$-quantales from Example 3. These results develop the quantitative and qualitative aspects of DC uniformly and algebraically.

13. Mean-Value Calculus

This section briefly discusses the Mean-Value Calculus (MVC) [ZH04, PR98]; an extension of DC that allows reasoning about the average length of time for which a property holds within an interval. In our setting, this means that predicates are evaluated in another quantale, which yields a different quantitative convolution algebra.

Now, in addition to the constructs of DC, the mean value of an integrable stream predicate $b\in{\it Int}$ over an interval $x$ is defined as follows. For the purpose of this section, we assume the intervals under consideration are finite, however, it is straightforward to extend the definitions below to the infinite case.

[TABLE]

It calculates the proportion of the interval for which $b$ holds as a value in the unit interval $[0,1]$ in , hence as a probability, so that $\theta:{\it Int}\to S(\real)\to[0,1]$. For a point interval, by definition, the mean value is the value of $b$ at that point.

To characterise the convolution algebra of mean values of MVC we can now use the target quantales over $[0,1]$ from Example 3, that is, $([0,1],\leq,\cdot,1)$, $([0,1],\leq,\min,1)$ or $([0,1],\geq,\max,0)$. Lifting results similar to Corollary 31 are now straightforward.

Corollary 32**.**

$\{\theta\,b\mid b\in{\it Int}\}$* forms a weak distributive quantale.*

Depending on the choice of the target quantale, we obtain the following convolutions

[TABLE]

which are similar to those for durations, but with values taken in $[0,1]$.

14. Remarks on the Isabelle Formalisation

Formalising the mathematical structures and theorems in this article is relatively straightforward using Isabelle, and often leads to readable definitions and proofs [DGHS17]. Isabelle’s built-in axiomatic type classes allow formalising the basic algebraic structures used. Partial semigroups, for instance, extend a predefined type class that provides an operation of multiplication.

class* partial-semigroup $=$ times $+$ *

*  fixes D $\mathord{:}$**$\mathord{:}$ *$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*a $\Rightarrow$ *$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$a $\Rightarrow$ bool

*  assumes mult-assocD*$\mathord{:}$* D y z $\wedge$ D x $($y $\cdot$ z$)$ $\longleftrightarrow$ D x y $\wedge$ D $($x $\cdot$ y$)$ z*

*  assumes mult-assoc*$\mathord{:}$* D x y $\wedge$ D $($x $\cdot$ y$)$ z $\Longrightarrow$ $($x $\cdot$ y$)$ $\cdot$ z $=$ x $\cdot$ $($y $\cdot$ z$)$*

Structures that depend on several type parameters, such as partial actions of partial multiplicative semigroups on sets, can be formalised as locales.

locale* partial-sg-laction $=$ *

*  fixes Dla $\mathord{:}$**$\mathord{:}$ *$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$a$\mathord{:}$**$\mathord{:}$*partial-semigroup $\Rightarrow$ *$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$b $\Rightarrow$ bool

*  and act $\mathord{:}$**$\mathord{:}$ $\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$a$\mathord{:}$$\mathord{:}$*partial-semigroup $\Rightarrow$ *$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*b $\Rightarrow$ *$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*b *$($$\alpha$**$)$ *

*  assumes act-assocD*$\mathord{:}$* D x y $\wedge$ Dla $($x $\odot$ y$)$ p $\longleftrightarrow$ Dla y p $\wedge$ Dla x $($**$\alpha$ y p*$)$**

*  and act-assoc*$\mathord{:}$* D x y $\wedge$ Dla $($x $\odot$ y$)$ p $\Longrightarrow$ $\alpha$ $($x $\odot$ y$)$ p $=$ $\alpha$ x $($**$\alpha$ y p*$)$**

Note that we write $\alpha\,x\,p$ instead of $x\circ p$, as $\circ$ is used for function composition in Isabelle. We extend this action to an action on a second semigroup:

locale* partial-sg-sg-laction $=$ partial-sg-laction $+$*

*  assumes act-distribD*$\mathord{:}$* D $($p$\mathord{:}$$\mathord{:}$$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$b$\mathord{:}$**$\mathord{:}$partial-semigroup$)$ q $\wedge$ Dla $($x$\mathord{:}$$\mathord{:}$$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$a$\mathord{:}$**$\mathord{:}$partial-semigroup$)$ $($p $\oplus$ q$)$*

*    $\longleftrightarrow$ Dla x p $\wedge$ Dla x q $\wedge$ D $($**$\alpha$ x p*$)$* $($**$\alpha$ x q*$)$**

*  and act-distrib*$\mathord{:}$* D p q $\wedge$ Dla x $($p $\oplus$ q$)$ $\Longrightarrow$ $\alpha$ x $($p $\oplus$ q$)$ $=$ $($**$\alpha$ x p*$)$* $\oplus$ $($**$\alpha$ x q*$)$*  *

Proposition 21, which states that the semidirect product of two partial semigroups forms a partial semigroup, can then be formalised as a sublocale statement.

definition* sd-D $\mathord{:}$**$\mathord{:}$ *$($$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*a $\times$ $\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$b$)$ $\Rightarrow$ *$($$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$a $\times$ $\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$b$)$ $\Rightarrow$ bool where

*  sd-D x y $\equiv$ D $($fst x$)$ $($fst y$)$ $\wedge$ Dla $($fst x$)$ $($snd y$)$ $\wedge$ D $($snd x$)$ $($**$\alpha$ $($fst x$)$ *$($snd y$)$$)$

definition* sd-prod $\mathord{:}$**$\mathord{:}$ *$($$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*a $\times$ $\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$b$)$ $\Rightarrow$ *$($$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*a $\times$ $\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$b$)$ $\Rightarrow$ *$($**$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$a $\times$ $\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$b$)$ where

*  sd-prod x y $=$ $($**$($fst x$)$ $\odot$ $($fst y$)$**$\mathord{,}$ $($snd x$)$ $\oplus$ $($**$\alpha$ $($fst x$)$ $($snd y$)$$)$$)$   *

*  *

sublocale* dp-semigroup*$\mathord{:}$* partial-semigroup sd-prod sd-D*

*  $\langle$proof$\rangle$ *

The sublocale statement requires a signature matching; here the instances of the product operation and the domain of definition of the partial semigroup must be declared. We supply a semidirect product operation and its domain of definition, which have been defined before the sublocale statement.

Relational convolution can be defined in Isabelle as follows.

definition* bmod-comp *$\mathord{:}$$\mathord{:}$

*   *$($$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*a $\Rightarrow$ *$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*b $\Rightarrow$ $\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$c $\Rightarrow$ bool$)$ $\Rightarrow$ *$($$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*b $\Rightarrow$ $\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$d $\mathord{:}$**$\mathord{:}$ proto-quantale$)$ $\Rightarrow$ $($$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*c $\Rightarrow$ $\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$d$)$ $\Rightarrow$ *$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*a $\Rightarrow$ *$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$*d *$($$\otimes$**$)$ where *

*  $\otimes$ R f g x $=$ $\bigsqcup$*$\{$f y $\cdot$ g z $\mid$y z$\mathord{.}$ R x y z$\}$**

definition* f $\star$ g $=$ $\otimes$ R f g*

The convolution operation $\otimes$ is supplied with a ternary relation $R$ (in previous sections we have written $\ast_{R}$), and then with functions $f$, $g$ and an element $x$ of suitable type. Isabelle allows us to write $f\star g$ (instead of $f\ast_{R}g$) when $R$ is fixed. In this example, the sort of the output of the function has been restricted to proto-quantales. In our formalisation we use even more general kinds of quantales. Our formalisations of variants of quantales are once more based on type classes. As a final example, we show how the lifting result from Theorem 11(b) can be captured as an instantiation statement in Isabelle.

instantiation* fun $\mathord{:}$**$\mathord{:}$ $($rel-semigroup$\mathord{,}$quantale$)$ quantale*

*  $\langle$proof$\rangle$ *

As expected, it states that functions from a relational semigroup, which has been formalised as a type class, into a quantale forms an instance of a quantale.

All constructions of partial semigroups and convolution algebras in the paper have been formalised by similar sublocale or instantiation statements, or by interpretation statements that are similar to instantiations.

Isabelle offers a range of proof tools to explore the structures in this article and reason about them. First of all, its counterexample generators are helpful, for instance, for debugging theories. Automated theorem provers, SMT solvers and built-in simplifiers yield a high degree of proof automation for simple equational reasoning with first-order structures. Reasoning with higher-order structures, such as quantales and convolutions, however may require a significant amount of user interaction and a granularity of proof much finer than that of mathematical textbooks.

Our entire formalisation can be found online in the Archive of Formal Proofs [DGHS17]. So far it covers most of the technical material up to Section 10; open and semi-closed intervals being a notable exception. Results on duration and mean-value calculi have not been included because in particular the construction of quantales over the extended non-negative reals or the unit interval require some background theory development for these number domains to be encoded within Isabelle. All theorems that have not been formalised are mentioned explicitly in the article; a list of cross-references between all results in the article and those in the Archive of Formal Proofs can be found in Appendix B.

Our Isabelle convolution components can serve as a basis for (a) formalising the concrete interval logics described in Section 10-13 and (b) building verification components for these using a shallow embedding of our algebraic semantics. In addition, our Isabelle components for relational convolution form a basis for formalised reasoning about resources, as for instance in separation logic [Rey02], and for formalising a wide range of models of computational interest, from (quantale-valued) relations and (weighted) languages to program traces, partial-order semantics for concurrency and even quantum logics in a uniform way, simply by setting up the appropriate partial semigroups [DHS16].

Experience shows that the simple axiomatic approach to algebras that underlies our formalisation is sufficient for many verification applications [AGS16, DGS15, GS16]. An in-depth formalisation of (partial) semigroups, their morphisms and subalgebras, however, requires the explicit consideration of carrier sets, for which our current approach is too limited. A categorical formalisation of the topics investigated may not even be feasible with Isabelle.

15. Conclusions

The main aim of this article has been a generalisation of our previous approach to convolution as a universal operation in computing [DHS16] to ternary relations. While the emphasis of the applications considered was on (generalised) interval logics, separation logic, in particular the view of separating conjunction as convolution, has been considered in a companion paper [DGS15]. In all these cases, the general approach consists in setting up the appropriate ternary relations, which are often generated by partial semigroups, partial monoids or combinations of these, and then using the general lifting construction to build a convolution algebra. If the target quantale used in the lifting is formed by the booleans, then the convolution algebra is an algebra of predicates, hence the lifting embodies a powerset construction with convolution as complex product. In more general cases, convolution algebras capture quantative aspects of computing systems such as durations, weights or probabilities, as our examples show.

The main features of the approach, including the most important lifting theorems, have already been formalised in Isabelle [DGHS17]. The resulting mathematical components provide first of all a basis for the design of verification components, which are currently under construction for separation logic and concurrent Kleene algebras. Similar components for interval logics and Duration Calculus, with applications in hybrid and cyberphysical systems verification, could be obtained along the same lines as instances of the general approach. Secondly, most of the computationally interesting models of variants of Kleene algebras within the Archive of Formal Proofs [AFP], which include relations, languages, sets of paths in a digraph, program traces, and matrices over Kleene algebras, could be obtained via convolution simply by setting up the appropriate partial semigroups.

Beyond that we envisage various avenues for future research. These include the investigation of other substructural logics, in particular linear logics, and the effect algebras that arise in the foundations of quantum mechanics as convolution algebras, the exploration of other quantitative applications that arise within stochastic or probabilistic systems, and last but not least, a consideration of the approach in the realm of higher category theory.

Acknowledgments

The authors would like to thank Mark Hepple for discussions on the Lambek calculus and references on this topic. Our investigation into the role of ternary relations in convolution was sparked by an insightful comment from one of our anonymous reviewers for [DHS16]. We are also grateful to Victor Gomes for his joint work on the Isabelle formalisation, and Alasdair Armstrong for additional Isabelle advice.

Appendix A Glossary of Algebraic Structures

Within the table the number of each definition is given.

[TABLE]

Appendix B Cross-References to Archive of Formal Proofs

[TABLE]

\justify

Results not formalised with Isabelle: Corollary 12, Lemma 13, Lemma 19, Lemma 20, Lemma 25, Lemma 26, Lemma 27, Lemma 28, Proposition 30, Corollary 31, and Corollary 32