🧫[EXPERIMENTAL] Very slow implementation of inequality

src/Builder.ml

@@ -17,6 +17,7 @@ struct
     type cof
     val cof : (dim, cof) Syntax.endo -> cof
     val eq : dim -> dim -> cof
+    val lt : dim -> dim -> cof
     val eq0 : dim -> cof
     val eq1 : dim -> cof
     val bot : cof
@@ -40,6 +41,8 @@ struct
       else
         Syntax.Endo.eq x y
 
+    let lt x y = cof @@ Syntax.Endo.lt x y
+
     let eq0 x = cof @@
       let (=) = equal_dim in
       if x = dim0 then
@@ -94,6 +97,8 @@ struct
             | true, false | false, true -> bot
             | _ -> eq x y
           end
+        | Some Lt (x, y) ->
+          lt x y
         | Some Meet phis -> meet @@ List.map go phis
         | Some Join phis -> join @@ List.map go phis
       in

src/Builder.mli

@@ -42,6 +42,8 @@ sig
     (** Smarter version of {!val:Syntax.Endo.eq} that checks equality. *)
     val eq : dim -> dim -> cof
 
+    val lt : dim -> dim -> cof
+
     (** [eq0 r] is [eq r dim0]. *)
     val eq0 : dim -> cof
 

src/Kusariyarou.ml

@@ -0,0 +1,66 @@
+open StdLabels
+open MoreLabels
+
+module type S =
+sig
+  type t
+  type vertex
+  val empty : t
+  val mem_vertex : vertex -> t -> bool
+  val add_vertex : vertex -> t -> t
+  val add_edge : vertex -> vertex -> t -> t
+  val reachable : vertex -> vertex -> t -> bool
+  val union : t -> t -> t
+end
+
+module Make (V : Map.OrderedType) : S with type vertex = V.t =
+struct
+  type vertex = V.t
+
+  module VMap = Map.Make (V)
+  type node = vertex list
+  type spanning = node VMap.t
+  type t = spanning VMap.t
+
+  let empty : t = VMap.empty
+
+  let mem_vertex (v : vertex) (g : t) : bool = VMap.mem v g
+
+  let add_vertex (v : vertex) (g : t) : t =
+    VMap.add ~key:v ~data:(VMap.singleton v []) g
+
+  let reachable (u : vertex) (v : vertex) (g : t) =
+    if not (mem_vertex u g && mem_vertex v g) then raise Not_found;
+    VMap.mem v (VMap.find u g)
+
+  let add_edge (u : vertex) (v : vertex) (g : t) =
+    if not (mem_vertex u g && mem_vertex v g) then raise Not_found;
+    if reachable u v g then g else
+      let mv = VMap.find v g in
+      let add_pointer i j m =
+        VMap.update ~key:i ~f:(fun l -> Some (j :: Option.get l)) @@
+        VMap.add ~key:j ~data:[] m
+      in
+      let rec meld i mx =
+        let f mx j = if VMap.mem j mx then mx else meld j @@ add_pointer i j mx in
+        List.fold_left ~f ~init:mx (VMap.find i mv)
+      in
+      let f mx =
+        if VMap.mem u mx && not (VMap.mem v mx) then
+          meld v @@ add_pointer u v mx
+        else
+          mx
+      in
+      VMap.map ~f g
+
+  let union (g1 : t) (g2 : t) : t = 
+    let f ~(key : vertex) ~(data : spanning) (init : t) : t =
+      let init = add_vertex key init in
+      let f ~key:key' ~data:_ init = 
+        let init = add_vertex key' init in 
+        add_edge key key' init
+      in
+      VMap.fold ~f ~init data
+    in
+    VMap.fold ~f ~init:g1 g2
+end 

src/Kusariyarou.mli

@@ -0,0 +1,35 @@
+(**
+   This library is based on "Amortized Efficiency of a Path Retrieval Data Structure" by G.F. Italiano, probably with O(log n) slowdown due to the use of {!module:Map}. Moreover, the analysis in the paper does not apply to a persistent data structure design (here) that supports branching. In other words, the amortized bound might not hold if editing operations are applied on previous versions of graphs, though merely checking reachability is okay.
+
+   This library is part of a larger project that implements cubical type theory, and may be changed or merged at any time.
+*)
+
+(** The interface of a graph. *)
+module type S =
+sig
+  (** The type of directed graphs. *)
+  type t
+
+  (** The type of vertices. *)
+  type vertex
+
+  (** The empty graph. *)
+  val empty : t
+
+  (** [mem_vertex v g] tests whether the vertex [v] is in the graph [g]. *)
+  val mem_vertex : vertex -> t -> bool
+
+  (** [add_vertex v g] adds the vertex [v] into the graph [g]. *)
+  val add_vertex : vertex -> t -> t
+
+  (** [add_edge u v g] adds an edge from [u] to [v] into the graph [g]. The two vertices must be already in the graph, or [Not_found] will be raised. *)
+  val add_edge : vertex -> vertex -> t -> t
+
+  (** [reachable u v g] tests whether there is a path from [u] to [v] in the transitive and reflexive closure of [g]. This means reachability is reflexive even if no loop was explicitly added to the graph. If either vertex is not in the graph, [Not_found] will be raised. *)
+  val reachable : vertex -> vertex -> t -> bool
+
+  val union : t -> t -> t
+end
+
+(** The functor that takes a vertex module and outputs a graph module. *)
+module Make : functor (V : Map.OrderedType) -> S with type vertex = V.t

src/Syntax.ml

@@ -1,5 +1,6 @@
 type ('r, 'a) endo =
   | Eq of 'r * 'r
+  | Lt of 'r * 'r
   | Join of 'a list
   | Meet of 'a list
 
@@ -11,6 +12,7 @@ module Endo =
 struct
   type ('r, 'a) t = ('r, 'a) endo =
     | Eq of 'r * 'r
+    | Lt of 'r * 'r
     | Join of 'a list
     | Meet of 'a list
 
@@ -22,16 +24,21 @@ struct
 
   let eq x y = Eq (x, y)
 
+  let lt x y = Lt (x, y)
+
   let map f =
     function
     | Eq _ as phi -> phi
+    | Lt _ as phi -> phi
     | Join l -> Join (List.map f l)
     | Meet l -> Meet (List.map f l)
 
   let dump dump_r dump_a fmt =
     function
     | Eq (r1, r2) ->
       Format.fprintf fmt "@[<hv 1>eq[@,@[%a@];@,@[%a@]]@]" dump_r r1 dump_r r2
+    | Lt (r1, r2) ->
+      Format.fprintf fmt "@[<hv 1>lt[@,@[%a@];@,@[%a@]]@]" dump_r r1 dump_r r2  
     | Join l ->
       Format.fprintf fmt "@[<hv 1>join[@,%a]@]"
         (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ";@,") dump_a) l
@@ -44,6 +51,7 @@ module Free =
 struct
   type nonrec ('r, 'a) endo = ('r, 'a) endo =
     | Eq of 'r * 'r
+    | Lt of 'r * 'r
     | Join of 'a list
     | Meet of 'a list
 
@@ -55,6 +63,7 @@ struct
   let cof c = Cof c
 
   let eq x y = cof @@ Endo.eq x y
+  let lt x y = cof @@ Endo.lt x y
   let join phis = cof @@ Endo.join phis
   let meet phis = cof @@ Endo.meet phis
   let bot = cof Endo.bot

src/Syntax.mli

@@ -2,6 +2,7 @@
     This is for multiple types (for example, abstract syntax) to {i embed} the langauge of cofibrations. *)
 type ('r, 'a) endo =
   | Eq of 'r * 'r
+  | Lt of 'r * 'r
   | Join of 'a list
   | Meet of 'a list
 
@@ -21,12 +22,16 @@ sig
   *)
   type ('r, 'a) t = ('r, 'a) endo =
     | Eq of 'r * 'r
+    | Lt of 'r * 'r
     | Join of 'a list
     | Meet of 'a list
 
   (** [eq x y] is [Eq (x, y)] *)
   val eq : 'r -> 'r -> ('r, 'a) t
 
+  (** [lt x y] is [Lt (x, y)] *)
+  val lt : 'r -> 'r -> ('r, 'a) t
+
   (** [join phis] is [Join phis] *)
   val join : 'a list -> ('r, 'a) t
 
@@ -59,6 +64,7 @@ sig
   *)
   type nonrec ('r, 'a) endo = ('r, 'a) endo =
     | Eq of 'r * 'r
+    | Lt of 'r * 'r
     | Join of 'a list
     | Meet of 'a list
 
@@ -80,6 +86,9 @@ sig
   (** [eq x y] is [Eq (x, y)] *)
   val eq : 'a -> 'a -> ('a, 'v) t
 
+  (** [lt x y] is [Lt (x, y)] *)
+  val lt : 'r -> 'r -> ('r, 'a) t
+
   (** [join phis] is [Cof (Join phis)] *)
   val join : ('a, 'v) t list -> ('a, 'v) t