Path algebras are used to describe path problems in directed graphs. Constructing a new path algebra involves de ning a carrier set, several operations, and proving that many algebraic properties hold. We describe work-in-progress on the development of a domain-speci c language for specifying path algebras where implementations and proofs are automatically constructed in a bottom-up fashion. Our initial motivation came from the development of Internet routing protocols, but we believe that the approach could have much wider applications. We have implemented the language using the Coq theorem prover.
Section 3 we specify the bottleneck semiring mentioned above, and show how required properties for a semiring can be automatically derived.
This is very much a work-in-progress, and we discuss some of our ongoing e orts in Section 4. 2
Our framework consists of a collection L of constructions of algebras (such as semirings), and a xed nite set of properties P for these algebraic structures. The goal is for every algebra de ned by composing constructions in L to decide for every property in P if it is true or false. We call such L to be closed w.r.t. P. To achieve this, for every construction c in L and every p 2 P we aim to have a rule of the following shape2
p(c(a1; : : : ; an)) , c;p(a1; : : : ; an) where c;p stands for some boolean expression over properties in P of algebras a1; : : : ; an. Let us call such rules | i -rules. Notice that, if c takes no arguments, the right hand side is either true or false. Now given an algebra de ned by constructions, we can use i -rules to infer properties in bottom-up way.
Insisting on i -rules may require adding new properties to P. Consider the selectivity
property (8xy: x y = x _ x y = y) for the direct product of semigroups (A; A) and (B; B).
Instantiating the selectivity property with the direct product construction gives us
8x1y1 2 A: 8x2y2 2 B: (x1 A y1 = x1 ^ x2 B y2 = x2) _ (x1 A y1 = y1 ^ x2 B y2 = y2) (
((8x1y1 2 A: x1 _ ((8x1y1 2 A: x1 _ ((8x1y1 2 A: x1 _ ((8x2y2 2 B: x2
A y1 = x1) ^ (8x2y2 2 B: x2 A y1 = y1) ^ (8x2y2 2 B: x2
B y2 = x2))
B y2 = y2)) A y1 = x1 _ x1 B y2 = x2 _ x2
A y1 = y1) ^ (8x2y2 2 B: x2 = y2))
B y2 = y2) ^ (8x1y1 2 A: x1 = y1))
If we do not have properties 8xy: x = y, 8xy: x y = x, and 8xy: x y = y in P, we need to add
them to get the i -rule. As system develops we need to add more and more auxiliary properties.
Which properties the nal system will contain becomes an empirical observation, which is hard
to predict beforehand. Tables in Appendix B list all i -rules we currently know. The formula
in (
SL(sProduct(S; S0)) , (L(S) ^ L(S0)) _ (R(S) ^ R(S0)) _
(SL(S) ^ SG(S0)) _ (SL(S0) ^ SG(S))
We consider ve di erent signatures shown in Fig. 1. All signatures have non-empty carrier.
Additionally, they have axioms that and are associative binary operators, and is a preorder
(re exive and transitive) relation. Fig. 3 gives de nitions of constructions for sets, semigroups
and preorders. Some constructions take arguments of signatures from Fig. 1 together with
additional axioms (we call them preconditions), e.g. a commutative and idempotent semigroup.
2 We use this font for constructions of algebras.
(
Sets (S) Semigroups (S; ) Preorders (S; ) Order semigroups (S; ; ) Bisemigroups (S; ; )
NE
NE, ASSOC
NE, REFL, TRANS
NE, REFL, TRANS, ASSOC
NE, ASSOC , ASSOC
Another goal we have is to give witnesses to properties in P with existential quanti ers. We can
split i -rule (
p(c(a1; : : : ; an)) (
c;p(a1; : : : ; an)
:p(c(a1; : : : ; an)) ( : c;p(a1; : : : ; an)
(
Some i -rules like LD(bAddOne(B)) , LD(B) ^ IDM(B ) ^ (RI(B) _ :IDM(B )) may look
unnecessarily complex, as classically it can be simpli ed to LD(bAddOne(B)) , LD(B) ^ RI(B).
Consider the negative form (
:LD(bAddOne(B)) ( :LD(B) _ :IDM(B ) _ (:RI(B) ^ :IDM(B )) Remember that the negation is pushed inside, e.g. :LD is 9xyz:z (x y) 6= (z x) (z y). To prove the implication, we construct three di erent counterexamples corresponding to three cases separated by disjunction. The rule explicitly says that we need to make a case split if dUnit is a singleton set I. (A B; ~ ) where (x1; x2) ~ (y1; y2) = dNat is a set N of natural numbers. tdhPeriordduicretcttapkreosdutwcto AsetsBA. and B and constructs >><>8((xx11;; xx22) 0 y2) iiff xx11 == (yx11 y1) 6= y1 dUnion takes two sets A and B and constructs their >(y1; y2) if x1 6= (x1 y1) = y1 disjoint union A ] B. > dFSets takes a sets A and constructs a set of all >:(x1 y1; 0B) if x1 6= (x1 y1) 6= y1 nite subsets of A, denoted by P(A). dFMinSets takes a preorder (A; ) and constructs ~ rst chooses according to , only if x1 = y1 it a set of all minimal nite subsets of A, denoted by chooses according to 0. The fourth case is used P (A). A subset X is minimal if X = min (X) when x1 and y1 are incomparable. sSelLex is similar to sLex. It does not require 0 swUhneirte ims ianse(mXig)r=oufpx(2I; KX)jw8hyer2e XK:yis6<thxegc.onstant to have the identity, but instead the has to be binary operation. selective. Consequently, the fourth case in ~ can sNatPlus is a semigroup (N; +). never happen. sNatMin is a semigroup (N; min). sFSetsUnion takes a set A and constructs a semisNatMax is a semigroup (N; max). group (P(A); [). sProduct takes two semigroups (A; ), (B; 0) sFSetsOp takes a semigroup (A; ) and constructs and constructs a semigroup (A B; ) where a semigroup (P(A); ^ ) where (saL1e;fbt1S)um ta(ake2s;bt2w)o=se(ma1igroau2p;sb1(A;0 b2)),.(B; 0) and X ^ Y = fx y j x 2 X; y 2 Y g constructs a semigroup (A ] B; A]B) where sFMinSetsUnion takes a preorder (A; ), s.t. is antisymmetric, and constructs a semigroup (P (A); [ ) where [ = min [. x A]B y = <>>>>>8yxx y iiifff xxx;22y AB2;;Ayy 22 BA scsm.oFtinM.nsitnrSueci^stts.saOanptsiestyamkmiegmsroeautnrpico(rPadnedr(Ase);mi^sigrm)oouwnphoet(roAen;e^, ;an=)d, >:x 0 y if x; y 2 B pLeftNaturalOrder takes a semigroup (A; ), s.t.
is commutative and idempotent, and constructs a preorder (A; L) where x L y , x y = x. sRightSum takes two semigroups (A; ), (B; 0) pRightNaturalOrder takes a semigroup (A; ), s.t. and constructs a semigroup (B ] A; A]B). is commutative and idempotent, and constructs sLex takes two semigroups (A; ) and (B; 0), s.t. a preorder (A; R) where x R y , x y = y.
is commutative and idempotent, and 0 has an pDual takes a preorder (A; ) and constructs a preidentity elements 0B. The resulting semigroup is order (A; ).
IDM(B ) holds or not in order to construct the counterexample. Classically the case split is trivial, but constructively we cannot do it for arbitrary B.
Splitting i -rules into (
All properties in P are de ned in Appendix A. In this section we explain reasons why some properties were initially added to P. Let us denote the initial set of properties by P0.
One of the aims of the system is to build semirings. Bisemigroups only guarantee associa
Constructor in L Order semigroups
oLeftNaturalOrder(S) oRightNaturalOrder(S)
Constructor in L Bisemigroups
bUnit bNatMinPlus
bNatMaxMin bProduct(B; B0)
bLex(B; B0) bSelLex(B; B0)
bFSetsOp(S) bFMinSets(O) bFMinSetsOpUnion(O)
bAddOne(B) bAddZero(B)
projection pLeftNaturalOrder(S) pRightNaturalOrder(S) projection projection
S
S projection sUnit sUnit sNatMin sNatPlus sNatMax sNatMin sProduct(B ; B0 ) sProduct(B ; B0 )
sLex(B ; B0 ) sProduct(B ; B0 ) sSelLex(B ; B0 ) sProduct(B ; B0 ) sFSetsUnion(SSet) sFSetsOp(S) sFMinSetsUnion(O ) sFMinSetsOp(O)
sFMinSetsOp(O) sFMinSetsUnion(O ) sLeftSum(sUnit; B ) sRightSum(B ; sUnit) sLeftSum(B ; sUnit) sRightSum(sUnit; B ) tivity. Hence, we need other semiring axioms to know if a bisemigroup is actually a semiring.
Studies of BGP [3] protocol show that path algebras are interesting even when operations and do not form a semiring. In such case we are not looking for optimal paths, but for locally optimal paths, where each node has the best path depending on what their neighbours have chosen. An interesting property in this scenario is the increasing property (8xy:x (y x) = x), which as shown by T.G. Gri n and J.L. Sobrinho [9] is needed for Dijkstra's algorithm to nd locally optimal solutions.
Another key property is: the identity for is also the annihilator for . It implies 0-stability property (8x:1 x = 1) used by M. Gondran and M. Minoux [2]. 0-stability guarantees the convergence of matrix multiplication shortest path algorithm in n steps, where n is the number of nodes in the graph.
Also properties like idempotency, selectivity or antisymmetry are in P0, because they are required for some constructions as preconditions. 2.3
Some properties de ned in Appendix A are only meaningful in the context where some other properties (say p1; : : : ; pn) are satis ed. We denote this by p(p1; : : : ; pn). If a property is de ned in a context or a construction has preconditions, the proofs of the i -rule take the context and preconditions as assumption. For example, to proof the i -rule for minimal set construction of bisemigroups and right increasing property we need to show
CM (bFMinSets(O)) ) IDM (bFMinSets(O)) )
LM(O) ) RM(O) ) ASM (O) ) (RI(bFMinSets(O)) , LND(O)) 2.4
We de ned various constructions of algebras and showed how i -rules can be used to prove properties. To make an automatic tool out of i -rules we need to re ect constructions in the collection L into a mutually inductive language (with a syntactic type for each signature). For each construction we have a corresponding syntactic constructor. To map back from terms in syntax to algebras, we have a semantics function that is mutually inductively de ned on the syntax structure, e.g. for bisemigroups the semantics function has type
BS ! (S; ; ; ~ ; ~) + error where BS is the syntactic category for bisemigroup speci cations, (S; ; ) is a bisemigroup, ~ contains proofs that this is actual a bisemigroup, i.e. S is not empty and ; are associative, ~ for each property in P contains a proof or a refutation. The semantics function fails and returns an error if some preconditions of constructors speci ed in the input do not hold.
We have implemented all de nitions of constructions and proved the i -rules in Coq. We also de ned syntax and the semantic function in Coq. Using code extraction mechanism [5], we generate an OCaml implementation of the semantics function that can be invoked without invoking the Coq theorem prover. This gives us a tool for quickly de ning algebras and getting their properties together with witnesses. Also since the semantics function provides implementations for the and operations, we can construct a concrete labelled graph and run a generalised shortest path algorithm. 3 3.1
To show how the language can be used, let us consider a graph where each edge has a distance
and a bandwidth. Say we want to nd best paths according to these two metrics. Bisemigroups
bNatMinPlus and bNatMaxMin can be used to represent distance and bandwidth respectively.
We can make one metric more signi cant by ordering pairs of metrics lexicographicly. Here are
the speci cations of algebras in our syntax:
bAddOne(bAddZero(bSelLex(bNatMinPlus; bNatMaxMin)))
bAddOne(bAddZero(bSelLex(bNatMaxMin; bNatMinPlus)))
However, the choice of which metric is more signi cant gives us algebras with signi cantly
di erent properties. The bisemigroup speci ed by (
LD(bAddOne(bAddZero(bSelLex(bNatMinPlus; bNatMaxMin)))) , LD(bAddZero(bSelLex(bNatMinPlus; bNatMaxMin))) ^
IDM (bAddZero(bSelLex(bNatMinPlus; bNatMaxMin))) ^ (RI(bAddZero(bSelLex(bNatMinPlus; bNatMaxMin))) _ :IDM (bAddZero(bSelLex(bNatMinPlus; bNatMaxMin)))) , LD(bSelLex(bNatMinPlus; bNatMaxMin)) ^
IDM(sLeftSum(sUnit; sSelLex(sNatMin; sNatMax))) ^
(
((F alse _ (T rue ^ T rue)) _ :(T rue ^ T rue)) , T rue Such derivations are done mechanically by our tool. In a similar way we can derive F alse for left distributivity of the second bisemigroup. The tool also generates a counterexample for left distributivity: (0; 1) ((1; 1) ~ (0; 0)) = (0; 2) 6= (0; 1) = ((0; 1) (1; 1)) ~ ((0; 1) (0; 0)) 3.2
As a second example, consider the semiring de ned by J. Monnot and O. Spanjaar [6] for nding best paths according to their bottleneck. Say we have a graph where edges are labelled by two independent metrics (two natural numbers). Values assigned to edges are partially ordered by comparing metrics pointwise. The weight of a path consists of a set of worst edges in the path. A path x is more preferred to another path y if for each edge in x there is a worse edge in y. We aim to have a semiring that calculates a set of such best paths between every pair of nodes in the graph.
In [6] the semiring is explicitly de ned together with non-trivial proofs of semiring axioms. By reverse engineering de nitions of the semiring operations, we can specify it in our language in the following way. We can represent pairs of metrics by E = sProduct(sNatMin, sNatMin). Weights of paths are represented by P = sFMinSetsUnion(pRightNaturalOrder(E)). Finally, the bisemigroup that can be used to compute sets of best paths is
B = bFMinSets(oRightNaturalOrder(P))
(
If we take acyclic graphs as in [6], we can compute shortest paths according to the semiring using Bellman-Ford algorithm (Fig. 5). However, the semiring is not selective and it cannot be used with Dijkstra's algorithm. From the tool we get witnesses (ff(1; 0)gg and ff(0; 1)gg) explaining where selectivity fails. 0 1 ff(1; 3)gg 0 2 ff(1; 1)gg 0 3 ff(1; 3); (3; 1)g; f(2; 3)gg 0 4 ff(1; 3); (3; 1)g; f(2; 3)gg 0 5 ff(1; 3); (3; 1); (2; 2)g; f2; 3gg 0 6 ff(1; 3); (3; 1)g; f(2; 3)gg 1 3 ff(3; 1)gg 1 4 ff(3; 1)gg 1 5 ff(3; 1); (2; 2)gg 1 6 ff(3; 1)gg 2 3 ff(2; 3)gg 2 4 ff(2; 3)gg 2 5 ff(2; 3)gg 2 6 ff(2; 3)gg 3 4 ff(1; 1)gg 3 5 ff(2; 2)gg 3 6 ff(1; 1)gg 4 6 ff(1; 1)gg 5 6 ff(3; 2)gg Our approach to language design requires many i -rules and it would be hard to ensure correctness without using a formal theorem prover. We have chosen the Coq theorem prover as it seems to meet our requirements quite well. Dependent types allow de ning signatures for algebras as dependent records. Constructive proofs in Coq t our need to associate witnesses to proofs of existential quanti ers. We haven't yet used some recent Coq features, such as type classes [10], which may simplify some of the infrastructure for our proofs.
A large part of our current e ort is directed at \closing" the i -rules listed in Appendix B. There is of course a con ict between the goal of closure and the goal of increased expressive power, and so various trade-o s have to be assessed at language design time.
Not all natural path problems can be expressed using bisemigroups. Many Internet routing protocols are best modelled by attaching functions to arcs in a graph. We are currently extending our system to encompass such algebraic structures.
A
We use shorthands: (x#y) , (x 6 y ^ y 6 x) and (x 7 y) , :(x#y). For bisemigroups denotes the left natural order.
P0 * * * * * * * *
ID(Context) DecSetoid SG TE FT Semigroup HI HA SL CM IDM L R LCD RCD LC RC AL AR TG(CM, IDM) Preorder TT ASM OrderSemigroup LM RM LND RND SND(IDM, ASM) IAUS(LM, RM, ASM, SL) IAF(LM, RM, ASM, SL) P0
ID(Context) RCC(CM , IDM ) LCC(CM , IDM ) LDT(CM , IDM ) RDT(CM , IDM ) LCP(CM , IDM ) RCP(CM , IDM ) RTID(HI ) LTID(HI ) PITLA(HI )
RITRA(HI )
sFSetsUnion(D) SG(D) bProduct(B,B') LD(B) ^ LD(B') RD(B) ^ RD(B') PITA(B) ^ PITA(B') PATI(B) ^ PATI(B') RSS(B) ^ RSS(B') ^ (RDT(B) _ RCEC(B')) ^ (RDT(B') _ RCEC(B)) LSS(B) ^ LSS(B') ^ (LDT(B) _ LCEC(B')) ^ (LDT(B') _ LCEC(B)) RCEC(B) ^ RCEC(B') ^ (RC(B ) _ RC(B' )) LCEC(B) ^ LCEC(B') ^ (LC(B ) _ LC(B' )) work-in-progress work-in-progress LDT(B) ^ LDT(B') RDT(B) ^ RDT(B') LCP(B) ^ LCP(B') ^ (LDT(B) _ LDT(B')) RCP(B) ^ RCP(B') ^ (RDT(B) _ RDT(B')) RI(B) ^ RI(B') LI(B) ^ LI(B') (RI(B) ^ RSI(B')) _ (RSI(B) ^ RI(B')) bLex(B,B') CM(B ), IDM(B ), HI(B' ) LD(B) ^ LD(B') ^ (LSS(B) _ LCD(B' )) ^ (LCEC(B) _ LTID(B')) ^ (LCC(B) _ RITRA(B')) RD(B) ^ RD(B') ^ (RSS(B) _ RCD(B' )) ^ (RCEC(B) _ RTID(B')) ^ (RCC(B) _ PITLA(B')) PITA(B) ^ PITA(B') PATI(B) ^ PATI(B') RSS(B) ^ RSS(B') ^ (RCEC(B) _ RDT(B')) LSS(B) ^ LSS(B') (LCEC(B) _ LDT(B')) RCEC(B) ^ RCEC(B') LCEC(B) ^ LCEC(B') (RCEC(B) _ RCP(B')) ^ RCC(B) ^ RCC(B') (LCEC(B) _ LCP(B')) ^ LCC(B) ^ LCC(B') LDT(B) ^ LDT(B') RDT(B) ^ RDT(B') LCP(B) ^ LCP(B') RCP(B) ^ RCP(B') RSI(B) _ (RI(B) ^ RI(B')) LSI(B) _ (LI(B) ^ LI(B')) RSI(B) _ (RI(B) ^ RSI(B')) ^
LSS(B) ^ LSS(B') bSelLex(B,B') CM(B ), SL(B ), CM(B' ) LD(B) ^ LD(B') ^ (LC(B ) _ LCD(B' )) RD(B) ^ RD(B') ^ (RC(B ) _ RCD(B' )) PITA(B) ^ PITA(B') PATI(B) ^ PATI(B') RSS(B) ^ RSS(B') RCEC(B) ^ RCEC(B') LCEC(B) ^ LCEC(B') RCC(B) ^ RCC(B') LCC(B) ^ LCC(B') LDT(B) ^ LDT(B') RDT(B) ^ RDT(B') LCP(B) ^ LCP(B') RCP(B) ^ RCP(B') RSI(B) _ (RI(B) ^ RI(B')) LSI(B) _ (LI(B) ^ LI(B')) RSI(B) _ (RI(B) ^ RSI(B')) bFSetsOp(S) True True True SG(S) False False SG(S) SG(S) RCD(S) LCD(S) False False LCD(S) RCD(S) L(S) R(S) False RTID LTID bProduct(B,B') (LI(B) ^ LSI(B')) (LSI(B) ^ LI(B')) RTID(B) ^ RTID(B')
LTID(B) ^ LTID(B') bAddZero(B) LD(B) RD(B)