Change labelled graph notation to x [ r ]> y

algebraic-graphs · Apr 15, 2018 · 760b3fe · 760b3fe
1 parent 237c361
commit 760b3fe
Show file tree

Hide file tree

Showing 3 changed files with 59 additions and 59 deletions.
diff --git a/src/Algebra/LabelledGraph.agda b/src/Algebra/LabelledGraph.agda
@@ -7,19 +7,19 @@ import Algebra.Dioid as Dioid
 data LabelledGraph (A : Set) : Set where
     ε   : LabelledGraph A      -- Empty graph
     v   : A -> LabelledGraph A -- Graph comprising a single vertex
-    _-[_]>_ : LabelledGraph A -> Dioid -> LabelledGraph A -> LabelledGraph A
+    _[_]>_ : LabelledGraph A -> Dioid -> LabelledGraph A -> LabelledGraph A
                                -- Connect two graphs
 
 _+_ : ∀ {A} -> LabelledGraph A -> LabelledGraph A -> LabelledGraph A
-g + h = g -[ Dioid.zero ]> h
+g + h = g [ Dioid.zero ]> h
 
 _*_ : ∀ {A} -> LabelledGraph A -> LabelledGraph A -> LabelledGraph A
-g * h = g -[ Dioid.one ]> h
+g * h = g [ Dioid.one ]> h
 
 infixl 4  _≡_
 infixl 8  _+_
 infixl 9  _*_
-infixl 9  _-[_]>_
+infixl 9  _[_]>_
 infix  10 _⊆_
 
 -- Equational theory of graphs
@@ -30,16 +30,16 @@ data _≡_ {A} : (x y : LabelledGraph A) -> Set where
     transitivity : ∀ {x y z : LabelledGraph A} -> x ≡ y -> y ≡ z -> x ≡ z
 
     -- Congruence
-    left-congruence  : ∀ {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> x -[ r ]> z ≡ y -[ r ]> z
-    right-congruence : ∀ {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> z -[ r ]> x ≡ z -[ r ]> y
+    left-congruence  : ∀ {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> x [ r ]> z ≡ y [ r ]> z
+    right-congruence : ∀ {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> z [ r ]> x ≡ z [ r ]> y
 
     -- Axioms
     zero-commutativity  : ∀ {x y : LabelledGraph A} -> x + y ≡ y + x
-    left-identity       : ∀ {x     : LabelledGraph A} {r   : Dioid} -> ε -[ r ]> x ≡ x
-    right-identity      : ∀ {x     : LabelledGraph A} {r   : Dioid} -> x -[ r ]> ε ≡ x
-    left-decomposition  : ∀ {x y z : LabelledGraph A} {r s : Dioid} -> x -[ r ]> (y -[ s ]> z) ≡ (x -[ r ]> y) + (x -[ r ]> z) + (y -[ s ]> z)
-    right-decomposition : ∀ {x y z : LabelledGraph A} {r s : Dioid} -> (x -[ r ]> y) -[ s ]> z ≡ (x -[ r ]> y) + (x -[ s ]> z) + (y -[ s ]> z)
-    label-addition      : ∀ {x y   : LabelledGraph A} {r s : Dioid} -> (x -[ r ]> y) + (x -[ s ]> y) ≡ (x -[ r Dioid.+ s ]> y)
+    left-identity       : ∀ {x     : LabelledGraph A} {r   : Dioid} -> ε [ r ]> x ≡ x
+    right-identity      : ∀ {x     : LabelledGraph A} {r   : Dioid} -> x [ r ]> ε ≡ x
+    left-decomposition  : ∀ {x y z : LabelledGraph A} {r s : Dioid} -> x [ r ]> (y [ s ]> z) ≡ (x [ r ]> y) + (x [ r ]> z) + (y [ s ]> z)
+    right-decomposition : ∀ {x y z : LabelledGraph A} {r s : Dioid} -> (x [ r ]> y) [ s ]> z ≡ (x [ r ]> y) + (x [ s ]> z) + (y [ s ]> z)
+    label-addition      : ∀ {x y   : LabelledGraph A} {r s : Dioid} -> (x [ r ]> y) + (x [ s ]> y) ≡ (x [ r Dioid.+ s ]> y)
 
 -- Subgraph relation
 _⊆_ : ∀ {A} -> LabelledGraph A -> LabelledGraph A -> Set

diff --git a/src/Algebra/LabelledGraph/Reasoning.agda b/src/Algebra/LabelledGraph/Reasoning.agda
@@ -24,8 +24,8 @@ infixl 8 _>>_
 _>>_ : ∀ {A} {x y z : LabelledGraph A} -> x ≡ y -> y ≡ z -> x ≡ z
 _>>_ = transitivity
 
-L : ∀ {A} {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> x -[ r ]> z ≡ y -[ r ]> z
+L : ∀ {A} {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> x [ r ]> z ≡ y [ r ]> z
 L = left-congruence
 
-R : ∀ {A} {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> z -[ r ]> x ≡ z -[ r ]> y
+R : ∀ {A} {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> z [ r ]> x ≡ z [ r ]> y
 R = right-congruence
diff --git a/src/Algebra/LabelledGraph/Theorems.agda b/src/Algebra/LabelledGraph/Theorems.agda
@@ -9,17 +9,17 @@ import Algebra.Graph as Graph
 import Algebra.Dioid.Bool as Bool
 
 
-associativity : ∀ {A} {a b c : LabelledGraph A} {r : Dioid} -> (a -[ r ]> b) -[ r ]> c ≡ a -[ r ]> (b -[ r ]> c)
+associativity : ∀ {A} {a b c : LabelledGraph A} {r : Dioid} -> (a [ r ]> b) [ r ]> c ≡ a [ r ]> (b [ r ]> c)
 associativity {_} {a} {b} {c} {r} = right-decomposition >> symmetry left-decomposition
 
-absorption : ∀ {A} {a b : LabelledGraph A} {r : Dioid} -> a -[ r ]> b ≡ a -[ r ]> b + a + b
+absorption : ∀ {A} {a b : LabelledGraph A} {r : Dioid} -> a [ r ]> b ≡ a [ r ]> b + a + b
 absorption {_} {a} {b} {r} =
   begin
-    (a -[ r ]> b) ≡⟨ symmetry right-identity ⟩
-    (a -[ r ]> b) -[ Dioid.zero ]> ε ≡⟨ right-decomposition ⟩
-    (a -[ r ]> b) + (a + ε) + (b + ε) ≡⟨ L (R right-identity ) ⟩
-    (a -[ r ]> b) + a + (b + ε) ≡⟨ R right-identity ⟩
-    (a -[ r ]> b) + a + b
+    (a [ r ]> b) ≡⟨ symmetry right-identity ⟩
+    (a [ r ]> b) [ Dioid.zero ]> ε ≡⟨ right-decomposition ⟩
+    (a [ r ]> b) + (a + ε) + (b + ε) ≡⟨ L (R right-identity ) ⟩
+    (a [ r ]> b) + a + (b + ε) ≡⟨ R right-identity ⟩
+    (a [ r ]> b) + a + b
   ∎
 
 idempotence : ∀ {A} {a : LabelledGraph A} -> a ≡ a + a
@@ -35,72 +35,72 @@ idempotence {_} {a} =
     a + a
   ∎
 
-left-absorption : ∀ {A} {a b : LabelledGraph A} {r : Dioid} -> a -[ r ]> b ≡ a -[ r ]> b + a
+left-absorption : ∀ {A} {a b : LabelledGraph A} {r : Dioid} -> a [ r ]> b ≡ a [ r ]> b + a
 left-absorption {_} {a} {b} {r} =
   begin
-    (a -[ r ]> b)                 ≡⟨ absorption ⟩
-    (a -[ r ]> b) + a + b         ≡⟨ L (R idempotence) ⟩
-    (a -[ r ]> b) + (a + a) + b   ≡⟨ associativity ⟩
-    (a -[ r ]> b) + (a + a + b)   ≡⟨ R zero-commutativity ⟩
-    (a -[ r ]> b) + (b + (a + a)) ≡⟨ R (symmetry associativity) ⟩
-    (a -[ r ]> b) + ((b + a) + a) ≡⟨ R (L zero-commutativity) ⟩
-    (a -[ r ]> b) + ((a + b) + a) ≡⟨ symmetry associativity ⟩
-    (a -[ r ]> b) + (a + b) + a   ≡⟨ L (symmetry associativity) ⟩
-    (a -[ r ]> b) + a + b + a     ≡⟨ L (symmetry absorption) ⟩
-    (a -[ r ]> b) + a
+    (a [ r ]> b)                 ≡⟨ absorption ⟩
+    (a [ r ]> b) + a + b         ≡⟨ L (R idempotence) ⟩
+    (a [ r ]> b) + (a + a) + b   ≡⟨ associativity ⟩
+    (a [ r ]> b) + (a + a + b)   ≡⟨ R zero-commutativity ⟩
+    (a [ r ]> b) + (b + (a + a)) ≡⟨ R (symmetry associativity) ⟩
+    (a [ r ]> b) + ((b + a) + a) ≡⟨ R (L zero-commutativity) ⟩
+    (a [ r ]> b) + ((a + b) + a) ≡⟨ symmetry associativity ⟩
+    (a [ r ]> b) + (a + b) + a   ≡⟨ L (symmetry associativity) ⟩
+    (a [ r ]> b) + a + b + a     ≡⟨ L (symmetry absorption) ⟩
+    (a [ r ]> b) + a
   ∎
 
-right-absorption : ∀ {A} {a b : LabelledGraph A} {r : Dioid} -> a -[ r ]> b ≡ a -[ r ]> b + b
+right-absorption : ∀ {A} {a b : LabelledGraph A} {r : Dioid} -> a [ r ]> b ≡ a [ r ]> b + b
 right-absorption {_} {a} {b} {r} =
   begin
-    (a -[ r ]> b)               ≡⟨ absorption ⟩
-    (a -[ r ]> b) + a + b       ≡⟨ R idempotence ⟩
-    (a -[ r ]> b) + a + (b + b) ≡⟨ symmetry associativity ⟩
-    (a -[ r ]> b) + a + b + b   ≡⟨ L (symmetry absorption) ⟩
-    (a -[ r ]> b) + b
+    (a [ r ]> b)               ≡⟨ absorption ⟩
+    (a [ r ]> b) + a + b       ≡⟨ R idempotence ⟩
+    (a [ r ]> b) + a + (b + b) ≡⟨ symmetry associativity ⟩
+    (a [ r ]> b) + a + b + b   ≡⟨ L (symmetry absorption) ⟩
+    (a [ r ]> b) + b
   ∎
 
-right-distributivity : ∀ {A} {a b c : LabelledGraph A} {r : Dioid} -> (a + b) -[ r ]> c ≡ a -[ r ]> c + b -[ r ]> c
+right-distributivity : ∀ {A} {a b c : LabelledGraph A} {r : Dioid} -> (a + b) [ r ]> c ≡ a [ r ]> c + b [ r ]> c
 right-distributivity {_} {a} {b} {c} {r} =
   begin
-    (a + b) -[ r ]> c                       ≡⟨ right-decomposition ⟩
-    a + b + (a -[ r ]> c) + (b -[ r ]> c)   ≡⟨ L zero-commutativity ⟩
-    (a -[ r ]> c) + (a + b) + (b -[ r ]> c) ≡⟨ L (symmetry associativity) ⟩
-    ((a -[ r ]> c) + a) + b + (b -[ r ]> c) ≡⟨ L (L (symmetry left-absorption)) ⟩
-    (a -[ r ]> c) + b + (b -[ r ]> c)       ≡⟨ associativity ⟩
-    (a -[ r ]> c) + (b + (b -[ r ]> c))     ≡⟨ R zero-commutativity ⟩
-    (a -[ r ]> c) + ((b -[ r ]> c) + b)     ≡⟨ R (symmetry left-absorption) ⟩
-    (a -[ r ]> c) + (b -[ r ]> c)
+    (a + b) [ r ]> c                       ≡⟨ right-decomposition ⟩
+    a + b + (a [ r ]> c) + (b [ r ]> c)   ≡⟨ L zero-commutativity ⟩
+    (a [ r ]> c) + (a + b) + (b [ r ]> c) ≡⟨ L (symmetry associativity) ⟩
+    ((a [ r ]> c) + a) + b + (b [ r ]> c) ≡⟨ L (L (symmetry left-absorption)) ⟩
+    (a [ r ]> c) + b + (b [ r ]> c)       ≡⟨ associativity ⟩
+    (a [ r ]> c) + (b + (b [ r ]> c))     ≡⟨ R zero-commutativity ⟩
+    (a [ r ]> c) + ((b [ r ]> c) + b)     ≡⟨ R (symmetry left-absorption) ⟩
+    (a [ r ]> c) + (b [ r ]> c)
   ∎
 
-left-distributivity : ∀ {A} {a b c : LabelledGraph A} {r : Dioid} -> a -[ r ]> (b + c) ≡ a -[ r ]> b + a -[ r ]> c
+left-distributivity : ∀ {A} {a b c : LabelledGraph A} {r : Dioid} -> a [ r ]> (b + c) ≡ a [ r ]> b + a [ r ]> c
 left-distributivity {_} {a} {b} {c} {r} =
   begin
-    a -[ r ]> (b + c)                   ≡⟨ left-decomposition ⟩
-    a -[ r ]> b + a -[ r ]> c + (b + c) ≡⟨ symmetry associativity ⟩
-    a -[ r ]> b + a -[ r ]> c + b + c   ≡⟨ L associativity ⟩
-    a -[ r ]> b + (a -[ r ]> c + b) + c ≡⟨ L (R zero-commutativity) ⟩
-    a -[ r ]> b + (b + a -[ r ]> c) + c ≡⟨ L (symmetry associativity) ⟩
-    a -[ r ]> b + b + a -[ r ]> c + c   ≡⟨ L (L (symmetry right-absorption)) ⟩
-    a -[ r ]> b + a -[ r ]> c + c       ≡⟨ associativity ⟩
-    a -[ r ]> b + (a -[ r ]> c + c)     ≡⟨ R (symmetry right-absorption) ⟩
-    a -[ r ]> b + a -[ r ]> c
+    a [ r ]> (b + c)                   ≡⟨ left-decomposition ⟩
+    a [ r ]> b + a [ r ]> c + (b + c) ≡⟨ symmetry associativity ⟩
+    a [ r ]> b + a [ r ]> c + b + c   ≡⟨ L associativity ⟩
+    a [ r ]> b + (a [ r ]> c + b) + c ≡⟨ L (R zero-commutativity) ⟩
+    a [ r ]> b + (b + a [ r ]> c) + c ≡⟨ L (symmetry associativity) ⟩
+    a [ r ]> b + b + a [ r ]> c + c   ≡⟨ L (L (symmetry right-absorption)) ⟩
+    a [ r ]> b + a [ r ]> c + c       ≡⟨ associativity ⟩
+    a [ r ]> b + (a [ r ]> c + c)     ≡⟨ R (symmetry right-absorption) ⟩
+    a [ r ]> b + a [ r ]> c
   ∎
 
 -- Notice that we can't define 'graph-laws' below for 'to-graph' as we can't derive the
 -- labelled graph laws from a graph alone. The two constructs are therefore not isomorphic.
 to-graph : ∀ {A} -> LabelledGraph A -> Graph A
 to-graph ε = Graph.ε
 to-graph (v x) = Graph.v x
-to-graph (x -[ r ]> y) with Bool.bool-dioid r
+to-graph (x [ r ]> y) with Bool.bool-dioid r
 ... | Bool.false = to-graph x Graph.+ to-graph y
 ... | Bool.true  = to-graph x Graph.* to-graph y
 
 from-graph : ∀ {A} -> Graph A -> LabelledGraph A
 from-graph Graph.ε = ε
 from-graph (Graph.v x) = v x
-from-graph (x Graph.+ y) = from-graph x -[ Dioid.zero ]> from-graph y
-from-graph (x Graph.* y) = from-graph x -[ Dioid.one  ]> from-graph y
+from-graph (x Graph.+ y) = from-graph x [ Dioid.zero ]> from-graph y
+from-graph (x Graph.* y) = from-graph x [ Dioid.one  ]> from-graph y
 
 graph-laws : ∀ {A} {x y : Graph A} -> x Graph.≡ y -> from-graph x ≡ from-graph y
 graph-laws {x = x} {.x} Graph.reflexivity = reflexivity