=Paper=
{{Paper
|id=None
|storemode=property
|title=Simplifying Pointer Kleene Algebra
|pdfUrl=https://ceur-ws.org/Vol-760/paper4.pdf
|volume=Vol-760
|dblpUrl=https://dblp.org/rec/conf/ate/DangM11
}}
==Simplifying Pointer Kleene Algebra==
https://ceur-ws.org/Vol-760/paper4.pdf
Simplifying Pointer Kleene Algebra
Han-Hing Dang∗, Bernhard Möller
Institut für Informatik, Universität Augsburg
D-86135 Augsburg, Germany
{dang,moeller}@informatik.uni-augsburg.de
Abstract
Pointer Kleene algebra has proved to be a useful abstraction for reasoning about reach-
ability properties and correctly deriving pointer algorithms. Unfortunately it comes with
a complex set of operations and defining (in)equations which exacerbates its practicability
with automated theorem proving systems but also its use by theory developers. Therefore
we provide an easier access to this approach by simpler axioms and laws which also are more
amenable to automatic theorem proving systems.
1 Introduction
Nowadays many first-order automated theorem proving systems are powerful enough and hence
applicable to a large variety of verification tasks. Algebraic approaches especially have already
been successfully treated by automatic reasoning in different application ranges [7, 8, 9, 16]. This
work concentrates on an algebraic calculus for the derivation of abstract properties of pointer
structures, namely pointer Kleene algebra [5]. This approach has proved to be an appropriate
abstraction for reasoning about pointer structures and the deduction of various pointer algo-
rithms [12, 13, 14]. Moreover the algebra enables by its (in)equation-based axioms the use of
automated theorem provers for deriving and proving assertions about pointer structures, e.g.,
concerning reachability, allocation and destructive updates. When analysing reachability, pro-
jections are used to constrain the links of interest. For instance, in a doubly linked list the set of
links in forward and backward direction each must be cycle-free, whereas, of course, the overall
link set is cyclic. Unfortunately the existing pointer algebra turns out to be difficult to handle
and to hinder automation. Therefore we provide a simplified version of pointer Kleene algebra
which, additionally, is more suitable for automation.
The paper is organised as follows: In Section 2, we define a concrete graph-based model of
pointer structures and illustrate the operations of pointer algebra in Section 3. Moreover some
basics are given on which these specific operations build. Section 4 then gives more suitable
axioms for automated deduction systems which are also easier to understand than the original
theory. We conclude with an outlook on further applications of this approach in Section 5.
2 A Matrix Model of Pointer Kleene Algebra
We start by giving a concrete model of pointer Kleene algebra that shows how to treat various
typical concepts of pointer structures algebraically. This model is based on matrices and rep-
resents the graph structure of storage with pointer links between records or objects. In [4] the
model is also called a fuzzy model because it builds on some notions from the theory of fuzzy
sets.
We assume a finite set L of edge labels of a graph with the known operations ∪, ∩. Moreover,
let V be a finite set of vertices. Then the carrier set P(L)V ×V of the model consists of matrices
∗
Research was partially sponsored by DFG Project ALGSEP — Algebraic Calculi for Separation Logic
20
Simplifying Pointer Kleene Algebra H.-H. Dang, B. Möller
with vertices in V as indices and subsets of L as entries. An entry A(x, y) = M ⊆ L in a
matrix A means that in the represented graph there are |M | edges from vertex x to vertex y,
labelled with the elements of M . The complete algebraic structure is (P(L)V ×V , ∪, ; , 0, 1, >)
with greatest element > and operators, for arbitrary matrices A, B ∈ P(L)V ×V and x, y ∈ V ,
(A ∪ B)(x, y) =df A(x, y) ∪ B(x, y) ,
S
(A; B)(x, y) =df z∈V (A(x, z) ∩ B(z, y)) ,
>(x, y) =df L,
0(x, y) =df ∅,
L if x = y ,
1(x, y) =df
∅ otherwise .
As an example consider a tree structure with L =df {left, right, val}. Clearly, the labels left
and right represent links to the left and right son (if present) of a node in a tree, respectively.
The destination of the label val is interpreted as the value of such a node. We will use “label”
and “link” as synonyms in the following. Figure 1 depicts a sample matrix and its corresponding
labelled directed graph, i.e., a tree with V =df {vi , ci : 1 ≤ i ≤ 3}.
v1 v2 v3 c1 c2 c3
v1 ∅ {left} {right} {val} ∅ ∅
v2 ∅ ∅ ∅ ∅ {val} ∅
v3 ∅ ∅ ∅ ∅ ∅ {val} c1 val v1
c1 ∅ ∅ ∅ ∅ ∅ ∅ left right
c2 ∅ ∅ ∅ ∅ ∅ ∅ c2 val v2 v3 val c3
c3 ∅ ∅ ∅ ∅ ∅ ∅
Figure 1: Example matrix and the corresponding labelled graph
Multiplication with the > matrix turns out to be quite useful for a number of issues. Left-
multiplying a matrix A with > produces a matrix where each column contains the union of the
labels in the corresponding column of A. Dually, right-multiplying a matrix A with > produces
a matrix where each row contains the union of the labels in the corresponding row of A. Finally,
multiplying A with > from both sides gives a constant matrix where each entry consists of the
union of all labels occurring in A.
L11 ··· L1n L1 · · · Ln L11 ··· L1n M1 ··· M1
.. .. = .. .. .. .. · > = .. .. (1)
>· . ··· . . ··· . . ··· . . ··· .
Ln1 · · · Lnn L1 · · · Ln Ln1 · · · Lnn Mn · · · Mn
S S
where Li = 1≤j≤n Lij and Mj = 1≤i≤n Lij . This entails
L11 ··· L1n M ··· M
.. .. · > = .. ..
>· . ··· . . ··· . (2)
Ln1 ··· Lnn M ··· M
S S
where M = Lij . Such matrices can be used to represent sets of labels in the model.
1≤j≤n 1≤i≤n
21
Simplifying Pointer Kleene Algebra H.-H. Dang, B. Möller
3 Basics and the Original Approach
Abstracting from the matrix model of pointer Kleene algebra we now define some fundamental
notions and explain special operations of the algebra. The basic algebraic structure of pointer
Kleene algebra in the sense of [4] is a quantale [1, 15]. This is, first, an idempotent semiring, i.e.,
a structure (S, +, ·, 0, 1), where + abstracts ∪ and · abstracts ; , and the following is required:
• (S, +, 0) forms an idempotent commutative monoid and (S, ·, 1) a monoid. This means,
for arbitrary x, y, z ∈ S,
x + (y + z) = (x + y) + z , x + y = y + x , x + 0 = 0 , x + x = x ,
x · (y · z) = (x · y) · z , x·1=x , 1·x=x .
• Moreover, · has to distribute over + and 0 has to be a multiplicative annihilator, i.e., for
arbitrary x, y, z ∈ S,
x · (y + z) = (x · y) + (x · z) , (x + y) · z = (x · z) + (y · z) ,
x·0=0 , 0·x=0 .
The natural order ≤ on an idempotent semiring is defined by x ≤ y ⇔df x + y = y. It is easily
verified that the matrix model indeed forms an idempotent semiring in which the natural order
coincides with pointwise inclusion of matrices.
Second, to form a quantale, (S, ≤) has to be a complete lattice and multiplication · has to
distribute over arbitrary joins. By this, + coincides with the binary supremum operator t. The
binary infimum operator is denoted by u ; in the model it coincides with the pointwise ∩ of
matrices. The greatest element of the quantale is denoted by >.
This structure is now enhanced to a Kleene algebra [10] by an iteration operator ∗ , axioma-
tised by the following unfold and induction laws:
1 + x · x∗ = x∗ , x · y + z ≤ y ⇒ x∗ · z ≤ y ,
1 + x∗ · x = x∗ , y · x + z ≤ y ⇒ z · x∗ ≤ y .
Besides this, the algebra considers special subidentities p ≤ 1, called tests. Multiplication
by a test therefore means restriction. Tests can also be seen as an algebraic counterpart of
predicates and thus have to form a Boolean subalgebra. The defining property is therefore that
a test must have a complement relative to 1, i.e., an element ¬p that satisfies p + ¬p = 1 and
p · ¬p = 0 = ¬p · p. In the matrix model tests are matrices that have non-empty entries at most
on their main diagonal; multiplication of a matrix M with a test p means pointwise intersection
of the rows or columns of M with the corresponding diagonal entry in p.
3.1 The Original Theory
An essential ingredient of pointer Kleene algebra is an operation that projects all entries of a
given matrix to links of a subset L0 ⊆ L. This is modelled by scalars 1 [4], which are tests
α, β, . . . that additionally commute with >, i.e., α · > = > · α. Analogously to (1) and (2) these
are diagonal matrices which are constant on the main diagonal. We will use the notation L(α)
to denote the unique set of labels that a scalar α comes with. By this, a scalar α in the model
corresponds to the matrix
L(α) if x = y ,
α(x, y) =
∅ otherwise .
1
The origin of this term lies in fuzzy relation theory and has similar behaviour as scalars in vector spaces.
22
Simplifying Pointer Kleene Algebra H.-H. Dang, B. Möller
It is immediate from the axioms that 0 and 1 are scalars.
Describing projection needs additional concepts. First, for arbitrary element x and scalar α,
α\x = x + ¬α · > . (3)
In the matrix model this adds the complement of L(α) to every entry in x. More abstractly, the
operation is a special instance of the left residual defined by the Galois connection x ≤ y\z ⇔df
x · y ≤ z; but this is of no further importance here.
The next concepts employed are the completion operator ↑ and its dual ↓ , also known from
the algebraic theory of fuzzy sets [18]. For arbitrary x, y ∈ S they are axiomatised as follows.
x↑ ≤ y ⇔ x ≤ y ↓ , (x · y ↓ )↑ = x↑ · y ↓ ,
(4)
α is a scalar and α 6= 0 implies α↑ = 1 , (x↓ · y)↑ = x↓ · y ↑ .
In the matrix model they can be described for a matrix M as follows
↑ L if M (x, y) 6= ∅ , ↓ L if M (x, y) = L ,
M (x, y) = M (x, y) =
∅ otherwise , ∅ otherwise .
In both cases each node x is either totally linked or not linked at all with another node y. Such
matrices containing only the entries ∅ and L are also called crisp [4]. They behave analogous to
Boolean matrices where ∅ plays the role of 0 and L the one of 1. In the abstract algebra crisp
elements are characterised by the equation x↑ = x. In particular, M ↑ maps a matrix M to the
least crisp matrix containing it, while M ↓ maps M to the greatest crisp matrix it contains.
Based on these operations and the particular elements of the algebra, projections Pα ( ) to
label sets L(α) represented by a scalar α can be abstractly defined for arbitrary x ∈ S by
Pα (x) =df α · (α\x)↓ . (5)
In the matrix model, projections w.r.t. scalars α are used to restrict each entry of a matrix
exactly to L(α). As an example consider the resulting matrix of the following projection with
L(α) = {left, right}
∅ {right} {left} {val} ∅ ∅ ∅ ∅
∅ ∅ ∅ {left, right}
) = ∅ ∅ ∅ {left, right}
P{left,right} (
{val} {left, right}
.
∅ ∅ ∅ {left, right} ∅ ∅
∅ {val} ∅ ∅ ∅ ∅ ∅ ∅
To see that this is achieved by Equation (5) consider first the term α\x in the matrix model.
This can be rewritten using Equation (3) into the term x + ¬α · >. Hence residuals add to each
entry of x all labels not in L(α). The operation ↓ is then used to keep only those entries in α\x
that contain the full set of labels L while all other label sets will be mapped to ∅. Finally the
multiplication with the scalar α again reduces all remaining L entries to L(α).
Finally we turn to the most important operator of pointer Kleene algebra. It calculates all
reachable nodes from a given set of nodes. The definition uses domain and codomain operations
p and q . They are characterised by the following equations, for arbitrary element x and test p,
x ≤ px · x , p(p · x) ≤ p , x ≤ x · xq , (x · p)q ≤ p .
We note that a third pair of axioms, the modality laws p(x · y) = p(x · py) and (x · y)q = (xq · y)q ,
is omitted here, because they are implied by another special property that holds for the matrix
23
Simplifying Pointer Kleene Algebra H.-H. Dang, B. Möller
model and also the algebra of binary relations. For domain, it reads x · > = px · > and is called
subordination of domain, since the direction x · > ≤ px · > follows from the above axioms, but the
reverse one does not. This is equivalent [4] to px = x · > u 1, which we postulate as an additional
axiom. This and the dual one for codomain then entail the above-mentioned modality laws.
Both operations are mappings from general elements to tests, i.e., the resulting matrices
in the model are diagonal matrices. More concretely, the domain operation extracts for every
vertex the set of labels on its outgoing edges while the codomain operator returns the labels on
the incoming edges. As a simple example for domain consider
p ∅ {right} {left}
{left, right} ∅ ∅
∅ ∅ {left, right} = ∅ {left, right} ∅ .
{val} {left, right} ∅ ∅ ∅ {left, right, val}
In [4] reachability is now defined by a mapping that takes two arguments: One argument
represents the set of starting nodes or addresses from which the reachable vertices are computed.
The other argument represents the graph structure in which the reachability analysis takes
place. Address sets are represented in this approach by crisp tests: an address belongs to the
set represented by p iff the corresponding entry in the main diagonal of p is L. Now assume
that m represents an address set. Then reach(m, x) is defined using the iteration operator ∗ by
∗
reach(m, x) = (m · (x↑ ) )q . (6)
The mapping reach calculates a test representing the set of vertices that are reachable from m
using arbitrarily labelled graph links of x. This “forgetting” of the concrete label sets is modelled
by completing the graph using the completion operator ↑ . Sample properties one wants to prove
about reach are
reach(m + n, x) = reach(m, x) + reach(n, x) , reach(reach(m, x), x) = reach(m, x) .
To restrict reachability analysis to a subset of labels, projections are combined with reach into
the mapping reach(m, Pα (x)) for a scalar α. By this, non-α links are deleted from x.
Finally, an important operation in connection with pointer structures is overriding one struc-
ture x by another one y, denoted y|x =df y + ¬py · x. Here entries of x for which also y provides
a definition are replaced by these and only the part of x not affected by y is preserved. This
operator enjoys a rich set of derived algebraic properties. For instance, it is interesting to see in
which way an overwriting affect reachability. One sample law for this is
py ↑ u reach(m, x) = 0 ⇒ reach(m, y|x) = reach(m, x) ,
i.e., when the domain of the overriding structure is not reachable from the overridden one it
does not affect reachability.
3.2 A Discussion on Automation
One sees that it is very onerous to define the domain specific operations of pointer Kleene
algebra from the basic operations. For example projections already include special subidentities
of the algebra, residuals and completion and its dual, where each operator itself comes with
lots of (in)equations defining behaviour. Furthermore by Equation (6) reach also uses crisp
subidentities and moreover includes the ↑ , iteration ∗ and the codomain operation. The inclusion
of that many axioms often irritates the proof systems and additionally increases the search space.
24
Simplifying Pointer Kleene Algebra H.-H. Dang, B. Möller
A naive encoding of these operations in the first-order automated theorem proving system2
Prover9 [11] already revealed that only a small set of basic properties for projections and reacha-
bility calculations could be derived automatically. We used this theorem prover since it performs
best for automated reasoning tasks within the presented basic algebraic structures [2]. Moreover,
it comes with the useful counterexample search engine Mace4 and outputs semi-readable proofs,
which often provide helpful hints. Of course, any other first-order ATP system could also be
used with the abstract algebraic approach, e.g., through the TPTP problem library [17].
The resulting ineffective automation could be due to the indirect axiomatisation of ↓ through
↑ by a Galois connection (cf. Definition (4)). In particular, deriving theorems for ↓ will often
require to show results for ↑ and vice versa. Furthermore, encoding subtypes as tests and
scalars by predicates may be another hindrance to a simple treatment of the axioms by ATP
systems. Such an encoding is also inappropriate for ATP systems like Waldmeister [6] which works
completely equation-based.
Moreover, using the Galois characterisation of residuals instead of the explicit characterisa-
tion in Equation (3) seems to additionally exacerbate the proof search. However, including that
characterisation does not seem to simplify the proof search significantly. Therefore we also got a
similar result with the application of ATP system when reasoning about restricted reachability.
Finally the given axiomatisations of the specific operators for this particular domain are
also difficult to grasp and handle for theory developers due to their complexity. Therefore, in
the next section we provide a simpler approach to pointer Kleene algebra which is easier to
understand and more amenable to ATP systems.
4 A Simpler Theory for Pointer Kleene Algebra
The preceding section has shown that the original pointer algebra uses quite a number of concepts
and ingredients. The present section is intended to show that one can do with a smaller toolbox
which also is more amenable to automation. As a first simplification we drop the assumption
that address sets need to be interpreted by crisp elements. Plain test elements also suffice to
represent source nodes for reach(p, x) since x is by definition already completed.
4.1 Projection
We continue with the notion of projecting a graph to a subgraph that is restricted to a set of
labels. For this we first want to find representatives for sets of labels in our algebra.
It is clear that constant matrices and sets of labels are in one-to-one correspondence. By
intersecting a constant matrix with the identity matrix one obtains a test which in the main
diagonal contains the represented set M of labels, see (1). Multiplying another matrix A with
this test from either side intersects all entries in A with M and hence projects A to the label
set M . The considered test can also be got by taking the domain of the resulting matrix. Note
that neither scalars nor residuals nor the operator ↓ are involved here.
The difference of the just described way to project matrices and projections Pα (x) can be
made clear in the example given after Equation (5). By our approach only the {val} entries of
the original matrix will be deleted while single {left} and {right} entries remain. It is reasonable
also to consider such entries in reachability calculations.
2
We abbreviate the term “automated theorem proving system” to ATP system in the following.
25
Simplifying Pointer Kleene Algebra H.-H. Dang, B. Möller
4.2 Domain and Codomain
As a further simplification, plain test elements can be represented in the algebra by domain or
codomain elements. In particular, such elements form Boolean subalgebras, resp. We give their
axiomatisation through a(x) and ac(x) which are the complements of the domain and codomain
of x, resp. From these domain and codomain can be retrieved as px = a(a(x)) and xq = ac(ac(x)).
The axioms read as follows:
a(x) · x = 0 , x · ac(x) = 0 ,
a(a(x)) + a(x) = 1 , ac(ac(x)) + ac(x) = 1 ,
a(x · y) ≤ a(x · a(a(y))) , ac(x · y) ≤ ac(ac(ac(x)) · y) .
The idea with this approach is to avoid explicit subsorting, i.e., introducing the set of tests as
a sort of its own, say by using predicates that assert that certain elements are tests, and to
characterise the tests implicitly as the images of the antidomain/anticodomain operators. The
axioms entail that those images coincide and form a Boolean algebra with + and · as join and
meet, resp.
The given characterisation seems to be still difficult to handle for ATP systems in that form.
Often a lot of standard Boolean algebra properties have to be derived first. Therefore we propose
an equivalent but more “efficient” axiomatisation at the end of the next section.
4.3 Completion
Next, we turn to the completion operator ↑ which is useful in analysing link-independent reach-
ability in graphs. Rather than axiomatising it indirectly through a Galois connection we char-
acterise it jointly with its complement ↑ similarly to domain and antidomain in Section 4.2. In
particular, we axiomatise x↑ as a left annihilator of x w.r.t. u, paralleling the statement that
a(x) is a left annihilator for x w.r.t. composition · .
The axioms show some similarity to the domain/antidomain ones, but also substantial dif-
ferences on which we will comment below. However, we still have, analogously to px = a(a(x)),
that x↑ = (x↑ )↑ ; for better readability we use this as an abbreviation in the axioms:
1↑ ≤ 1 , x↑ u x ≤ 0 , > ≤ 0↑ ,
x↑ u y ↑ = (x + y)↑ , x↑ + y ↑ = (x↑ u y ↑ )↑ ,
(x · y ↑ )↑ = x↑ · y ↑ , (x↑ · y)↑ = x↑ · y ↑ .
Notice that the inequations can be strengthened to equations. The most striking difference
to antidomain are the De-Morgan-like axioms and the axioms concerning multiplication. We
cannot use the axiom x · y ↑ ≤ (x · y ↑ )↑ instead because it is not valid in the matrix model.
Therefore the De Morgan laws do not follow but rather have to be put as additional axioms.
They clearly state that the image of ↑ is closed under u and +.
We list a number of useful consequences of the axioms; they are all very quickly shown by
Prover9. A sample input file can be found in the appendix.
x ≤ x↑ , >↑ = > , 0↑ = 0 ,
↑ ↑ ↑
(x ) = x , ↑
> =0, 0↑ = > ,
(x↑ + y ↑ )↑ = x↑ u y ↑ , (x↑ u y ↑ )↑ = x↑ + y ↑ ,
(x↑ + y ↑ )↑ = x↑ u y ↑ , (x↑ u y ↑ )↑ = x↑ + y ↑ ,
x ≤ y ⇒ y ↑ ≤ x↑ , x ≤ y ⇒ x↑ ≤ y ↑ ,
x↑ = 0 ⇔ x = 0 , x↑ = > ⇔ x = 0 , x↑ = 0 ⇔ x = 0 ,
↑ ↑ ↑
(x ) = x , ↑ ↑ ↑ ↑ ↑
(x · y ) = x · y , (x + y)↑ = x↑ + y ↑ .
26
Simplifying Pointer Kleene Algebra H.-H. Dang, B. Möller
In particular, the image of ↑ and hence of ↑ , i.e., the set of crisp elements, forms a Boolean
algebra. Moreover, ↑ is a closure operator. By general results therefore ↑ preserves all existing
suprema and, in a complete lattice, has an upper adjoint, which of course is ↓ . To axiomatise
↓ we can use the Galois adjunction x↑ ≤ y ⇔ x ≤ y ↓ . This entails standard laws as e.g.
(x · y ↓ )↑ = x↑ · y ↓ , (x↓ · y)↑ = x↑ · y ↓ , (x↓ )↑ ≤ x , x ≤ (x↑ )↓ .
With the help of ↓ one can show that the image of ↑ is also closed under the iteration ∗ . A last
speciality concerns the domain/codomain operation. By the subordination axiom for domain it
can be verified that p(x↑ ) = (px)↑ .
Altogether we retrieve Ehm’s result that, in a semiring with domain, the image of ↑ , forms
again a Kleene algebra with domain. Extending that, our axiomatisation yields that this algebra
is even Boolean.
Inspired by the above axiomatisation, we now present a new axiomatisation of antidomain
and anticodomain that explicitly states De-Morgan-like dualities to facilitate reasoning.
a(x) · x = 0 , a(0) = 1 , x · ac(x) = 0 , ac(0) = 1 ,
a(x) · a(y) = a(x + y) , ac(x) · ac(y) = ac(x + y) ,
a(x) + a(y) = a(a(a(x)) · a(a(y))) , ac(x) + ac(y) = ac(ac(ac(x)) · ac(ac(y))) ,
a(x · y) ≤ a(x · a(a(y))) , ac(x · y) ≤ ac(ac(ac(x)) · y) .
Using Prover9 we have shown that this axiomatisation is equivalent to the standard axiomati-
sation of antidomain/anticodomain. And indeed, the automatic proofs of the Boolean algebra
properties of tests as well as of the mentioned properties of reach are much faster with it.
5 Outlook
This work provides a more suitable axiomatisation of special operations used in pointer Kleene
algebra. These axioms are more applicable for ATP systems since less operations and less
subtypes of the algebra has to be considered. Moreover the (in)equations of our approach
enables a simpler encoding of the algebra for ATP systems due to explicit subsorting. This
will also partially include the usage of ATP systems as Waldmeister for such particular problem
domains.
It can be seen that the axiomatisations of antidomain (or anticodomain) and anticompletion
are very similar. This motivates to further abstract from the concrete involved operations and
to define a restriction algebra that replays general derivations.
Moreover, this approach will be used to characterise sharing and sharing patterns in pointer
structures within an algebraic approach to separation logic [3]. This will include the ability to
reason algebraically about reachability in abstractly defined data structures.
References
[1] J. H. Conway. Regular Algebra and Finite Machines. Chapman & Hall, 1971.
[2] H.-H. Dang and P. Höfner. First-order theorem prover evaluation w.r.t. relation- and Kleene algebra.
In R. Berghammer, B. Möller, and G. Struth, editors, Relations and Kleene Algebra in Computer
Science — PhD Programme at RelMiCS 10/AKA 05, number 2008-04 in Technical Report, pages
48–52. Institut für Informatik, Universität Augsburg, 2008.
[3] H.-H. Dang, P. Höfner, and B. Möller. Algebraic separation logic. Journal of Logic and Algebraic
Programming, 80(6):221–247, 2011.
27
Simplifying Pointer Kleene Algebra H.-H. Dang, B. Möller
[4] T. Ehm. The Kleene Algebra of Nested Pointer Structures: Theory and Applications. PhD thesis,
Fakultät für Angewandte Informatik, Universität Augsburg, 2003.
[5] T. Ehm. Pointer Kleene algebra. In R. Berghammer, B. Möller, and G. Struth, editors, RelMiCS,
volume 3051 of Lecture Notes in Computer Science, pages 99–111. Springer, 2004.
[6] T. Hillenbrand, A. Buch, R. Vogt, and B. Löchner. WALDMEISTER - High-Performance Equational
Deduction. Journal of Automated Reasoning, 18:265–270, 1997.
[7] P. Höfner and G. Struth. Automated reasoning in Kleene algebra. In F. Pfenning, editor, Automated
Deduction — CADE-21, volume 4603 of Lecture Notes in Artificial Intelligence, pages 279–294.
Springer, 2007.
[8] P. Höfner and G. Struth. On automating the calculus of relations. In A. Armando, P. Baumgartner,
and G. Dowek, editors, Automated Reasoning (IJCAR 2008), volume 5159 of Lecture Notes in
Computer Science, pages 50–66. Springer, 2008.
[9] P. Höfner, G. Struth, and G. Sutcliffe. Automated verification of refinement laws. Annals of Math-
ematics and Artificial Intelligence, 55:35–62, February 2009.
[10] D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Information
and Computation, 110(2):366–390, 1994.
[11] W. McCune. Prover9 and Mace4.
. (accessed July 26, 2011).
[12] B. Möller. Some applications of pointer algebra. In M. Broy, editor, Programming and Mathematical
Method, number 88 in NATO ASI Series, Series F: Computer and Systems Sciences, pages 123–155.
Springer, 1992.
[13] B. Möller. Calculating with pointer structures. In Proceedings of the IFIP TC2/WG 2.1 International
Workshop on Algorithmic Languages and Calculi, pages 24–48. Chapman & Hall, 1997.
[14] B. Möller. Calculating with acyclic and cyclic lists. Information Sciences, 119(3-4):135–154, 1999.
[15] K. I. Rosenthal. Quantales and their Applications, volume 234 of Pitman Research Notes in Mathe-
matics Series. Longman Scientific & Technical, 1990.
[16] G. Struth. Reasoning automatically about termination and refinement. In S. Ranise, editor, 6th
International Workshop on First-Order Theorem Proving, volume Technical Report ULCS-07-018,
Department of Computer Science, pages 36–51. University of Liverpool, 2007.
[17] G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts,
v3.5.0. Journal of Automated Reasoning, 43(4):337–362, 2009.
[18] M. Winter. A new algebraic approach to L-fuzzy relations convenient to study crispness. Information
Sciences, 139(3-4):233–252, 2001.
A Prover9 Encoding of Pointer Kleene Algebra
1 op(450, infix, "+"). % Addition
2 op(440, infix, ";"). % Multiplication
3 op(420, infix, "^"). % Meet
4 op(400, postfix, "*"). % Iteration
5 op(410, prefix, "@"). % Antidomain
6 op(410, prefix, "!"). % Anticodomain
7 op(410, prefix, "?"). % Anticompletion
8 % --- Additive commutative and idempotent monoid
9 x+(y+z) = (x+y)+z.
10 x+y = y+x.
11 x+0 = x.
12 x+x = x.
13 % --- Order
14 x <= y <-> x+y = y.
15 % --- Definition of top
16 x <= T.
28
Simplifying Pointer Kleene Algebra H.-H. Dang, B. Möller
17 % --- Multiplicative monoid
18 x;(y;z) = (x;y);z.
19 1;x = x.
20 x;1 = x.
21 % --- Distributivity laws
22 x;(y+z) = x;y + x;z.
23 (x+y);z = x;z + y;z.
24 % ---Annihilation
25 0;x = 0.
26 x;0 = 0.
27 % --- Definition of meet
28 (x<=y & x<=z) <-> x <= y^z.
29 x^(y+z) = x^y + x^z.
30 % --- Definition of domain
31 @0 = 1.
32 @x;x = 0.
33 @x;@y = @(x+y).
34 @x+@y = @(@@x;@@y).
35 @(x;y) = @(x;@@y).
36 @@x = (x;T) ^ 1. % --- Subordination of domain
37 % --- Definition of anticodomain
38 !0 = 1.
39 x;!x = 0.
40 !x;!y = !(x+y).
41 !x+!y = !(!!x;!!y).
42 !(x;y) = !(!!x;y).
43 !!x = (T;x) ^ 1. % --- Subordination of codomain
44 % --- Definition of completion
45 ??1 = 1.
46 ?0 = T.
47 ?x^x = 0.
48 ?x ^ ?y = ?(x + y).
49 ?x + ?y = ?(??x ^ ??y).
50 ??(x ; ??y) = ??x ; ??y.
51 ??(??x ; y) = ??x ; ??y.
52 % --- Iteration - Unfold laws
53 1 + x ; x* = x*.
54 1 + x* ; x = x*.
55 % --- Iteration - Induction laws
56 x;y + z <= y -> x* ; z <= y.
57 y;x + z <= y -> z ; x* <= y.
58 % --- Reachability
59 reach(x,y) = !!(@@x;(??y)*).
60 % --- Projection
61 P(x,y) = @@((T;x);T);y.
29