\documentclass[12pt]{article}
\usepackage{alltt}
\usepackage{fullpage}
\newcommand{\isf}{\tt}
\renewcommand{\topfraction}{.8}
\renewcommand{\floatpagefraction}{.8}
\newenvironment{spec}
{\par\setlength{\baselineskip}{.16in} \begin{flushleft} \small \begin{alltt}}{\end{alltt}\end{flushleft}\par\normalsize\setlength{\baselineskip}{.19in}\noindent\hspace*{-0.08in}}
\begin{document}
\thispagestyle{empty}
\setcounter{page}{0}
{ % ---------------------- TITLEPAGE ---------------------------
\Large \bf \noindent
NASA Technical Memorandum 1998-206923
~\\ ~\\ ~\\ ~\\
\LARGE \bf \noindent
A PVS Graph Theory Library
~\\ ~\\
\begin{flushleft} \setlength{\baselineskip}{.25in}
\noindent
\Large \bf Ricky W. Butler \\
{\em \large Langley Research Center, Hampton, Virginia} \\
~\\
\Large \bf Jon A. Sjogren \\
{\em \large Air Force Office of Scientific Research}
~\\
\end{flushleft}
~\\ ~\\
~\\ ~\\ ~\\ ~\\
February 1998
~\\ ~\\
~\\ ~\\ ~\\
\normalsize
National Aeronautics and \\
Space Administration \\
Langley Research Center \\
Hampton, Virginia 23681-0001
} % ---------------------- END TITLEPAGE ---------------------------
\newpage
\thispagestyle{empty}
\begin{abstract}
This paper documents the NASA Langley PVS graph theory library. The
library provides fundamental definitions for graphs, subgraphs, walks,
paths, subgraphs generated by walks, trees, cycles, degree, separating
sets, and four notions of connectedness. Theorems provided include
Ramsey's and Menger's and the equivalence of all four notions of
connectedness.
\end{abstract}
%\newpage
\tableofcontents
\newpage
\section{Introduction}
This paper documents the NASA Langley PVS graph theory library.
The library develops the fundamental concepts and properties
of finite graphs.
\section{Definition of a Graph}
The standard mathematical definition of a graph is that it is an
ordered pair of sets (V,E) such that E is a subset of the ordered
pairs pairs of V. Typically V and E are assumed to be finite though
sometimes infinite graphs are treated as well. The NASA library
is restricted to finite graphs only. The set V is called the
vertices of the graph and the set E is called the edges of the graph.
Although PVS directly supports ordered pairs, we have chosen the
PVS record structure to define a graph. The advantage of the
record structure is that it provides names for the vertex and
edge sets rather than \verb|proj_1| and \verb|proj_2|.
For efficiency reasons, it is preferable to define a graph in
PVS in two steps. We begin with the definition of a \verb|pregraph|:
\begin{spec}
pregraph: TYPE = [# vert : finite_set[T],
edges: finite_set[doubleton[T]] #]
\end{spec}
A \verb|pregraph| is a structured type with two components:
\verb|vert| and \verb|edges|. The \verb|vert| component is a
finite set over an arbitrary type \verb|T|. This represents the
vertices of the graph. The \verb|edges| component is a finite
set of doubletons (i.e. sets with exactly two members) of \verb|T|.
Thus, an edge is defined by designating its two end vertices.
The type \verb|finite_set| is defined in the PVS finite sets
library. It is a subtype of the type \verb|set| which is defined
in the PVS prelude as follows:
\begin{spec}
sets [T: TYPE]: THEORY
BEGIN
set: TYPE = [T -> bool]
x, y: VAR T
a, b, c: VAR set
p: VAR [T -> bool]
member(x, a): bool = a(x)
emptyset: set = {x | false}
subset?(a, b): bool = (FORALL x: member(x, a) => member(x, b))
union(a, b): set = {x | member(x, a) OR member(x, b)}
intersection(a, b): set = {x | member(x, a) AND member(x, b)}
END sets
\end{spec}
A set is just a boolean-valued function of the element type.
i.e., a function from \verb|T| into \verb|bool|. In PVS this
is written as \verb|[T -> bool]|. If \verb|x| is a member of
a set \verb|S|, the expression \verb|S(x)| evaluates to \verb|true|,
otherwise it evaluates to \verb|false|.
Finite sets are defined as follows:
\begin{spec}
S: VAR set[T]
is_finite(S): bool = (EXISTS (N: nat, f: [(S) -> below[N]]): injective?(f))
finite_set: TYPE = \{ S | is_finite(S) \} CONTAINING emptyset[T]
\end{spec}
Thus finite sets are sets which can be mapped onto ${0 .. N}$ for
some $N$. The cardinality function \verb|card| is defined as follows:
\begin{spec}
inj_set(S): (nonempty?[nat]) =
\{ n | EXISTS (f : [(S)->below[n]]) : injective?(f) \}
card(S): nat = min(inj_set(S))
\end{spec}
All of the standard properties about \verb|card| have been proved and
are available:
\begin{spec}
card_union : THEOREM card(union(A,B)) = card(A) + card(B) -
card(intersection(A,B))
card_add : THEOREM card(add(x,S)) = card(S) +
IF S(x) THEN 0 ELSE 1 ENDIF
card_remove : THEOREM card(remove(x,S)) = card(S) -
IF S(x) THEN 1 ELSE 0 ENDIF
card_subset : THEOREM subset?(A,B) IMPLIES card(A) <= card(B)
card_emptyset : THEOREM card(emptyset[T]) = 0
card_singleton: THEOREM card(singleton(x)) = 1
\end{spec}
Now we are ready to define a graph as follows:
\begin{spec}
graph: TYPE = \{g: pregraph | (FORALL (e: doubleton[T]): edges(g)(e) IMPLIES
(FORALL (x: T): e(x) IMPLIES vert(g)(x))) \}
\end{spec}
A \verb|graph| is a \verb|pregraph| where the \verb|edges| set contains
doubleton sets with elements restricted to the
\verb|vert| set. The \verb|doubleton| type is defined as follows:
\begin{spec}
doubletons[T: TYPE]: THEORY
BEGIN
x,y,z: VAR T
dbl(x,y): set[T] = \{t: T | t = x OR t = y\}
S: VAR set[T]
doubleton?(S): bool = (EXISTS x,y: x /= y AND S = dbl(x,y))
doubleton: TYPE = \{S | EXISTS x,y: x /= y AND S = dbl(x,y)\}
END doubletons
\end{spec}
For example, suppose the base type \verb|T| is defined as follows:
\begin{spec}
T: TYPE = \{a,b,c,d,e,f,g\}
\end{spec}
Then the following \verb|pregraph| is also a \verb|graph|:
\begin{spec}
(# vert := \{a,b,c\},
edges := \{ \{a,b\}, \{b,c\} \} #)
\end{spec}
whereas
\begin{spec}
(# vert := \{a,b,c\},
edges := \{ \{a,b\}, \{b,d\}, \{a,g\} \} #)
\end{spec}
is a \verb|pregraph| but is not a \verb|graph|
\footnote{PVS does not allow {\tt \{ .. \} } as set constructors.
These must be constructed in PVS using LAMBDA expressions or
through use of the functions {\tt add}, {\tt emptyset}, etc.}.
The size of a graph is defined as follows:
\begin{spec}
size(G): nat = card[T](vert(G))
\end{spec}
A singleton graph with one vertex \verb|x| (i.e. size is 1) can
be constructed using the following function:
\begin{spec}
singleton_graph(v): graph = (# vert := singleton[T](v),
edges := emptyset[doubleton[T]] #)
\end{spec}
For convenience we define a number of predicates:
\begin{spec}
edge?(G)(x,y): bool = x /= y AND edges(G)(dbl[T](x,y))
empty?(G): bool = empty?(vert(G))
singleton?(G): bool = (size(G) = 1)
isolated?(G): bool = empty?(edges(G))
\end{spec}
The net result is that we have the following:
\begin{quote}
\begin{tabular}{lp{4.2in}}
\verb|vert(G)| & vertices of graph \verb|G| (a finite set of \verb|T|)\\
\verb|edges(G)| & edges of a graph \verb|G| (a finite set of doubletons taken from \verb|vert(G)|)\\
\verb|edge?(G)(x,y)| & true IFF there is an edge between vertices
\verb|x| and \verb|y| \\
\verb|empty?(G)| & true IFF the graph \verb|G| has no vertices \\
\verb|singleton?(G)| & true IFF graph \verb|G| has only 1 vertex \\
\verb|isolated?(G)| & true IFF graph \verb|G| has no edges \\
\end{tabular}
\end{quote}
The following useful lemmas are provided:
\begin{spec}
x,y,v: VAR T
e: VAR doubleton[T]
G: var graph
edge?_comm : LEMMA edge?(G)(y, x) IMPLIES edge?(G)(x, y)
edge_has_2_verts : LEMMA x /= v AND e(x) AND e(v) IMPLIES e = dbl(x,v)
edge_in_card_gt_1 : LEMMA edges(G)(e) IMPLIES card(vert(G)) > 1
not_singleton_2_vert : LEMMA NOT empty?(G) AND NOT singleton?(G)
IMPLIES (EXISTS (x,y: T): x /= y AND
vert(G)(x) AND vert(G)(y))
\end{spec}
These definitions and lemmas are located in the \verb|graphs| theory.
\section{Graph Operations}
The theory \verb|graph_ops| defines the following operations on a graph:
\begin{quote}
\begin{tabular}{lp{4.2in}}
\verb|union(G1,G2)| & creates a graph that is a union of \verb|G1|
and \verb|G2| \\
\verb|del_vert(G,v)| & removes vertex \verb|v| and all adjacent edges to
\verb|v| from the graph \verb|G| \\
\verb|del_edge(e,G)| & creates subgraph with edge \verb|e| removed from
\verb|G| \\
\end{tabular}
\end{quote}
These operations are defined as follows:
\begin{spec}
union(G1,G2): graph[T] = (# vert := union(vert(G1),vert(G2)),
edges := union(edges(G1),edges(G2)) #)
del_vert(G: graph[T], v: T): graph[T] =
(# vert := remove[T](v,vert(G)),
edges := {e | edges(G)(e) AND NOT e(v)} #)
del_edge(G,e): graph[T] = G WITH [edges := remove(e,edges(G))]
\end{spec}
The following is a partial list of the properties that
have been proved:
\begin{spec}
del_vert_still_in : LEMMA FORALL (x: (vert(G))):
x /= v IMPLIES vert(del_vert(G, v))(x)
size_del_vert : LEMMA FORALL (v: (vert(G))):
size(del_vert(G,v)) = size(G) - 1
edge_in_del_vert : LEMMA (edges(G)(e) AND NOT e(v)) IMPLIES
edges(del_vert(G,v))(e)
del_vert_comm : LEMMA del_vert(del_vert(G, x), v) =
del_vert(del_vert(G, v), x)
del_edge_lem3 : LEMMA edges(G)(e2) AND e2 /= e IMPLIES
edges(del_edge(G,e))(e2)
vert_del_edge : LEMMA vert(del_edge(G,e)) = vert(G)
del_vert_edge_comm : LEMMA del_vert(del_edge(G, e), v) =
del_edge(del_vert(G, v), e)
\end{spec}
\section{Graph Degree}
The theory \verb|graph_deg| develops the concept of degree
of a vertex. The following functions are defined:
\begin{quote}
\begin{tabular}{lp{4.2in}}
\verb|incident_edges(v,G)| & returns set of edges attached to
vertex \verb|v| in graph G\\
\verb|deg(v,G)| & number of edges attached to vertex \verb|v| in
graph G \\
\end{tabular}
\end{quote}
Formally they are specified as follows:
\begin{spec}
v: VAR T
G,GS: VAR graph[T]
incident_edges(v,G) : finite_set[doubleton[T]]
= \{e: doubleton[T] | edges(G)(e) AND e(v) \}
deg(v,G): nat = card(incident_edges(v,G))
\end{spec}
The following useful properties are proved
\begin{spec}
deg_del_edge : LEMMA e = dbl(x,y) AND edges(G)(e) IMPLIES
deg(y, G) = deg(y, del_edge(G, e)) + 1
deg_edge_exists : LEMMA deg(v,G) > 0 IMPLIES
(EXISTS e: e(v) AND edges(G)(e))
deg_to_card : LEMMA deg(v,G) > 0 IMPLIES size(G) >= 2
del_vert_deg_0 : LEMMA deg(v,G) = 0 IMPLIES edges(del_vert(G,v)) = edges(G)
deg_del_vert : LEMMA x /= v AND edges(G)(dbl[T](x, v))
IMPLIES deg(v, del_vert(G, x)) =
deg(v, G) - 1
del_vert_not_incident: LEMMA x /= v AND NOT edges(G)(dbl[T](x, v)) IMPLIES
deg(x, del_vert(G, v)) = deg(x, G)
singleton_deg: LEMMA singleton?(G) IMPLIES deg(v, G) = 0
\end{spec}
\section{Subgraphs}
The subgraph relation is defined as a predicate named \verb|subgraph?|:
\begin{spec}
G1,G2: VAR graph[T]
subgraph?(G1,G2): bool = subset?(vert(G1),vert(G2)) AND
subset?(edges(G1),edges(G2))
\end{spec}
The subgraph type is defined using this predicate:
\begin{spec}
Subgraph(G: graph[T]): TYPE = \{ S: graph[T] | subgraph?(S,G) \}
\end{spec}
The subgraph generated by a vertex set is defined as follows:
\begin{spec}
i: VAR T
e: VAR doubleton[T]
subgraph(G, V): Subgraph(G) =
(G WITH [vert := \{i | vert(G)(i) AND V(i) \},
edges := \{e | edges(G)(e) AND
(FORALL (x: T): e(x) IMPLIES V(x)) \}])
\end{spec}
The following properties have been proved:
\begin{spec}
finite_vert_subset : LEMMA is_finite(LAMBDA (i:T): vert(G)(i) AND V(i))
subgraph_vert_sub : LEMMA subset?(V,vert(G)) IMPLIES
vert(subgraph(G,V)) = V
subgraph_lem : LEMMA subgraph?(subgraph(G,V),G)
SS: VAR graph[T]
subgraph_smaller : LEMMA subgraph?(SS, G) IMPLIES
size(SS) <= size(G)
\end{spec}
These definitions and lemmas are located in the \verb|subgraphs| theory.
\section{Walks and Paths}
Walks are defined using finite sequences which are defined in the \verb|seq_def| theory:
\begin{spec}
seq_def[T: TYPE]: THEORY
BEGIN
finite_seq: TYPE = [# l: nat, seq: [below[l] -> T] #]
END
\end{spec}
We begin by defining a \verb|prewalk| as follows:
\begin{spec}
prewalk: TYPE = \{w: finite_seq[T] | l(w) > 0\}
\end{spec}
where, as before, \verb|T| is the base type of vertices. A \verb|prewalk|
is a finite sequence of vertices. Thus, if we make the declaration:
\begin{spec}
w: VAR prewalk
\end{spec}
\verb|l(w)| is the length of the prewalk and \verb|seq(w)(i)| is the
\verb|i|th element in the sequence. Prewalks are contrained to be
greater than 1 in length. We have used the PVS conversion mechanism,
so that \verb|w(i)| can be written instead of \verb|seq(w)(i)|. A
walk is then defined as follows:
\begin{spec}
s,ps,ww: VAR prewalk
verts_in?(G,s): bool = (FORALL (i: below(l(s))): vert(G)(seq(s)(i)))
walk?(G,ps): bool = verts_in?(G,ps) AND
(FORALL n: n < l(ps) - 1 IMPLIES
edge?(G)(ps(n),ps(n+1)))
Seq(G) : TYPE = \{w: prewalk | verts_in?(G,w)\}
Walk(G): TYPE = \{w: prewalk | walk?(G,w)\}
\end{spec}
A walk is just a \verb|prewalk| where all of the vertices are in the
graph and there is an edge between each consecutive element of the
sequence. The dependent type \verb|Walk(G)| defines the domain (or
type) of all walks in a graph \verb|G|. The dependent type
\verb|Seq(G)| defines the domain (or type) of all prewalks in a
particular graph \verb|G|.
The predicates \verb|from?| and \verb|walk_from?| identify sequences and
walks from one particular vertex to another.
\begin{spec}
from?(ps,u,v): bool = seq(ps)(0) = u AND seq(ps)(l(ps) - 1) = v
walk_from?(G,ps,u,v): bool =
seq(ps)(0) = u AND seq(ps)(l(ps) - 1) = v AND walk?(G,ps)
\end{spec}
The function \verb|verts_of| returns the set of vertices that are in a walk:
\begin{spec}
verts_of(ww: prewalk): finite_set[T] =
\{t: T | (EXISTS (i: below(l(ww))): ww(i) = t)\}
\end{spec}
Similarly, the function \verb|edges_of| returns the set of edges that are in a walk:
\begin{spec}
edges_of(ww): finite_set[doubleton[T]] = \{e: doubleton[T] |
EXISTS (i: below(l(ww)-1)): e = dbl(ww(i),ww(i+1))\}
\end{spec}
Below are listed some of the proved properties about walks:
\begin{spec}
G,GG: VAR graph[T]
x,u,v: VAR T
i,j,n: VAR nat
ps: VAR prewalk
verts_in?_concat: LEMMA FORALL (s1,s2: Seq(G)): verts_in?(G,s1 o s2)
verts_in?_caret : LEMMA FORALL (j: below(l(ps))): i <= j IMPLIES
verts_in?(G,ps) IMPLIES verts_in?(G,ps^(i,j))
vert_seq_lem : LEMMA FORALL (w: Seq(G)): n < l(w) IMPLIES vert(G)(w(n))
verts_of_subset : LEMMA FORALL (w: Seq(G)): subset?(verts_of(w),vert(G))
edges_of_subset : LEMMA walk?(G,ps) IMPLIES subset?(edges_of(ps),edges(G))
walk_verts_in : LEMMA walk?(G,ps) IMPLIES verts_in?(G,ps)
walk_from_vert : LEMMA FORALL (w: prewalk,v1,v2:T):
walk_from?(G,w,v1,v2) IMPLIES
vert(G)(v1) AND vert(G)(v2)
walk_edge_in : LEMMA walk?(G,ps) AND
subset?(edges_of(ps),edges(GG)) AND
subset?(verts_of(ps),vert(GG))
IMPLIES walk?(GG,ps)
\end{spec}
The \verb|walks| theory also proves some useful operators for walks:
\begin{quote}
\begin{tabular}{lp{5.0in}}
\verb|gen_seq1(G,u)| & create a prewalk of length 1 consisting of a single vertex \verb|u| \\
\verb|gen_seq2(G,u,v)| & create a prewalk of length 2 from \verb|u| to \verb|v| \\
\verb|trunc1(p)| & return a prewalk equal to \verb|p| except the last vertex has been removed \\
\verb|add1(p,v)| & return a prewalk equal to \verb|p| except the vertex \verb|v| has been added \\
\verb|rev(p)| & return a finite sequence that is the reverse of \verb|p| \\
\verb|o| & concatenates two finite sequences \\
\verb|^(m,n)| & returns a finite sequence from the \verb|m .. n| elements of a sequence. For
example if \verb|p = v0 -> v1 -> v2 -> v3 -> v4|, then \verb|p^(1,2) = v1 -> v2|. \\
\end{tabular}
\end{quote}
These are defined formally as follows:
\begin{spec}
gen_seq1(G, (u: (vert(G)))): Seq(G) =
(# l := 1, seq := (LAMBDA (i: below(1)): u) #)
gen_seq2(G, (u,v: (vert(G)))): Seq(G) =
(# l := 2,
seq := (LAMBDA (i: below(2)):
IF i = 0 THEN u ELSE v ENDIF) #)
Longprewalk: TYPE = \{ps: prewalk | l(ps) >= 2\}
trunc1(p: Longprewalk ): prewalk = p^(0,l(p)-2)
add1(ww,x): prewalk = (# l := l(ww) + 1,
seq := (LAMBDA (ii: below(l(ww) + 1)):
IF ii < l(ww) THEN seq(ww)(ii) ELSE x ENDIF)
#)
fs, fs1, fs2, fs3: VAR finite_seq
m, n: VAR nat
o(fs1, fs2): finite_seq =
LET l1 = l(fs1),
lsum = l1 + l(fs2)
IN (# l := lsum,
seq := (LAMBDA (n:below[lsum]):
IF n < l1
THEN seq(fs1)(n)
ELSE seq(fs2)(n-l1)
ENDIF) #);
emptyarr(x: below[0]): T
emptyseq: fin_seq(0) = (# l := 0, seq := emptyarr #) ;
p: VAR [nat, nat] ;
^(fs: finite_seq, (p: [nat, below(l(fs))])):
fin_seq(IF proj_1(p) > proj_2(p) THEN 0
ELSE proj_2(p)-proj_1(p)+1 ENDIF) =
LET (m, n) = p
IN IF m > n
THEN emptyseq
ELSE (# l := n-m+1,
seq := (LAMBDA (x: below[n-m+1]): seq(fs)(x + m)) #)
ENDIF ;
rev(fs): finite_seq = (# l := l(fs),
seq := (LAMBDA (i: below(l(fs))): seq(fs)(l(fs)-1-i))
#)
\end{spec}
The following is a partial list of the proven properties about walks:
\begin{spec}
gen_seq1_is_walk: LEMMA vert(G)(x) IMPLIES walk?(G,gen_seq1(G,x))
edge_to_walk : LEMMA u /= v AND edges(G)(edg[T](u, v)) IMPLIES
walk?(G,gen_seq2(G,u,v))
walk?_add1 : LEMMA walk?(G,ww) AND vert(G)(x)
AND edge?(G)(seq(ww)(l(ww)-1),x)
IMPLIES walk?(G,add1(ww,x))
walk?_rev : LEMMA walk?(G,ps) IMPLIES walk?(G,rev(ps))
walk?_caret : LEMMA i <= j AND j < l(ps) AND walk?(G,ps)
IMPLIES walk?(G,ps^(i,j))
yt: VAR T
p1,p2: VAR prewalk
walk_merge: LEMMA walk_from?(G, p1, v, yt) AND
walk_from?(G, p2, u, yt)
IMPLIES
(EXISTS (p: prewalk): walk_from?(G, p, u, v))
\end{spec}
A path is a walk that does not encounter the same vertex more than once. The predicate
\verb|path?| identifies paths:
\begin{spec}
ps: VAR prewalk
path?(G,ps): bool = walk?(G,ps) AND (FORALL (i,j: below(l(ps))):
i /= j IMPLIES ps(i) /= ps(j))
\end{spec}
Similarly the predicate \verb|path_from?| identifies paths from vertex \verb|s| to \verb|t|:
\begin{spec}
path_from?(G,ps,s,t): bool = path?(G,ps) AND from?(ps,s,t)
\end{spec}
Corresponding dependent types are defined:
\begin{spec}
Path(G): TYPE = \{p: prewalk | path?(G,p)\}
Path_from(G,s,t): TYPE = \{p: prewalk | path_from?(G,p,s,t) \}
\end{spec}
The following is a partial list of proven properties:
\begin{spec}
G: VAR graph[T]
x,y,s,t: VAR T
i,j: VAR nat
p,ps: VAR prewalk
path?_caret : LEMMA i <= j AND j < l(ps) AND path?(G,ps)
IMPLIES path?(G,ps^(i,j))
path_from?_caret: LEMMA i <= j AND j < l(ps) AND path_from?(G, ps, s, t)
IMPLIES path_from?(G, ps^(i, j),seq(ps)(i),seq(ps)(j))
path?_rev : LEMMA path?(G,ps) IMPLIES path?(G,rev(ps))
path?_gen_seq2 : LEMMA vert(G)(x) AND vert(G)(y) AND
edge?(G)(x,y) IMPLIES path?(G,gen_seq2(G,x,y))
path?_add1 : LEMMA path?(G,p) AND vert(G)(x)
AND edge?(G)(seq(p)(l(p)-1),x)
AND NOT verts_of(p)(x)
IMPLIES path?(G,add1(p,x))
path?_trunc1 : LEMMA path?(G,p) AND l(p) > 1 IMPLIES
path_from?(G,trunc1(p),seq(p)(0),seq(p)(l(p)-2))
\end{spec}
These definitions and lemmas about paths are located in the \verb|paths| theory.
\section{Connected Graphs}
The library provides four different definitions for connectedness of a graph and
provides proofs that they are are equivalent. These are named \verb|connected|,
\verb|path_connected|, \\
\verb|piece_connected|, and \verb|complected|:
\begin{spec}
G,G1,G2,H1,H2: VAR graph[T]
connected?(G): RECURSIVE bool = singleton?(G) OR
(EXISTS (v: (vert(G))): deg(v,G) > 0
AND connected?(del_vert(G,v)))
MEASURE size(G)
path_connected?(G): bool = NOT empty?(G) AND
(FORALL (x,y: (vert(G))):
(EXISTS (w: Walk(G)): seq(w)(0) = x AND
seq(w)(l(w)-1) = y))
piece_connected?(G): bool = NOT empty?(G) AND
(FORALL H1,H2: G = union(H1,H2) AND
NOT empty?(H1) AND NOT empty?(H2)
IMPLIES NOT empty?(intersection(vert(H1),
vert(H2))))
complected?(G): bool = IF isolated?(G) THEN singleton?(G)
ELSIF (EXISTS (v: (vert(G))): deg(v,G) = 1) THEN
(EXISTS (x: (vert(G))): deg(x,G) = 1 AND
connected?(del_vert(G,x)))
ELSE
(EXISTS (e: (edges(G))):
connected?(del_edge(G,e)))
ENDIF
\end{spec}
These definitions are located in the \verb|graph_conn_defs| theory. The
following lemmas about equivalence are located in the theory
\verb|graph_connected|:
\begin{spec}
graph_connected[T: TYPE]: THEORY
BEGIN
G: VAR graph[T]
conn_eq_path : THEOREM connected?(G) = path_connected?(G)
path_eq_piece: THEOREM path_connected?(G) = piece_connected?(G)
piece_eq_conn: THEOREM piece_connected?(G) = connected?(G)
conn_eq_complected: THEOREM connected?(G) = complected?(G)
END graph_connected
\end{spec}
\section{Circuits}
A slightly non-traditional definition of circuit is used. A circuit is
a walk that starts and ends in the same place (i.e. a \verb|pre_circuit|) and is
cyclically reduced (i.e. \verb|cyclically_reduced?|).
\begin{spec}
reducible?(G: graph[T], w: Seq(G)): bool = (EXISTS (k: posnat): k <
l(w) - 1 AND w(k-1) = w(k+1))
reduced?(G: graph[T], w: Seq(G)): bool = NOT reducible?(G,w)
cyclically_reduced?(G: graph[T], w: Seq(G)): bool = l(w) > 2 AND
reduced?(G,w) AND w(1) /= w(l(w)-2)
pre_circuit?(G: graph[T], w: prewalk): bool = walk?(G,w) AND
w(0) = w(l(w)-1)
circuit?(G: graph[T], w: Seq(G)): bool = walk?(G,w) AND
cyclically_reduced?(G,w) AND
pre_circuit?(G,w)
\end{spec}
The following properties are proved in the \verb|circuit_deg| theory:
\begin{spec}
cir_deg_G : LEMMA (EXISTS (a,b: (vert(G))): vert(G)(z) AND
a /= b AND edge?(G)(a,z) AND edge?(G)(b,z) ) IMPLIES
deg(z,G) >= 2
circuit_deg : LEMMA FORALL (w: Walk(G),i: below(l(w))): circuit?(G,w)
IMPLIES deg(w(i),G_from(G,w)) >= 2
\end{spec}
\section{Trees}
Trees are defined recursively as follows:
\begin{spec}
G: VAR graph[T]
tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR
(EXISTS (v: (vert(G))): deg(v,G) = 1 AND
tree?(del_vert[T](G,v)))
MEASURE size(G)
\end{spec}
and the \verb|Tree| type is defined as follows:
\begin{spec}
Tree: TYPE = \{G: graph[T] | tree?(G)\}
\end{spec}
The fundamental property that trees have no circuits is proved in \verb|tree_circ| theory.
\begin{spec}
tree_no_circuits: THEOREM (FORALL (w: Walk(G)): tree?(G) =>
NOT circuit?(G,w))
\end{spec}
\section{Ramsey's Theorem}
This work builds upon a verification of this theorem by
Natarajan Shankar and the paper entitled ``The Boyer-Moore Prover and
Nuprl: An Experimental Comparison'' by David Basin and Matt
Kaufmann\footnote{CLI Technical Report 58, July 17, 1990.}.
\begin{spec}
i, j: VAR T
n, p, q, ii: VAR nat
g: VAR graph[T]
G: VAR Graph[T] % nonempty
V: VAR finite_set[T]
contains_clique(g, n): bool =
(EXISTS (C: finite_set[T]):
subset?(C,vert(g)) AND card(C) >= n AND
(FORALL i,j: i/=j AND C(i) AND C(j) IMPLIES edge?(g)(i,j)))
contains_indep(g, n): bool =
(EXISTS (D: finite_set[T]):
subset?(D, vert(g)) AND card(D) >= n AND
(FORALL i, j: i/=j AND D(i) AND D(j) IMPLIES NOT edge?(g)(i, j)))
subgraph_clique: LEMMA (FORALL (V: set[T]):
contains_clique(subgraph(g, V), p)
IMPLIES contains_clique(g, p))
subgraph_indep : LEMMA (FORALL (V: set[T]):
contains_indep(subgraph(g, V), p)
IMPLIES contains_indep(g, p))
ramseys_theorem: THEOREM (EXISTS (n: posnat):
(FORALL (G: Graph[T]): size(G) >= n
IMPLIES (contains_clique(G, l1) OR
contains_indep(G, l2))))
\end{spec}
\section{Menger's Theorem}
To state menger's theorem one must first define minimum separating sets. This is fairly
complicated in a formal system. We begin with the concept of a separating set:
\begin{verbatim}
G: VAR graph[T]
v,s,t: VAR T
e: VAR doubleton[T]
V: VAR finite_set[T]
del_verts(G,V): graph[T] =
(# vert := difference[T](vert(G),V),
edges := {e | edges(G)(e) AND
(FORALL v: V(v) IMPLIES NOT e(v))} #)
separates(G,V,s,t): bool = NOT V(s) AND NOT V(t) AND
NOT (EXISTS (w: prewalk): walk_from?(del_verts(G,V),w,s,t))
\end{verbatim}
In other words \verb|V| \verb|separates| \verb|s| and \verb|t| when
its removal disconnects \verb|s| and \verb|t|. To define the minimum
separating set, we use an abstract minimum function defined in the
\verb|abstract_min| theory. The net result is that we end up with a
function \verb|min_sep_set| with all of the following desired
properties
\begin{spec}
min_sep_set(G,s,t): finite_set[T] = min[seps(G,s,t),
(LAMBDA (v: seps(G,s,t)): card(v)),
(LAMBDA (v: seps(G,s,t)): true)]
separable?(G,s,t): bool = (s /= t AND NOT edge?(G)(s,t))
min_sep_set_edge: LEMMA NOT separable?(G,s,t) IMPLIES
min_sep_set(G,s,t) = vert(G)
min_sep_set_card: LEMMA FORALL (s,t: (vert(G))): separates(G,V,s,t)
IMPLIES card(min_sep_set(G,s,t)) <= card(V)
min_sep_set_seps: LEMMA separable?(G,s,t) IMPLIES
separates(G,min_sep_set(G,s,t),s,t)
min_sep_set_vert: LEMMA separable?(G,s,t) AND min_sep_set(G,s,t)(v)
IMPLIES vert(G)(v)
ends_not_in_min_sep_set: LEMMA separable?(G,s,t) AND min_sep_set(G, s, t)(v)
IMPLIES v /= s AND v /= t
\end{spec}
We then define \verb|sep_num| as follows:
\begin{spec}
sep_num(G,s,t): nat = card(min_sep_set(G,s,t))
\end{spec}
Next, we define a predicate \verb|independent?| that defines when two paths are independent:
\begin{spec}
independent?(w1,w2: prewalk): bool =
(FORALL (i,j: nat): i > 0 AND i < l(w1) - 1 AND
j > 0 AND j < l(w2) - 1 IMPLIES
seq(w1)(i) /= seq(w2)(j))
\end{spec}
The concept of a set of independent paths is defined as follows:
\begin{spec}
set_of_paths(G,s,t): TYPE = finite_set[Path_from(G,s,t)]
ind_path_set?(G,s,t,(pset: set_of_paths(G,s,t))): bool =
(FORALL (p1,p2: Path_from(G,s,t)):
pset(p1) AND pset(p2) AND p1 /= p2
IMPLIES independent?(p1,p2))
\end{spec}
In other words, a set of paths is an \verb|ind_path_set?| if all pairs of paths in the set
are independent.
We can now state Menger's theorem in both directions:
\begin{spec}
easy_menger: LEMMA FORALL (ips: set_of_paths(G,s,t)):
separable?(G,s,t) AND
ind_path_set?(G,s,t,ips) IMPLIES
card(ips) <= sep_num(G,s,t)
hard_menger: AXIOM separable?(G,s,t) AND sep_num(G,s,t) = K AND
vert(G)(s) AND vert(G)(t)
IMPLIES
(EXISTS (ips: set_of_paths(G,s,t)):
card(ips) = K AND ind_path_set?(G,s,t,ips))
\end{spec}
The hard direction of menger has only been formally proved for the \verb|K = 2| case.
\begin{spec}
hard_menger: LEMMA separable?(G,s,t) AND sep_num(G,s,t) = 2 AND
vert(G)(s) AND vert(G)(t)
IMPLIES
(EXISTS (ips: set_of_paths(G,s,t)):
card(ips) = 2 AND ind_path_set?(G,s,t,ips))
\end{spec}
\section{PVS Theories}
The following is a list of the PVS theories and description:
\begin{quote}
\begin{tabular}{lp{5.0in}}
\verb|abstract_min| & abstract definition of min \\
\verb|abstract_max| & abstract definition of max \\
\verb|circuit_deg| & degree of circuits \\
\verb|circuits| & theory of circuits \\
\verb|cycle_deg| & degree of cycle \\
\verb|doubletons| & theory of doubletons used for definition of edge \\
\verb|graphs| & fundamental definitiion of a graph \\
\verb|graph_complected| & unusual definition of connected graph \\
\verb|graph_conn_defs| & defs of piece, path, and structural connectedness \\
\verb|graph_conn_piece| & structural connected $supset$ piece connected \\
\verb|graph_connected| & all connected defs are equivalent \\
\verb|graph_path_conn| & path connected $supset$ structural connected \\
\verb|graph_piece_path| & piece connected $supset$ path connected \\
\verb|graph_deg| & definition of degree \\
\verb|graph_deg_sum| & theorem relating vertex degree and number of edges \\
\verb|graph_inductions| & vertex and edge inductions for graphs \\
\verb|graph_ops| & delete vertex and delete edge operations \\
\verb|h_menger| & hard menger \\
\verb|ind_paths| & definition of independent paths \\
\verb|max_subgraphs| & maximal subgraphs with specified property \\
\verb|max_subtrees| & maximal subtrees with specified property \\
\verb|meng_scaff| & scaffolding for hard menger proof \\
\verb|meng_scaff_defs| & scaffolding for hard menger proof \\
\verb|meng_scaff_prelude| & scaffolding for hard menger proof \\
\verb|menger| & menger's theorem \\
\verb|min_walk_reduced| & theorem that minimum walk is reduced \\
\verb|min_walks| & minimum walk satisfying a property \\
\verb|path_lems| & some useful lemmas about paths \\
\verb|path_ops| & deleting vertex and edge operations \\
\verb|paths| & fundamental definition and properties about paths \\
\verb|ramsey_new| & Ramsey's theorem \\
\verb|reduce_walks| & operation to reduce a walk \\
\verb|sep_set_lems| & properties of separating sets \\
\verb|sep_sets| & definition of separating sets \\
\verb|subgraphs| & generation of subgraphs from vertex sets \\
\verb|subgraphs_from_walk| & generation of subgraphs from walks \\
\verb|subtrees| & subtrees of a graph \\
\verb|tree_circ| & theorem that tree has no circuits \\
\verb|tree_paths| & theorem that tree has only one path between vertices \\
\verb|trees| & fundamental definition of trees \\
\verb|walk_inductions| & induction on length of a walk \\
\verb|walks| & fundamental definition and properties of walks \\
\end{tabular}
\end{quote}
The PVS specifications are available at:
\begin{spec}
http://atb-www.larc.nasa.gov/ftp/larc/PVS-library/.
\end{spec}
\section{Concluding Remarks}
This paper gives a brief overview of the NASA Langley PVS Graph Theory Library.
The library provides definitions and lemmas for graph operations such as deleting a vertex
or edge, provides definitions for vertex degree, subgraphs, minimal subgraphs,
walks and paths, notions of connectedness, circuit and trees. Both Ramsey's Theorem
and Menger's Theorem are provided.
\appendix
\section{APPENDIX: Other Supporting Theories}
\subsection{Graph Inductions}
The graph theory library provides two basic means of performing induction
on a graph: induction on the number of vertices and induction on the
number of edges.
\begin{spec}
G,GG: VAR graph[T]
P: VAR pred[graph[T]]
graph_induction_vert : THEOREM (FORALL G:
(FORALL GG: size(GG) < size(G) IMPLIES P(GG))
IMPLIES P(G))
IMPLIES (FORALL G: P(G))
graph_induction_edge : THEOREM (FORALL G:
(FORALL GG: num_edges(GG) < num_edges(G) IMPLIES P(GG))
IMPLIES P(G))
IMPLIES (FORALL G: P(G))
\end{spec}
These theorems can be invoked using the PVS strategy \verb|INDUCT|. For example
\begin{spec}
(INDUCT "G" 1 "graph_induction_vert")
\end{spec}
invokes vertex induction on formula 1. They are available in
theory \verb|graph_inductions|.
These induction theorems were proved by rewriting with the following lemmas
\begin{spec}
size_prep : LEMMA (FORALL G : P(G)) IFF
(FORALL n, G : size(G) = n IMPLIES P(G))
num_edges_prep : LEMMA (FORALL G : P(G)) IFF
(FORALL n, G : num_edges(G) = n IMPLIES P(G))
\end{spec}
which converts the theorem into formulas that are universally quantified
over the naturals. The resulting formulas were then easily proved using
PVS's built-in theorem for strong induction:
\begin{spec}
NAT_induction: LEMMA
(FORALL j: (FORALL k: k < j IMPLIES p(k)) IMPLIES p(j))
IMPLIES (FORALL i: p(i))
\end{spec}
\subsection{Subgraphs Generated From Walks}
The graph theory library provides a function \verb|G_from| that constructs a
subgraph of a graph \verb|G| that contains the vertices and edges of a walk \verb|w|:
\begin{spec}
G_from(Ggraph[T], w: Walk(G)): Subgraph(G) = (# vert := verts_of(w),
edges := edges_of(w) #)
\end{spec}
The following properties of \verb|G_from| have been proved:
\begin{spec}
vert_G_from : LEMMA FORALL (w: Walk(G), i: below(l(w))):
vert(G_from(G, w))(w(i))
edge?_G_from : LEMMA FORALL (w: Walk(G), i: below(l(w)-1)):
edge?(G_from(G, w))(w(i), w(i+1))
vert_G_from_not : LEMMA FORALL (w: Walk(G)):
subset?(vert(G_from(G, w)), vert(GG)) AND
NOT verts_of(w)(v)
IMPLIES
subset?(vert(G_from(G, w)), remove[T](v, vert(GG)))
del_vert_subgraph: LEMMA FORALL (w: Walk(G), v: (vert(GG))):
subgraph?(G_from(G, w), GG) AND
NOT verts_of(w)(v) IMPLIES
subgraph?(G_from(G, w), del_vert(GG, v))
\end{spec}
This lemmas are available in the theory \verb|subgraphs_from_walk|.
\subsection{Maximum Subgraphs}
Given a graph \verb|G| we say that a subgraph \verb|S| is maximal with respect
to a particular property \verb|P| if it is the largest subgraph that satisfies
the property. Formally we write:
\begin{spec}
maximal?(G: graph[T], S: Subgraph(G),P: Gpred(G)): bool = P(S) AND
(FORALL (SS: Subgraph(G)): P(SS) IMPLIES
size(SS) <= size(S))
\end{spec}
We can define a function that returns the maximum subgraph under the assumption
that there exists at least one subgraph that satisfies the predicate. Therefore
this function is only defined on a subtype of \verb|P|, namely \verb|Gpred|:
\begin{spec}
G: VAR graph[T]
Gpred(G): TYPE = {P: pred[graph[T]] | (EXISTS (S: graph[T]):
subgraph?(S,G) AND P(S))}
\end{spec}
We now define \verb|max_subgraph| as follows:
\begin{spec}
max_subgraph(G: graph[T], P: Gpred(G)): {S: Subgraph(G) | maximal?(G,S,P)}
\end{spec}
The following useful properties of \verb|max_subgraph| have been proved:
\begin{spec}
max_subgraph_def : LEMMA FORALL (P: Gpred(G)):
maximal?(G,max_subgraph(G,P),P)
max_subgraph_in : LEMMA FORALL (P: Gpred(G)): P(max_subgraph(G,P))
max_subgraph_is_max : LEMMA FORALL (P: Gpred(G)):
(FORALL (SS: Subgraph(G)): P(SS) IMPLIES
size(SS) <= size(max_subgraph(G,P)))
\end{spec}
These definitions and lemmas are located in the theory \verb|max_subgraphs|.
A similar theory for subtrees is available in the theory \verb|max_subtrees|.
\subsection{Minimum Walks}
Given that a walk \verb|w| from vertex \verb|x| to vertex \verb|y|
exists, we sometimes need to find the shortest walk from \verb|x| to
\verb|y|. The theory \verb|min_walks| provides a function
\verb|min_walk_from| that returns a walk that is minimal. It is
defined formally as follows:
\begin{spec}
v1,v2,x,y: VAR T
G: VAR graph[T]
gr_walk(v1,v2): TYPE = {G: graph[T] | vert(G)(v1) AND vert(G)(v2) AND
(EXISTS (w: Seq(G)):
walk_from?(G,w,v1,v2))}
min_walk_from(x,y,(Gw:gr_walk(x,y))): Walk(Gw) =
min[Seq(Gw),(LAMBDA (w: Seq(Gw)): l(w)),
(LAMBDA (w: Seq(Gw)): walk_from?(Gw,w,x,y))]
\end{spec}
The following properties of \verb|min_walk_from| have been established:
\begin{spec}
is_min(G,(w: Seq(G)),x,y): bool = walk?(G,w) AND
(FORALL (ww: Seq(G)): walk_from?(G,ww,x,y) IMPLIES
l(w) <= l(ww))
min_walk_def: LEMMA FORALL (Gw: gr_walk(x,y)):
walk_from?(Gw,min_walk_from(x,y,Gw),x,y) AND
is_min(Gw, min_walk_from(x,y,Gw),x,y)
min_walk_in : LEMMA FORALL (Gw: gr_walk(x,y)):
walk_from?(Gw,min_walk_from(x,y,Gw),x,y)
min_walk_is_min: LEMMA FORALL (Gw: gr_walk(x,y), ww: Seq(Gw)):
walk_from?(Gw,ww,x,y) IMPLIES
l(min_walk_from(x,y,Gw)) <= l(ww)
reduced?(G: graph[T], w: Seq(G)): bool =
(FORALL (k: nat): k > 0 AND k < l(w) - 1 IMPLIES w(k-1) /= w(k+1))
x,y: VAR T
min_walk_is_reduced: LEMMA FORALL (Gw: gr_walk(x,y)):
reduced?(Gw,min_walk_from(x,y,Gw))
\end{spec}
These lemmas are available in the theories \verb|min_walks| and \verb|min_walk_reduced|.
\subsection{Abstract Min and Max Theories}
The need for a function that returns the smallest or largest object
that satisfies a particular predicate arises in many contexts. For
example, one may need a minimal walk from \verb|s| to \verb|t| or
the maximal subgraph that contains a tree. Thus, it is
useful to develop abstract min and max theories that can be
instantiated in multiple ways to provide different min and max
functions. Such a theory must be parameterized by
\begin{quote}
\begin{tabular}{lp{5.0in}}
\verb|T: TYPE| & the type of the object for which a \verb|min| function is needed \\
\verb|size:[T -> nat]| & the ``size'' function by which objects are compared \\
\verb|P: pred[T]| & the property that the min function must satisfy \\
\end{tabular}
\end{quote}
Formally we have
\begin{spec}
abstract_min[T: TYPE, size: [T -> nat], P: pred[T]]: THEORY
\end{spec}
and
\begin{spec}
abstract_max[T: TYPE, size: [T -> nat], P: pred[T]]: THEORY
\end{spec}
To simplify the following discussion, only the \verb|abstract_min| theory will
be elaborated in detail. The \verb|abstract_max| theory is conceptually
identical.
In order for a minimum function to be defined, it is necessary that
at least one object exists that satisfies the property. Thus, the theory
contains the following assuming clause
\begin{spec}
ASSUMING
T_ne: ASSUMPTION EXISTS (t: T): P(t)
ENDASSUMING
\end{spec}
User's of this theory are required to prove that this assumption
holds for their type \verb|T| (via PVS's TCC generation mechanism).
A function \verb|minimal?(S: T)| is then defined as follows:
\begin{spec}
minimal?(S): bool = P(S) AND
(FORALL (SS: T): P(SS) IMPLIES size(S) <= size(SS))
\end{spec}
Using PVS's dependent type mechanism,
\verb|min| is specified by constraining it's return type to be the subset of
\verb|T| that satisfies \verb|minimal?|:
\begin{spec}
min: \{S: T | minimal?(S)\}
\end{spec}
If there are multiple instances of objects that are minimal, the
theory does not specify which object is selected by \verb|min|. It just
states that \verb|min| will return one of the minimal ones. This
definition causes PVS to generate the following proof obligation
(i.e. TCC):
\begin{spec}
min_TCC1: OBLIGATION (EXISTS (x: {S: T | minimal?(S)}): TRUE);
\end{spec}
This was proved using a function \verb|min_f|, defined as follows:
\begin{spec}
is_one(n): bool = (EXISTS (S: T): P(S) AND size(S) = n)
min_f: nat = min[nat]({n: nat | is_one(n)})
\end{spec}
to construct the required \verb|min| function. The \verb|T_ne| assumption
is sufficient to guarantee that \verb|min_f| is well-defined.
The following properties have been proved about \verb|min|:
\begin{spec}
min_def: LEMMA minimal?(min)
min_in : LEMMA P(min)
min_is_min: LEMMA P(SS) IMPLIES size(min) <= size(SS)
\end{spec}
These properties are sufficient for most applications.
%\bibliographystyle{/home/rwb/bib/NASA}
%\bibliography{/home/rwb/bib/database}
\end{document}