From ab8df8880bcb1745ef7cc0664280ce2d36dfe5a0 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 29 Jun 2018 21:47:26 0400
Subject: [PATCH] books/bookvol13 add additional ideas to explore
Goal: Proving Axiom Sane

books/bookvol13.pamphlet  1142 +++++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  4 +
src/axiomwebsite/patches.html  2 +
4 files changed, 1122 insertions(+), 28 deletions()
diff git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 6ad3f57..f367e6d 100644
 a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ 2,6 +2,7 @@
\newcommand{\VolumeName}{Volume 13: Proving Axiom Correct}
\usepackage{bbold}
\usepackage{amsmath}
+\usepackage{turnstile}
\input{bookheader.tex}
\mainmatter
\setcounter{chapter}{0} % Chapter 1
@@ 17,6 +18,33 @@ automating the process. Automated machine proofs are not possible
in general but will exist for known algorithms.
\begin{quote}
+{\bf This is an exercise in Omphaloskepsis}\\
+ Tim Daly
+\end{quote}
+
+\begin{quote}
+{\bf Coq is the tactical nuclear weapons of programming. You need to be
+quite clever to use them. And indeed, when people first start to use
+them you don't hear from them for two years, they sort of 'go dark'
+and then they emerge with all their pain receptors destroyed and they
+say Coq the only way to live, to do everything in Coq. "I don't write
+programs anymore, I just write Coq proofs"}\\
+ Simon PeytonJones \cite{Peyt17}
+\end{quote}
+
+\begin{quote}
+{\bf It is an intrinsic part of the duty of everyone who professes to
+compose algorithms to supply a proof that his text indeed represents a
+proper algorithm.}\\
+ Edsgar Dijkstra \cite{Dijk71}
+\end{quote}
+
+\begin{quote}
+{\bf If what you are working on is not important, why are you working on it?}\\
+ Richard Hamming \cite{Hamm95}
+\end{quote}
+
+\begin{quote}
{\bf Q: Why bother doing proofs about programming languages? They are almost
always boring if the definitions are right.}
@@ 24,6 +52,15 @@ always boring if the definitions are right.}
\end{quote}
\begin{quote}
+{\bf The Misfortunes of a Trio of Mathematicians Using Computer Algebra
+Systems: Can We Trust In Them?}\\
+ Dur{\'a}n, P{\'e}rez, and Varona \cite{Dura14}\\
+{\bf Certainly not.}  Tim Daly\\
+{\bf Yeah, well, that's just, like, your opinion, man}\\
+ Jeff Bridges, The Big Lebowski
+\end{quote}
+
+\begin{quote}
{\bf If programming is understood not as the writing of instructions for
this or that computing machine but as the design of methods of
computation that it is the computer's duty to execute, then it no
@@ 168,6 +205,38 @@ math and the code.}\\
\chapter{Why this effort will not succeed}
+\begin{quote}
+When something is important enough, you do it even if the odds
+are not in your favor.\\
+ Elon Musk
+\end{quote}
+
+\begin{quote}
+{\bf The ancient Greeks gave (western) civilization quite a few
+gifts, but we should beware of Greeks bearing gifts. The gifts of theatre
+and democracy were definitely good ones, and perhaps even the gift of
+philosophy, but the 'gift' of the socalled 'axiomatic method' and the
+notion of 'rigorous' proof did much more harm than good. If we want
+to maximize Mathematical Knowledge, and its Management, we have to
+return to Euclid this dubious gift, and giveup our fanatical insistence
+on perfect rigor. Of course, we should not go to the other extreme, of
+demanding that everything should be nonrigorous. We should encourage
+diversity of proofstyles and rigor levels, and remember that nothing is
+absolutely sure in this world, and there does not exist an absolutely
+rigorous proof, nor absolute certainty, and 'truth' has many shades and
+levels.}\\
+ Doron Zeilberger \cite{Zeil10}
+\end{quote}
+
+\begin{quote}
+{\bf The thing that differentiates scientist is purely an artistic
+ability to discern what is a good idea, what is a beautiful idea, what
+is worth spending time on, and most importantly, what is a problem
+that is sufficiently interesting, yet sufficiently difficult, that it
+hasn't yet been solved, but the time for solving it has come now.}\\
+ Savas Dimopoulos; Stanford University
+\end{quote}
+
This is an effort to prove Axiom correct. That is, we wish to prove
that the algorithms provide correct, trustworthy answers.
@@ 431,6 +500,17 @@ proofs which were checked algorithmically.
\chapter{Here is a problem}
+\begin{quote}
+The world needs both logicians and verifiers, and we need one
+another. Logicians need verifiers to keep their work relevant, and
+verifiers need logicians to keep them honest. (In typical human
+fashion, most logicians think they know all they need to about real
+verification problems for developing theories, and most verifiers
+think they know enough about logic to verify programs. They're
+probably both wrong.)\\
+ Lamport and Owicki \cite{Lamp81}
+\end{quote}
+
Axiom has a domainspecific language for mathematical computation
called Spad. This is implemented in Common Lisp. Our version of
Common Lisp compiles to C. The C code is then compiled to machine
@@ 449,11 +529,148 @@ is sufficient to show that the compile step is correct.
\subsection{Defining the Spad syntax}
\subsection{Defining the Spad semantics}
+Gordon \cite{Gord89} describes formal reasoning about programs that
+can be based directly on the semantics of the programming language, or
+done in a special purpose logic like Hoare logic.
+
+O'Donnell \cite{Odon81} raises questions about the logical soundness
+of rules used in Hoare logic reasoning.
+
+Manna and Waldinger \cite{Mann78a} introduce the notion of
+{\sl sometime} as a conditional invariant that sometimes is true.
+
Floyd \cite{Floy67}, Back \cite{Back81}, Caldwell \cite{Cald97},
Filliatre \cite{Fill03}, Filliatre and Paskevich \cite{Fill13}
+\subsection{Type Resolution}
+
+In Kaes \cite{Kaes88} we find that there is a semantical difference
+between overloading and polymorphism: in the case of the overloaded
+$+$ operator, we would expect different code to be executed for
+integer and real addition respectively, whereas we expect the code of
+$len$ to be usable for lists of any type. This distinction has led to
+the name ``adhoc polymorphism''.
+
+{\bf Parametric Polymorphism}: One semantic object can have different
+types at each usage, all being instances of a single type expression
+over variables.
+
+{\bf Overloading} (``adhoc polymorphism''): A single name can be used
+to denote different semantic objects, the types of these objects being
+completely unrelated.
+
+{\bf Parametric Overloading}: A single name can be used to denote
+several objects, the types of these objects being instances of a
+single type expression over some extended set of type variables.
+
+Cardelli and Wegner \cite{Card85} refines Strachey by introducing a
+new form of polymorphism called {\sl inclusion polymorphism} to model
+subtypes and inheritance. Parametric and inclusion polymorphism are
+classified as the two major subcategories of ``universal
+polymorphism'' which is contrasted with nonuniversal or adhoc
+polymorphism.
+\begin{verbatim}
+  parametric
+  universal 
+   inclusion
+ polymorphism 
+   overloading
+  ad hoc 
+  coercion
+\end{verbatim}
+
+Parametric polymorphism is so called because the uniformity of type
+structure is normally achieved by type parameters, but uniformity can
+be achieved in different ways, and this more general concept is called
+{\sl universal polymorphism}. Universally polymorphic functions will
+normally work on an infinite number of types (all the types having a
+given common structure), whereas an adhoc polymorphic function will
+only work on a finite set of different and potentially unrelated
+types.
+
+In {\sl parametric polymorphism}, a polymorphic function has an
+implicit or explicit type parameter which determines the type of the
+argument for each application of that function. In {\sl inclusion
+polymorphism} an object can be viewed as belonging to many different
+classes that need not be disjoint; that is, there may be inclusion of
+classes.
+
+There are at least 4 kinds of escapes from a monomorphic type.
+\begin{itemize}
+\item {\sl Overloading}: Integer constants may have both type integer
+and real.
+\item {\sl Coercion}: An integer value can be used where a real is
+expected, and vice versa.
+\item {\sl Subtyping}: Elements of a subrange type also belong to
+superrange types.
+\item {\sl Value Sharing}: {\tt nil} in Pascal is a constant that is
+shared by all the pointer types.
+\end{itemize}
+
+Wadler and Blott \cite{Wadl88} point out that it would be nice if
+polymorphic equality could be extended to include userdefined
+equality operations over abstract types. To implement this, we would
+need to require that every object carry with it a pointer to a
+{\sl method}, a procedure for performing the equality test. If we are
+to have more than one operation with this property, then each object
+should carry with it a pointer to a {\sl dictionary} of appropriate
+methods.
+
+In the case of polymorphic equality, this means that {\sl both}
+arguments of the equality function will contain a pointer to the same
+dictionary (since they are both of the same type). This suggests that
+perhaps dictionaries should be passed around independently of objects,
+now polymorphic equality would be passed one dictionary and two
+objects (minus dictionaries). This is the intuition behind type
+classes and the translation method they describe.
+
+It is natural to think of adding assertions to the class declaration,
+specifying properties that each instance must satisfy:
+\begin{verbatim}
+ class EQ a where
+ (==) :: a > a > Bool
+ % (==) is an equivalence relation
+
+ class Num a where
+ zero, one :: a
+ (+), (*) :: a > a > a
+ negate :: a > a
+ % (zero, one, (+), (*), negate) form a ring
+
+\end{verbatim}
+
+It is valid for any proof to rely on these properties, so long as one
+proves that they hold for each instance declaration. Here the
+assertions have simply been written as comments; a more sophisticated
+system could perhaps verify or use such assertions.
+
+It is reasonable to allow a class to apply to more than one type
+variable. For instance, we might have
+\begin{verbatim}
+ class Coerce a b where
+ coerce :: a > b
+
+ instance Coerce Int Float where
+ coerce  convertIntToFloat
+
+\end{verbatim}
+
+In this case, the assertion {\tt Coerce a b} might be taken as
+equivalent to the assertion that {\tt a} is a subtype of {\tt b}. This
+suggests a relation between this work and work on bounded
+quantification and on subtypes.
+
\section{Proving the Logic}
+Soundness has two aspects, closed world and open world. \cite{Bonn18}
+
+Closed world soundness assumes all progremas are type checked by the
+same type system. Open world soundness not only require closed world
+soundness, but also that the guarantees upheld under closed world
+assumptions cannot be broken by foreign code. The introduction and
+consideration of foreign code is the essential difference between
+openworld and closed world soundness. See gradualtyping.
+
Proving programs correct involves working with a second programming
language, the proof language, that is wellfounded on some theory.
Proofs (programs), can be reduced (compiled) in this new language
@@ 465,17 +682,114 @@ the proof language. Unfortunately that is not (yet?) the case with Spad.
The COQ system language, Gallina, is the closest match to Spad.
+Barras and Werner \cite{Barr18} formalize the definition and the
+metatheory of the Calculus of Constructions (CC) using the proof
+assistant Coq. In particular, we prove strong normalization and
+decidability of type inference. From the latter proof, we extract
+a certified Objective Caml program which performs type inference
+in CC and use this code to build a smallscale certified proofchecker.
+
+Gordon \cite{Gord89} derives the rules of Hoare logic
+{\sl mechanically} from the semantics of a simple imperative
+programming language.
+
+Igarashi et al. \cite{Igar75}
+defined a program to compute the
+subgoals from a program and its postcondition.
+
+Katz and Manna \cite{Katz75} look at various methods of proving
+termination including
+\begin{itemize}
+\item using the 'noinfinitelydescendingchain property of
+wellfounded sets (Floyd's approach)
+\item bounding a counter associated with each loop ({\sl loop}
+approach)
+\item showing that some exit of each loop must be taken ({\sl exit}
+approach)
+\item inducting on the structure of the data domain (Burstall's
+approach)
+\end{itemize}
Davis \cite{Davi09},
Myreen and Davis \cite{Myre11}, Myreen and Davis \cite{Myre14},
Davis and Myreen \cite{Davi15}
+\subsection{Typing and Subtyping}
+
+Dolan's PhD Thesis \cite{Dola16} on Algebraic Subtyping.
+Henri Tuhola \cite{Tuho18} notes that
+solving the problem of subtyping does not directly solve the problem
+of coercion. Coercion extends the type and doesn't narrow it.
+
+Dolan and Mycroft \cite{Dola17} note that, given
+\begin{verbatim}
+ select p v d = if (p v) then v else d
+\end{verbatim}
+only by ignoring the
+orientation of the data flows could we conclude that $d$'s type flows
+to the argument of $p$, even though $p$ never mentions $d$. ML's type
+inference turns data flows into equality constraints between types so
+information about the {\sl direction} of data flow is ignored. Since
+equality is symmetric, data flow is treated as unidirectional. But
+support for subtyping cares about the direction of data flow. With
+subtyping, a source of data must provide at least the guarantees that
+the destination requires, but is free to provide more.
+
\subsection{Defining the Algebra specifications}
Talpin and Jouvelot \cite{Talp92}
+\subsection{Termination}
+
+Hughes \cite{Hugh90} talks about a lazy approach to termination, while
+gluing programs together. Functional languages allow whole progams to
+be glued together. A complete functional program is just a function
+from its inputs to its output. If $f$ and $g$ are such programs, then
+$(g \cdot f)$ is a program that, when applied to its input, computes
+\[g (f {\rm\ input})\]
+The program $f$ computes its output, which is used as the input to
+program $g$. This might be implemented conventionally by storing the
+output from $f$ in a temporary file. The problem with this is that the
+temporary file might occupy so much memory that it is impractical to
+glue the programs together in this way. Functional languages provde a
+solution to this problem. The two programs $f$ and $g$ are run
+together in strict synchronization. Program $f$ is started only when
+$g$ is trying to read. Then $f$ is suspended and $g$ is run until it
+ties to read another input. As an added bonus, if $g$ terminates
+without reading all of $f$'s output, then $f$ is aborted. Program $f$
+can even be a nonterminating program, producing an infinite amount of
+output, since it will be terminated forcibly as soon as $g$ is
+finished. This allows termination conditions to be separated from loop
+bodies  a powerful modularization.
+
+Since this method of evaluation runs $f$ as little as possible, it is
+called ``lazy evaluation''. It makes it practical to modularize a
+program as a generator that constructs a large number of possible
+answers, and a selector that chooses the appropriate one.
+
+{\bf IDEA:} write (lazy $f$) for nonterminating programs to simplify
+proofs.
+
+Sites \cite{Site74} offers some thoughts on proving clean termination
+of programs.
+
+Katz and Manna \cite{Katz75} take a closer look at termination.
+
\section{Proving the Lisp}
+Guttman, et al. \cite{Gutt95} in the VL!SP project showed how to
+produce a comprehensively verified implementation for a
+programming language, namely Scheme.
+
+Leroy \cite{Lero09} describes the development and formal verification
+(proof of semantic preservation) of a compiler backend from Cminor
+(a simple imperative intermediate language) to PowerPC assembly code,
+using the Coq proof assistant.
+
+Manolios and Moore \cite{Mano03} describe a method for introducing
+'partial functions' in to ACL2. This is necessary for Common Lisp
+as most functions are not total.
+
Myreen \cite{Myre12}
\section{Proving the Compiler}
@@ 484,8 +798,17 @@ Myreen \cite{Myre10}
\section{Proving to the metal}
Myreen and Gordon \cite{Myre09}, Myreen, Slind, and Gordon \cite{Myre09a}
+Myreen, Slind, and Gordon \cite{Myre09a} presents a compiler which
+produces machine code from functions defined in the logic of a theorem
+prover, and at the same time proves that the generated code executes
+the source functions.
+Myreen and Gordon \cite{Myre09},
+
+Gordon, et al. \cite{Gord06} describes a compiler that automatically
+translates recursive function definitions in higher order logic to
+clocked synchronous hardware Compilation is by mechanised proof in
+the HOL4 system. In particular, this models functions as circuits.
Domipheus \cite{Domi18} provides a VHDL (hardware description language)
CPU which provides the actual electrical timing of signals all the way
@@ 956,6 +1279,171 @@ d & = & ra+sb
\end{array}
\]
+\chapter{GCD in Miranda by Broda, et al.}
+
+In Broda, et al. \cite[p. 55]{Brod94} they consider the greatest
+common divisor, {\tt gcd}, of two natural numbers:
+\begin{verbatim}
+ gcd :: num > num > num
+ pre: nat(x) & nat(y)
+ post: nat(z) & zx & zy (ie z is a common divisor)
+  &(A)n:nat(nx & ny > nz)
+  (ie any other common divisor divides it)
+  where z = (gcd x y)
+\end{verbatim}
+
+We have introduced some notation in the pre and postconditions:
+\begin{itemize}
+\item (A) just means $\forall$, that is 'for all', written in standard
+keyboard characters. $\exists$ would be (E).
+\item $$ means 'divides', or 'is a factor of'. (Note that it is not
+the same symbol as the division sign '$/$'.)
+\[z~~x \Leftrightarrow \exists y: nat. (x=z \times y)\]
+\item When we write '$y:nat$', we are using the predicate $nat$ as
+though it were a Miranda type, though it is not. You can think of
+'$nat(y)$' and '$y:nat$' as meaning exactly the same, namely that $y$
+is a natural number. But the typestyle notation is particularly
+useful with quantifiers:
+\[\begin{array}{lr}
+\exists y : nat, P & {\rm means\ }\exists y. (nat(y) \land P)\\
+&({\rm 'there\ is\ a\ natural\ number\ } y {\rm\ for\ which\ }
+P {\rm\ holds}')\\
+\forall y : nat, P & {\rm means\ }\forall y. (nat(y) \implies P)\\
+&({\rm 'for\ all\ natural\ numbers\ } y, P {\rm\ holds}')\\
+\end{array}\]
+\end{itemize}
+
+Be sure to understnad these, and in particular why it is that
+$\exists$ goes naturally with $\land$, and $\forall$ with
+$\implies$. They are patterns that arise very frequently when you are
+translating from English into logic.
+
+There is a small unexpected feature. You might expect the
+postcondition to say that any other common divisor is {\sl less} than
+$z$, rather than dividing it: in other words that $z$ is indeed the
+{\sl greatest} common divisor. There is just a single case where this
+makes a difference, namely when $x$ and $y$ are both 0. All numbers
+divide 0, so amongst the common divisors of $x$ and $y$ there is no
+greatest one. The specification as given has the effect of specifying
+\begin{verbatim}
+ gcd 0 0 = 0
+\end{verbatim}
+
+{\bf Proposition 1}: For any two natural numbers $x$ and $y$, there is
+at most one $z$ satifying the specification for $(gcd x y)$.
+
+{\bf Proof}: Lex $z1$ and $z2$ be two values satisfying the
+specification for $(gcd x y)$; we must show that they are equal. All
+common divisors of $x$ and $y$ divide $z2$, so, in particular, $z1$
+does. Similiarly, $z2$ divides $z1$. Hence for some positive natural
+numbers $p$ and $q$, we have $z1=z2 \times p$, $z2=z1 \times q$, so
+$z1 = z1 \times p \times q$. It follow that either $z1 = 0$, in which
+case also $z2=0$, or $p\times q=1$, in which case $p=q=1$. In either
+case, $z1=z2$.
+
+Note that we have not actually proved that there is {\sl any} value
+$z$ satisfying the specification; only that there cannot be more than
+one. But we shall soon have an implementation showing how to find a
+suitable $z$, so then we shall know that there is exactly one possible
+result.
+
+{\sl Euclid's algorithm} relies on the following fact.
+
+{\bf Proposition 2}: Let $x$ and $y$ be natural numbers, $y\ne
+0$. Then the common divisors of $x$ and $y$ are the same as those of
+$y$ and $(x{\rm\ mod\ }y)$.
+
+{\bf Proof}: For natural numbers $x$ and $y$ there are two fundamental
+properties of integer division, which in fact are enough to specify it
+uniquely: if $y\ne 0$ (precondition), the (postcondition)
+\[x=u\times (x{\rm\ div\ }y) + (x{\rm\ mod\ }y)\]
+\[0 \le (x{\rm\ mod\ }y) < y\]
+Suppose $n$ is a common divisor of $y$ and $(x{\rm\ mod\ y}y)$. That
+is, there is a $p$ such that $y=n\times p$ and a $q$ such that
+$(x{\rm\ mod\ }y)=n\times q$. Then
+\[x=y\times(x{\rm\ div\ }y)+(x{\rm\ mod\ }y)=
+n\times (p\times (x{\rm\ div\ }y)+q)\]
+so $n$ also divides $z$. Hence every common divisor of $y$ and
+$(x{\rm\ mod\ }y)$ is also a common divisor of $x$ and $y$. The
+converse is also true, by a similar proof. $\quad\blacksquare$
+
+It follows that, provided $y\ne 0$, $(gcd x y)$ must equal
+$(gcd y (x{\rm\ mod\ }y))$. On the other hand, $(gcd x 0)$ must be
+$x$. This is because $x~~x$ and $x~~0$, and any common divisor of
+$x$ and 0 obviously divides $x$, so $x$ satisfies the specification
+for $(gcd x 0)$. We can therefore write the following definition:
+\[\begin{array}{rcl}
+gcd x y & = x & {\rm if\ }y=0\\
+ & = gcd y (x {\rm\ mod\ } y) & {\rm otherwise}
+\end{array}\]
+
+{\tt Question}: Does this definition satisfy the specification?
+
+Let $x$ and $y$ be natural numbers, and let $z=(gcd x y)$. We must
+show that $z$ has the properties given by the postcondition, and
+there are two cases corresponding to the two clauses in the
+definition:
+
+$y=0 : z = x$ We have already noted that this satisfies the
+specification.
+
+$y\ne 0 : z = (gcd y (x{\rm\ mod\ }y))$ What we have seen shows that
+{\sl provided that z} satisfies the specification for
+$(gcd y (x{\rm\ mod\ }y))$, then it also satisfies the specification
+for $(gcd x y)$ as required. $\quad\blacksquare$
+
+But how do we know that the recursive call gives the right answer? How
+do we know that it gives any answer at all? (conceivably, the
+recursion might never bottom out.) Apparently, we have having to
+{\sl assume} that {\tt gcd} satisfies its specification in order to
+{\sl prove} that it satisfies its specification.
+
+The answer is that we {\sl are} allowed to assume it! But there is a
+catch. This apparently miraculous circular reasoning must be
+justified, and the key is to notice that the recursive call uses
+simpler arguments: the pair of arguments $y$ with $x{\rm\ mod\ }y)$ is
+'simpler' than the pair $x$ and $y$, in the sense that the second
+argument is smaller: $x{\rm\ mod\ }y < y$.
+
+As we go down the recursion, the second argument, always a natural
+number, becomes smaller and smaller, but never negative. This cannot
+go on for ever, so the recursion must eventually terminate. This at
+least proves termination, but it also justifies the
+{\sl circular reasoning}. For suppose that {\tt gcd} does not always
+work correctly. What might be the smallest bad $y$ for which
+$gcd x y$ may go wrong (for some $x$)? Not 0  gcd x 0 always works
+correctly. Suppose $Y$ is the smallest bad $y$, and $gcd X Y$ goes
+wrong. Then $Y > 0$, so
+\begin{verbatim}
+ gcd X Y = gcd Y (X mod Y)
+\end{verbatim}
+But $X{\rm\ mod\ }Y$ is good (since $X{\rm\ mod\ }Y < Y$), so the
+recursive call works correctly, so (we have already reasoned)
+$gcd X Y$ does also  a contradiction.
+
+We call the value $y$ in $gcd x y$ a {\sl recursion variant} for our
+definition of {\tt gcd}. It is a rough measure of the depth of
+recursion needed, and always decreases in the recursive calls.
+
+Let us now state this as a reasoning principle:
+\begin{verbatim}
+ In proving that a recursive function satisfies its specificaiton,
+ you are allowed to assume that the recursive calls work correclty
+  provided that you can define a recursion variant for the function.
+\end{verbatim}
+
+A recursion variant for a function must obey the following rules:
+\begin{itemize}
+\item It is calculated from the arguments of the function
+\item It is a natural number (at least when the preconditions of the
+function hold). For instances, in {\tt gcd} the recursion variant of $y$.
+\item It is calculated (trivially) from the function's arguments
+$x$ and $y$)
+\item It always decreases in the recursive calls. For the recursive
+call $gcd y (x{\rm\ mod\ }y)$, the recursion variant $x{\rm\ mod\ }y$
+is less than $y$, the variant for $gcd x y$.
+\end{itemize}
+
\chapter{GCD in Nuprl by Anne Trostle}
Quoted from \cite{Tros13}:
@@ 3336,31 +3824,87 @@ Proof.\\
End gcd.\\
\chapter{Other Ideas to Explore}
Computerising Mathematical Text \cite{Kama15} explores various ways of
capturing mathematical reasoning.

Chlipala \cite{Chli15} gives a pragmatic approach to COQ.
MedinaBulo et al. \cite{Bulo04} gives a formal verification of
Buchberger's algorithm using ACL2 and Common Lisp.

Th\'ery \cite{Ther01} used COQ to check an implementation of Buchberger's
algorithm.

Pierce \cite{Pier15} has a Software Foundations course in COQ with
downloaded files in Pier15.tgz.

Spitters \cite{Spit11} Type Classes for Mathematics in Coq. Also see
\verbhttp://www.eelis.net/research/mathclasses/

Mahboubi \cite{Mahb16} Mathematical Components. This book contains a
proof of the Euclidean algorithm using COQ.

Aczel \cite{Acze13} Homotopy Type Theory

Santas \cite{Sant95} A Type System for Computer Algebra
+\section{Aczel \cite{Acze13}}
+Homotopy Type Theory
+
+\section{Chlipala \cite{Chli15}}
+gives a pragmatic approach to COQ.
+
+\section{Dijkstra \cite{Dijk72a}}
+
+Unlike later texts, Dijkstra does not require a descreasing value to
+do induction. Instead, he says
+
+Let us consider the sequence of values
+\[d_0,d_1,d_2,d_3,\ldots\eqno{1}\]
+given by
+\[{\rm for\ }i=0 d_i=D\eqno{2a}\]
+\[{\rm for\ }i>0 d_i=f(d_{i1}\eqno{2b}\]
+where $D$ is a given value and $f$ a given (computable) function. It
+is asked to make the value of the variable ``$d$'' equal to the first
+value $d_k$ in the sequence that satisfies a given (computable)
+condition ``prop''. It is given that such a value exists for finite
+$k$. A more formal definition of the requirement is to establish the
+relation
+\[d=d_k\eqno{3}\]
+where $k$ is given by the (truth of the) expressions
+\[prop(d_k)\eqno{4}\]
+and
+\[{\rm {\bf non}\ prop} (d_i){\rm\ for\ all\ }i{\rm\ satisfying\ }
+0 \le i < k\eqno{5}\]
Homann \cite{Homa94} algorithm schemata
+We now consider the following program part:
+\[\begin{array}{l}
+``d:=D ;\\
+{\rm {\bf\ while\ non}\ prop} (d){\rm\ do\ }d:=f(d)\\
+\end{array}\]
+in which the first line represents the initialization and the second
+one the loop, controlled by the (hopefully selfexplanatory)
+repetition {\bf while...do}.
+
+A more formal definition of the semantics of the repetition clause is
+by stating that
+\[``{\bf while\ }B{\bf\ do\ }S''\]
+is semantically equivalent with
+\[``{\bf if\ }B{\bf\ do\ begin\ }S;{\bf\ while\ }B{\bf\ do\ }S{\bf\
+end}''\]
+expressing that ``{\bf non} B'' is the necessary and sufficient
+condition for the repetition to terminate.)
+
+\section{Feferman \cite{Fefe95}}
+
+Questions of definedness are ubiquitous in mathematics. Informally,
+these involve reasoning about expressions which may or may not have a
+value. This paper surveys work on logics in which such reasoning can
+be carried out directly, especially in conputational contexts. It
+begins with a general logic of ``partial terms'', continues with
+partial combinatory and lambda calculi, and concludes with an
+expressively right theory of partial functions and polymorphic types,
+where termination of functional programs can be established in a
+natural way.
+
+In recursion theory and conputer science, questions of definedness
+usually have to deal with termination of an algorithm; typically, this
+is given recursively rather than explicitly, for example in Euclid's
+algorithm for $gcd(a,b)$ of natural numbers $a,b$:
+\[gcd(a,b)=[a {\rm\ if\ }b=0 {\rm\ else\ }gcd(b,rem(a,b))]\eqno{(1)}\]
+One proves by complete induction on $b$ that
+\[{\rm forall\ }a, gcd(a,b){\rm\ is\ defined}\]
+Of course, justification of such reasoning presupposes a semantical
+account of recursive definitions. In particular, on the face of it,
+(1) requires definition of the functional
+$F(b)=\lambda a.gcd(a,b)$ by recursion of the form
+\[F(b)=G(b,F~\uparrow~b)\]
+and justification of {\sl that} requires proof by induction on the
+natural numbers of the statement that for each $x$ there is a unique
+function(al) $F_x$ with domain $[0,x]$ such that for all $y\le x$
+\[F_x(y)=G(y,F_x~\uparrow~y)\]
+then $F(b)$ is defined to be $F_b(b)$ for the unique such $F_b$ with
+${\rm dom}(F_b)=[0,b]$.
+
+\section{Homann \cite{Homa94}}
+algorithm schemata
Name: gcd(?a,?b)=?g\\
Signature: ?A $\times$ ?A $\rightarrow$ ?A\\
@@ 3373,6 +3917,187 @@ gcd(u,v) = gcd(v,u)\\
gcd(u,v) = gcd(v, u mod v)\\
gcd(u,0) = u
+\section{Igarashi et al. [Igar75]}
+
+Igarashi et al. \cite{Igar75}
+
+The genera idea of how to go about verifying an asserted program is to
+reduce this problem to questions about whether certain associated
+logical conditions are true of theorems in various standard
+firstorder theories.
+
+It will become evident from the examples that a great deal of
+elementary simplification of verification conditions is both necessary
+and easy to do. The truth of many of the conditions will be
+established at the simplification stage.
+
+What has become evident is that the Verification Condition Generator (VCG)
+is not a trivial element in this type of verification system. In order
+to make such a system practical, the amount of documentation the user
+is required to supply with his program should be restricted to what
+would be considered natural for human understanding of what the
+program and its subprograms do.
+
+In the logic of programs containing assertions they are of three kinds
+\begin{enumerate}
+\item assertions
+\item statements of the form P\{A\}Q where P, Q are assertions and A
+is a program or asserted program. P\{A\}Q means ``if P is true of the
+input state and A halts then Q is true of the output state''
+\item procedure declarations of the form $p(x;y)$ PROC K where $p$ is
+a procedure name, $x$ and $y$ are lists of variable and value
+parameters respectively, and $K$ is a program or asserted program (the
+procedure body), in which the variables designated by $y$ do not occur
+in the lefthand side of an assignment statement, nor occur as a
+variable parameter in a procedure statement.
+\end{enumerate}
+
+If a primitive procedure name, say $q$, occurs in a program about
+which we are to prove a certain theorem, we have to either give a set
+of (nonlogical) axioms of the form $P\{q(x;y)\}R$ or a defining axiom
+for $q$.
+
+Here we study the properties of the set V of axioms and rules of
+inference used by VCG. One of our main concerns is that the rules of
+inference in V should be unambiguous in the sense that only one rule
+is applicable to generate subgoals from any given goal. This will
+certainly be the case if no two rules have conclusoins which have
+common substitution instances, a property which is true of V.
+
+The core rules:
+
+\begin{tabular}{ll}
+{\sl Axioms} &\\
+C1. assignment axioms: & $\displaystyle
+P\vert_t^x\{x\leftarrow t\}P$\\
+&\\
+C2. frame axioms: & $\displaystyle
+P\{q(x;t)\}P$ provided $\lnot(x\in VAR(P))$\\
+&\\
+C3. procedure declarations: & $\displaystyle
+p(x;y)$ PROC K\\
+&\\
+C4. logical theorems: & $P$ for all $P$ s.t. $\vdash P$\\
+&\\
+{\sl Rules}&\\
+C5. consequence: &
+$\displaystyle\frac{P\supset Q\quad Q\{A\}R}{P\{A\}R}\quad
+\displaystyle\frac{P\{A\}Q\quad Q\supset R}{P\{A\}R}$\\
+&\\
+C6. and/or: &
+$\displaystyle\frac{P\{A\}Q\quad R\{A\}S}{P\land R\{A\}Q\land S}\quad
+\displaystyle\frac{P\{A\}Q\quad R\{A\}S}{P\lor R\{A\}Q\lor S}$\\
+&\\
+C7. composition: &
+$\displaystyle\frac{P\{A\}Q\quad Q\{B\}R}{P\{A;B\}R}$\\
+&\\
+C8.conditional: &
+$\displaystyle\frac{P\land R\{A\}Q\quad P\land\lnot R\{B\}Q}
+{P\{if\ R\ then\ A\ else\ B\}Q}$\\
+&\\
+C9. substitution:
+& $\displaystyle(L)\quad\frac{P(x;y)\{q(x;y)\}Q(x;y)}
+{P(z;y)\{q(z;y)\}Q(z;y)}$\\
+&\\
+& $\displaystyle(R)\quad\frac{P(x;y)\{q(x;y)\}Q(x;y)}
+{P(x;s)\{q(x;s)\}Q(x;s)}$\\
+&\\
+C10. procedure call: &
+$\displaystyle\frac{p(x;y){\rm\ PROC\ }K(p)\quad P\{r(x;y)\}Q
+\dststile{}{} P\{K(r)\}Q}
+{P\{p(x;y)\}Q}$\\
+\end{tabular}
+
+Note that in C9 (1) $s$ does not contain members of $x$;
+(ii) members of $x$ must be distinct and $x$ must contain no variable
+occurring in $P(x;y)$ or $Q(x;y)$ except possibly members of $x$.
+
+Note that in C10 $p$ does not occur in the proof of the right hand
+premiss, and $r$ does not occur in any other assumption in that proof.
+
+The rules in the following table are stated in the form in which they
+are used to generate subgoals. Thus, for example in the case of the
+assignment rule V1, the axiom $Q(e)\{x\leftarrow e\}Q(x)$ is ommitted
+from the premisses since it is true and therefore not generated as a
+subgoal. The composition rule is not used to generate subgoals (it
+would be a source of ambiguity) but is included in the other
+rules. VCG does not require assertions at conditional statements. It
+'marks' the conditional tests in the subgoals of the conditional rule,
+and uses them as assertions that permit a slightly different rule of
+consequence. The normal rule of consequence, V3 (ii) would usually
+lead to a verification condition of the form $Q\supset R^\prime$
+where $R^\prime$ is some formula involving $R$. Most likely the proof
+of $R^\prime$ would depend on the premiss $P$ and in such a case
+$Q\supset R^\prime$ is unlikely to be provable.
+
+V1. {\sl Simple assignment}
+\[\frac{P\{A\}Q(e)}{P\{A;x\leftarrow e\}Q(x)}\]
+
+V2. Array assignment
+\[\frac{P\{A\}R (if\ i=j\ then\ e\ else\ B[i])}
+{P\{A;B[j]\leftarrow e\}R(B[i])}\]
+
+V3. Consequence
+\[(i)\frac{P\supset Q}{P\{Null\}Q^\prime}
+\quad\frac{P\{A\}Q\quad Q\supset R}{P\{A;Q\}R}
+\quad\frac{P\{A\}Q\supset R}{P\{A;Qif\}R}\]
+
+V4. Iteration
+\[\frac{P\{A\}R\quad R\land S\{B\}R\quad R\land\lnot S\supset Q}
+{P\{A; R;\ while\ S\ do\ B\}Q}\quad{\rm\ where\ R\ is\ an\ assertion}\]
+
+V5. Conditional
+\[\frac{P\{A; Qif; B\}R\quad P\{A;\lnot Qif; C\}R}
+{P\{A;\ if\ Q\ then\ B\ else\ C\}R}\]
+
+V6. Goto
+\[\frac{P\{A\}\ assertion\ (L)}{P\{A; goto\ L\}Q}\]
+
+V7. Procedure call
+\[U(x;v)\{q(x;v)\}W(x;v)\dststile{}{}
+\frac{P\{A\}U(a;e)\land\forall a(W(a;e)\supset R)}
+{P\{A;q(a;e)\}R}\]
+
+V8. Procedure declaration
+\[\frac{P\{q(x;v)\}R\dststile{}{} P\{K\}R}
+{P\{procedure\ q(x;v); K\}R}\]
+
+Notation: P,Q,R,S are Boolean Assertions. Null denotes the empty
+program. Q(e) denotes the substitution of e for x in Q(x). In V6,
+'assertion (L)' denotes the assertion at label L.
+
+B[i] denotes the $i^{th}$ element in array B. In each of the rules A
+can be Null. Qif denotes a 'marked' Boolean assertion Q.
+
+\section{Kamareddine [Kama15]}
+
+Kamareddine \cite{Kama15}
+Computerising Mathematical Text explores various ways of
+capturing mathematical reasoning.
+
+\section{Mahboubi \cite{Mahb16}}
+Mathematical Components. This book contains a
+proof of the Euclidean algorithm using COQ.
+
+\section{MedinaBulo et al. \cite{Bulo04}}
+gives a formal verification of
+Buchberger's algorithm using ACL2 and Common Lisp.
+
+\section{Pierce \cite{Pier15}}
+has a Software Foundations course in COQ with
+downloaded files in Pier15.tgz.
+
+\section{Santas \cite{Sant95}}
+A Type System for Computer Algebra
+
+\section{Spitters \cite{Spit11}}
+Type Classes for Mathematics in Coq. Also see
+\verbhttp://www.eelis.net/research/mathclasses/
+
+\section{Th\'ery \cite{Ther01}}
+used COQ to check an implementation of Buchberger's
+algorithm.
+
\appendix
\chapter{The Global Environment}
@@ 3666,6 +4391,76 @@ Clarke shows several proofs
\subsection{Davenport \cite{Dave02}}
+\subsection{Davenport \cite{Dave12b}}
+
+\subsection{Davenport \cite{Dave18}}
+
+The following definition is valid whenever we have a concept of
+division.
+
+{\bf Definition} {\sl h is said to be a greatest commmon divisor, or
+g.c.d, of f and g if, and only if
+\begin{enumerate}
+\item h divides both f and g
+\item if h' divides both f and g, then h' divides h
+\end{enumerate}
+
+This definition clearly extends to any number of arguments. The g.c.d
+is normally written gcd(f,g).}
+
+Note that we have defined a g.c.d. whereas it is more common to talke
+of {\sl the} g.c.d. However 'a' is correct. We normally say that 2 is
+{\sl the} g.c.d of 4 and 6, but in fact $2$ is equally a g.c.d. of 4
+and 6.
+
+{\bf Definition} {\sl if $a=u*b$ where $u$ is a unit, we say that $a$
+and $b$ are associates.}
+
+{\bf Proposition} {\sl if h and h' are greatest common divisors of a
+and b, they are associates.}
+
+{\bf Example} (Greatest common divisors need not exist) {\sl Consider
+the set of all integers with $\sqrt{5}$. 2 clearly divides both 6 and
+$2+2\sqrt{5}$. However, so does $1+\sqrt{5}$ (since
+$6 = (1+\sqrt{5})(1\sqrt{5})$), yet there is no multiple of both 2
+and $1+\sqrt{5}$ which divides both.}
+
+{\bf Definition} {\sl A ring R is said to be an integral domain if
+there is a neutral element 1 such that $1*a=a$ and, whenever
+$a*b=0$ at least one of a and b are zero.}
+
+{\bf Definition} {\sl An integral docmain is which any two elements
+have a greatest common divisor is known as a g.c.d. domain.}
+
+If $R$ is a g.c.d domain, then the elements of the field of fractions
+can be simplified by cancelling a g.c.d. between numerator and
+denomiator, oftan called ``reducing to lowest terms''. While this
+simplifies fractions, it does not guarantee that they are normal or
+canonical. One might think that $\frac{0}{1}$ was the unique
+representation of zero required for normality, but what of
+$\frac{0}{1}$? Equally, $\frac{1}{2}=\frac{1}{2}$, and in general
+we have to remove the ambiguity caused by units. In the case of
+rational numbers, we do this automatically by making the denominator
+positive, but the general case is more difficult.
+
+{\sl Definition} {\sl h is said to be a least common multiple, or
+l.c.m. of f and g if, and only if
+\begin{enumerate}
+\item both f and g divide h
+\item if both f and g divide h', the h divides h'
+\end{enumerate}}
+
+This definition clearly extends to any number of arguments. The
+l.c.m. is normally written lcm(f,g).
+
+{\bf Proposition} {\sl If gcd(f,g) exists, then $fg/gcd(f,g)$ is a
+least common multiple of f and g.}
+
+This result is normally written as $fg=gcd(f,g)lcm(f,g)$, but this is
+only true up to associates. We should also note that this result does
+not extend to any number of arguments: in general
+$fgh \ne gcd(f,g,g)lcm(f,g,h)$.
+
\subsection{Davis \cite{Davi09}}
Davis creates a verified proof checker by creating a simple, obviously
@@ 3738,7 +4533,8 @@ at some point before the loop using such a label.
Function and Concept seminal paper
Fr\"uhwirht \cite{Frue91} details optimistic type systems for logic programs.
+Fr\"uhwirht \cite{Frue91} details optimistic type systems for logic
+programs.
\subsection{Harrison \cite[p13]{Harr98}}
@@ 4028,6 +4824,167 @@ P6.3 & $\land$ & (Y odd) $\land$ X=Y\\
Typed Predicate Calculus giving declarative meaning to
logic programs with type declarations and type inference.
+\subsection{Manna and Waldinger \cite{Mann78a}}
+
+{\bf Greatest Common Divisor of Two Numbers}
+
+In the previous two examples, we have applied the
+intermittentassertion method to programs involving only one loop. The
+following program, which computes the greatest common divisor (gcd) of
+two positive integers, is introduced to show how the
+intermittentassertion method is applied to a program with more
+complex loop structure.
+
+We define $gcd(y,y)$, where $x$ and $y$ are positive integers, as the
+greatest integer that divides both $x$ and $y$, that is
+\[gcd(x,y) = max\{u:u~\vert~x and u~\vert~y\}\]
+
+For instance, $gcd(9,12)=3$ and $gcd(12,25)=1$. The program is
+\begin{verbatim}
+ input(x,y)
+start:
+more: if x = y
+ then finish: output(y)
+ else reducex: if x > y
+ then x < x  y
+ goto reducex
+ reducey: if y > x
+ then y < y  x
+ goto reducey
+ goto more
+\end{verbatim}
+
+This program is motivated by the following properties of the $gcd$:
+\[\begin{array}{l}
+gcd(x,y) = y{\rm\ if\ } x = y\\
+gcd(x,y) = gcd(xy,y){\rm\ if\ } x > y\\
+gcd(x,y) = gcd(x,yx){\rm\ if\ } y > x
+\end{array}\]
+
+We would like to use the intermittentassertion method to prove the
+total correctness of this program. The total correctness can be
+expressed as follows:
+
+{\bf Theorem}: If {\sl sometime} $x=a$, $y=b$ and $b>0$ at start
+then {\sl sometime} $y=gcd(a,b)$ at finish.
+
+To prove this theorem, we need a lessa that describes the internal
+behaavior of the program.
+
+{\bf Lemma}: If\\
+{\sl sometime} $x=a$, $y=b$, and $a,b > 0$ at {\tt more} or \\
+{\sl sometime} $x=a$, $y=b$, and $a,b > 0$ at {\tt reducex} or\\
+{\sl sometime} $x=a$, $y=b$, and $a,b > 0$ at {\tt reducey},\\
+then {\sl sometime} $y=gcd(a,b)$ at {\tt finish}
+
+To show that the lemma implies the theorem, we assume that
+
+{\sl sometime} $x=a$, $yb$, and $a,b > 0$ at {\tt start}.
+
+Then control passes to {\tt more}, so that
+
+{\sl sometime} $x=a$, $yb$, and $a,b > 0$ at {\tt more}.
+
+But then the lemma implies that
+
+{\sl sometime} $y=gcd(a,b)$ at {\tt finish},
+
+which is the desired conclusion of the theorem.
+
+It remains to prove the lemma. We suppose
+
+{\sl sometime} $x=a$, $y=b$, and $a,b > 0$ at {\tt more} or \\
+{\sl sometime} $x=a$, $y=b$, and $a,b > 0$ at {\tt reducex} or\\
+{\sl sometime} $x=a$, $y=b$, and $a,b > 0$ at {\tt reducey},
+
+The proof proceeds by induction on $a+b$; we assume inductively that
+the lemma holds whenever $x=a^\prime$ and $y=b^\prime$, where
+$a^\prime + b^\prime < a + b$, and show that
+
+{\sl sometime} $y=gcd(a,b)$ at {\tt finish}.
+
+We must distinguish between three cases.
+
+{\bf Case $a = b$}. Regardless of whether control is at {\tt more},
+{\tt reducex}, or {\tt reducey}, control passes to {\tt finish} with
+$y=b$, so that
+
+{\sl sometime} $y=b$ at {\tt finish}
+
+But in this case $b=gcd(a,b)$, by a given property of the $gcd$
+function, so we have
+
+{\sl sometime} $y=gcd(a,b)$ at {\tt finish}.
+
+which is the desired conclusion of the lemma.
+
+{\bf Case $a > b$}. Regardless of whether control is at {\tt more},
+{\tt reducex}, or {\tt reducey}, control reaches {\tt reducex} and
+passes around the top inner loop, resetting $x$ to $ab$, so that
+
+{\sl sometime} $x = a  b$ and $y = b$ at {\tt reducex}
+
+For simplicity, let us denote $ab$ and $b$ by $a^\prime$ and
+$b^\prime$, respectively. Note that
+
+$a^\prime, b^\prime > 0$\\
+$a+b > a^\prime + b^\prime$, and\\
+$gcd(a^\prime,b^\prime) = gcd(ab,b) = gcd(a,b)$
+
+This last condition follows by a given property of the $gcd$.
+
+Because $a^\prime, b^\prime > 0$ and $a+b > a^\prime+b^\prime$, the
+induction hypothesis implies that
+
+{\sl sometime} $y=gcd(a^\prime,b^\prime)$ at {\tt finish}.
+
+i.e., by the third condition above,
+
+{\sl sometime} $y=gcd(a,b)$ at {\tt finish}.
+
+{\bf Case $b > a$}. This case is disposed of in a manner symmetric to
+the previous case.
+
+This concludes the proof of the lemma. The total correctness of the
+program is thus extablished.
+
+It is not difficult to prove the partial correctness of the above
+program by using the conventional invariantassertion method. For
+instance, to prove that the program is partially correct with respect
+to the input specification
+
+$x_0 > 0$ and $y_0 > 0$
+
+and output specification
+
+$y=gcd(x_0,y_0)$
+
+(where $x_0$ and $y_0$ are the initial values of $x$ and $y$), we can
+use the same invariant assertion
+
+$x,y > 0$ and $gcd(x,y) = gcd(x_0,y_0)$
+
+at each of the labels {\tt more}, {\tt reducex} and {\tt reducey}.
+
+In contrast, the termination of this program is awkward to prove by
+the conventional wellfounded ordering method, because it is possible
+to pass from {\tt more} to {\tt reducex}, {\tt reducex} to
+{\tt reducey}, or from {\tt reducey} to {\tt more} without changing
+any of the program variables. One of the simplest proofs of the
+termination of the $gcd$ program by this method involves taking the
+wellfounded set to be the pairs of nonnegative integers ordered by
+the regular lexicographic ordering. When the expresion corresponding
+to the loop labels are taken to be
+
+$(x+y,2)$ at {\tt more}\\
+if $x\ne y$ then $(x+y,1)$ else $(x+y,4)$ at {\tt reducex}, and\\
+if $x
books/bookvolbib add references
20180629.01.tpd.patch
books/*.sty add latex style files
+20180629.02.tpd.patch
+books/bookvol13 add additional ideas to explore

1.9.1