Pointer Kleene algebra has proved to be a useful abstraction for reasoning about reachability properties and correctly deriving pointer algorithms. Unfortunately it comes with a complex set of operations and de ning (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.
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 jM j 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 2 P(L)V V and x; y 2 V , (A [ B)(x; y) (A; B)(x; y) >(x; y) 0(x; y) 1(x; y) =df =df =df =df =df
A(x; y) [ B(x; y) ; Sz2V (A(x; z) \ B(z; y)) ; L ; ; ; ; L if x = y ; otherwise :
As an example consider a tree structure with L =df fleft; right; valg. 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 fvi; ci : 1 i 3g.
v1 v2 v3 c1 c2 c3 v1 ; ; ; ; ; ;
v2 fleftg
v3 frightg
c1 fvalg ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; c2 ; fvalg ; ; ; ; c3 ; ; fvalg ; ; ; c1 val v1
left c2 val v2 right v3 val c3
Multiplication with the > matrix turns out to be quite useful for a number of issues. Leftmultiplying 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.
0L11
. > B@ ..
Ln1
0L1 Lnn
L1
Ln1
... CA Ln 0L11
.
B@ ..
Ln1
L1n 1 .
.. CA Lnn
0M1
Mn
M1 1
... CA Mn where Li = S1 j n Lij and Mj = S1 i n Lij . This entails 0L11
. > B@ ..
Ln1
L1n 1
... CA > = Lnn 0M
M 1 ... CA M where M =
S S 1 j n 1 i n
Lij . Such matrices can be used to represent sets of labels in the model.
(
Basics and the Original Approach (S; +; 0) forms an idempotent commutative monoid and (S; ; 1) a monoid. This means, for arbitrary x; y; z 2 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 2 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 de ned by x y ,df x + y = y. It is easily veri ed 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 in mum 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 , axiomatised by the following unfold and induction laws: 1 + x x = x , x y + z 1 + x x = x , y x + z y ) x y ) z x z y , 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 de ning property is therefore that a test must have a complement relative to 1, i.e., an element :p that satis es 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
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 scalars1 [4], which are tests
; ; : : : that additionally commute with >, i.e., > = > . Analogously to (
Describing projection needs additional concepts. First, for arbitrary element x and scalar , nx = x + : > : 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 de ned by the Galois connection x ynz ,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 2 S they are axiomatised as follows.
x" y , x y# , is a scalar and 6= 0 implies " = 1 , (x y#)" = x" y# , (x# y)" = x# y" .
In the matrix model they can be described for a matrix M as follows
(
M #(x; y) = ; L if M (x; y) = L ; 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 de ned for arbitrary x 2 S by P (x) =df ( nx)# : 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( ) = fleft; rightg 0 ; frightg
; ; Pfleft;rightg(BB@fvalg fleft; rightg ; fvalg fleftg ; ; ;
fvalg 1 0; ; ; ; 1
fleft; rightgCC) = BB; ; ; fleft; rightgCC :
; A @; fleft; rightg ; ; A
; ; ; ; ;
To see that this is achieved by Equation (
Finally we turn to the most important operator of pointer Kleene algebra. It calculates all reachable nodes from a given set of nodes. The de nition uses domain and codomain operations p and q. They are characterised by the following equations, for arbitrary element x and test p, 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 p0
; frightg @ ; ; fvalg fleft; rightg
fleftg 1 0fleft; rightg fleft; rightgA = @ ; ; ;
; fleft; rightg ; ; ; fleft; right; valg 1 A :
In [4] reachability is now de ned 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 i the corresponding entry in the main diagonal of p is L. Now assume
that m represents an address set. Then reach(m; x) is de ned using the iteration operator by
reach(m; x) = (m (x") )q :
(
Finally, an important operation in connection with pointer structures is overriding one structure x by another one y, denoted yjx =df y + :py x. Here entries of x for which also y provides a de nition are replaced by these and only the part of x not a ected 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 a ect reachability. One sample law for this is
py" u reach(m; x) = 0 ) reach(m; yjx) = reach(m; x) ; i.e., when the domain of the overriding structure is not reachable from the overridden one it does not a ect reachability. 3.2
One sees that it is very onerous to de ne the domain speci c 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 de ning behaviour. Furthermore by Equation (
A naive encoding of these operations in the rst-order automated theorem proving system2 Prover9 [11] already revealed that only a small set of basic properties for projections and reachability 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 rst-order ATP system could also be used with the abstract algebraic approach, e.g., through the TPTP problem library [17].
The resulting ine ective automation could be due to the indirect axiomatisation of # through
" by a Galois connection (cf. De nition (
Moreover, using the Galois characterisation of residuals instead of the explicit
characterisation in Equation (
Finally the given axiomatisations of the speci c operators for this particular domain are also di cult 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 rst simpli cation we drop the assumption that address sets need to be interpreted by crisp elements. Plain test elements also su ce to represent source nodes for reach(p; x) since x is by de nition already completed. 4.1
We continue with the notion of projecting a graph to a subgraph that is restricted to a set of labels. For this we rst want to nd 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 (
The di erence of the just described way to project matrices and projections P (x) can be
made clear in the example given after Equation (
2We abbreviate the term \automated theorem proving system" to ATP system in the following. 4.2
As a further simpli cation, 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 ; a(a(x)) + a(x) = 1 ; a(x y) a(x a(a(y))) ;
x ac(x) = 0 ; ac(ac(x)) + ac(x) = 1 ; 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 di cult to handle for ATP systems in that form. Often a lot of standard Boolean algebra properties have to be derived rst. Therefore we propose an equivalent but more \e cient" axiomatisation at the end of the next section. 4.3
Next, we turn to the completion operator " which is useful in analysing link-independent reachability in graphs. Rather than axiomatising it indirectly through a Galois connection we characterise 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 differences 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 x" u y" = (x + y)" ; (x y")" = x" y" ; 0 ;
> x" + y" = (x" u y")" ; (x" y)" = x" y" : 0" ; Notice that the inequations can be strengthened to equations. The most striking di erence 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 le can be found in the appendix.
x x" ; (x")" = x" ; >" = > ; >" = 0 ; (x" + y")" = x" u y" ; (x" + y")" = x" u y" ; 0" = 0 ; 0" = > ; (x" u y")" = x" + y" ; (x" u y")" = x" + y" ;
y" ; x y ) y" x" = 0 , x = 0 ; (x")" = x" ;
x" ; x y ) x" x" = > , x = 0 ; (x" y")" = x" y" ;
x" = 0 , x = 0 ; (x + y)" = x" + y" : 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 veri ed 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 ;
a(x) a(y) = a(x + y) ; a(x) + a(y) = a(a(a(x)) a(a(y))) ; a(x y) a(x a(a(y))) ; x ac(x) = 0 ; ac(0) = 1 ; ac(x) ac(y) = ac(x + y) ; ac(x) + ac(y) = ac(ac(ac(x)) ac(ac(y))) ; ac(x y) ac(ac(ac(x)) y) : Using Prover9 we have shown that this axiomatisation is equivalent to the standard axiomatisation 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
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 de ne 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 de ned data structures.
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. 17 % --- Multiplicative monoid 18 x;(y;z) = (x;y);z. 19 1;x = x. 20 x;1 = x. 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. 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.