\documentstyle[12pt,fullpage,alltt]{article}
\input{psfig}
\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 xxxxxx
~\\ ~\\ ~\\ ~\\
\LARGE \bf \noindent
Ramsey's Theorem Revisited In PVS Using The Finite Sets Library
~\\ ~\\
\begin{flushleft} \setlength{\baselineskip}{.25in}
\noindent
\Large \bf Ricky W. Butler \\
{\em \large Langley Research Center, Hampton, Virginia} \\
~\\
~\\
\end{flushleft}
~\\ ~\\
~\\ ~\\ ~\\ ~\\
August 1996
~\\ ~\\
~\\
\normalsize
National Aeronautics and \\
Space Administration \\
Langley Research Center \\
Hampton, Virginia 23681-0001
} % ---------------------- END TITLEPAGE ---------------------------
\newpage
\thispagestyle{empty}
\begin{abstract}
This paper ...
\end{abstract}
%\newpage
\tableofcontents
\newpage
\section{Introduction}
This paper develops a specification and proof of Ramsey's Theorem
using the PVS system augmented with the newly developed finite sets
library. 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.}.
A second theorem (i.e. the sum of the degrees of the vertices of a graph
is twice the number of edges) is proved to illustrate that the
graph formalism is useful for more than just Ramsey's Theorem.
\section{Informal Presentation of Ramsey's Theorem}
A finite graph is a finite set of vertices $V$ and a symmetric
relation $edge?$ defined on these vertices. A {\em clique} $C$ of a %
finite graph $G$ is a subset of $V$ where all elements have an edge
between them (i.e. $ \forall v_1,v_2: v_1, v_2 \in C \supset
\mbox{edge?}(v_1,v_2)$.) An {\em independent set} $D$ is a subset of
$V$ where there are no edges between any pair of elements
(i.e. $ \forall v_1,v_2: v_1, v_2 \in D \supset \mbox{NOT
~edge?}(v_1,v_2)$.) If the cardinality of a clique $C$ is $l$, then
it is called an {\em l-clique}.
Similarly, if the cardinality of a independent set $D$ is $l$, then
it is called an {\em l-independent set}. This provides
enough framework to express Ramsey's Theorem:
~\\
\noindent
{\em Ramsey's Theorem:} For all $l_1, l_2$, there exists an $n$ such
that for all graphs containing at least $n$ vertices, the graph will
contain eith an $l_1$ clique or an $l_2$ independent set. The smallest
such $n$ is often called the Ramsey number corresponding to $l_1, l_2$.
~\\
\noindent
{\em Proof.} The proof is by induction on the sum of $l_1$ and $l_2$.
The base case is deals with empty cliques and empty independent sets and
is trivial. The induction step ...............
\section{Formalization of Ramsey's Theorem in PVS}
It is natural to begin with the definition of a graph. Natarajan Shankar
defined a graph as follows:
\begin{spec}
graph: TYPE = [# vertices : SETOF[nat],
edges: (symmetric?[nat]) #]
\end{spec}
The \verb|graph| type is a PVS record consisting of two fields. The
first field, labeled \verb|vertices|, is a set of natural numbers and
the second field, labeled \verb|edges|, is a symmetric relation over
the naturals\footnote{This essentially converts a digraph into an
undirected graph.}. The identifier \verb|symmetric?| is defined in
the PVS prelude as follows:
\begin{spec}
relations [T: TYPE]: THEORY
BEGIN
R: VAR PRED[[T, T]]
x, y, z: VAR T
symmetric?(R): bool = FORALL x, y: R(x, y) IMPLIES R(y, x)
END relations
\end{spec}
Although this definition was adequate for Ramsey's Theorem, it is not
as general as one might desire. In particular, the set of vertices are
not drawn from an abstract type. The following is preferable:
\begin{spec}
graph: TYPE = [# vertices : set[T],
edge?: (symmetric?[T]) #]
\end{spec}
where \verb|T| is an \verb|TYPE| defined via a theory parameter. It
appears that Shankar defined graphs over the \verb|nat|s so that he
could conveniently count the number of vertices in a graph as
follows:\footnote{The PVS finite sets library was not available at
that time.}
\begin{spec}
n: VAR nat
P: VAR set[nat]
count(n, P): RECURSIVE nat =
(IF n>0 THEN (IF P(n-1) THEN 1 ELSE 0 ENDIF) + count(n-1, P)
ELSE 0 ENDIF)
MEASURE (LAMBDA n, (P: PRED[nat]): n)
G: VAR graph
size(G, n): nat = count(n, vertices(G))
\end{spec}
The function \verb|count| can be used to compute the cardinality of a set
when you know the cardinality is less than some value \verb|n|.
Alternatively one can assert the existence of such an \verb|n|, as
he does in the definition of \verb|contains_clique|
\begin{spec}
contains_clique(G, n): bool =
(EXISTS (C: set[nat]):
subset(C,vertices(G)) AND
(EXISTS m: count(m,C) >=n) AND
(FORALL i,j: i/=j AND C(i) AND C(j) IMPLIES edges(G)(i,j)))
\end{spec}
Using the recently developed finite sets
library\footnote{See appendix XXXXXXXXXXXXXX if you are unfamiliar
with it.}, this can be significantly
improved:
\begin{spec}
graph: TYPE = [# vertices : set[T],
edge?: (symmetric?[T]) #]
finite_graph: TYPE = {g: graph[T] | is_finite(vertices(g))}
size(GG: finite_graph): nat = card(vertices(GG))
\end{spec}
The type \verb|finite_graph| is a subtype of the parent \verb|graphs| type
where \verb|vertices| must satisfy the \verb|is_finite| predicate. This
allows us to use the cardinality function \verb|card|, defined in the
finite sets library. The function
\verb|contains_clique| can be defined as follows:
\begin{spec}
contains_clique(g, n): bool =
(EXISTS (C: finite_set[T]):
subset?(C,vertices(g)) AND card(C) >= n AND
(FORALL i,j: i/=j AND C(i) AND C(j) IMPLIES edge?(g)(i,j)))
\end{spec}
Note that there is no artificial existential quantifier.
Similarly,
\verb|contains_indep| can be defined as follows:
\begin{spec}
contains_indep(g, n): bool =
(EXISTS (D: finite_set[T]):
subset?(D, vertices(g)) AND card(D) >= n AND
(FORALL i, j: i/=j AND D(i) AND D(j) IMPLIES NOT edge?(g)(i, j)))
\end{spec}
Ramsey's theorem can now be expressed as follows:
\begin{spec}
ramseys_theorem: THEOREM (EXISTS (n: posnat):
(FORALL (G: Graph): size(G) >= n
IMPLIES (contains_clique(G, l1) OR
contains_indep(G, l2))))
\end{spec}
rather than
\begin{spec}
ramsey_thm: THEOREM
(FORALL p,q: p+q=i
IMPLIES
(FORALL (G: graph): (EXISTS m: size(G,m)>= ramsey(p,q))
IMPLIES (contains_clique(G, p) OR
contains_indep(G, q))))
\end{spec}
It should be noted that we have followed Shankar in defining the
\verb|edge?| relation over the entire range of the base type,
rather than just over the set of vertices. Experimentation
with
\begin{spec}
graph: TYPE = [# vertices : set[T],
edge?: (symmetric?[(vertices)]) #]
\end{spec}
showed that this is a much more complex and awkward structure
to work with. The only drawback of the first method is
that one must be careful not to construct the
set of edges of the graph as
\verb!{ \{v1,v2\} | edges(G)(v1,v2)}!. The set of edges
must be constructed by explicitly restricting the members of the set
to edges that are incident to vertices in the graph as follows:
\begin{spec}
\{ \{v1,v2\} | v1, v2 \( \in \) vertices(G) AND edges(G)(v1,v2) \}
\end{spec}
By supplying a function \verb|edge_set| defined as follows
\begin{spec}
in_vertices?(e,G): bool = (FORALL (x: T): e(x) IMPLIES vertices(G)(x))
is_edge?(G: graph, e: doubleton[T]): bool = in_vertices?(e,G) AND
edge?(G)(dbl_to_pair(e))
edge_set(G): set[doubleton[T]] = {e: doubleton[T] | is_edge?(G,e)}
\end{spec}
this problem should be avoidable. To demonstrate that this is a
viable strategy a theorem requiring induction on edges is developed
using this formalism in a subsequent section entitled
``Proof of a Theorem Concerning Edges and Degree''.
\section{Proof of Ramsey's Theorem}
In this section an outline of the proof in PVS will be presented.
To accomplish the proof by induction on the sum of $l_1$ and
$l_2$ the following lemma is first proved\footnote{Ramsey's
theorem follows trivially from this lemma by instantiation
of \verb|ii| with \verb|l1+l2|.}.
\begin{spec}
ramsey_lem: LEMMA (FORALL l1,l2: l1+l2=ii IMPLIES
(EXISTS (n: posnat):
(FORALL (G: Graph[T]): size(G) >= n
IMPLIES (contains_clique(G, l1) OR
contains_indep(G, l2)))))
\end{spec}
We issue \verb|(INDUCT "ii")| which produced two subgoals one for
the base case and one for the induction step. The base case
after \verb|SKOSIMP*| is
\begin{spec}
{-1} l1!1 + l2!1 = 0
|-------
{1} (EXISTS (n: posnat):
(FORALL (G: Graph[T]):
size(G) >= n
IMPLIES (contains_clique(G, l1!1) OR contains_indep(G, l2!1))))
\end{spec}
We instantiate with an uninterpreted function representing the Ramsey number:
\begin{spec}
Rule? (INST 1 "ramsey(l1!1,l2!1)")
ramsey_lem.1 :
[-1] l1!1 + l2!1 = 0
|-------
{1} (FORALL (G: Graph[T]):
size(G) >= ramsey(l1!1, l2!1)
IMPLIES (contains_clique(G, l1!1) OR contains_indep(G, l2!1)))
Rerunning step: (SKOSIMP*)
Repeatedly Skolemizing and flattening,
this simplifies to:
ramsey_lem.1 :
[-1] l1!1 + l2!1 = 0
{-2} size(G!1) >= ramsey(l1!1, l2!1)
|-------
{1} contains_clique(G!1, l1!1)
{2} contains_indep(G!1, l2!1)
\end{spec}
\begin{spec}
Rerunning step: (EXPAND "contains_clique")
Expanding the definition of contains_clique,
this simplifies to:
ramsey_lem.1 :
[-1] l1!1 + l2!1 = 0
[-2] size(G!1) >= ramsey(l1!1, l2!1)
|-------
{1} (EXISTS (C: finite_set[T]):
subset?(C, vertices(G!1))
AND card(C) >= l1!1
AND
(FORALL (i: T), (j: T):
i /= j AND C(i) AND C(j) IMPLIES edge?(G!1)(i, j)))
[2] contains_indep(G!1, l2!1)
Rerunning step: (INST 1 "emptyset[T]")
Instantiating the top quantifier in 1 with the terms:
emptyset[T],
this yields 2 subgoals:
ramsey_lem.1.1 :
[-1] l1!1 + l2!1 = 0
[-2] size(G!1) >= ramsey(l1!1, l2!1)
|-------
{1} subset?(emptyset[T], vertices(G!1))
AND card(emptyset[T]) >= l1!1
AND
(FORALL (i: T), (j: T):
i /= j AND emptyset[T](i) AND emptyset[T](j)
IMPLIES edge?(G!1)(i, j))
[2] contains_indep(G!1, l2!1)
\end{spec}
then finish off with \verb|GRIND|.
The induction step after \verb|SKOSIMP*| is
\begin{spec}
{-1} (FORALL (l1: nat), (l2: nat):
l1 + l2 = j!1
IMPLIES
(EXISTS (n: posnat):
(FORALL (G: Graph[T]):
size(G) >= n
IMPLIES
(contains_clique(G, l1) OR contains_indep(G, l2)))))
{-2} l1!1 + l2!1 = j!1 + 1
|-------
{1} (EXISTS (n: posnat):
(FORALL (G: Graph[T]):
size(G) >= n
IMPLIES (contains_clique(G, l1!1) OR contains_indep(G, l2!1))))
\end{spec}
After dealing with two trivial cases (i.e., \verb|l2!1 = 0| and \verb|l1!1 = 0|)
\begin{spec}
[-1] (FORALL (l1: nat), (l2: nat):
l1 + l2 = j!1
IMPLIES
(EXISTS (n: posnat):
(FORALL (G: Graph[T]):
size(G) >= n
IMPLIES
(contains_clique(G, l1) OR contains_indep(G, l2)))))
[-2] l1!1 + l2!1 = j!1 + 1
|-------
{1} l2!1 = 0
[2] l1!1 = 0
[3] (EXISTS (n: posnat):
(FORALL (G: Graph[T]):
size(G) >= n
IMPLIES (contains_clique(G, l1!1) OR contains_indep(G, l2!1))))
\end{spec}
\begin{spec}
Rule? (INST-CP -1 "l1!1" "l2!1-1")
(INST -1 "l1!1-1" "l2!1")
(ASSERT)
(SKOSIMP*)
ramsey_lem.2.2.2.1.1 :
{-1} (FORALL (G: Graph[T]):
size(G) >= n!1
IMPLIES (contains_clique(G, l1!1 - 1) OR contains_indep(G, l2!1)))
{-2} (FORALL (G: Graph[T]):
size(G) >= n!2
IMPLIES (contains_clique(G, l1!1) OR contains_indep(G, l2!1 - 1)))
[-3] l1!1 + l2!1 = 1 + j!1
|-------
[1] l2!1 = 0
[2] l1!1 = 0
[3] (EXISTS (n: posnat):
(FORALL (G: Graph[T]):
size(G) >= n
IMPLIES (contains_clique(G, l1!1) OR contains_indep(G, l2!1))))
\end{spec}
The suitable \verb|n| is \verb|"n!1+n!2|:
\begin{spec}
Rule? (INST 3 "n!1+n!2")
(SKOSIMP*)
[-1] (FORALL (G: Graph[T]):
size(G) >= n!1
IMPLIES (contains_clique(G, l1!1 - 1) OR contains_indep(G, l2!1)))
[-2] (FORALL (G: Graph[T]):
size(G) >= n!2
IMPLIES (contains_clique(G, l1!1) OR contains_indep(G, l2!1 - 1)))
[-3] l1!1 + l2!1 = 1 + j!1
{-4} size(G!1) >= n!1 + n!2
|-------
[1] l2!1 = 0
[2] l1!1 = 0
{3} contains_clique(G!1, l1!1)
{4} contains_indep(G!1, l2!1)
\end{spec}
\begin{spec}
Rerunning step: (LEMMA "card_r1_r2")
(INST?)
(ASSERT)
ramsey_lem.2.2.2.1.1 :
[-1] card(r1(G!1)) + card(r2(G!1)) >= size(G!1) - 1
[-2] (FORALL (G: Graph[T]):
size(G) >= n!1
IMPLIES (contains_clique(G, l1!1 - 1) OR contains_indep(G, l2!1)))
[-3] (FORALL (G: Graph[T]):
size(G) >= n!2
IMPLIES (contains_clique(G, l1!1) OR contains_indep(G, l2!1 - 1)))
[-4] l1!1 + l2!1 = 1 + j!1
[-5] size(G!1) >= n!1 + n!2
|-------
[1] l2!1 = 0
[2] l1!1 = 0
[3] contains_clique(G!1, l1!1)
[4] contains_indep(G!1, l2!1)
\end{spec}
\begin{spec}
Rerunning step: (CASE "card(r1(G!1)) >= n!1")
Rerunning step: (INST -3 "SG1(G!1)")
Rerunning step: (EXPAND "size")
ramsey_lem.2.2.2.1.1.1.1 :
[-1] card(r1(G!1)) >= n!1
{-2} (card(r1(G!1)) + card(r2(G!1)) >= (card(vertices(G!1)) - 1))
{-3} ((card(vertices(SG1(G!1))) >= n!1)
IMPLIES
(contains_clique(SG1(G!1), l1!1 - 1)
OR contains_indep(SG1(G!1), l2!1)))
{-4} (FORALL (G: Graph[T]):
((card(vertices(G)) >= n!2)
IMPLIES
(contains_clique(G, l1!1) OR contains_indep(G, l2!1 - 1))))
[-5] l1!1 + l2!1 = 1 + j!1
{-6} (card(vertices(G!1)) >= n!1 + n!2)
|-------
[1] l2!1 = 0
[2] l1!1 = 0
[3] contains_clique(G!1, l1!1)
[4] contains_indep(G!1, l2!1)
\end{spec}
\begin{spec}
Rerunning step: (SPLIT -3)
Rerunning step: (NAME "Vo" "choose(vertices(G!1))")
Rerunning step: (CASE "contains_clique(subgraph(G!1,add(Vo,
vertices(SG1(G!1)))), l1!1)")
Splitting conjunctions,
this yields 3 subgoals:
Case splitting on
contains_clique(subgraph(G!1,add(Vo,
vertices(SG1(G!1)))), l1!1),
this yields 2 subgoals:
ramsey_lem.2.2.2.1.1.1.1.1.1 :
{-1} contains_clique(subgraph(G!1, add(Vo, vertices(SG1(G!1)))), l1!1)
[-2] choose(vertices(G!1)) = Vo
[-3] contains_clique(SG1(G!1), l1!1 - 1)
|-------
[1] l2!1 = 0
[2] l1!1 = 0
[3] contains_clique(G!1, l1!1)
\end{spec}
************* FINISH PROOF *************8
\section{Proof of a Theorem Concerning Edges and Degree}
In this section the robustness of our graph definition is explored
through proof of a theorem quite different from Ramsey's:
\noindent
{\em Theorem} The sum of the degrees of the vertices of a graph equals
two times the number of edges.
Before we can state this in PVS we must formalize the notion of
degree
\begin{spec}
edges_on_vertex(v,G) : finite_set[doubleton[T]]
= {e: edges_type(G) | member(v,e)}
degree(v,G): nat = card(edges_on_vertex(v,G))
\end{spec}
The function \verb|edges_on_vertex(v,G)| returns the set of edges
incident on vertex \verb|v| and \verb|degree| is simply defined as the
cardinality of this set.
The theorem can then be formally stated as follows
\begin{spec}
degree_thm: THEOREM sum(vertices(G), (LAMBDA (v: T): degree(v,G))) =
2 * num_edges(G)
\end{spec}
where \verb|sum| is defined in the finite sets library (see theorey
\verb|finite_sets_sum_real|.pvs) as
\begin{spec}
sum(S,f) : RECURSIVE real =
IF (empty?(S)) THEN 0
ELSE f(choose(S)) + sum(rest(S),f)
ENDIF MEASURE (LAMBDA S,f: card(S))
\end{spec}
and \verb|num_edges| is
\begin{spec}
num_edges(G): nat = card(edge_set(G))
\end{spec}
The proof of this theorem is accomplished by induction on the number of edges.
\appendix
\section{A Rapid Introduction to the PVS Finite Sets Library}
NOTE. Finite sets are a special kind of set which are defined in a PVS library.
Sets in PVS are similar to sets in Ehdm. Sets are defined in the PVS prelude
(A bunch of definitions/lemmas globally available) as:
\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)
empty?(a): bool = (FORALL x: NOT member(x, a))
emptyset: set = {x | false}
nonempty?(a): bool = NOT empty?(a)
fullset: set = {x | true}
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)}
% A choice function for nonempty sets
choose(p: (nonempty?)): (p) = epsilon(p)
rest(a): set = IF empty?(a) THEN a ELSE remove(choose(a), a) ENDIF
END sets
\end{spec}
A set is just a boolean-values function of the TYPE (in PVS the
keyword FUNCTION is optional so "function [T -> bool]" can be
abbreviated as "[T -> bool]"). The function is only true for members
of the set (i.e., a kind of characteristic function). All of the
usual operators are available including "choose" which is defined
using Hilbert's epsilon operator. It returns an arbitrary member of
the set satisfying the given predicate.
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 = (is_finite) CONTAINING emptyset[T]
\end{spec}
Thus to demonstrate that a set is finite, an injective function from
the set into [0,N] must be exhibited. The "card" function is available
for finite sets:
\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 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}
\section{Alternate Definition of Graph and Implications/Tradeoffs}
\begin{spec}
graph: TYPE = [# vertices : set[T],
edges: set[doubleton[T]] #]
\end{spec}
\bibliographystyle{/home/rwb/bib/NASA}
\bibliography{/home/rwb/bib/database}
\end{document}