1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta http-equiv="content-language" content="en">
<meta name="author" content="Damien Pous">
<meta name="keywords" content="Coq proof assistant; Relation algebra; Kleene algebra; Kleene algebra with tests; KAT; regular expressions; finite automata; decision procedure; matrices; matrix; binary relations">
<style type="text/css">
<!--
#toc {
position: fixed;
left: 0;
top: 0;
background-color:#DDF;
padding:10px;
}
#toc ul li { list-style: none; margin: 0px; padding: 0px }
#toc a { text-decoration:none }
#contents { margin-left:13%; margin-right:5% }
-->
</style>
<title>Relation Algebra and KAT in Coq</title>
</head>
<body>
<div id="toc">
<a href="#desc">Description</a><br>
<a href="#apps">Applications</a><br>
<a href="#download">Download</a><br>
<a href="#relw">Related papers</a><br>
<a href="#doc">Documentation</a><br>
. <a href="#doc:tac">tactics</a><br>
. <a href="#doc:list">modules</a><br>
. <a href="#doc:deps">dependencies</a><br>
<a href="#notes">Notes</a><br>
<a href="#authors">Authors</a>
<a href="#ack">Acknowledgements</a>
</div>
<div id="contents">
<p align="right"><a href="http://perso.ens-lyon.fr/damien.pous/">Damien Pous' home page</a></p>
<h1 id="desc">Relation Algebra and KAT in Coq</h1>
<table>
<tr>
<td>
<p>
This Coq development is a modular library about relation algebra:
those algebras admitting heterogeneous binary relations as a model,
ranging from partially ordered monoid to residuated Kleene allegories
and Kleene algebra with tests (KAT). </p>
<p> This library presents this large family of algebraic theories in a
modular way; it includes several high-level reflexive
tactics:</p> <ul>
<li> <code>kat</code>, which decides the (in)equational theory of KAT;
<li> <code>hkat</code>, which decides the Hoare (in)equational theory of KAT
(i.e., KAT with Hoare hypotheses);
<li> <code>ka</code>, which decides the (in)equational theory of KA;
<li> <code>ra</code>, a normalisation based partial decision procedure for Relation
algebra;
<li> <code>ra_normalise</code>, the underlying normalisation tactic.
</ul>
</td>
<td>
<img src="ra.png" alt="the cloud of relation algebra fragments">
</td>
</tr>
</table>
<p>
The tactic for Kleene algebra with tests is obtained by reflection,
using a simple bisimulation-based algorithm working on the appropriate
automaton of partial derivatives, for the generalised regular
expressions corresponding to KAT.
Combined with a formalisation of KA completeness, and then of KAT
completeness on top of it, this provides entirely axiom-free decision
procedures for all models of these theories (including relations,
languages, traces, min-max and max-plus algebras, etc...). </p>
<p>
Algebraic structures are generalised in a categorical way: composition
is typed like in categories, allowing us to reach "heterogeneous"
models like rectangular matrices or heterogeneous binary relations,
where most operations are partial. We exploit untyping theorems to
avoid polluting decision algorithms with these additional typing
constraints.
</p>
<h2 id="apps"> Applications </h2>
<p>
We give a few examples of applications of this library to program
verification: </p>
<ul>
<li> a formalisation of a paper by Dexter Kozen and Maria-Cristina Patron.
showing how to certify compiler optimisations using KAT.
(See <a
href="http://www.cs.cornell.edu/~kozen/papers/opti.pdf">their paper</a>,
and the Coq module
<code><a href="html/RelationAlgebra.compiler_opts.html">compiler_opts</a></code>.)
<li> a formalisation of the IMP programming language, followed by: 1/ some
simple program equivalences that become straightforward to prove
using our tactics; 2/ a formalisation of Hoare logic rules for partial correctness in the
above language: all rules except the assignation one are proved by a
single call to the <code>hkat</code> tactic. (See module <code><a href="html/RelationAlgebra.imp.html">imp</a></code>)
<li> a proof of the equivalence of two flowchart schemes, due to
Paterson. The informal paper proof takes one page; Allegra Angus and
Dexter Kozen gave a six pages long proof using KAT; our Coq proof is
about 100 lines.
(See <a
href="http://www.cs.cornell.edu/~kozen/papers/allegra.pdf">Angus and Kozen's paper</a>
and the Coq module <code><a href="html/RelationAlgebra.paterson.html#lab13">paterson</a></code>.)
</ul>
<h2 id="download">Download</h2>
This library is available through opam, under the name <em>coq-relation-algebra</em>,
as well as on <a href="https://github.com/damien-pous/relation-algebra">GitHub</a>.
<h2 id="relw">Related papers or talks</h2>
<ul>
<li> The tactic for KAT and its various applications are described
in <br>
<a href="http://dx.doi.org/10.1007/978-3-642-39634-2_15">
<em>Kleene Algebra with Tests and Coq Tools for while Programs</em></a>.
D. Pous, in Proc. ITP'13, LNCS 7998, July 2013.
<li> A beta version of this library was presented at <a
href="http://www.cl.cam.ac.uk/conference/ramics13/">RAMiCS</a>, September 2012: <a href="http://www.cl.cam.ac.uk/conference/ramics13/pous.pdf">slides</a>.
<li> The generalisation to typed structures, and the untyping
theorems are explained in details in <br>
<a href="http://perso.ens-lyon.fr/damien.pous/utas">
Untyping Typed Algebras and Colouring Cyclic Linear Logic</a>.
D. Pous, <em>Logical Methods in Computer Science</em>, 2012.<br>
<li> A description of ATBR, the ancestor of this library (see the <a
href="#notes">notes</a> below) appeared in<br>
<a href="http://www.lmcs-online.org/ojs/viewarticle.php?id=934&layout=abstract"><em>
Deciding Kleene Algebras in Coq</em></a>.
T. Braibant and D. Pous, <em>Logical Methods in Computer Science</em>,
2012.<br><br>
<li> We closely follow the work of Dexter Kozen for KA and KAT
completeness proofs:
<ul>
<li>
<a href="http://www.cs.cornell.edu/~kozen/papers/ka.pdf">
A completeness theorem for Kleene algebras and the algebra of
regular events</a>.
D. Kozen. <em>Information and Computation</em>, 110(2):366-390, May 1994.
<li>
<a href="http://www.cs.cornell.edu/~kozen/papers/gs.pdf">
Kleene algebra with tests: Completeness and
decidability</a>.
D. Kozen and F. Smith.
In Proc. <em>CSL'96</em>, vol. 1258 of LNCS, pages 244-259, 1996.
Springer-Verlag.
</ul>
<li> Our decision algorithm for KAT is probably folklore: its uses
the obvious generalisation of the partial derivatives automaton to
KAT regular expressions, together with a standard on-the-fly bisimulation
algorithm. See the following papers for the coalgebraic treatment of
KA and KAT:
<ul>
<li> <a
href="http://www.cwi.nl/~janr/papers/files-of-papers/1998_CONCUR_automata_and_coinduction.pdf">
Automata and coinduction (an exercise in coalgebra)</a>.
J. Rutten. In Proc <em>CONCUR '98</em>, LNCS 1466, Springer, 1998, pp. 194-218.
<li> <a href="http://www.cs.cornell.edu/~kozen/papers/ChenPucella.pdf">
On the coalgebraic theory of Kleene algebra with tests</a>.
D. Kozen.
Technical Report, Computing and Information Science, Cornell University, March 2008.
</ul>
</ul>
<h2 id="doc">Documentation</h2>
<h3 id="doc:tac">Provided tactics</h3>
<ul>
<li> Decision tactics:
<ul>
<li> <code>ka</code>: equational theory of Kleene algebra;
<li> <code>kat</code>: equational theory of Kleene algebra with tests;
<li> <code>hkat</code>: Hoare theory of Kleene algebra with tests:
it exploits hypotheses of the shape <code>p==0</code>,
<code>[a]==[b]</code>, <code>[a]*p == p*[a]</code>, <code>[a]*p ==
[p]</code>, <code>[a]*p == [p]</code>, and all similar ones.
<li> <code>lattice</code>: solves lattice (in)equations, using
focused proof search (modular tactic: it works from preorders to
bounded distributed lattices).
</ul>
<li> Incomplete decision tactics:
<ul>
<li> <code>ra</code>: tries to solve relation algebra (in)equations, by
normalisation and comparison. This tactic is modular: it applies
to all algebraic theories present in the library.
<li> <code>hlattice</code>: tries to solve the Horn theory of lattices
(modular tactic)
</ul>
<li> Normalisation tactics:
<ul>
<li> <code>ra_normalise</code>: normalise the current goal (modular tactic);
<li> <code>ra_simpl</code>: normalise the current goal, without
distributing composition over unions (modular tactic).
</ul>
<li> Rewriting tactics:
<ul>
<li> <code>mrewrite</code>: rewriting modulo associativity of
composition (ad-hoc tactic); more AC rewriting tools are available using the <code>AAC_tactics</code> library.
</ul>
<li> Other tactics:
<ul>
<li> <code>lattice.dual</code>: prove goals by lattice duality;
<li> <code>monoid.dual</code>: prove goals by categorical duality;
<li> <code>neg_switch</code>: revert a goal to exploit the Boolean
negation involution;
<li> <code>cnv_switch</code>: revert a goal to exploit the
converse involution.
</ul>
</ul>
<h3 id="doc:list">Succinct description of each module</h3>
<p>Each module is documented; links below point to the coqdoc generated
documentation; see <a href="#doc:deps">below for dependencies</a>.
The coqdoc table of contents is <a href="html/toc.html">here</a>.</p>
<ul>
<li>Utilities
<ul>
<li> <code><a href="html/RelationAlgebra.common.html">common</a></code>: basic tactics and definitions used
throughout the library
<li> <code><a href="html/RelationAlgebra.comparisons.html">comparisons</a></code>: types with decidable equality
and ternary comparison function
<li> <code><a href="html/RelationAlgebra.positives.html">positives</a></code>: simple facts about binary positive numbers
<li> <code><a href="html/RelationAlgebra.ordinal.html">ordinal</a></code>: finite ordinals, finite sets of
finite ordinals
<li> <code><a href="html/RelationAlgebra.pair.html">pair</a></code>: encoding pairs of ordinals as ordinals
<li> <code><a href="html/RelationAlgebra.powerfix.html">powerfix</a></code>: simple pseudo-fixpoint iterator
<li> <code><a href="html/RelationAlgebra.lset.html">lset</a></code>: sup-semilattice of finite sets represented as lists
</ul>
<li>Algebraic hierarchy
<ul>
<li> <code><a href="html/RelationAlgebra.level.html">level</a></code>: bitmasks allowing us to refer to an
arbitrary point in the hierarchy
<li> <code><a href="html/RelationAlgebra.lattice.html">lattice</a></code>: ``flat'' structures, from preorders
to Boolean lattices
<li> <code><a href="html/RelationAlgebra.monoid.html">monoid</a></code>: typed structures, from partially
ordered monoids to residuated Kleene lattices
<li> <code><a href="html/RelationAlgebra.kat.html">kat</a></code>: Kleene algebra with tests
<li> <code><a href="html/RelationAlgebra.kleene.html">kleene</a></code>: Basic facts about Kleene algebra
<li> <code><a href="html/RelationAlgebra.factors.html">factors</a></code>: Basic facts about residuated structures
<li> <code><a href="html/RelationAlgebra.relalg.html">relalg</a></code>: Standard relation algebra facts and definitions
</ul>
<li>Models
<ul>
<li> <code><a href="html/RelationAlgebra.prop.html">prop</a></code>: distributed lattice of Prop-ositions
<li> <code><a href="html/RelationAlgebra.boolean.html">boolean</a></code>: Boolean trivial lattice, extended
to a monoid.
<li> <code><a href="html/RelationAlgebra.rel.html">rel</a></code>: heterogeneous binary relations
<li> <code><a href="html/RelationAlgebra.srel.html">srel</a></code>: heterogeneous binary relations over setoids
<li> <code><a href="html/RelationAlgebra.fhrel.html">fhrel</a></code>: heterogeneous binary relations over finite types (requires <code>ssreflect</code>)
<li> <code><a href="html/RelationAlgebra.lang.html">lang</a></code>: word languages (untyped)
<li> <code><a href="html/RelationAlgebra.traces.html">traces</a></code>: trace languages (typed and untyped)
<li> <code><a href="html/RelationAlgebra.glang.html">glang</a></code>: guarded string languages (typed and untyped)
</ul>
<li>Free models
<ul>
<li> <code><a href="html/RelationAlgebra.lsyntax.html">lsyntax</a></code>: free lattice (Boolean expressions)
<li> <code><a href="html/RelationAlgebra.atoms.html">atoms</a></code>: atoms of the free Boolean lattice over a finite set
<li> <code><a href="html/RelationAlgebra.syntax.html">syntax</a></code>: free relation algebra
<li> <code><a href="html/RelationAlgebra.regex.html">regex</a></code>: regular expressions (untyped)
<li> <code><a href="html/RelationAlgebra.gregex.html">gregex</a></code>: generalised regular expressions
(typed - for KAT completeness)
<li> <code><a href="html/RelationAlgebra.ugregex.html">ugregex</a></code>: untyped generalised regular
expressions (for KAT decision procedure)
<li> <code><a href="html/RelationAlgebra.kat_reification.html">kat_reification</a></code>: tools and definitions for
KAT reification
</ul>
<li>Relation algebra tools
<ul>
<li> <code><a href="html/RelationAlgebra.normalisation.html">normalisation</a></code>: normalisation and
semi-decision tactics for relation algebra
<li> <code><a href="html/RelationAlgebra.rewriting.html">rewriting</a></code>: rewriting modulo associativity of composition
<li> <code><a href="html/RelationAlgebra.rewriting_aac.html">rewriting_aac</a></code>: bridge with AAC_tactics (requires <code>AAC_tactics</code>)
<li> <code><a href="html/RelationAlgebra.move.html">move</a></code>: tools to easily move subterms inside a product
</ul>
<li>Linear algebra
<ul>
<li> <code><a href="html/RelationAlgebra.sups.html">sups</a></code>: finite suprema/infima (a la bigop from
ssreflect)
<li> <code><a href="html/RelationAlgebra.sums.html">sums</a></code>: finite sums
<li> <code><a href="html/RelationAlgebra.matrix.html">matrix</a></code>: matrices over all structures
supporting this construction
<li> <code><a href="html/RelationAlgebra.matrix_ext.html">matrix_ext</a></code>: additional operations and
properties about matrices
<li> <code><a href="html/RelationAlgebra.rmx.html">rmx</a></code>: matrices of regular expressions
<li> <code><a href="html/RelationAlgebra.bmx.html">bmx</a></code>: matrices of Booleans
</ul>
<li>Untyping theorems
<ul>
<li> <code><a href="html/RelationAlgebra.untyping.html">untyping</a></code>: untyping theorem for structures
below Kleene algebra with converse
<li> <code><a href="html/RelationAlgebra.kat_untyping.html">kat_untyping</a></code>: untyping theorem for guarded
string languages (and thus, KAT)
</ul>
<li>Automata
<ul>
<li> <code><a href="html/RelationAlgebra.dfa.html">dfa</a></code>: deterministic finite state automata,
decidability of language inclusion
<li> <code><a href="html/RelationAlgebra.nfa.html">nfa</a></code>: matricial non-deterministic finite
state automata, formal evaluation into regular expressions
<li> <code><a href="html/RelationAlgebra.ugregex_dec.html">ugregex_dec</a></code>: decision of guarded string
language equivalence of generalised regular expressions, using
partial derivatives
</ul>
<li>Completeness
<ul>
<li> <code><a href="html/RelationAlgebra.ka_completeness.html">ka_completeness</a></code>: (untyped) completeness of Kleene algebra
<li> <code><a href="html/RelationAlgebra.kat_completeness.html">kat_completeness</a></code>: (typed) completeness of Kleene
algebra with tests
<li> <code><a href="html/RelationAlgebra.kat_tac.html">kat_tac</a></code>: decision tactics for KA and KAT,
elimination of Hoare hypotheses to get <code>hkat</code>
</ul>
<li>Applications to program verification
<ul>
<li> <code><a href="html/compiler_opts.html">compiler_opts</a></code>: verification of compiler
optimisations in KAT
<li> <code><a
href="html/paterson.html">paterson</a></code>:
challenging equivalence of two flowchart schemes, due to Paterson
<li> <code><a href="html/imp.html">imp</a></code>: formalisation of the IMP programming
language, proving program equivalence using KAT, embedding of
Hoare logic for partial correctness
</ul>
</ul>
<h3 id="doc:deps">Modules dependencies</h3>
<div align="left">
<svg width="600pt" height="600pt" viewBox="0.00 0.00 1160 1052.00"
xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<use xlink:href="depgraph.svg#graph0"></use>
</svg>
</div>
<h2 id="notes">Notes</h2>
<p> This library started by a complete rewrite of the <a
href="http://sardes.inrialpes.fr/~braibant/atbr">ATBR</a> library we
developed with Thomas Braibant. There was two main reasons for not
reusing this code: </p>
<ul>
<li> The way we designed the algebraic hierarchy in ATBR, using
typeclasses, did not scale to the richer structures we present here (converse,
residuals, allegories), was not modular enough, and did not allow us
to define easily the Boolean lattice of tests needed in KAT. Here we
follow a completely different approach, which seems to scale pretty
well but required restarting from scratch.
<li> The fact that we were proving the (algebraic) completeness of
KA using the efficient algorithm we designed for deciding language
equivalence of regular expressions was sub-optimal: as a consequence
of this choice, our proofs were over-complicated. Instead, by using
a different path here, we prove KA completeness in about 200 lines
of definitions and 200 lines of proofs. This refactorisation was
essential to reach KAT with a reasonable amount of efforts.
</ul>
<h2 id="authors">Authors</h2>
<ul>
<li> Damien Pous (2012-), CNRS - LIP, ENS Lyon (UMR 5668), France
<li> Christian Doczkal (2018-), CNRS - LIP, ENS Lyon (UMR 5668), France
<li> Insa Stucke (2015-2016), Dpt of CS, University of Kiel, Germany
<li> Coq development team (2013-)
</ul>
<h2 id="ack">Acknowledgements</h2>
I am grateful to Thomas Braibant, with whom we developed the ancestor
of this library, clearing the ground for this subsequent work.
</div>
<br><br>
<hr>
<address>http://perso.ens-lyon.fr/damien.pous/ra/</address>
</body> </html>
|
