=Paper=
{{Paper
|id=None
|storemode=property
|title=A Domain-Specific Language for the Specification of Path Algebras
|pdfUrl=https://ceur-ws.org/Vol-760/paper7.pdf
|volume=Vol-760
|dblpUrl=https://dblp.org/rec/conf/ate/NaudziunasG11
}}
==A Domain-Specific Language for the Specification of Path Algebras==
https://ceur-ws.org/Vol-760/paper7.pdf
A Domain-Specific Language for
the Specification of Path Algebras
Vilius Naudžiūnas Timothy G. Griffin
Computer Laboratory Computer Laboratory
University of Cambridge University of Cambridge
Vilius.Naudziunas@cl.cam.ac.uk Timothy.Griffin@cl.cam.ac.uk
Abstract
Path algebras are used to describe path problems in directed graphs. Constructing a new
path algebra involves defining a carrier set, several operations, and proving that many alge-
braic properties hold. We describe work-in-progress on the development of a domain-specific
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 appli-
cations. We have implemented the language using the Coq theorem prover.
1 Introduction
Finding shortest paths in a graph is one of the fundamental problems in computer science.
Algorithms for solving shortest path problems, such as Dijkstra’s or Bellman-Ford, are widely
used. Generalizations of shortest paths to semirings and related structures has been an active
area of research for over forty years (see [2] for a survey). Recently, this approach has been
further extended with exotic algebras that lack distributivity but can still be used to find locally
optimal paths [7, 8]. We refer to such algebras, with or without distributivity, as path algebras.
Constructing a new path algebra involves defining a carrier set, several operations, and
proving that many algebraic properties hold. With complex constructions such proofs can
be quite challenging. In one example that we look at closely in Section 3, J. Monnot and
O. Spanjaar [6] define a bottleneck semiring for solving certain combinatorial problems. The
proofs that show the constructed algebra is in fact a semiring are non-trivial.
This paper describes a domain-specific language for the specification of path algebras. The
goal is automating the implementation and verification of specified algebras. The language is
designed so that the specification writer simply supplies a high-level expression comprised of
names of built-in algebras and algebraic constructors (direct product, lexicographic product,
etc.). The specified algebra’s implementation and proofs (or refutations) for all covered prop-
erties are then derived in a bottom-up syntax-directed manner. Details of our approach are
described in Section 2.
We have implemented1 our language using the Coq theorem prover [1]. However, in our
approach all interactive theorem proving is performed at language design time. Specification
writers use a tool implemented in OCaml code that has been automatically extracted [5] from
our Coq implementation. That is, specification writers are not required to do any interactive
theorem proving.
Our initial motivation came from the development of Internet routing protocols, where the
intended specification writers are network operators or protocols designers who are not well
versed in the art of proving theorems [4]. However, we feel that this approach may have appli-
cations in other areas such as Operations Research. In particular, our implementation allows
algebra designers to quickly explore a large space of specifications. By way of illustration, in
1
The implementation is available at http://www.cl.cam.ac.uk/~tgg22/metarouting.
46
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
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 efforts in Section 4.
2 Language Engineering
Our framework consists of a collection L of constructions of algebras (such as semirings), and
a fixed finite set of properties P for these algebraic structures. The goal is for every algebra
defined 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 ∈ P we aim to have a rule of the following shape2
p(c(a1 , . . . , an )) ⇔ βc,p (a1 , . . . , an ) (1)
where βc,p stands for some boolean expression over properties in P of algebras a1 , . . . , an . Let us
call such rules — iff-rules. Notice that, if c takes no arguments, the right hand side is either true
or false. Now given an algebra defined by constructions, we can use iff-rules to infer properties
in bottom-up way.
Insisting on iff-rules may require adding new properties to P. Consider the selectivity prop-
erty (∀xy. 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
∀x1 y1 ∈ A. ∀x2 y2 ∈ B. (x1 ⊕A y1 = x1 ∧ x2 ⊕B y2 = x2 ) ∨ (x1 ⊕A y1 = y1 ∧ x2 ⊕B y2 = y2 ) (2)
To get the iff-rule, we need to simplify (2), so that it becomes a boolean expression of properties
of only A or only B. Consequently, we get
((∀x1 y1 ∈ A. x1 ⊕A y1 = x1 ) ∧ (∀x2 y2 ∈ B. x2 ⊕B y2 = x2 )) (3)
∨ ((∀x1 y1 ∈ A. x1 ⊕A y1 = y1 ) ∧ (∀x2 y2 ∈ B. x2 ⊕B y2 = y2 ))
∨ ((∀x1 y1 ∈ A. x1 ⊕A y1 = x1 ∨ x1 ⊕A y1 = y1 ) ∧ (∀x2 y2 ∈ B. x2 = y2 ))
∨ ((∀x2 y2 ∈ B. x2 ⊕B y2 = x2 ∨ x2 ⊕B y2 = y2 ) ∧ (∀x1 y1 ∈ A. x1 = y1 ))
If we do not have properties ∀xy. x = y, ∀xy. x ⊕ y = x, and ∀xy. x ⊕ y = y in P, we need to add
them to get the iff-rule. As system develops we need to add more and more auxiliary properties.
Which properties the final system will contain becomes an empirical observation, which is hard
to predict beforehand. Tables in Appendix B list all iff-rules we currently know. The formula
in (3) corresponds to the iff-rule in Table 3:
SL(sProduct(S, S 0 )) ⇔ (L(S) ∧ L(S 0 )) ∨ (R(S) ∧ R(S 0 )) ∨
(SL(S) ∧ SG(S 0 )) ∨ (SL(S 0 ) ∧ SG(S))
We consider five different 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
(reflexive and transitive) relation. Fig. 3 gives definitions 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.
47
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
ID Name Signature Axioms
D Sets (S) NE
S Semigroups (S, ⊕) NE, ASSOC
P Preorders (S, ≤) NE, REFL, TRANS
O Order semigroups (S, ≤, ⊕) NE, REFL, TRANS, ASSOC
B Bisemigroups (S, ⊕, ⊗) NE, ASSOC⊕ , ASSOC⊗
Figure 1: A table of signatures with axioms. Notice that we have forgetful projections between
signatures. Bisemigroups have two projection to semigroups as we can drop either ⊕ or ⊗.
ID Name Formula
NE Non-empty ∃x.T rue
ASSOC Associative ∀xyz.x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z
REFL Reflexive ∀x.x ≤ x
TRANS Transitive ∀xyz.x ≤ y ⇒ y ≤ z ⇒ x ≤ z
Figure 2: Definitions of axioms used in signatures.
Note that a construction not only has to define the appropriate operations and relations, but
also to make sure that these operations satisfy required axioms.
To define bisemigroups and order semigroups it is enough to define their projections (Fig. 4).
The last two constructions in Fig. 4 add special elements. bAddOne(B) and bAddZero(B) are
equivalent to bisemigroups (B ] {1}, ⊕B , ⊗B ) and (B ] {0}, ⊕B , ⊗B ) respectively, where 1 is
annihilator for ⊕B and identity for ⊗B , and 0 is identity for ⊕B and annihilator for ⊗B .
2.1 Witnesses
Another goal we have is to give witnesses to properties in P with existential quantifiers. We can
split iff-rule (1) into two implication.
p(c(a1 , . . . , an )) ⇐ βc,p (a1 , . . . , an ) (4)
¬p(c(a1 , . . . , an )) ⇐ ¬βc,p (a1 , . . . , an ) (5)
By ¬ we mean that the negation in front of p and βc,p is pushed through quantifiers to relation
symbols. One of the implication is responsible for proving a property with existential quantifier.
Say it is (5). If it is proved constructively, the proof says how to construct a witness for existential
quantifier in ¬p from witnesses of existential quantifiers in ¬βc,p . Consequently, we can construct
witnesses in bottom-up way as well as infer properties.
Some iff-rules like LD(bAddOne(B)) ⇔ LD(B) ∧ IDM(B⊕ ) ∧ (RI(B) ∨ ¬IDM(B⊕ )) may look
unnecessarily complex, as classically it can be simplified to LD(bAddOne(B)) ⇔ LD(B) ∧ RI(B).
Consider the negative form (5) of this rule
¬LD(bAddOne(B)) ⇐ ¬LD(B) ∨ ¬IDM(B⊕ ) ∨ (¬RI(B) ∧ ¬IDM(B⊕ ))
Remember that the negation is pushed inside, e.g. ¬LD is ∃xyz.z ⊗ (x ⊕ y) 6= (z ⊗ x) ⊕ (z ⊗ y).
To prove the implication, we construct three different counterexamples corresponding to three
cases separated by disjunction. The rule explicitly says that we need to make a case split if
48
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
dUnit is a singleton set I. ~ ) where (x1 , x2 ) ⊕
(A × B, ⊕ ~ (y1 , y2 ) =
dNat is a set N of natural numbers.
(x1 , x2 ⊕0 y2 ) if x1 = y1
dProduct takes two sets A and B and constructs
their direct product A × B.
(x , x )
1 2 if x1 = (x1 ⊕ 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.
(x1 ⊕ y1 , 0B ) if x1 6= (x1 ⊕ y1 ) 6= y1
dFSets takes a sets A and constructs a set of all
finite subsets of A, denoted by P(A).
~ first chooses according to ⊕, only if x1 = y1 it
⊕
dFMinSets takes a preorder (A, ≤) and constructs
chooses according to ⊕0 . The fourth case is used
a set of all minimal finite subsets of A, denoted by
when x1 and y1 are incomparable.
P≤ (A). A subset X is minimal if X = min≤ (X)
sSelLex is similar to sLex. It does not require ⊕0
where min≤ (X) = {x ∈ X | ∀y ∈ X.y 6< x}.
to have the identity, but instead the ⊕ has to be
sUnit is a semigroup (I, K) where K is the constant
~ can
selective. Consequently, the fourth case in ⊕
binary operation.
never happen.
sNatPlus is a semigroup (N, +).
sFSetsUnion takes a set A and constructs a semi-
sNatMin is a semigroup (N, min).
group (P(A), ∪).
sNatMax is a semigroup (N, max).
sFSetsOp takes a semigroup (A, ⊕) and constructs
sProduct takes two semigroups (A, ⊕), (B, ⊕0 )
and constructs a semigroup (A × B, ⊕× ) where ˆ where
a semigroup (P(A), ⊕)
(a1 , b1 ) ⊕× (a2 , b2 ) = (a1 ⊕ a2 , b1 ⊕0 b2 ).
ˆ Y = {x ⊕ y | x ∈ X, y ∈ Y }
X⊕
sLeftSum takes two semigroups (A, ⊕), (B, ⊕0 ) and
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⊕y if x, y ∈ A sFMinSetsOp takes an order semigroup (A, ≤, ⊕),
x if x ∈ A, y ∈ B s.t. ≤ is antisymmetric and ⊕ is monotone, and
x ⊕A]B y = constructs a semigroup (P≤ (A), ⊕ˆ ≤ ) where ⊕
ˆ≤ =
y if x ∈ B, y ∈ A
ˆ
min≤ ◦ ⊕.
x ⊕0 y if x, y ∈ 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 pre-
identity elements 0B . The resulting semigroup is order (A, ≥).
Figure 3: Constructions of sets, semigroups and preorders.
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 iff-rules into (4) and (5) helps us in using the framework that is under development
where we do not have iff-rules. If βc,p in (4) is different from βc,p in (5), we can still generate
proofs and compute witnesses, but we may run into situations where we cannot decide if some
property is true or false.
2.2 Key Properties
All properties in P are defined 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-
49
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
Constructor in L ≤ projection ⊕ projection
Order semigroups
oLeftNaturalOrder(S) pLeftNaturalOrder(S) S
oRightNaturalOrder(S) pRightNaturalOrder(S) S
Constructor in L ⊕ projection ⊗ projection
Bisemigroups
bUnit sUnit sUnit
bNatMinPlus sNatMin sNatPlus
bNatMaxMin sNatMax sNatMin
bProduct(B, B 0 ) sProduct(B⊕ , B⊕0
) sProduct(B⊗ , B⊗0
)
bLex(B, B 0 ) sLex(B⊕ , B⊕0
) sProduct(B⊗ , B⊗0
)
bSelLex(B, B 0 ) sSelLex(B⊕ , B⊕0
) sProduct(B⊗ , B⊗0
)
bFSetsOp(S) sFSetsUnion(SSet ) sFSetsOp(S)
bFMinSets(O) sFMinSetsUnion(O≤ ) sFMinSetsOp(O)
bFMinSetsOpUnion(O) sFMinSetsOp(O) sFMinSetsUnion(O≤ )
bAddOne(B) sLeftSum(sUnit, B⊕ ) sRightSum(B⊗ , sUnit)
bAddZero(B) sLeftSum(B⊕ , sUnit) sRightSum(sUnit, B⊗ )
Figure 4: Constructions for order semigroups and bisemigroups. S ranges over semigroups,
B, B 0 — over bisemigroups, O — over order semigroups. We use indexes (Set, ⊕, ⊗, ≤) to
denote projected algebras. In addition to axioms inherited from projections bSelLex requires
B⊕0 to be commutative, and bAddOne requires B to be commutative.
⊕
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 (∀xy.x ⊕ (y ⊗ x) = x),
which as shown by T.G. Griffin and J.L. Sobrinho [9] is needed for Dijkstra’s algorithm to find
locally optimal solutions.
Another key property is: the identity for ⊕ is also the annihilator for ⊗. It implies 0-stability
property (∀x.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 Iff-Rules in Context
Some properties defined in Appendix A are only meaningful in the context where some other
properties (say p1 , . . . , pn ) are satisfied. We denote this by p(p1 , . . . , pn ). If a property is defined
in a context or a construction has preconditions, the proofs of the iff-rule take the context and
preconditions as assumption. For example, to proof the iff-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))
50
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
2.4 Putting it all together
We defined various constructions of algebras and showed how iff-rules can be used to prove
properties. To make an automatic tool out of iff-rules we need to reflect 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 defined on the
syntax structure, e.g. for bisemigroups the semantics function has type
BS → (S, ⊕, ⊗, ~π , ρ
~) + error
where BS is the syntactic category for bisemigroup specifications, (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 specified in the input do not hold.
We have implemented all definitions of constructions and proved the iff-rules in Coq. We also
defined syntax and the semantic function in Coq. Using code extraction mechanism [5], we gen-
erate an OCaml implementation of the semantics function that can be invoked without invoking
the Coq theorem prover. This gives us a tool for quickly defining 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 Examples
3.1 Lexicographic Product
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 find 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 significant by ordering pairs of metrics lexicographicly. Here are
the specifications of algebras in our syntax:
bAddOne(bAddZero(bSelLex(bNatMinPlus, bNatMaxMin))) (6)
bAddOne(bAddZero(bSelLex(bNatMaxMin, bNatMinPlus))) (7)
However, the choice of which metric is more significant gives us algebras with significantly
different properties. The bisemigroup specified by (6) is a semiring, but the one specified by (7)
is not distributive. We illustrate how we can check these properties using iff-rules in Appendix B
by proving left distributivity of the first bisemigroup.
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))) ∧
51
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
(RI(bSelLex(bNatMinPlus, bNatMaxMin)) ∨
¬IDM(sLeftSum(sUnit, sSelLex(sNatMin, sNatMax))))
⇔ (LD(bNatMinPlus) ∧ LD(bNatMaxMin) ∧ (LC(sNatPlus) ∨ LCD(sNatMin))) ∧
(IDM(sUnit) ∧ IDM(sSelLex(sNatMin, sNatMax))) ∧
((RSI(bNatMinPlus) ∨ (RI(bNatMinPlus) ∧ RI(bNatMaxMin))) ∨
¬(IDM(sUnit) ∧ IDM(sSelLex(sNatMin, sNatMax))))
⇔ (LD(bNatMinPlus) ∧ LD(bNatMaxMin) ∧ (LC(sNatPlus) ∨ LCD(sNatMin))) ∧
(IDM(sUnit) ∧ IDM(sNatMax)) ∧
((RSI(bNatMinPlus) ∨ (RI(bNatMinPlus) ∧ RI(bNatMaxMin))) ∨
¬(IDM(sUnit) ∧ IDM(sNatMax)))
⇔ (T rue ∧ T rue ∧ (T rue ∨ F alse)) ∧ (T rue ∧ T rue) ∧
((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, 0)) = (0, 2) 6= (0, 1) = ((0, 1) ⊗× (1, 1)) ⊕
(0, 1) ⊗× ((1, 1) ⊕ ~ ((0, 1) ⊗× (0, 0))
3.2 The Bottleneck Semiring
As a second example, consider the semiring defined by J. Monnot and O. Spanjaar [6] for finding
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 defined together with non-trivial proofs of semiring axioms.
By reverse engineering definitions 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)) (8)
Most importantly, in order to come up with the specification, we do not need to look to the
proofs given in [6] — these can be generated automatically using the iff-rules as in the previous
example.
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 ({{(1, 0)}} and {{(0, 1)}})
explaining where selectivity fails.
52
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
t9 1 JJJ t9 4 JJJ
tt tt
(3,1)J (1,1)J
t(1,3) JJ tt(1,1) JJ
tt % t %
0 JJJ t9 3 JJJ t9 6
t t tt
(1,1)J (2,2)J
JJ tt(2,3) JJ t(3,2)
% t % tt
2 5
0−1 {{(1, 3)}} 1−4 {{(3, 1)}} 3−4 {{(1, 1)}}
0−2 {{(1, 1)}} 1−5 {{(3, 1); (2, 2)}} 3−5 {{(2, 2)}}
0−3 {{(1, 3), (3, 1)}, {(2, 3)}} 1−6 {{(3, 1)}} 3−6 {{(1, 1)}}
0−4 {{(1, 3), (3, 1)}, {(2, 3)}} 2−3 {{(2, 3)}} 4−6 {{(1, 1)}}
0−5 {{(1, 3), (3, 1), (2, 2)}, {2, 3}} 2−4 {{(2, 3)}} 5−6 {{(3, 2)}}
0−6 {{(1, 3), (3, 1)}, {(2, 3)}} 2−5 {{(2, 3)}}
1−3 {{(3, 1)}} 2−6 {{(2, 3)}}
Figure 5: At the top is the example graph taken from [6]. At the bottom are the results computed
by the tool using the bisemigroup defined in (8). For each pair of nodes we have a set of best
paths. Each path is valued by a set of worst edges on that path.
4 Discussion, Future Work
Our approach to language design requires many iff-rules and it would be hard to ensure correct-
ness 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 defining signatures for algebras as
dependent records. Constructive proofs in Coq fit our need to associate witnesses to proofs of
existential quantifiers. 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 effort is directed at “closing” the iff-rules listed in Appendix B.
There is of course a conflict between the goal of closure and the goal of increased expressive
power, and so various trade-offs 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.
References
[1] Y. Bertot and P. Castéran. Interactive theorem proving and program development: Coq’Art: the
calculus of inductive constructions. Springer-Verlag, 2004.
[2] M. Gondran and M. Minoux. Graphs, Dioids and Semirings: New Models and Algorithms. Springer,
2008.
[3] T. G. Griffin, F. B. Shepherd, and G. Wilfong. The stable paths problem and interdomain routing.
IEEE/ACM Transactions on Networking (TON), 10(2):232–243, 2002.
[4] T. G. Griffin and J. L. Sobrinho. Metarouting. SIGCOMM, 35:1–12, August 2005.
[5] P. Letouzey. A new extraction for coq. Types for proofs and programs, pages 617–617, 2003.
[6] J. Monnot and O. Spanjaard. Bottleneck shortest paths on a partially ordered scale. 4OR: A
Quarterly Journal of Operations Research, 1(3):225–241, 2003.
[7] J. Sobrinho and T. G. Griffin. Routing in equilibrium. In 19th International Symposium on Mathe-
matical Theory of Networks and Systems (MTNS 2010), 2010.
53
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
[8] J. L. Sobrinho. An algebraic theory of dynamic network routing. IEEE/ACM Transactions on
Networking, 13(5):1160–1173, October 2005.
[9] J. L. Sobrinho and T. G. Griffin. Routing in equilibrium. Mathematical Theory of Networks and
System, 2010.
[10] B. Spitters and E Van Der Weegen. Developing the algebraic hierarchy with type classes in coq.
ITP 2010. International Conference on Interactive Theorem Proving, 2010.
A Property Set P
We use shorthands: (x#y) ⇔ (x 6≤ y ∧ y 6≤ x) and (x ≶ y) ⇔ ¬(x#y). For bisemigroups ≤ denotes the left natural order.
P0 ID(Context) Description Formula
DecSetoid
SG Singleton ∃c.∀x.x = c
TE Has exactly two elements ∃ab.∀x.a 6= b ∧ (x = a ∨ x = b)
FT Finite ∃l : list S.∀x.x ∈ l
Semigroup
* HI Has identity ∃i.∀x.(i ⊕ x = x) ∧ (x ⊕ i = x)
* HA Has annihilator ∃w.∀x.(w ⊕ x = w) ∧ (x ⊕ w = w)
* SL Selective ∀xy.(x ⊕ y = x) ∨ (x ⊕ y = y)
* CM Commutative ∀ab.a ⊕ b = b ⊕ a
* IDM Idempotent ∀x.x ⊕ x = x
L Always returns the left argument ∀ab.a ⊕ b = a
R Always returns the right argument ∀ab.a ⊕ b = b
LCD Left condensed ∀abc.a ⊕ b = a ⊕ c
RCD Right condensed ∀abc.b ⊕ a = c ⊕ a
LC Left cancelative ∀xyz.z ⊕ x = z ⊕ y ⇒ x = y
RC Right cancelative ∀xyz.x ⊕ z = y ⊕ z ⇒ x = y
AL Anti-left ∀xy.x ⊕ y 6= x
AR Anti-right ∀xy.x ⊕ y 6= y
TG(CM, IDM) ∀xyz.x ⊕ y ⊕ z = x ⊕ z ∨ x ⊕ y ⊕ z = y ⊕ z
Preorder
* TT Total ∀xy.x ≤ y ∨ y ≤ x
* ASM Antisymmetric ∀xy.x ≤ y ∧ y ≤ x ⇒ x = y
OrderSemigroup
* LM Left monotonic ∀axy.x ≤ y ⇒ (a ⊕ x ≤ a ⊕ y)
* RM Right monotonic ∀xya.x ≤ y ⇒ x ⊕ a ≤ y ⊕ a
LND Left non-decreasing ∀xy.x ≤ x ⊕ y
RND Right non-decreasing ∀xy.x ≤ y ⊕ x
SND(IDM, ASM) Selective non-decreasing ∀xy.x ≤ x ⊕ y ∨ y ≤ x ⊕ y
IAUS(LM, RM, ASM, SL) ∀xyz.x#y ⇒ x⊕y = y ⇒ y⊕x = y ⇒ z #y ⇒
x=z
IAF(LM, RM, ASM, SL) ∀xyz.x#y ⇒ x⊕y = y ⇒ y ⊕x = y ⇒ x⊕z =
z ⇒ z ⊕ x = z ⇒ x 6= z ⇒ (y ⊕ z = z ∧ z ⊕ y =
z) ∨ z ≤ y
RT Right total ∀abc.(b ⊕ a) ≤ (c ⊕ a) ∨ (c ⊕ a) ≤ (b ⊕ a)
LT Left total ∀abc.(a ⊕ b) ≤ (a ⊕ c) ∨ (a ⊕ c) ≤ (a ⊕ b)
RMCC(RT) ∀xyzw.(x⊕z) < (y ⊕z) ⇒ (y ⊕w) < (x⊕w) ⇒
(x ⊕ z) ≤ (y ⊕ w) ∨ (y ⊕ w) ≤ (x ⊕ z)
LMCC(LT) ∀xyzw.(z ⊕x) < (z ⊕y) ⇒ (w⊕y) < (w⊕x) ⇒
(z ⊕ x) ≤ (w ⊕ y) ∨ (w ⊕ y) ≤ (z ⊕ x)
Bisemigroup
* LD Left distributive ∀abc.c ⊗ (a ⊕ b) = (c ⊗ a) ⊕ (c ⊗ b)
* RD Right distributive ∀abc.(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)
* PITA(HI⊕ , HA⊗ ) Plus identity is times annihilator α ⊕ = ω⊗
* PATI(HA⊕ , HI⊗ ) Plus annihilator is times identity ω⊕ = α ⊗
* RSI(CM⊕ , IDM⊕ ) Right strict increasing ∀xy.x < x ⊗ y
* LSI(CM⊕ , IDM⊕ ) Left strict increasing ∀xy.x < y ⊗ x
RI(CM⊕ , IDM⊕ ) Right increasing ∀xy.x ⊕ (x ⊗ y) = x
LI(CM⊕ , IDM⊕ ) Left increasing ∀xy.x ⊕ (y ⊗ x) = x
RSS(CM⊕ , IDM⊕ ) ∀abc.(a < b ⇔ a ⊗ c < b ⊗ c)
LSS(CM⊕ , IDM⊕ ) ∀abc.(a < b ⇔ c ⊗ a < c ⊗ b)
RCEC(CM⊕ , IDM⊕ ) ∀xyz.x ⊗ z = y ⊗ z ⇒ (x ≶ y)
LCEC(CM⊕ , IDM⊕ ) ∀xyz.z ⊗ x = z ⊗ y ⇒ (x ≶ y)
54
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
P0 ID(Context) Description Formula
RCC(CM⊕ , IDM⊕ ) ∀xyz.x ⊗ z # y ⊗ z ⇒ (x ≶ y)
LCC(CM⊕ , IDM⊕ ) ∀xyz.z ⊗ x # z ⊗ y ⇒ (x ≶ y)
LDT(CM⊕ , IDM⊕ ) Left discrete ∀xyz.¬(z ⊗ x < z ⊗ y)
RDT(CM⊕ , IDM⊕ ) Right discrete ∀xyz.¬(x ⊗ z < y ⊗ z)
LCP(CM⊕ , IDM⊕ ) Left comparable ∀xyz.z ⊗ x ≶ z ⊗ y
RCP(CM⊕ , IDM⊕ ) Right comparable ∀xyz.x ⊗ z ≶ y ⊗ z
RTID(HI⊕ ) ∀xyz.(x ⊗ z) ⊕ (y ⊗ z) = α⊕ ⊗ z
LTID(HI⊕ ) ∀xyz.(z ⊗ x) ⊕ (z ⊗ y) = z ⊗ α⊕
PITLA(HI⊕ ) Plus identity is times left annihila- ∀x.α⊕ ⊗ x = α⊕
tor
RITRA(HI⊕ ) Plus identity is times right annihi- ∀x.x ⊗ α⊕ = α⊕
lator
B Iff-Rules
dProduct(D,D’) dUnion(D,D’) dFSets(D) dFMinSets(P)
Prec.
SG SG(D) ∧ SG(D’) False False False
TE (SG(D) ∧ TE(D’)) ∨ (SG(D’) ∧ TE(D)) SG(D) ∧ SG(D’) SG(D) SG(P)
FT FT(D) ∧ FT(D’) FT(D) ∧ FT(D’) FT(D) FT(P)
Table 2: DecSetoid rules
sProduct(S,S’) sLex(S,S’) sSelLex(S,S’) sLeftSum(S,S’)
Prec. CM(S), IDM(S), CM(S), SL(S)
HI(S’)
HI HI(S) ∧ HI(S’) HI(S) HI(S) ∧ HI(S’) HI(S’)
HA HA(S) ∧ HA(S’) HA(S) ∧ HA(S’) HA(S) ∧ HA(S’) HA(S)
SL (L(S) ∧ L(S’)) ∨ (R(S) ∧ R(S’)) ∨ SL(S) ∧ SL(S’) SL(S’) SL(S) ∧ SL(S’)
(SL(S) ∧ SG(S’)) ∨ (SL(S’) ∧ SG(S))
CM CM(S) ∧ CM(S’) CM(S’) CM(S’) CM(S) ∧ CM(S’)
IDM IDM(S) ∧ IDM(S’) IDM(S’) IDM(S’) IDM(S) ∧ IDM(S’)
L L(S) ∧ L(S’) SG(S) ∧ L(S’) SG(S) ∧ L(S’) False
R R(S) ∧ R(S’) SG(S) ∧ R(S’) SG(S) ∧ R(S’) False
LCD LCD(S) ∧ LCD(S’) SG(S) ∧ SG(S’) SG(S) ∧ LCD(S’) False
RCD RCD(S) ∧ RCD(S’) SG(S) ∧ SG(S’) SG(S) ∧ RCD(S’) False
LC LC(S) ∧ LC(S’) SG(S) ∧ LC(S’) (SG(S) ∨ (¬SG(S’) ∧ LC(S) ∧ AL(S) ∧
SG(S’))) ∧ LC(S’) SG(S’)
RC RC(S) ∧ RC(S’) SG(S) ∧ RC(S’) (SG(S) ∨ (¬SG(S’) ∧ RC(S) ∧ AR(S) ∧
SG(S’))) ∧ RC(S’) SG(S’)
AL AL(S) ∨ AL(S’) SG(S) ∧ AL(S’) SG(S) ∧ AL(S’) False
AR AR(S) ∨ AR(S’) SG(S) ∧ AR(S’) SG(S) ∧ AR(S’) False
TG (TG(S) ∧ SG(S’)) ∨ (TG(S’) ∧ SG(S)) work-in-progress work-in-progress SL(S) ∧ TG(S’)
Table 3: Semigroup rules
sFSetsUnion(D) sFSetsOp(S) sFMinSetsUnion(P) sFMinSetsOp(O)
Prec. ASM(P) ASM(O)
HI True HI(S) True pos : HI(O)
HA FT(D) True pos : FT(P) True
SL SG(D) L(S) ∨ R(S) ∨ TT(P) SL(O) ∧ (¬SL(O) ∨ (IAUS(O) ∧ IAF(O)))
(TE(S) ∧ IDM(S))
CM True CM(S) True CM(O)
IDM True SL(S) True IDM(O) ∧ (¬IDM(O) ∨ SND(O))
L False False False False
R False False False False
LCD False False False False
RCD False False False False
LC False False False False
RC False False False False
AL False False False False
AR False False False False
55
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
sFSetsUnion(D) sFSetsOp(S) sFMinSetsUnion(P) sFMinSetsOp(O)
TG SG(D) work-in-progress work-in-progress work-in-progress
Table 4: Semigroup rules. Rules prefixed with pos : mean that we know only
positive implication (4)
pLeftNaturalOrder(S) pRightNaturalOrder(S) pDual(P)
Prec. CM(S), IDM(S) CM(S), IDM(S)
TT SL(S) SL(S) TT(P)
ASM True True ASM(P)
Table 5: Preorder rules
oLeftNaturalOrder(S) oRightNaturalOrder(S)
Prec. CM(S), IDM(S) CM(S), IDM(S)
LM True True
RM True True
LND SG(S) True
RND SG(S) True
SND SL(S) True
IAUS True True
IAF True True
RT TG(S) TG(S)
LT TG(S) TG(S)
RMCC True SL(S)
LMCC True SL(S)
Table 6: OrderSemigroup rules
bProduct(B,B’) bLex(B,B’) bSelLex(B,B’) bFSetsOp(S)
Prec. CM(B⊕ ), IDM(B⊕ ), HI(B’⊕ ) CM(B⊕ ), SL(B⊕ ), CM(B’⊕ )
LD LD(B) ∧ LD(B’) LD(B) ∧ LD(B’) ∧ (LSS(B) LD(B) ∧ LD(B’) ∧ (LC(B⊗ ) True
∨ LCD(B’⊗ )) ∧ (LCEC(B) ∨ ∨ LCD(B’⊗ ))
LTID(B’)) ∧ (LCC(B) ∨ RI-
TRA(B’))
RD RD(B) ∧ RD(B’) RD(B) ∧ RD(B’) ∧ (RSS(B) RD(B) ∧ RD(B’) ∧ (RC(B⊗ ) True
∨ RCD(B’⊗ )) ∧ (RCEC(B) ∨ RCD(B’⊗ ))
∨ RTID(B’)) ∧ (RCC(B) ∨
PITLA(B’))
PITA PITA(B) ∧ PITA(B’) PITA(B) ∧ PITA(B’) PITA(B) ∧ PITA(B’) True
PATI PATI(B) ∧ PATI(B’) PATI(B) ∧ PATI(B’) PATI(B) ∧ PATI(B’) SG(S)
RSS RSS(B) ∧ RSS(B’) ∧ RSS(B) ∧ RSS(B’) ∧ RSS(B) ∧ RSS(B’) False
(RDT(B) ∨ RCEC(B’)) ∧ (RCEC(B) ∨ RDT(B’))
(RDT(B’) ∨ RCEC(B))
LSS LSS(B) ∧ LSS(B’) ∧ LSS(B) ∧ LSS(B’) ∧ LSS(B) ∧ LSS(B’) False
(LDT(B) ∨ LCEC(B’)) ∧ (LCEC(B) ∨ LDT(B’))
(LDT(B’) ∨ LCEC(B))
RCEC RCEC(B) ∧ RCEC(B’) ∧ RCEC(B) ∧ RCEC(B’) RCEC(B) ∧ RCEC(B’) SG(S)
(RC(B⊗ ) ∨ RC(B’⊗ ))
LCEC LCEC(B) ∧ LCEC(B’) ∧ LCEC(B) ∧ LCEC(B’) LCEC(B) ∧ LCEC(B’) SG(S)
(LC(B⊗ ) ∨ LC(B’⊗ ))
RCC work-in-progress (RCEC(B) ∨ RCP(B’)) ∧ RCC(B) ∧ RCC(B’) RCD(S)
RCC(B) ∧ RCC(B’)
LCC work-in-progress (LCEC(B) ∨ LCP(B’)) ∧ LCC(B) ∧ LCC(B’) LCD(S)
LCC(B) ∧ LCC(B’)
LDT LDT(B) ∧ LDT(B’) LDT(B) ∧ LDT(B’) LDT(B) ∧ LDT(B’) False
RDT RDT(B) ∧ RDT(B’) RDT(B) ∧ RDT(B’) RDT(B) ∧ RDT(B’) False
LCP LCP(B) ∧ LCP(B’) ∧ LCP(B) ∧ LCP(B’) LCP(B) ∧ LCP(B’) LCD(S)
(LDT(B) ∨ LDT(B’))
RCP RCP(B) ∧ RCP(B’) ∧ RCP(B) ∧ RCP(B’) RCP(B) ∧ RCP(B’) RCD(S)
(RDT(B) ∨ RDT(B’))
RI RI(B) ∧ RI(B’) RSI(B) ∨ (RI(B) ∧ RI(B’)) RSI(B) ∨ (RI(B) ∧ RI(B’)) L(S)
LI LI(B) ∧ LI(B’) LSI(B) ∨ (LI(B) ∧ LI(B’)) LSI(B) ∨ (LI(B) ∧ LI(B’)) R(S)
RSI (RI(B) ∧ RSI(B’)) ∨ RSI(B) ∨ (RI(B) ∧ RSI(B’)) RSI(B) ∨ (RI(B) ∧ RSI(B’)) False
(RSI(B) ∧ RI(B’))
56
A Domain-Specific Language for the Specification of Path Algebras V. Naudžiūnas, T. G. Griffin
bProduct(B,B’) bLex(B,B’) bSelLex(B,B’) bFSetsOp(S)
LSI (LI(B) ∧ LSI(B’)) ∨ LSI(B) ∨ (LI(B) ∧ LSI(B’)) LSI(B) ∨ (LI(B) ∧ LSI(B’)) False
(LSI(B) ∧ LI(B’))
RTID RTID(B) ∧ RTID(B’) RTID(B) ∧ RTID(B’) ∧ RTID(B) ∧ RTID(B’) ∧ False
(RDT(B) ∨ RCD(B’⊗ )) ∧ (RDT(B) ∨ RCD(B’⊗ ))
(RCP(B) ∨ PITLA(B’))
LTID LTID(B) ∧ LTID(B’) LTID(B) ∧ LTID(B’) ∧ LTID(B) ∧ LTID(B’) ∧ False
(LDT(B) ∨ LCD(B’⊗ )) ∧ (LDT(B) ∨ LCD(B’⊗ ))
(LCP(B) ∨ RITRA(B’))
PITLA PITLA(B) ∧ PITLA(B’) PITLA(B) ∧ PITLA(B’) PITLA(B) ∧ PITLA(B’) True
RITRA RITRA(B) ∧ RITRA(B’) RITRA(B) ∧ RITRA(B’) RITRA(B) ∧ RITRA(B’) True
Table 7: Bisemigroup rules
bFMinSets(O) bFMinSetsOpUnion(O) bAddOne(B) bAddZero(B)
Prec. LM(O), RM(O), AMS(O) LM(O), RM(O), AMS(O) CM(B⊕ )
LD True IDM(O) ∧ LND(O) ∧ RND(O) LD(B) ∧ IDM(B⊕ ) ∧ LD(B)
(RI(B) ∨ ¬IDM(B⊕ ))
RD True IDM(O) ∧ LND(O) ∧ RND(O) RD(B) ∧ IDM(B⊕ ) ∧ RD(B)
(LI(B) ∨ ¬IDM(B⊕ ))
PITA True work-in-progress PITA(B) True
PATI work-in-progress True True PATI(B)
RSS False False RSS(B) ∧ LSI(B) False
LSS False False LSS(B) ∧ RSI(B) False
RCEC TT(O) SL(O) ∧ (¬SL(O) ∨ (IAUS(O) ∧ IAF(O))) RCEC(B) SL(B⊕ )
LCEC TT(O) SL(O) ∧ (¬SL(O) ∨ (IAUS(O) ∧ IAF(O))) LCEC(B) SL(B⊕ )
RCC RT(O) ∧ (¬RT(O) ∨ SL(O) ∧ (¬SL(O) ∨ (IAUS(O) ∧ IAF(O))) SL(B⊕ ) RCC(B)
RMCC(O))
LCC LT(O) ∧ (¬LT(O) ∨ SL(O) ∧ (¬SL(O) ∨ (IAUS(O) ∧ IAF(O))) SL(B⊕ ) LCC(B)
LMCC(O))
LDT False False False False
RDT False False False False
LCP LT(O) ∧ (¬LT(O) ∨ SL(O) ∧ (¬SL(O) ∨ (IAUS(O) ∧ IAF(O))) SL(B⊕ ) LCP(B)
LMCC(O))
RCP RT(O) ∧ (¬RT(O) ∨ SL(O) ∧ (¬SL(O) ∨ (IAUS(O) ∧ IAF(O))) SL(B⊕ ) RCP(B)
RMCC(O))
RI LND(O) RND(O) RI(B) RI(B)
LI RND(O) RND(O) LI(B) LI(B)
RSI False False False False
LSI False False False False
RTID False False False False
LTID False False False False
PITLA True work-in-progress PITLA(B) True
RITRA True work-in-progress RITRA(B) True
Table 8: Bisemigroup rules
57