# Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with
Tests††thanks:  Preprint of: I. Sedlár and J.J. Wannenburg: Embedding Kozen-
Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Tests. In: A.
Ciabattoni, E. Pimentel, R. J. G. B. de Queiroz (Eds.): _Proc. 28th Int.
Conference of Logic, Language, Information, and Computation (WoLLIC 2022)_ ,
pp. 221-236. LNCS 13468. Springer, 2022. (Available online at
https://link.springer.com/chapter/10.1007/978-3-031-15298-6_14.)

Igor Sedlár and Johann J. Wannenburg  The Czech Academy of Sciences, Institute
of Computer Science
Pod Vodárenskou věží 271/2, Prague, The Czech Republic

###### Abstract

Kozen and Tiuryn have introduced the substructural logic $\mathsf{S}$ for
reasoning about correctness of while programs (ACM TOCL, 2003). The logic
$\mathsf{S}$ distinguishes between tests and partial correctness assertions,
representing the latter by special implicational formulas. Kozen and Tiuryn’s
logic extends Kleene altebra with tests, where partial correctness assertions
are represented by equations, not terms. Kleene algebra with codomain,
$\mathsf{KAC}$, is a one-sorted alternative to Kleene algebra with tests that
expands Kleene algebra with an operator that allows to construct a Boolean
subalgebra of tests. In this paper we show that Kozen and Tiuryn’s logic
embeds into the equational theory of the expansion of $\mathsf{KAC}$ with
residuals of Kleene algebra multiplication and the upper adjoint of the
codomain operator.

##### Keywords:

Hoare logic, Kleene algebra with codomain, Kleene algebra with tests, Partial
correctness, Substructural logic

##  1 Introduction

Kleene algebra with tests [10], KAT, is a simple algebraic framework for
verifying properties of propositional while programs. KAT is two-sorted,
featuring a Boolean algebra of tests embedded into a Kleene algebra of
programs. The equational theory of KAT is PSPACE-complete [2] and KAT subsumes
Propositional Hoare logic, PHL [11]. A PHL partial correctness assertion
$\\{b\\}\,p\,\\{c\\}$, meaning that $c$ holds after each terminating execution
of program $p$ in a state satisfying $b$, is represented in KAT by the
equation $bp\bar{c}=0$ or, equivalently, $bp=bpc$. The universal Horn theory
(or the quasi-equational theory) of KAT consisting of quasi-equations of the
form $E\longrightarrow p=q$ where $E$ is a finite set of equations of the form
$r=0$ embeds into the equational theory of KAT [13] and is therefore PSPACE-
complete as well.

Kozen and Tiuryn [14] introduce a substructural logic S that extends KAT and
represents partial correctness assertions as implicational formulas
$bp\Rightarrow c$. They argue that the implicational rendering of partial
correctness assertions has certain advantages over the equational one, e.g. it
facilitates a better distinction between local and global properties. PHL
embeds into S and S is PSPACE-complete [12]. Kozen and Tiuryn prove that S
induces a left-handed KAT structure on programs. However, a more thorough
discussion of the relation of S to residuated extensions of Kleene algebra,
such as Pratt’s action logic [18], or to substructural logics in general is
not provided. We believe that a deeper investigation of these connections
would shed more light on the landscape of program logics and algebras.

In this paper we prove an embedding result that contributes to this. We note
that a simple extension of KAT with a residual $\to$ of the Kleene algebra
multiplication does not enable an obvious embedding of S: implication formulas
of S are test-like in the sense that they entail the multiplicative unit $1$,
but terms $p\to b$ of residuated KAT are not test-like, even if $b$ is. To
avoid this problem, we work with Kleene algebra with codomain, KAC [3, 5], a
one-sorted alternative to KAT featuring a test-forming codomain operator
$\mathsf{c}$. In particular, we introduce an extension of KAC with both
residuals of Kleene algebra multiplication and the upper adjoint $\mathsf{e}$
of the codomain operator, which we call SKAT. We show that
$\mathsf{c}(p\to\mathsf{e}(b))$ behaves like $p\Rightarrow b$ of S. Our main
technical result is that S embeds into the equational theory of
$\mathsf{SKAT}^{*}$, the class of algebras in SKAT that are based on
∗-continuous Kleene algebras.

The paper is structured as follows. Section 2 recalls KAT and S. Section 3
introduces a residuated version of KAT. We show that a naive translation of
the implication connective of S into the residual operation does not
constitute an embedding. In Section 4 we recall KAC and in Section 5 we
introduce SKAT and SKAT∗. Section 6 establishes the embedding result. Section
7 concludes the paper and lists some interesting open problems.

##  2 KAT and S

In this section we recall KAT (Sect. 2.1) and we outline S (Sect. 2.2).

###  2.1 Kleene algebra with tests

We assume that the reader is familiar with the notion of an _idempotent
semiring_.

######  Definition 1.

A _Kleene algebra_ [8] is an idempotent semiring $(K,\cdot,+,1,0)$ expanded
with an operation ${}^{*}:K\to K$ such that

$\displaystyle 1+xx^{*}\leq x^{*}$ (1) $\displaystyle 1+x^{*}x\leq x^{*}$ (2)
$\displaystyle y+xz\leq z\implies x^{*}y\leq z$ (3) $\displaystyle y+zx\leq
z\implies yx^{*}\leq z$ (4)

A Kleene algebra is _∗ -continuous_ iff it satisfies the condition

$xy^{*}z=\sum_{n\geq 0}xy^{n}z$ (5)

where $y^{0}=1$ and $y^{n+1}=y^{n}y$. $\sum X$ is the supremum of the set
$X\subseteq K$ with respect to the partial order induced by Kleene algebra
addition $+$.

It follows from the definition that $x^{*}$ is the least element $z$ such that
$1\leq z$, $xz\leq z$ and $zx\leq z$. A standard example of a Kleene algebra
is a relational Kleene algebra where $K$ is a set of binary relations over
some set $S$, $\cdot$ is relational composition, $+$ is set union, ∗ is
reflexive transitive closure, $1$ is identity on $S$ and $0$ is the empty set.
A relational Kleene algebra where $K$ is the power set of some $S\times S$
will be called _fully relational_. Another standard example is the Kleene
algebra of regular languages over a finite alphabet, where ∗ corresponds to
finite iteration (Kleene star). Relational Kleene algebras and Kleene algebras
of regular languages are both ∗-continuous. Part of the definition of
∗-continuous Kleene algebras is the requirement that suprema of sets of
elements of the form $xy^{n}z$ exist. Not each Kleene algebra is ∗-continuous
[7], but the equational theories of Kleene algebras and ∗-continuous Kleene
algebras coincide [8].

######  Definition 2.

A _Kleene algebra with tests_ [10] is a structure
$(K,B,\cdot,+,^{*},1,0,\,\bar{}\,)$ such that

  * •

$(K,\cdot,+,^{*},1,0)$ is a Kleene algebra,

  * •

$B\subseteq K$, and

  * •

$(B,\cdot,+,\,\bar{}\,,1,0)$ is a Boolean algebra.

A Kleene algebra with tests is ∗-continuous if its underlying Kleene algebra
is.

Every Kleene algebra is a Kleene algebra with tests; take $B=\\{0,1\\}$ and
define $\bar{0}=1$, $\bar{1}=0$ and $\bar{x}=x$ for $x\notin\\{1,0\\}$.111In
contrast to the standard formulation of Kleene algebra with tests [10], we
consider $\,\bar{\,}\,$ to be defined on all elements of $K$. A standard
example of a (∗-continuous) Kleene algebra with tests is a relational Kleene
algebra expanded with a Boolean subalgebra of the _negative cone_ , i.e. the
elements $x\leq 1$, which in the relational case are subsets of the identity
relation. The class of Kleene algebras with tests is denoted as $\mathsf{KAT}$
and the class of ∗-continuous Kleene algebras with tests is denoted as
$\mathsf{KAT^{*}}$. As in the test-free case, the equational theory of
$\mathsf{KAT}$ is identical to the equational theory of $\mathsf{KAT}^{*}$
[13].

Kleene algebras with tests are able to represent while programs and facilitate
equational reasoning about their partial correctness:

  * •

$\mathbf{skip}=1$

  * •

$p;q=pq$

  * •

$\textbf{if}\>b\>\textbf{then}\>p\>\textbf{else}\>q$ $=(bp)+(\bar{b}q)$

  * •

$\textbf{while}\>b\>\textbf{do}\>p$ $=(bp)^{*}\bar{b}$

  * •

$\\{b\\}\,p\,\\{c\\}$ corresponds to $bp\bar{c}=0$

###  2.2 Substructural logic of partial correctness

This section outlines the substructural logic S [14] that allows to represent
a partial correctness assertion by a formula (term) instead of an equation as
in KAT. As with KAT, the logic S is many-sorted. Let
$\mathsf{B}=\\{\mathsf{b}_{i}\mid i\in\omega\\}$ be the set of test variables
and let $\mathsf{P}=\\{\mathsf{p}_{i}\mid i\in\omega\\}$ be the set of program
variables. We define the following sorts of syntactic objects:

tests | $b,c:=\mathsf{b}_{i}\mid 0\mid b\Rightarrow c$
---|---
programs | $p,q:=\mathsf{p}_{i}\mid b\mid p\oplus q\mid p\otimes q\mid p^{+}$
formulas | $f,g:=b\mid p\Rightarrow f$
environments | $\Gamma,\Delta:=\epsilon\mid\Gamma,p\mid\Gamma,f$
sequents | $\Gamma\vdash f$

We define $1:=0\Rightarrow 0$, $\neg b:=b\Rightarrow 0$ and $p^{*}:=1\oplus
p^{+}$. We will sometimes write $pq$ instead of $p\otimes q$ and $\bar{b}$
instead of $\neg b$. Let $\mathsf{E}=\mathsf{B}\cup\mathsf{P}$ and let
$Ex_{\mathsf{S}}$, the set of $\mathsf{S}$-expressions, be the union of the
sets of formulas, programs and environments.

Kozen and Tiuryn introduce three kinds of semantics for their language:
semantics based on guarded strings, traces and binary relations, respectively.
We will work only with binary relational semantics.

######  Definition 3.

A _Kozen–Tiuryn model_ is a pair $M=(W,V)$, where $W$ is a non-empty set and
$V:\mathsf{E}\to 2^{W\times W}$ such that
$V(\mathsf{b})\subseteq\mathrm{id}_{W}$ for all $\mathsf{b}\in\mathsf{B}$.

For each Kozen–Tiuryn model $M$, we define the _$M$ -interpretation_ function
$\scalebox{0.9}{{[}}\,\scalebox{0.9}{{]}}_{M}:Ex_{\mathsf{S}}\to 2^{W\times
W}$ as follows:

  * •

$\scalebox{0.9}{{[}}\mathsf{b}\scalebox{0.9}{{]}}_{M}=V(\mathsf{b})$

  * •

$\scalebox{0.9}{{[}}\mathsf{p}\scalebox{0.9}{{]}}_{M}=V(\mathsf{p})$

  * •

$\scalebox{0.9}{{[}}0\scalebox{0.9}{{]}}_{M}=\emptyset$

  * •

$\scalebox{0.9}{{[}}b\Rightarrow
c\scalebox{0.9}{{]}}_{M}=\\{(s,s)\mid(s,s)\not\in\scalebox{0.9}{{[}}b\scalebox{0.9}{{]}}_{M}\text{
or }(s,s)\in\scalebox{0.9}{{[}}c\scalebox{0.9}{{]}}_{M}\\}$

  * •

$\scalebox{0.9}{{[}}p\oplus
q\scalebox{0.9}{{]}}_{M}=\scalebox{0.9}{{[}}p\scalebox{0.9}{{]}}_{M}\cup\scalebox{0.9}{{[}}q\scalebox{0.9}{{]}}_{M}$

  * •

$\scalebox{0.9}{{[}}p\otimes
q\scalebox{0.9}{{]}}_{M}=\scalebox{0.9}{{[}}p\scalebox{0.9}{{]}}_{M}\circ\scalebox{0.9}{{[}}q\scalebox{0.9}{{]}}_{M}$

  * •

$\scalebox{0.9}{{[}}p^{+}\scalebox{0.9}{{]}}_{M}=\scalebox{0.9}{{[}}p\scalebox{0.9}{{]}}_{M}^{+}$

  * •

$\scalebox{0.9}{{[}}p\Rightarrow f\scalebox{0.9}{{]}}_{M}=\\{(s,s)\mid\forall
t.(s,t)\in\scalebox{0.9}{{[}}p\scalebox{0.9}{{]}}_{M}\implies(t,t)\in\scalebox{0.9}{{[}}f\scalebox{0.9}{{]}}_{M}\\}$

  * •

$\scalebox{0.9}{{[}}\epsilon\scalebox{0.9}{{]}}_{M}=\mathrm{id}_{W}$

  * •

$\scalebox{0.9}{{[}}\Gamma,\Delta\scalebox{0.9}{{]}}_{M}=\scalebox{0.9}{{[}}\Gamma\scalebox{0.9}{{]}}_{M}\circ\scalebox{0.9}{{[}}\Delta\scalebox{0.9}{{]}}_{M}$

(Here + denotes transitive closure and $\circ$ denotes relational
composition.)

A sequent $\Gamma\vdash f$ is _valid in $M$_ iff, for all $s,t\in W$, if
$(s,t)\in\scalebox{0.9}{{[}}\Gamma\scalebox{0.9}{{]}}_{M}$, then
$(t,t)\in\scalebox{0.9}{{[}}f\scalebox{0.9}{{]}}_{M}$.

Observe that
$\scalebox{0.9}{{[}}f\scalebox{0.9}{{]}}_{M}\subseteq\mathrm{id}_{W}$ for all
formulas $f$; if $(s,s)\in\scalebox{0.9}{{[}}f\scalebox{0.9}{{]}}_{M}$, then
we may say that formula $f$ is true in $s$. Note that
$\scalebox{0.9}{{[}}bp\Rightarrow c\scalebox{0.9}{{]}}_{M}$ is the set of
$(s,s)$ such that, for all $t$, if
$(s,s)\in\scalebox{0.9}{{[}}b\scalebox{0.9}{{]}}_{M}$ and
$(s,t)\in\scalebox{0.9}{{[}}p\scalebox{0.9}{{]}}_{M}$, then
$(t,t)\in\scalebox{0.9}{{[}}c\scalebox{0.9}{{]}}_{M}$. Hence, $bp\Rightarrow
c$ represents a partial correctness assertion: the formula is true in $s$ iff
$b$ is true in $s$ and $p$ connects $s$ with a state $t$ only if $c$ is true
in $t$.

Figure 1 shows the sequent proof system for $\mathsf{S}$. A sequent
$\Gamma\vdash f$ is _provable in $\mathsf{S}$_ iff there is a finite sequence
of sequents that ends with $\Gamma\vdash f$ each of which is either of the
form (Id) or (I$0$), or is derived from previous sequents using some of the
inference rules.

######  Theorem 1 (Kozen and Tiuryn).

$\Gamma\vdash f$ is provable in $\mathsf{S}$ iff $\Gamma\vdash f$ is valid in
all models $M$.

  * (Id)

$b\vdash b$

  * (TC)

$\dfrac{\Gamma,b,\Delta\vdash f\qquad\Gamma,\bar{b},\Delta\vdash
f}{\Gamma,\Delta\vdash f}$

  * (R$\Rightarrow$)

$\dfrac{\Gamma,p\vdash f}{\Gamma\vdash p\Rightarrow f}$

  * (I$\otimes$)

$\dfrac{\Gamma,p,q,\Delta\vdash f}{\Gamma,p\otimes q,\Delta\vdash f}$

  * (I$\oplus$)

$\dfrac{\Gamma,p,\Delta\vdash f\qquad\Gamma,q,\Delta\vdash f}{\Gamma,p\oplus
q,\Delta\vdash f}$

  * (I+)

$\dfrac{g,p\vdash f\qquad g,p\vdash g}{g,p^{+}\vdash f}$

  * (E+)

$\dfrac{\Gamma,p^{+},\Delta\vdash f}{\Gamma,p,\Delta\vdash f}$

  * (CC+)

$\dfrac{\Gamma,p^{+},\Delta\vdash f}{\Gamma,p^{+},p^{+},\Delta\vdash f}$

  * (I$0$)

$\Gamma,0,\Delta\vdash f$

  * (cut)

$\dfrac{\Gamma\vdash g\qquad\Gamma,g,\Delta\vdash f}{\Gamma,\Delta\vdash f}$

  * (I$\Rightarrow$)

$\dfrac{\Gamma,p,f,\Delta\vdash g}{\Gamma,p\Rightarrow f,p,\Delta\vdash g}$

  * (E$\otimes$)

$\dfrac{\Gamma,p\otimes q,\Delta\vdash f}{\Gamma,p,q,\Delta\vdash f}$

  * (E$\oplus_{1}$)

$\dfrac{\Gamma,p\oplus q,\Delta\vdash f}{\Gamma,p,\Delta\vdash f}$

  * (E$\oplus_{2}$)

$\dfrac{\Gamma,p\oplus q,\Delta\vdash f}{\Gamma,q,\Delta\vdash f}$

  * (W$f$)

$\dfrac{\Gamma,\Delta\vdash g}{\Gamma,f,\Delta\vdash g}$

  * (W$p$)

$\dfrac{\Gamma\vdash f}{p,\Gamma\vdash f}$

Figure 1: The sequent proof system for $\mathsf{S}$.

S can be seen as a substructural logic [19]. From that point of view, S is an
extension of the Multiplicative-additive Lambek calculus with the transitive
closure operator +. However, S contains some rules not usual from the
substructural logic perspective, namely, the sort-specific weakening rules
(W$f$) and (W$p$), and the implication-formula rules (TC) and
(I$\Rightarrow$). It is therefore interesting to inquire how S relates to
mainstream substructural logics. The embedding result of Section 6 is helpful
in this respect.

##  3 Residuated KAT

The crucial difference between KAT and S is that the latter contains an
implication operator $\Rightarrow$ that is used to formalize partial
correctness assertions as formulas (terms) of the language. Therefore, one may
wonder if S can be thought of as KAT expanded with a residual of Kleene
algebra multiplication. In this section we introduce residuated KAT, RKAT, and
we show that a naive mapping from S to RKAT is not an embedding.

We note that residuated Kleene algebras with tests were studied also in [6].
In that framework, however, it is assumed by definition that the negative cone
of the underlying Kleene algebra forms a Boolean algebra of tests. Kozen [10]
argues, however, that this approach is not entirely satisfactory: tests are
usually easily decidable (unlike other propositions, such as halting
assertions), and not each Kleene algebra has a Boolean negative cone. Our
definition of residuated Kleene algebras with tests adds residuals to KAT
defined as usual.

######  Definition 4.

A _residuated idempotent semiring_ is a structure of the form
$(K,\cdot,+,\to,\hookrightarrow,1,0)$ where

  * •

$(K,\cdot,+,1,0)$ is an idempotent semiring, and

  * •

$\to,\hookrightarrow$ are binary operations on $K$ satisfying the _residuation
laws_

$xy\leq z\iff x\leq y\to z\iff y\leq x\hookrightarrow z$ (6)

In residuated idempotent semirings, $\to$ is called the _right residual_ of
$\cdot$ and $\hookrightarrow$ is called the _left residual_. An idempotent
semiring is called _right-residuated_ (_left-residuated_) if it is a reduct of
a residuated idempotent semiring with only the right (left) residual. Note
that residuated idempotent semirings necessarily have a top element: $x0\leq
0$ implies $x\leq 0\to 0$ and $0x\leq 0$ implies $x\leq 0\hookrightarrow 0$.

The study of residuated semirings has some precedent. Pratt adds residuals to
Kleene algebras to obtain _action algebras_ [18], and Kozen adds a lattice
meet operation to action algebras to obtain _action lattices_ [9]; see also
[6]. Equational theories of both action algebras and action lattices are
undecidable [15].

######  Definition 5.

A _right-residuated Kleene algebra with tests_ is a structure of the form
$(K,B,\cdot,+,\,^{*},\to,\,\bar{\,}\,,1,0)$ where

  * •

$(K,B,\cdot,+,\,^{*},\,\bar{\,}\,,1,0)\in\mathsf{KAT}$, and

  * •

$(K,\cdot,+,\to,1,0)$ is a right-residuated idempotent semiring.

We will usually call right-residuated Kleene algebras with tests just
residuated. The class of residuated Kleene algebras with tests will be denoted
as RKAT.

One may be tempted to define $\bar{x}$ as $x\to 0$, but this temptation is
better resisted. Note that $0\in B$ in every Kleene algebra with tests, but
$0\to 0$ is the top element. Hence, if we have a residuated Kleene algebra
with tests where $B$ does not contain the top element, then $B$ is not closed
under the operation $x\to 0$. An example of such an algebra is given in Figure
2, where $B=\\{0,1\\}$ and $+$ is join behaving as indicated in the diagram on
the left: $0\to 0=\top$ but $\bar{0}=1$.

$0$$1$$\top$$B$

$\to$ 0 1 $\top$ 0 $\top$ $\top$ $\top$ 1 0 1 $\top$ $\top$ 0 0 $\top$ $\cdot$
0 1 $\top$ 0 0 0 0 1 0 1 $\top$ $\top$ 0 $\top$ $\top$ ∗ 0 1 $\top$ 1 1 $\top$

Figure 2: A residuated Kleene algebra with tests where $x\to 0$ is not test
complementation.

For a similar reason, formulas $p\Rightarrow b$ of S do not directly translate
into $p\to b$; the former entail $1$, but the latter do not, as we have seen.
However, a consideration of the relational case sheds some light on the
matter. Recall that for $R\subseteq S\times S$ and
$B\subseteq\mathrm{id}_{S}$,

$\displaystyle R\to B=\\{(s,u)\mid\forall v.\,(u,v)\in R\implies(s,v)\in B\\}$
$\displaystyle R\Rightarrow B=\\{(u,u)\mid\forall v.\,(u,v)\in
R\implies(v,v)\in B\\}$

Now consider two operations $c,e:2^{S\times S}\to 2^{S\times S}$ such that

$\displaystyle c(R)=\\{(u,u)\mid\exists s.\,(s,u)\in R\\}$ (7) $\displaystyle
e(R)=\\{(s,u)\mid(u,u)\in R\\}$ (8)

Note that $c$ and $e$ form a _Galois connection_ in the sense that, for all
binary relations $Q$ and $R$ on $S$,

$c(R)\subseteq Q\iff R\subseteq e(Q)\,.$ (9)

We have the following observation.

######  Proposition 1.

For all $R\subseteq S\times S$ and $B\subseteq\mathrm{id}_{S}$,

$c(R\to e(B))=R\Rightarrow B$ (10)

###### Proof.

If $(u,u)\in R\Rightarrow B$, then $(u,u)\in R\to e(B)$ since $(v,v)\in B$ iff
$(u,v)\in e(B)$ by (8). But then obviously $(u,u)\in c(R\to e(B))$. Hence,
$R\Rightarrow B\,\subseteq\,c(R\to e(B))$. Conversely, assume that $(u,u)\in
c(R\to e(B))$ and $(u,v)\in R$, then $(s,u)\in R\to e(B)$ by (7) and so
$(s,v)\in e(B)$. It follows that $(v,v)\in B$. Hence, $(u,u)\in R\Rightarrow
B$ and so $c(R\to e(B))\,\subseteq\,R\Rightarrow B$. ∎

Hence, it seems that expanding RKAT with abstractions of $c$ and $e$ would
make it possible to express the implication operator of S. An abstraction of
$\mathsf{c}$ was added to semirings and Kleene algebras in the works on Kleene
algebra with (co)domain [5, 3]. We discuss Kleene algebra with codomain in the
next section.

##  4 Kleene algebra with codomain

Kleene algebra with codomain, KAC, is a one-sorted alternative to KAT: instead
of assuming the existence of a Boolean subalgebra of tests, KAC introduces a
unary _codomain_ operation $\mathsf{c}$ such that the set of $\mathsf{c}(x)$
for $x$ in the underlying Kleene algebra forms a Boolean algebra. One of the
motivations for studying one-sorted alternatives to Kleene algebra with tests
is that they seem to be better suited to automated theorem proving (see [5],
p. 194). Our presentation follows [5, 3], where a symmetric variant of KAC,
namely, Kleene algebra with _domain_ , was studied.

Kleene algebras with codomain add to Kleene algebras a unary operator that
generalizes the _anticodomain_ operator on binary relations:

$a(R)=\\{(u,u)\mid\neg\exists s.(s,u)\in R\\}\,.$ (11)

Note that, assuming (7), $c(R)=a(a(R))$.

######  Definition 6.

A _Kleene algebra with codomain_ is an algebra of the form
$(K,\cdot,+,\,^{*},\mathsf{a},1,0)$ where $\mathsf{a}:K\to K$ such that

$\displaystyle x\cdot\mathsf{a}(x)\leq 0$ (12) $\displaystyle\mathsf{a}(x\cdot
y)\leq\mathsf{a}\big{(}\mathsf{a}(\mathsf{a}(x))\cdot y\big{)}$ (13)
$\displaystyle\mathsf{a}(x)+\mathsf{a}(\mathsf{a}(x))=1$ (14)

We define $\mathsf{c}(x):=\mathsf{a}(\mathsf{a}(x))$.

Note that the relational anticodomain operator (11) satisfies the above
equations.

######  Proposition 2.

In every Kleene algebra with codomain, the operator $\mathsf{c}$ satisfies the
following codomain equations:

$\displaystyle x\leq x\cdot\mathsf{c}(x)$ (15)
$\displaystyle\mathsf{c}(xy)=\mathsf{c}(\mathsf{c}(x)\cdot y)$ (16)
$\displaystyle\mathsf{c}(x)\leq 1$ (17) $\displaystyle\mathsf{c}(0)=0$ (18)
$\displaystyle\mathsf{c}(x+y)=\mathsf{c}(x)+\mathsf{c}(y)$ (19)

Moreover, $\mathsf{c}$ has the following properties:

$\displaystyle\mathsf{c}(\mathsf{c}(x))=\mathsf{c}(x)$ (20)
$\displaystyle\mathsf{c}(x)\cdot\mathsf{c}(x)=\mathsf{c}(x)$ (21)
$\displaystyle\mathsf{c}(xy)\leq\mathsf{c}(y)$ (22) $\displaystyle x\leq
x\mathsf{c}(y)\implies\mathsf{c}(x)\leq\mathsf{c}(y)$ (23)

###### Proof.

For the codomain equations, see [5], Theorem 8.7, and the more detailed proof
of the theorem in Appendix D of [4]. The arguments there are given for the
domain and antidomain operators, but similar arguments work for codomain and
anticodomain.

The fixpoint property (20) follows from
$\mathsf{c}(xy)=\mathsf{c}(\mathsf{c}(x)\cdot y)$ and idempotence (21) follows
from the fixpoint property, $x\leq x\cdot\mathsf{c}(x)$, and
$\mathsf{c}(x)\leq 1$. The codomain restriction property (22) is established
by noting that
$\mathsf{c}(xy)\leq\mathsf{c}(\mathsf{c}(x)y)\leq\mathsf{c}(1y)\leq\mathsf{c}(y)$.
The least preserver property (23) is established by noting that $x\leq
x\mathsf{c}(y)$ implies
$\mathsf{c}(x)\leq\mathsf{c}(x\mathsf{c}(y))\leq\mathsf{c}(\mathsf{c}(y))\leq\mathsf{c}(y)$.
∎

######  Proposition 3.

Let $\mathsf{c}(K)=\\{x\mid x\in K\And\exists y.(x=\mathsf{c}(y))\\}$. In
every Kleene algebra with codomain,

  1. 1.

$(\mathsf{c}(K),\cdot,+,1,0)$ is a subalgebra of $(K,\cdot,+,1,0)$;

  2. 2.

$(\mathsf{c}(K),\cdot,+,1,0)$ is a bounded distributive lattice;

  3. 3.

$\mathsf{c}(x)+\mathsf{a}(\mathsf{c}(x))=1$ and
$\mathsf{c}(x)\cdot\mathsf{a}(\mathsf{c}(x))=0$.

Hence, $\mathsf{c}(\mathscr{K})=(\mathsf{c}(K),\cdot,+,\mathsf{a},1,0)$ is a
Boolean algebra.

###### Proof.

1\. follows from $\mathsf{c}(1)=1$, $\mathsf{c}(0)=0$,
$\mathsf{c}(x)+\mathsf{c}(y)=\mathsf{c}(x+y)$, and
$\mathsf{c}(x)\cdot\mathsf{c}(y)=\mathsf{c}(\mathsf{c}(x)\cdot\mathsf{c}(y))$.
We verified the latter using Prover 9 [16]. 2. follows from 1., together with
$\mathsf{c}(x)\leq 1$ and $\mathsf{c}(x)=\mathsf{c}(x)\mathsf{c}(x)$ of
Proposition 2. 3. follows from the axioms for $\mathsf{a}$. ∎

It can be shown that every full relational KAT can be seen as a KAC where
$\mathsf{a}$ is the relational anticodomain operation,
$\mathsf{a}(R):=\\{(u,u)\mid\neg\exists s.\,(s,u)\in R\\}$. Moreover,
Proposition 3 shows that every KAC gives rise to a KAT. A more detailed
argument involving a translation from the language of KAT into the language of
KAC then shows that the equational theory of KAT embeds into the equational
theory of KAC. We omit the details.

##  5 SKAT: Residuated KAC with a Galois connection

In this section, we introduce SKAT, an extension of KAC with both residuals of
Kleene algebra multiplication and the upper adjoint of the codomain operator.
The ∗-continuous variant of SKAT will be denoted as $\mathsf{SKAT^{*}}$. The
next section shows that S embeds into the equational theory of
$\mathsf{SKAT^{*}}$.

######  Definition 7.

An _$\mathsf{S}$ -type Kleene algebra with codomain_ is a structure of the
form $(K,\cdot,+,\to,\hookrightarrow\,^{*},\mathsf{a},\mathsf{e},1,0)$ where

  * •

$(K,\cdot,+,\hookrightarrow,\to,\,^{*},1,0)$ is a residuated Kleene algebra,

  * •

$(K,\cdot,+,\,^{*},\mathsf{a},1,0)$ is a Kleene algebra with codomain, and

  * •

$\mathsf{e}$ is a unary operation on $K$ that satisfies the following:

$\displaystyle\mathsf{a}(\mathsf{a}(\mathsf{e}(x)))\leq x$ (24) $\displaystyle
x\leq\mathsf{e}(\mathsf{a}(\mathsf{a}(x)))$ (25)
$\displaystyle\mathsf{e}(x)\leq\mathsf{e}(x+y)$ (26)

An $\mathsf{S}$-type Kleene algebra with codomain is ∗-continuous iff its
underlying Kleene algebra is ∗-continuous. The class of $\mathsf{S}$-type
Kleene algebras with codomain will be denoted as SKAT and the class of the
∗-continuous ones as $\mathsf{SKAT}^{*}$.

We will call $\mathsf{S}$-type Kleene algebras with codomain simply SKAT-
algebras. We will usually omit bracketing between elements of
$\\{\mathsf{a},\mathsf{e}\\}$, writing $\mathsf{e}\mathsf{c}(x)$ instead of
$\mathsf{e}(\mathsf{c}(x))$, for instance.

Every SKAT-algebra is a Kleene algebra with codomain by definition, and so the
test algebra $(\mathsf{c}(\mathscr{K}),\cdot,+,\mathsf{a},1,0)$ of each SKAT-
algebra $\mathscr{K}$ is a Boolean algebra. It is well known that residuated
Kleene algebras form a variety [18], and so SKAT forms a variety.

######  Proposition 4.

The following hold in each $\mathsf{SKAT}$-algebra:

$\displaystyle\mathsf{c}(x)\leq y\iff x\leq\mathsf{e}(y)$ (27)
$\displaystyle\mathsf{c}(x\to y)\leq x\to x\mathsf{c}(y)$ (28)
$\displaystyle\mathsf{a}(x)=\mathsf{c}(\mathsf{c}(x)\to 0)$ (29)

###### Proof.

(27) follows directly from the SKAT axioms concerning $\mathsf{e}$. (28) is
established as follows. Take any $z$ such that $\mathsf{c}(z)=z$; note that
$\mathsf{c}(x\to y)$ is of this form. We reason as follows:

  * $z\leq\mathsf{c}(x\to y)\implies zx\leq\mathsf{c}(x\to y)x\overset{(\ref{cod_locality})}{\implies}\mathsf{c}(zx)\leq\mathsf{c}((x\to y)x)$

  * $\implies\mathsf{c}(zx)\leq\mathsf{c}(y)\implies zx\mathsf{c}(zx)\leq\mathsf{c}(z)x\mathsf{c}(y)\implies zx\leq x\mathsf{c}(y)$

  * $\implies z\leq x\to x\mathsf{c}(y)\implies\mathsf{c}(z)\leq\mathsf{c}(x\to x\mathsf{c}(y))\implies z\leq\mathsf{c}(x\to x\mathsf{c}(y))$.

(29) is established as follows. Note that
$\mathsf{a}\mathsf{c}(x)=\mathsf{a}(x)$ by (13) and
$\mathsf{c}(x)\mathsf{a}(x)=\mathsf{a}(x)\mathsf{c}(x)$ by Proposition 3.
Hence, $\mathsf{a}(x)\leq\mathsf{c}(x)\to 0$ by (12) and residuation. It
follows that $\mathsf{c}\mathsf{a}(x)\leq\mathsf{c}(\mathsf{c}(x)\to 0)$ and
so $\mathsf{a}(x)\leq\mathsf{c}(\mathsf{c}(x)\to 0)$.

The converse inequality follows from

$x\mathsf{c}(y)=0\implies\mathsf{c}(x)\leq\mathsf{a}(y)$ (30)

In particular, $\mathsf{c}(\mathsf{c}(x)\to 0)\mathsf{c}(x)=0$ by (28), and so
$\mathsf{c}\mathsf{c}(\mathsf{c}(x)\to 0)\leq\mathsf{a}(x)$ by (30), which
means that $\mathsf{c}(\mathsf{c}(x)\to 0)\leq\mathsf{a}(x)$ by the fixpoint
property (20). The quasi-equation (30) is established similarly as the quasi-
equation (26) on p. 386 of [4]. If $x\mathsf{c}(y)=0$, then
$\mathsf{a}(\mathsf{c}(x)\mathsf{c}(y))=1$ and so
$\mathsf{c}(x)\mathsf{c}(y)=0$. But then

$\mathsf{c}(x)=\mathsf{c}(x)(\mathsf{c}(y)+\mathsf{a}(y))=\mathsf{c}(x)\mathsf{c}(y)+\mathsf{c}(x)\mathsf{a}(y)=\mathsf{c}(x)\mathsf{a}(y)\leq\mathsf{a}(y)\,.$

∎

We note that an extension of Kleene algebra with domain with a right residual
of Kleene algebra multiplication is considered in [4, 5]. However, the goal
there is to induce a Heyting algebra of tests, and $\to$ is assumed to be a
partial operation, defined only on the test algebra. It is also assumed that
the test algebra is closed under $\to$, which we may transpose to the setting
that uses codomain instead of domain as follows:

$\mathsf{c}(\mathsf{c}(x)\to\mathsf{c}(y))=\mathsf{c}(x)\to\mathsf{c}(y)$ (31)

In our setting, $\to$ is a total operation which is not included in the
signature of (Boolean) test algebras. It can also be shown that (31) does not
hold; see Fig. 3. Operations $\cdot$ and ∗ are defined as in Fig. 2,
$\hookrightarrow$ is identical to $\to$. It is easily verified that
$\mathsf{c}(0)\to\mathsf{c}(0)=\top$, and $\mathsf{c}(\top)=1$.

$0$$1$$\top$

$\to$ 0 1 $\top$ 0 $\top$ $\top$ $\top$ 1 0 1 $\top$ $\top$ 0 0 $\top$
$\mathsf{a}$ 0 1 $\top$ 1 0 $0$ $\mathsf{e}$ 0 1 $\top$ 0 $\top$ $\top$

Figure 3: A SKAT-algebra falsifying (31).

##  6 The embedding result

In this section we prove that S embeds into the equational theory of SKAT∗.

Let $\mathsf{X}=\\{\mathsf{x}_{i}\mid i\in\omega\\}$ be a countable set of
variables. The set of terms $Tm$ is the set of expressions formed using the
following grammar:

$p,q:=\mathsf{x}_{i}\mid 1\mid 0\mid p\cdot q\mid p+q\mid p\to q\mid
p^{*}\mid\mathsf{c}(p)\mid\mathsf{e}(p)\,.$

(We abuse the notation by re-using the same variables that range over programs
in S, but this will hopefully cause no confusion.) An equation is an ordered
pair of terms, denoted as $p\approx q$. We use $p\preceq q$ as short for
$p+q\approx q$. If $\mathscr{K}\in\mathsf{SKAT}$, then a _$\mathscr{K}$
-valuation_ is any homomorphism from $Tm$ into $\mathscr{K}$. An equation
$p\approx q$ _is satisfied_ by a $\mathscr{K}$-valuation  [ ] iff
$\scalebox{0.9}{{[}}p\scalebox{0.9}{{]}}=\scalebox{0.9}{{[}}q\scalebox{0.9}{{]}}$.
The equational theory of SKAT (SKAT∗) is the set of equations that are
satisfied by all $\mathscr{K}$ valuations where $\mathscr{K}\in\mathsf{SKAT}$
($\mathscr{K}\in\mathsf{SKAT}^{*}$).

######  Definition 8.

We define $Tr:Ex_{\mathsf{S}}\to Tm$ as follows:

  * •

$Tr(\mathsf{p}_{n})=\mathsf{x}_{2n}$

  * •

$Tr(\mathsf{b}_{n})=\mathsf{c}(\mathsf{x}_{2n+1})$

  * •

$Tr(0)=\mathsf{c}(0)$

  * •

$Tr(b\Rightarrow c)=\mathsf{c}(Tr(b)\to\mathsf{e}(Tr(c)))$

  * •

$Tr(p\oplus q)=Tr(p)+Tr(q)$

  * •

$Tr(p\otimes q)=Tr(p)\cdot Tr(q)$

  * •

$Tr(p^{+})=Tr(p)\cdot Tr(p)^{*}$

  * •

$Tr(p\Rightarrow f)=\mathsf{c}(Tr(p)\to\mathsf{e}(Tr(f)))$

  * •

$Tr(\epsilon)=1$

  * •

$Tr(\Gamma,\Delta)=Tr(\Gamma)\cdot Tr(\Delta)$

######  Theorem 2.

A sequent $\Gamma\vdash f$ is provable in $\mathsf{S}$ iff
$\mathsf{c}\big{(}Tr(\Gamma)\big{)}\leq Tr(f)$ belongs to the equational
theory of $\mathsf{SKAT}^{*}$.

Theorem 2 is established in two steps. First we show that every model $M$ of S
with a valuation  [ ] can be transformed into a
$\mathscr{M}\in\mathsf{SKAT}^{*}$ and a $\mathscr{M}$-valuation  [ [ ] ] such
that
$\scalebox{0.9}{{[}}\alpha\scalebox{0.9}{{]}}=\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}Tr(\alpha)\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}$
for all $\alpha\in Ex_{\mathsf{S}}$. Then we show by induction on the length
of $\mathsf{S}$-proofs that if $\Gamma\vdash f$ is provable in $\mathsf{S}$,
then $\mathsf{c}\big{(}Tr(\Gamma)\big{)}\preceq Tr(f)$ belongs to the
equational theory of $\mathsf{SKAT}^{*}$.

######  Lemma 1.

Let $M=(W,V)$ be a model of $\mathsf{S}$ and let  [ ] be a $M$-interpretation.
Then there is $\mathscr{M}\in\mathsf{SKAT}^{*}$ and a $\mathscr{M}$-valuation
[ [ ] ] such that, for all $\alpha\in Ex_{\mathsf{S}}$,

$\scalebox{0.9}{{[}}\alpha\scalebox{0.9}{{]}}=\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}Tr(\alpha)\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}$
(32)

###### Proof.

Fix $M=(W,V)$. Let $\mathscr{M}$ be the full relational residuated Kleene
algebra of binary relations on $W$; define
$\mathsf{a}(R)=\\{(u,u)\mid\neg\exists s.\,(s,u)\in R\\}$ and
$\mathsf{e}(R)=\\{(s,u)\mid(u,u)\in R\\}$; note that
$\mathsf{c}(R)=\\{(u,u)\mid\exists s.(s,u)\in R\\}$.222Recall that $R\to
Q=\\{(s,u)\mid\forall v.\,(u,v)\in R\implies(s,u)\in Q\\}$ and
$R\hookrightarrow Q=\\{(s,u)\mid\forall v.\,(v,s)\in R\implies(v,u)\in Q\\}$.
It is easily checked that $\mathscr{M}\in\mathsf{SKAT}^{*}$. In order to prove
(24), note that $(s,t)\in\mathsf{c}\mathsf{e}(R)$ only if $s=t$ and there is
$u$ such that $(u,t)\in\mathsf{e}(R)$, which holds only if $s=t$ and $(t,t)\in
R$. In order to prove (25), note that $(s,t)\in R$ implies
$(t,t)\in\mathsf{c}(R)$, which implies $(s,t)\in\mathsf{e}\mathsf{c}(R)$.
Finally, $\mathsf{e}$ is obviously monotonic, which entails (26).

Define  [ [ ] ] as the unique SKAT homomorphism from $Tm$ to $\mathscr{M}$
satisfying the following, for all $n\in\omega$:

  * •

$\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}\mathsf{x}_{2n}\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}=\scalebox{0.9}{{[}}\mathsf{p}_{n}\scalebox{0.9}{{]}}$;

  * •

$\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}\mathsf{x}_{2n+1}\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}=\scalebox{0.9}{{[}}\mathsf{b}_{n}\scalebox{0.9}{{]}}$.

We will prove (32) by induction on $\alpha$. First we prove that (32) holds
for all tests $b$ by induction on $b$. The base case is established as
follows. We know by definition that
$\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}Tr(\mathsf{b}_{n})\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}=\mathsf{c}\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}\mathsf{x}_{2n+1}\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}=\mathsf{c}\scalebox{0.9}{{[}}\mathsf{b}_{n}\scalebox{0.9}{{]}}$.
The latter is $\\{(u,u)\mid\exists
s.\,(s,u)\in\scalebox{0.9}{{[}}\mathsf{b}_{n}\scalebox{0.9}{{]}}\\}=\scalebox{0.9}{{[}}\mathsf{b}_{n}\scalebox{0.9}{{]}}$,
since
$\scalebox{0.9}{{[}}\mathsf{b}_{n}\scalebox{0.9}{{]}}\subseteq\mathrm{id}_{W}$.
The induction step is established as follows.
$\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}Tr(0)\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}=\mathsf{c}\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}0\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}=\emptyset=\scalebox{0.9}{{[}}0\scalebox{0.9}{{]}}$
and the other case uses (10) of Proposition 1 (we are working with a
relational Kleene algebra):

$\displaystyle\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}Tr(b\Rightarrow
c)\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}$
$\displaystyle=\mathsf{c}(\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}Tr(b)\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}\to\mathsf{e}\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}Tr(c)\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}})$
$\displaystyle=\mathsf{c}(\scalebox{0.9}{{[}}b\scalebox{0.9}{{]}}\to\mathsf{e}\scalebox{0.9}{{[}}c\scalebox{0.9}{{]}})$
$\displaystyle\overset{\eqref{teTo}}{=}\scalebox{0.9}{{[}}b\Rightarrow
c\scalebox{0.9}{{]}}$

This shows that (32) holds for all tests $b$. The fact that it holds for all
programs is established by easy induction ($Tr$ virtually commutes with Kleene
algebra operations). Next, we show that (32) holds for all formulas. The only
thing to prove is the induction step for $\alpha=p\Rightarrow f$. The claim
can be established using (10) as before. The claim for environments is
trivial. ∎

######  Lemma 2.

If $\Gamma\vdash f$ is provable in $\mathsf{S}$, then
$\mathsf{c}\big{(}Tr(\Gamma)\big{)}\preceq Tr(f)$ belongs to the equational
theory of $\mathsf{SKAT}^{*}$.

###### Proof.

We reason by induction on the length of proofs. We note that the proof of this
lemma, namely the claim for the (I+) rule, is the only point where the
assumption of ∗-continuity seems to be required.

A useful fact to note is that $Tr(f)$ is of the form $\mathsf{c}(p)$ for all
formulas $f$. By a translation of a sequent $\Gamma\vdash f$ we mean the
equation $\mathsf{c}(Tr(\Gamma))\preceq Tr(f)$. We will prove that
translations of axioms of $\mathsf{S}$ are in the equational theory of
$\mathsf{SKAT}^{*}$, and that if translations of all premises of an inference
rule of $\mathsf{S}$ are in the equational theory of $\mathsf{SKAT}^{*}$, then
so is the consequence of the rule. (If $p\preceq q$ is in the equational
theory of $\mathsf{SKAT}^{*}$, then we say that $p\preceq q$ is valid.)

  * (Id)

$\mathsf{c}(Tr(b))\preceq Tr(b)$ is valid since
$\mathsf{c}\mathsf{c}(x)\leq\mathsf{c}(x)$ by (20).

  * (I0)

$\mathsf{c}(Tr(\Gamma)\cdot Tr(0)\cdot Tr(\Delta))\preceq Tr(f)$ is valid
since $Tr(0)=\mathsf{c}(0)=0$.

  * (TC)

$\dfrac{\mathsf{c}\big{(}Tr(\Gamma)Tr(b)Tr(\Delta)\big{)}\preceq
Tr(f)\quad\mathsf{c}\big{(}Tr(\Gamma)Tr(b\Rightarrow
0)Tr(\Delta)\big{)}\preceq
Tr(f)}{\mathsf{c}\big{(}Tr(\Gamma)Tr(\Delta)\big{)}\preceq Tr(f)}$
preserves validity thanks to (19) and (29):

    * $\mathsf{c}(x\mathsf{c}(y)z)\leq a$ and $\mathsf{c}(x\mathsf{c}(\mathsf{c}(y)\to 0)z)\leq a$

    * $\overset{(\ref{cod_additive})}{\implies}$ $\mathsf{c}\big{(}x\mathsf{c}(y)z\,+\,x\mathsf{c}(\mathsf{c}(y)\to 0)z\big{)}\leq a$

    * $\overset{(\ref{cod_to_ant})}{\implies}$ $\mathsf{c}\big{(}x\mathsf{c}(y)z\,+\,x\mathsf{a}(y)z\big{)}\leq a$

    * $\implies$ $\mathsf{c}\big{(}x\big{(}\mathsf{c}(y)+\mathsf{a}(y)\big{)}z\big{)}\leq a$

    * $\overset{(\ref{ant_lem})}{\implies}$ $\mathsf{c}(xz)\leq a$

  * (cut)

$\dfrac{\mathsf{c}(Tr(\Gamma))\preceq
Tr(g)\qquad\mathsf{c}\big{(}Tr(\Gamma)Tr(g)Tr(\Delta)\big{)}\preceq
Tr(f)}{\mathsf{c}\big{(}Tr(\Gamma)Tr(\Delta)\big{)}\preceq Tr(f)}$
preserves validity thanks to (15) and (19):

    * $\mathsf{c}(x)\leq a_{2}$ and $\mathsf{c}(xa_{2}y)\leq a_{1}$

    * $\implies$ $x\mathsf{c}(x)y\leq xa_{2}y$ and $\mathsf{c}(xa_{2}y)\leq a_{1}$

    * $\overset{(\ref{cod_preserver})}{\implies}$ $xy\leq xa_{2}y$ and $\mathsf{c}(xa_{2}y)\leq a_{1}$

    * $\overset{(\ref{cod_additive})}{\implies}$ $\mathsf{c}(xy)\leq\mathsf{c}(xa_{2}y)$ and $\mathsf{c}(xa_{2}y)\leq a_{1}$

    * $\implies$ $\mathsf{c}(xy)\leq a_{1}$

  * (R$\Rightarrow$)

$\dfrac{\mathsf{c}(Tr(\Gamma)Tr(p))\preceq
Tr(f)}{\mathsf{c}(Tr(\Gamma))\preceq Tr(p\Rightarrow f)}$ preserves validity
thanks to (27) and (19):

    * $\mathsf{c}(xy)\leq z$ $\overset{(\ref{cod_Galois})}{\implies}$ $xy\leq\mathsf{e}(z)$

    * $\implies$ $x\leq y\to\mathsf{e}(z)$ $\overset{(\ref{cod_additive})}{\implies}$ $\mathsf{c}(x)\leq\mathsf{c}(y\to\mathsf{e}(z))$

  * (I$\Rightarrow$)

$\dfrac{\mathsf{c}\big{(}Tr(\Gamma)Tr(p)Tr(f)Tr(\Delta)\big{)}\preceq
Tr(g)}{\mathsf{c}\big{(}Tr(\Gamma)Tr(p\Rightarrow
f)Tr(p)Tr(\Delta)\big{)}\preceq Tr(g)}$ preserves validity thanks to (28) and
the fact that (27) entails
$\mathsf{c}\mathsf{e}\mathsf{c}(y)\leq\mathsf{c}(y)$:

$\displaystyle\mathsf{c}(x\to\mathsf{e}\mathsf{c}(y))x\,\leq\,(x\to
x\,\mathsf{c}\mathsf{e}\mathsf{c}(y))x\,\leq\,x\,\mathsf{c}\mathsf{e}\mathsf{c}(y)\,\leq\,x\mathsf{c}(y)$

(Recall that $Tr(p\Rightarrow f)=\mathsf{c}(q\to\mathsf{e}\mathsf{c}(r))$ for
some terms $q,r$.)

  * (I$\otimes)$

follows directly from the definition of $Tr$, and so do (E$\otimes$),
(I$\oplus$), (E$\oplus_{1}$) and (E$\oplus_{2}$).

  * (I+)

$\dfrac{\mathsf{c}(Tr(g)Tr(p))\preceq Tr(f)\quad\mathsf{c}(Tr(g)Tr(p))\preceq
Tr(g)}{\mathsf{c}\big{(}Tr(g)Tr(p)Tr(p)^{*}\big{)}\preceq Tr(f)}$.
It can be proven by induction on $n$, using (16), that if
$\mathsf{c}(yx)\leq\mathsf{c}(z)$ and $\mathsf{c}(yx)\leq y$, then $\forall
n\geq 0.\,\mathsf{c}(yxx^{n})\leq\mathsf{c}(z)$. By (27), $\forall n\geq
0.\,yxx^{n}\leq\mathsf{e}\mathsf{c}(z)$, and so by ∗-continuity
$yxx^{*}\leq\mathsf{e}\mathsf{c}(z)$, which means that
$\mathsf{c}(yxx^{*})\leq\mathsf{c}(z)$. (Note that ∗-continuity entails that
infinite suprema of elements of the form $xy^{*}z$ exist.) In fact, this is
the only point where we need to assume ∗-continuity.

  * (E+)

follows from the fact that $x\leq xx^{*}$ in Kleene algebras; and (CC+)
follows from the fact that $x^{*}xx^{*}\leq x^{*}$.

  * (W$f$)

$\dfrac{\mathsf{c}(Tr(\Gamma)Tr(\Delta))\preceq
Tr(g)}{\mathsf{c}(Tr(\Gamma)Tr(f)Tr(\Delta))\preceq Tr(g)}$ preserves validity
thanks to $\mathsf{c}(x)\leq 1$.

  * (W$p$)

$\dfrac{\mathsf{c}(Tr(\Gamma))\preceq
Tr(f)}{\mathsf{c}(Tr(p)Tr(\Gamma))\preceq Tr(f)}$ follows from (22).

This concludes the proof of the lemma. ∎

Now we are in the position to prove Theorem 2.

###### Proof.

If $\Gamma\vdash f$ is not provable in S, then there is a model $M$ and an
interpretation function  [ ] such that
$(w,u)\in\scalebox{0.9}{{[}}\Gamma\scalebox{0.9}{{]}}$ and
$(u,u)\notin\scalebox{0.9}{{[}}f\scalebox{0.9}{{]}}$ by Kozen and Tiuryn’s
relational completeness theorem. By Lemma 1, there is
$\mathscr{M}\in\mathsf{SKAT}^{*}$ and a $\mathscr{M}$-valuation  [ [ ] ] such
that
$(u,u)\in\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}\mathsf{c}(Tr(\Gamma))\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}$
and
$(u,u)\notin\scalebox{0.9}{{[}}\\!\\!\scalebox{0.9}{{[}}Tr(f)\scalebox{0.9}{{]}}\\!\\!\scalebox{0.9}{{]}}$.
Hence, $\mathsf{c}(Tr(\Gamma))\preceq Tr(f)$ is not in the equational theory
of SKAT∗. Conversely, if $\Gamma\vdash f$ is provable in S, then
$\mathsf{c}(Tr(\Gamma))\preceq Tr(f)$ is in the equational theory of SKAT∗ by
Lemma 2. ∎

##  7 Conclusion

We have shown in this paper that Kozen and Tiuryn’s substructural logic of
partial correctness S embeds into the equational theory of an extension of
∗-continuous Kleene algebra with codomain with both residuals of the Kleene
algebra multiplication and the upper adjoint of the codomain operator,
$\mathsf{SKAT}^{*}$. We believe that this result sheds more light on the
landscape of program logics and algebras.

A number of interesting problems remain open:

  1. 1.

Does $\mathsf{S}$ embed into the equational theory of $\mathsf{SKAT}$?

  2. 2.

Which residuated Kleene algebras extend to algebras in SKAT or SKAT∗? Is the
equational theory of SKAT (SKAT∗) a conservative extension of the equational
theory of residuated (∗-continuous) Kleene algebras?

  3. 3.

Related to the previous problem, is the equational theory of
$\mathsf{SKAT}^{*}$ identical to the equational theory of $\mathsf{SKAT}$? The
equational theory of ∗-continuous residuated Kleene algebras is not identical
to the equational theory of residuated Kleene algebras [1].

  4. 4.

What are the free algebras in $\mathsf{SKAT}$ and $\mathsf{SKAT}^{*}$? McLean
[17] shows that regular sets of labelled pointed trees form free Kleene
algebras with domain, and a version of his construction may turn out to apply
to our case as well.

  5. 5.

What is the complexity of the equational theories of $\mathsf{SKAT}$ and
$\mathsf{SKAT}^{*}$? The equational theory of ∗-continuous residuated Kleene
algebras is $\Pi^{0}_{1}$-complete (hence not r.e.) and the equational theory
of residuated Kleene algebras is $\Sigma^{0}_{1}$-complete.

  6. 6.

Consider the set of terms generated by the following restricted grammar:

$p,q:=\mathsf{x}_{i}\mid 1\mid 0\mid p\cdot q\mid p+q\mid
p^{*}\mid\mathsf{c}(p)\mid\mathsf{c}(p\to\mathsf{e}\mathsf{c}(q))\,.$

Is the fragment of the equational theory of $\mathsf{SKAT}$ restricted to
terms generated by this grammar decidable?

  7. 7.

What are the Gentzen systems sound and (weakly) complete for $\mathsf{SKAT}$,
in the style of [6]?

#### Acknowledgement

We are grateful to two anonymous reviewers for valuable suggestions. The first
author is grateful to Vít Punčochář for discussions that led to the work on
this paper, and to the audience at the Proof Theory Seminar of the Steklov
Mathematical Institute for illuminating discussion after his talk on 14
February 2022. The work of the second author was carried out within the
project Supporting the Internationalization of the Institute of Computer
Science of the Czech Academy of Sciences (no.
CZ.02.2.69/0.0/0.0/18_053/0017594), funded by the Operational Programme
Research, Development and Education of the Ministry of Education, Youth and
Sports of the Czech Republic. The project is co-funded by the EU.

## References

  * [1] W. Buszkowski.  On Action Logic: Equational Theories of Action Algebras.  Journal of Logic and Computation, 17(1):199–217, 10 2006.
  * [2] E. Cohen, D. Kozen, and F. Smith.  The complexity of Kleene algebra with tests.  Technical Report TR96-1598, Computer Science Department, Cornell University, July 1996.
  * [3] J. Desharnais, B. Möller, and G. Struth.  Kleene algebra with domain.  ACM Trans. Comput. Logic, 7(4):798–833, oct 2006.
  * [4] J. Desharnais and G. Struth.  Modal semirings revisited.  In International Conference on Mathematics of Program Construction, pages 360–387. Springer, 2008.
  * [5] J. Desharnais and G. Struth.  Internal axioms for domain semirings.  Science of Computer Programming, 76(3):181–203, 2011.  Special issue on the Mathematics of Program Construction (MPC 2008).
  * [6] P. Jipsen.  From semirings to residuated Kleene lattices.  Studia Logica, 76(2):291–303, Mar 2004.
  * [7] D. Kozen.  On Kleene algebras and closed semirings.  In B. Rovan, editor, International Symposium on Mathematical Foundations of Computer Science, pages 26–47. Springer, 1990.
  * [8] D. Kozen.  A completeness theorem for Kleene algebras and the algebra of regular events.  Information and Computation, 110(2):366 – 390, 1994.
  * [9] D. Kozen.  On action algebras.  In Logic and Information Flow, pages 78 – 88. MIT Press, 1994\.
  * [10] D. Kozen.  Kleene algebra with tests.  ACM Trans. Program. Lang. Syst., 19(3):427–443, May 1997.
  * [11] D. Kozen.  On Hoare logic and Kleene algebra with tests.  ACM Trans. Comput. Logic, 1(1):60–76, July 2000.
  * [12] D. Kozen.  Automata on guarded strings and applications.  Technical report, Cornell University, 2001.
  * [13] D. Kozen and F. Smith.  Kleene algebra with tests: Completeness and decidability.  In D. van Dalen and M. Bezem, editors, Computer Science Logic, pages 244–259, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg.
  * [14] D. Kozen and J. Tiuryn.  Substructural logic and partial correctness.  ACM Trans. Computational Logic, 4(3):355–378, July 2003.
  * [15] S. Kuznetsov.  Action logic is undecidable.  ACM Trans. Comput. Logic, 22(2):1–26, May 2021.
  * [16] W. McCune.  Prover9 and Mace4.  `http://www.cs.unm.edu/~mccune/prover9/`, 2005–2010.
  * [17] B. McLean.  Free kleene algebras with domain.  Journal of Logical and Algebraic Methods in Programming, 117:100606, 2020.
  * [18] V. Pratt.  Action logic and pure induction.  In Logics in AI. European workshop JELIA ’90, Amsterdam, the Netherlands, September 10-14, 1990. Proceedings, pages 97–120. Berlin etc.: Springer-Verlag, 1991.
  * [19] G. Restall.  An Introduction to Substrucutral Logics.  Routledge, London, 2000.