The Coq mailing list

[Fred Smith <fsmith1024 AT gmail.com>]

The second paper by Mokhov was also very interesting.  Thanks for the pointers.

-Fred

On Tue, Dec 4, 2018 at 8:56 PM Fred Smith <fsmith1024 AT gmail.com> wrote:

Hi Ray,

Thanks for pointing out this work.  It was a thought provoking read.  My own experience with imperative control-flow graphs matches their experience pretty well.

-Fred

On Mon, Dec 3, 2018 at 4:27 PM Xuanrui Qi <xqi01 AT cs.tufts.edu> wrote:

Hello Fred,

I will go slightly off-topic here and suggest two alternative (more
advanced) encodings of graphs: it might be overkill for what you are
doing, but they are good purely functional encodings of graphs (which
may or may not be cyclic).

The first encoding is a purely applicative encoding invented by Norman
Ramsey and Jõao Dias based on Huet's zipper. It is first described in
their ML Workshop 2005 paper (
https://www.cs.tufts.edu/~nr/pubs/zipcfg.pdf). Norman and Jõao
invented this representation to implement CFGs, but I think it could be
adapted to normal graphs as well.

The other is an algebraic, higher-order representation, presented in
the Haskell 2017 functional pearl "Algebraic Graphs with Class" by
Andrey Mokhov (
https://eprint.ncl.ac.uk/file_store/production/239461/EF82F5FE-66E3-4F64-A1AC-A366D1961738.pdf
). The code presented makes heavy use of type classes, but I believe it
could be modified to not use type classes (and, failing that, Coq does
have type classes anyway).

Since both representations are pure and total, I think they could be
adapted into Coq easily. It would probably be totally overkill for your
task at hand, but they seem like good, clever, purely functional
representations of graphs in general.

-Ray

On Sun, 2018-12-02 at 15:25 -0500, Fred Smith wrote:
> Hi,
>
> I am looking for engineering advice to help me understand the
> tradeoffs between different ways of encoding the same information in
> Coq.
>
> As my exercise, I am trying to encode paths in a graph.  For
> simplicity these are just lists of edges where each edge ends where
> the next edge begins.
>
> Below is a Coq file that uses 3 different encodings.  Two inductive
> ones, and the third as a predicate.  What are the pros and cons of
> these choices?
>
> Thanks,
>
> Fred
>
> ----- path.v below -----
>
> (* Experiments in encoding paths in Coq.
>
> A path is simply a list of edges where the destination of the
> preceding edge is the source of the next edge.
>
> *)
>
> Require Import List.
>
> Definition vertex := nat.
> Definition edge := (vertex * vertex)%type.
>
> (* Simple encoding as lists with a predicate *)
> Fixpoint path (l : list edge) :=
>   match l with
>   | nil => False
>   | hd :: tl => (match tl with
>                  | nil => True
>                  | hd2 :: tl2 => (snd hd) = (fst hd2)
>                  end) /\ (path tl)
>   end.
>
> (* Define as a subset. *)
> Definition Path := { l : list edge | path l }.
>
> (* Encode as an inductive definition that makes the path correct by
> construction.  Note, need to include the vertex endpoints in the type
> to enforce the invariants. *)
> Inductive pathI : vertex -> vertex -> Set :=
> | path_tl : forall e:edge, pathI (fst e) (snd e)
> | path_hd : forall e:edge, forall v1 v2:vertex, forall p:pathI v1 v2,
> (snd e) = v1 -> pathI (fst e) v2.
>
> (* We could write a symmetrical encoding as well. *)
> Inductive pathS : vertex -> vertex -> Set :=
> | pathS_edge : forall e:edge, pathS (fst e) (snd e)
> | pathS_compose : forall v1 v2 v3 : vertex, forall p1 : pathS v1 v2,
> forall p2 : pathS v2 v3, pathS v1 v3.
>
>                                     
> (* Which of these encoding is preferred?
>   1. Predicate encoding allows reuse of list facts and definitions,
> but requires lemmas connecting them together.
>   2. Inductive encoding requires reimplmenting all list elements.
>   3. Symmetric encoding makes simple equality not work, requires a
> special equality operator.
>  *)
>
>