On Tools for Completeness of Kleene Algebra with Hypotheses

2025-05-02 0 0 706.68KB 55 页 10玖币

侵权投诉

Logical Methods in Computer Science

Volume 20, Issue 2, 2024, pp. 8:1–8:55

https://lmcs.episciences.org/

Submitted Oct. 25, 2022

Published May 16, 2024

ON TOOLS FOR COMPLETENESS

OF KLEENE ALGEBRA WITH HYPOTHESES

DAMIEN POUS a, JURRIAAN ROT b, AND JANA WAGEMAKER c

aCNRS, LIP, ENS de Lyon

e-mail address: Damien.Pous@ens-lyon.fr

bRadboud University, Nijmegen

e-mail address: Jurriaan.Rot@ru.nl

cReykjavik University, Reykjavik

e-mail address: janaw@ru.is

Abstract.

In the literature on Kleene algebra, a number of variants have been proposed

which impose additional structure speciﬁed by a theory, such as Kleene algebra with

tests (KAT) and the recent Kleene algebra with observations (KAO), or make speciﬁc

assumptions about certain constants, as for instance in NetKAT. Many of these variants

ﬁt within the unifying perspective oﬀered by Kleene algebra with hypotheses, which comes

with a canonical language model constructed from a given set of hypotheses. For the case

of KAT, this model corresponds to the familiar interpretation of expressions as languages

of guarded strings.

A relevant question therefore is whether Kleene algebra together with a given set of

hypotheses is complete with respect to its canonical language model. In this paper, we

revisit, combine and extend existing results on this question to obtain tools for proving

completeness in a modular way.

We showcase these tools by giving new and modular proofs of completeness for KAT,

KAO and NetKAT, and we prove completeness for new variants of KAT: KAT extended

with a constant for the full relation, KAT extended with a converse operation, and a version

of KAT where the collection of tests only forms a distributive lattice.

1. Introduction

Kleene algebras (KA) [

Kle56

Con71

] are algebraic structures involving an iteration operation,

Kleene star, corresponding to reﬂexive-transitive closure in relational models and to language

iteration in language models. Its axioms are complete w.r.t. relational models and language

models [

Koz91

Kro91

Bof90

], and the resulting equational theory is decidable via automata

algorithms (in fact, PSpace-complete [MS72, HRS76]).

This paper is an extended version of the paper with the same title which appeared in Proc. RAMiCS

2021 [

PRW21

]; we summarise the additions at the end of the Introduction. This work has been supported by

the ERC (CoVeCe, grant No 678157), by the LABEX MILYON (ANR-10-LABX-0070), within the program

ANR-11-IDEX-0007, and by the project ‘Mode(l)s of Veriﬁcation and Monitorability’ (MoVeMent) (grant No

217987) of the Icelandic Research Fund.

LOGICAL METHODS

IN COMPUTER SCIENCE DOI:10.46298/LMCS-20(2:8)2024

⃝Creative Commons

8:2 D. Pous, J. Rot, and J. Wagemaker Vol. 20:2

These structures were later extended in order to deal with common programming

constructs. For instance, Kleene algebras with tests (KAT) [

Koz97

], which combine Kleene

algebra and Boolean algebra, make it possible to represent the control ﬂow of while programs.

Kleene star is used for while loops, and Boolean tests are used for the conditions of such

loops, as well as the conditions in if-then-else statements. Again, the axioms of KAT are

complete w.r.t. appropriate classes of models, and its equational theory remains in PSpace.

Proving so is non-trivial: Kozen’s proof reduces completeness of KAT to completeness of

KA, via a direct syntactic transformation on terms.

Another extension is Concurrent Kleene algebra (CKA) [

HMSW11

], where a binary

operator for parallelism is added. The resulting theory is characterised by languages of

pomsets rather than languages of words, and is ExpSpace-complete [

BPS17

]. Trying to

have both tests and concurrency turned out to be non-trivial, and called for yet another

notion: Kleene algebras with observations (KAO) [

KBR+19

], which are again complete w.r.t.

appropriate models, and decidable.

When used in the context of program veriﬁcation, e.g., in a proof assistant, such

structures make it possible to write algebraic proofs of correctness, and to mechanise some

of the steps: when two expressions

and

representing two programs happen to be

provably equivalent in KA, KAT, or KAO, one does not need to provide a proof, one can

simply call a certiﬁed decision procedure [

BP10

KN12

Pou13

]. However, this is often not

enough [

KP00

AK01

HK02

]: most of the time, the expressions

and

are provably equal

only under certain assumptions on their constituents. For instance, to prove that (

)

∗

and

a∗b∗

are equal, one may have to use the additional assumption

. In other words,

one would like to prove equations under some assumptions, to have algorithms for the Horn

theory of Kleene algebra and its extensions rather than just their equational theories.

Unfortunately, those Horn theories are typically undecidable [

Koz96

Koz02

], even with

rather restricted forms of hypotheses (e.g., commutation of speciﬁc pairs of letters, as in the

above example). Nevertheless, important and useful classes of hypotheses can be ‘eliminated’,

by reducing to the plain and decidable case of the equational theory. This is, for instance,

the case for Hoare hypotheses [

Koz00

], of the shape

= 0, which allow to encode Hoare

triples for partial correctness in KAT.

In some cases, one wants to exploit hypotheses about speciﬁc constituents (e.g,

and

in the above example). In other situations, one wants to exploit assumptions on the whole

structure. For instance, in commutative Kleene algebra [

Red64

Con71

Bru19

], one assumes

that the product is commutative everywhere.

Many of these extensions of Kleene algebra (KAT, KAO, commutative KA, speciﬁc

hypotheses) ﬁt into the generic framework of Kleene algebra with hypotheses [

DKPP19

providing in each case a canonical model in terms of closed languages.

We show that we recover standard models in this way, and we provide tools to establish

completeness and decidability of such extensions, in a modular way. The key notion is

that of reduction from one set of hypotheses to another. We summarise existing reductions,

provide new ones, and design a toolbox for combining those reductions together. We use

this toolbox in order to obtain new and modular proofs of completeness for KAT, KAO and

NetKAT [

AFG+14

]; to prove completeness of KAT with a full element and KAT with a

converse operation, two extensions that were formerly proposed for KA alone, respectively

in [

PW22

] and [

B´

ES95

EB95

]; and to prove completeness for the variant of KAT where

tests are only assumed to form a distributive lattice.

Vol. 20:2 ON TOOLS FOR COMPLETENESS OF KLEENE ALGEBRA WITH HYPOTHESES 8:3

Outline. We ﬁrst recall Kleene algebra, Kleene algebra with hypotheses, and the key

concept of reduction (Section 2). Then we design a ﬁrst toolbox for reductions (Section 3):

a collection of primitive reductions, together with lemmas allowing one to combine them

together in a modular fashion. We exemplify those tools by using them to give a new proof

of completeness for KAT (Section 4).

After this ﬁrst example, we develop more systematic tools for reductions (Section 5):

lemmas to combine more than two reductions at a time, and lemmas to prove the resulting

side-conditions more eﬃciently. We ﬁnally demonstrate the ﬂexibility of our approach in

a series of examples of increasing complexity: KAO (Section 6), KAT with a full element

(Section 7), KAT with converse (Section 8), KA with positive tests (KAPT—Section 9), and

NetKAT (Section 10).

The ﬁrst appendix contains an abstract theory of least closures in complete lattices,

which we base our toolbox on (Appendix A). Two subsequent appendices contain proofs

omitted from the main text (a direct soundness proof for Kleene algebra with hypotheses—

Appendix B, and proofs related to guarded strings for KAT—Appendix C).

Diﬀerences with the conference version. This paper is a revised and extended version of

an earlier paper in the proceedings of RaMiCS 2021 [

PRW21

]. Besides various improvements,

and inclusion of most proofs, here are the main diﬀerences w.r.t. the conference version.

Section 3.3 is new, it provides a general technique to construct reductions via ﬁnite

automata. We use it to establish some of the basic reductions from Section 3.4.

With the exception of Proposition 5.1, Section 5 on advanced tools is new (e.g., Propo-

sition 5.3 or development on overlaps). This section makes it possible to present most

examples using ‘tables’ (Tables 1 to 5), which we consider as a new contribution concerning

methodology. Lemma 3.10, which makes it possible to obtain reductions for hypotheses of

the shape e≤1 is also new; we need it to deal with NetKAT.

The examples of KAT with a full element, KAT with converse, and NetKAT, are new

(Sections 7, 8 and 10); the example of KAPT (Section 9) is presented more uniformly,

thanks to the new tools. Appendix A on the abstract theory of least closures is entirely

new; it makes it possible to get rid of all proofs by transﬁnite induction that we used in the

conference version. Appendix C was publicly available via the author version of [

PRW21

but not oﬃcially published.

Preliminaries, notation. We write 1 for the empty word and

for the concatenation of

two words

u, v

. Given a set

, subsets of

form a complete lattice

⟨P(X),⊆,S⟩

. Given

two functions

f, g

, we write

f◦g

for their composition: (

f◦g

)(

) =

(

)). We write

for

the identity function. Functions into a complete lattice, ordered pointwise, form a complete

lattice where suprema are computed pointwise. We reuse the same notations on such lattices:

for instance, given two functions

f, g :Y→ P

(

), we write

f⊆g

when

∀y∈Y, f

(

)

⊆g

(

or f∪gfor the function mapping y∈Yto f(y)∪g(y).

A function

f:P

(

)

→ P

(

) is monotone if for all

S, S′∈ P

(

S⊆S′

implies

(

)

⊆f

(

S′

); it is a closure if it is monotone and satisﬁes

id ⊆f

and

f◦f⊆f

. When

a closure, we have

f◦f

, and for all

S, S′

S⊆f

(

S′

) iﬀ

(

)

⊆f

(

S′

). These notions are

generalised to arbitrary complete lattices in Appendix A.

8:4 D. Pous, J. Rot, and J. Wagemaker Vol. 20:2

2. Kleene algebra with hypotheses, closures, reductions

AKleene algebra [

Con71

Koz91

] is a tuple (

,·,∗,

1) such that (

,·,

1) is an

idempotent semiring, and

∗

is a unary operator on

such that for all

x, y ∈K

the following

axioms are satisﬁed:

1 + x·x∗≤x∗x+y·z≤z⇒y∗·x≤z x +y·z≤y⇒x·z∗≤y

Here, as later in the paper, we write

x≤y

as a shorthand for

. Given the

idempotent semiring axioms,

≤

is a partial order in every Kleene algebra, and all operations

are monotone w.r.t. that order. The seemingly missing law 1 +

x∗·x≤x∗

is derivable from

these axioms.

Languages over some alphabet, as well as binary relations on a given set, are standard

examples of Kleene algebras.

We let e, f range over regular expressions over an alphabet Σ, deﬁned by:

e, f ::= e+f|e·f|e∗|0|1|a∈Σ

We write T(Σ) for the set of such expressions, or simply Twhen the alphabet is clear from

the context. We usually write

for

e·f

, and

for

e·e∗

. Given alphabets Σ and Γ, a

function

→ T

(Γ) extends uniquely to a homomorphism

h:T

(Σ)

→ T

(Γ), referred to

as the homomorphism generated by

. As usual, every regular expression

gives rise to a

language

JeK∈ P

(Σ

∗

). Given regular expressions

e, f

, we write

KA ⊢e

when

derivable from the axioms of Kleene algebra. (Equivalently, when the equation

holds

universally, in all Kleene algebras.)

The central theorem of Kleene algebra is the following:

Theorem 2.1 (Soundness and Completeness of KA [

Koz91

Kro91

Bof90

]).For all regular

expressions e, f ∈ T, we have:

KA ⊢e=fif and only if JeK=JfK.

As a consequence, the equational theory of Kleene algebras is decidable.

2.1. Hypotheses. Our goal is to extend this result to the case where we have additional

hypotheses on some of the letters of the alphabet, or axioms restricting the behaviour of

certain operations. Those are represented by sets of inequations, i.e., pairs (

e, f

) of regular

expressions written

e≤f

for the sake of clarity. Given a set

of such inequations, we write

KAH⊢e≤f

when the inequation

e≤f

is derivable from the axioms of Kleene algebra

and the hypotheses in

(similarly for equations). By extension, we write

KAH⊢H′

when

KAH⊢e≤f

for all

e≤f

H′

. Since the ambient theory will systematically be KA, we

will sometimes abbreviate KAH⊢H′as H⊢H′, to alleviate notation.

Note that we consider letters of the alphabet as constants rather than variables. In

particular, while we have

KAba≤ab ⊢

(

)

∗≤a∗b∗

, we do not have

KAba≤ab ⊢

(

)

∗≤a∗c∗

Formally, we use a notion of derivation where there is no substitution rule, and where we have

all instances of Kleene algebra axioms as axioms. When we want to consider hypotheses that

are universally valid, it suﬃces to use all their instances. For example, to deﬁne commutative

Kleene algebra, we simply use the inﬁnite set {ef ≤fe |e, f ∈ T}.

Vol. 20:2 ON TOOLS FOR COMPLETENESS OF KLEENE ALGEBRA WITH HYPOTHESES 8:5

2.2. Closures associated to hypotheses. We associate a canonical language model to

Kleene algebra with a set of hypotheses H, deﬁned by closure under H[DKPP19].

For u, v ∈Σ∗and L⊆Σ∗, let uLv ≜{uxv |x∈L}.

Deﬁnition 2.2 (

-closure).Let

be a set of hypotheses and let

L⊆

∗

be a language.

The

-closure of

, denoted as

H⋆

(

), is the smallest language containing

such that for

all e≤f∈Hand u, v ∈Σ∗, if uJfKv⊆H⋆(L), then uJeKv⊆H⋆(L).

For every set of hypotheses H,H⋆is indeed a closure (also see Section 3.1).

In many cases,

will consist of inequations whose members are words rather than

arbitrary expressions. In that case, there is an intuitive string rewriting characterisation

of the function

H⋆

. Given words

u, v

, we write

⇝

when

can be obtained from

replacing an occurrence as a subword of the right-hand side of an inequation of

by its

left-hand side. Further write

⇝

∗

for the reﬂexive-transitive closure of

⇝

. Then we have

u∈H⋆(L) iﬀ u

⇝

∗

Hvfor some word v∈L.

Example 2.3. Let

{ab ≤bc}

. We have

baab

⇝

Hbabc

⇝

Hbbcc

, whence

baab ∈

H⋆({bbcc}). For L=Jbc∗K, we have H⋆(L) = Ja∗bc∗K.

This notion of closure gives a closed interpretation of regular expressions,

H⋆J−K

, for

which KAHis sound:

Theorem 2.4. KAH⊢e=fimplies H⋆JeK=H⋆JfK.

Proof.

This is basically [

DKPP19

, Theorem 2], which is proved there by constructing a

model of

KAH

. We provide a direct proof in Appendix B, by induction on the derivation.

In the sequel, we shall prove the converse implication, completeness, for speciﬁc choices

of H: we say that KAHis complete if for all expressions e, f:

H⋆JeK=H⋆JfKimplies KAH⊢e=f .

Remark 2.5. Thanks to the presence of sum in the syntax of regular expressions (so that

KAH⊢e≤f

iﬀ

KAH⊢e

), and to the fact that

H⋆

is a closure, we have the

following counterpart to Theorem 2.4 for soundness w.r.t inequations:

KAH⊢e≤fimplies JeK⊆H⋆JfK.

Similarly, KAHis complete if and only if for all expressions e, f,

JeK⊆H⋆JfKimplies KAH⊢e≤f .

We could hope that completeness always holds, notably because the notion of closure

is invariant under inter-derivability of the considered hypotheses, as a consequence of the

following lemma:

Lemma 2.6 [

KBS+20

, Lemma 4.10].Let

and

H′

be sets of hypotheses. If

H⊢H′

then

H′⋆⊆H⋆.

(There, H′⋆⊆H⋆means pointwise inclusion of functions, i.e., for all L,H′⋆(L)⊆H⋆(L).)

Another property witnessing the canonicity of the

-closed language interpretation is

that it is sound and complete w.r.t. ∗-continuous models [DKPP19, Theorem 2].

Unfortunately, there are concrete instances for which

KAH

is known to be incomplete.

For instance, there is a ﬁnitely presented monoid (thus a ﬁnite set

of equations) such

that

{(e, f)|H0⋆JeK=H0⋆JfK}

is not recursively enumerable [

KM14

, Theorem 1]. Since

derivability in KAHis recursively enumerable as soon as His, KAH0cannot be complete.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

LogicalMethodsinComputerScienceVolume20,Issue2,2024,pp.8:1–8:55https://lmcs.episciences.org/SubmittedOct.25,2022PublishedMay16,2024ONTOOLSFORCOMPLETENESSOFKLEENEALGEBRAWITHHYPOTHESESDAMIENPOUSa,JURRIAANROTb,ANDJANAWAGEMAKERcaCNRS,LIP,ENSdeLyone-mailaddress:Damien.Pous@ens-lyon.frbRadboudUniversity,N...

展开>> 收起<<

On Tools for Completeness of Kleene Algebra with Hypotheses.pdf

共55页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

On Tools for Completeness of Kleene Algebra with Hypotheses

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: