\documentclass[11pt,twoside]{article}

\usepackage{latexsym}
\usepackage{code}
\usepackage{proof}
\usepackage{fancyhdr}
\usepackage{lecnotes}

\newcommand{\lecdate}{September 5, 2006}
\newcommand{\lecnum}{3}
\newcommand{\lectitle}{Induction}

\newcommand{\nil}{[\,]}
\newcommand{\cons}[2]{[#1|#2]}

\begin{document}

\maketitle

\noindent

One of the reasons we are interested in high-level programming
languages is that, if properly designed, they allow rigorous
reasoning about properties of programs.  We can prove that our
programs won't crash, or that they terminate, or that they
satisfy given specifications.  Logic programs are particularly
amenable to formal reasoning.

In this lecture we explore induction, with an emphasis on
\emph{induction on the structure of deductions} sometimes called
\emph{rule induction} in order to prove properties of logic
programs.

\setcounter{section}{\lecnum}
\subsection{From Logical to Operational Meaning}

A logic program has multiple interpretations.  One is as a set
of inference rules to deduce logical truths.  Under this
interpretation, the order in which the rules are written down, or
the order in which the premisses to a rule are listed, are
completely irrelevant: the true propositions and even the
structure of the proofs remain the same.  Another interpretation
is as a program, where proof search follows a fixed strategy.  As
we have seen in prior lectures, both the order of the rules and
the order of the premisses of the rules play a significant role
and can make the difference between a terminating and a
non-terminating computation and in the order in which answer
substitutions are returned.

The different interpretations of logic programs are linked.  The
strength of that link depends on the presence or absence of
purely operational constructs such as conditionals or cut, and on
the details of the operational semantics that we have not yet
discussed.

The most immediate property is \emph{soundness} of the operational
semantics: if a query $A$ succeeds with a substitution $\theta$, then
the result of applying the substitution $\theta$ to $A$ (written
$A\theta$) is true under the logical semantics.  In other words,
$A\theta$ has a proof.  This holds for pure logic programs but does not
hold in the presence of logic variables together with
negation-as-failure, as we have seen in the last lecture.

Another property is \emph{completeness} of the operational
semantics: if there is an instance of the query $A$ that has a
proof, then the query should succeed.  This does not hold, since
logic programs do not necessarily terminate even if there is a
proof.

But there are some intermediate points.  For example, the
property of \emph{non-deterministic completeness} says that if
the interpreter were always allowed to choose which rule to use
next rather than having to use the first applicable one, then the
interpreter would be complete.  Pure logic programs are complete
in this sense.  This is important because it allows us to
interpret finite failure as falsehood: if the interpreter returns
with the answer `\cd{no}' it has explored all possible choices.
Since none of them has led to a proof, and the interpreter is
non-deterministically complete, we know that no proof can exist.

Later in the course we will more formally establish soundness and
non-deterministic completeness for pure logic programs.  It is
relevant for this lecture, because when we want to reason about
logic programs it is important to consider at which level of
abstraction this reasoning takes place: Do we consider the
logical meaning?  Or the operational meaning including the
backtracking behavior?  Or perhaps the non-deterministic
operational meaning?  Making a mistake here could lead to a
misinterpretation of the theorem we proved, or to a large amount
of unnecessary work.  We will point out such consequences as we
go through various forms of reasoning.

\subsection{Rule Induction}

We begin by reasoning about the logical meaning of programs.
As a simple example, we go back to the unary encoding of
natural numbers from the first lecture.  For reference
we repeat
% the type predicate $\msf{nat}$
% \[ \infer[\msf{nz}]{\msf{nat}(\z)}{\mathstrut}
%   \hspace{5em}
%   \infer[\msf{ns}]{\msf{nat}(\s(N))}{\msf{nat}(N)}
%\]
% and
the predicates for $\msf{even}$ and $\msf{plus}$
\[ \begin{array}{c}
 \infer[\msf{evz}]{\msf{even}(\z)}{\mathstrut}
 \hspace{5em}
 \infer[\msf{evs}]{\msf{even}(\s(\s(N)))}{\msf{even}(N)} \\[1em]
 \infer[\msf{pz}]{\msf{plus}(\z, N, N)}{\mathstrut}
 \hspace{5em}
 \infer[\msf{ps}]{\msf{plus}(\s(M), N, \s(P))}{\msf{plus}(M, N, P)}
\end{array} \]

Our aim is to prove that the sum of two even numbers is even.
It is not immediately obvious how we can express this property
on the relational specification.  For example, we might say:
\begin{quote}\it
For any $m$, $n$, and $p$, if $\msf{even}(m)$ and
$\msf{even}(n)$ and $\msf{plus}(m, n, p)$ then $\msf{even}(p)$.
\end{quote}
Or we could expressly require the existence of a sum $p$ and the
fact that it is even:
\begin{quote}\it
For any $m$, $n$, if $\msf{even}(m)$ and $\msf{even}(n)$ then there
exists a $p$ such that $\msf{plus}(m, n, p)$ and $\msf{even}(p)$.
\end{quote}
If we knew that $\msf{plus}$ is a total function in its first two
arguments (that is, ``\textit{For any $m$ and $n$ there exists a
unique $p$ such that $\msf{plus}(m, n, p)$.}''), then
these two would be equivalent (see Exercise~\ref{exc:plus}).

We will prove it in the second form.  The first idea for this
proof is usually to examine the definition of $\msf{plus}$ and
see that it is defined structurally over its first argument $m$:
the rule $\msf{pz}$ accounts for $\z$ and the rule $\msf{ps}$
reduces $\s(m)$ to $m$.  This suggests an induction over $m$.
However, in the predicate calculus (and therefore also in our
logic programming language), $m$ can be an arbitrary term and is
therefore not a good candidate for induction.

Looking at the statement of the theorem, we see we are given the
information that $\msf{even}(m)$.  This means that we have a
deduction of $\msf{even}(m)$ using only the two rules $\msf{evz}$
and $\msf{evs}$, since we viewed these two rules as a complete
definition of the predicate $\msf{even}(m)$.  This licenses us to
proceed by induction on the structure of the deduction of
$\msf{even}(m)$.  This is sometimes called \emph{rule induction}.
If we want to prove a property for all proofs of a judgment, we
consider each rule in turn.  We may assume the property for all
premisses of the rule and have to show that it holds for the
conclusion.  If we can show this for all rules, we know the
property must hold for all deductions.

In our proofs, we will need names for deductions.  We use script
letters $\DD$, $\EE$, and so on, to denote deduction and use
the two-dimensional notation
\[ \deduce{J}{\DD} \]
if $\DD$ is a deduction of $J$.

\begin{theorem}
For any $m$, $n$, if $\msf{even}(m)$ and
$\msf{even}(n)$ then there exists a $p$ such that $\msf{plus}(m, n, p)$
and $\msf{even}(p)$.
\end{theorem}
\begin{proof}
By induction on the structure of the deduction $\DD$ of $\msf{even}(m)$.
\begin{description}
\item[Case:]
$\DD = \lowered{\infer[\msf{evz}]
                      {\msf{even}(\z)}
                      {\mathstrut}}$
where $m = \z$.
\begin{tabbing}
$\msf{even}(n)$ \` Assumption \\
$\msf{plus}(\z, n, n)$ \` By rule $\msf{pz}$ \\
There exists $p$ such that $\msf{plus}(\z, n, p)$ and $\msf{even}(p)$
\` Choosing $p = n$
\end{tabbing}
\item[Case:]
$\DD = \lowered{\infer[\msf{evs}]
                      {\msf{even}(\s(\s(m')))}
                      {\deduce{\msf{even}(m')}{\DD'}}}$
where $m = \s(\s(m'))$.
\begin{tabbing}
$\msf{even}(n)$ \` Assumption \\
$\msf{plus}(m', n, p')$ and $\msf{even}(p')$ for some $p'$ \` By ind.\ hyp. on $\DD'$ \\
$\msf{plus}(\s(m'), n, \s(p'))$ \` By rule $\msf{ps}$ \\
$\msf{plus}(\s(\s(m')), n, \s(\s(p')))$ \` By rule $\msf{ps}$ \\
$\msf{even}(\s(\s(p')))$ \` By rule $\msf{evs}$ \\
There exists $p$ such that $\msf{plus}(\s(\s(m')), n, p)$ and $\msf{even}(p)$ \\
\` Choosing $p = \s(\s(p'))$.
\end{tabbing}
\end{description}
\end{proof}

We have written here the proof in each case line-by-line, with a
justification on the right-hand side.  We will generally follow
this style in this course, and you should arrange the answers to
exercises in the same way because it makes proofs relatively easy
to check.

\subsection{Deductions and Proofs}

One question that might come to mind is: Why did we have to carry
out an inductive proof by hand in the first place?  Isn't logic
programming proof search according to a fixed strategy, so can't
we get the operational semantics to do this proof for us?

Unfortunately, logic programming search has some severe
restrictions so that it is usable as a programming language and
has properties such as soundness and non-deterministic
completeness.  The restrictions are placed both on the forms of
programs and the forms of queries.  So far, in the logic that
underlies Prolog, rules establish only atomic predicates.
Furthermore, we can only form queries that are conjunctions of
atomic propositions, possibly with some variables.  This means
that queries are purely \emph{existential}: we asked whether
there \emph{exists} some instantiation of the variables so that
there \emph{exists} a proof for the resulting proposition
as in the query \cd{?- plus(s(z), s(s(z)), P)} where we simultaneously
ask for a $p$ and a proof of $\msf{plus}(\s(\z), \s(\s(\z)), p)$.

On the other hand, our theorem above is primarily
\emph{universal} and only on the inside do we see an
\emph{existential} quantifier: ``\textit{For every $m$ and $n$,
and for every deduction $\DD$ of $\msf{even}(m)$ and $\EE$ of
$\msf{even}(n)$ there exists a $p$ and deductions $\mathcal{F}$
of $\msf{plus}(m,n,p)$ and $\mathcal{G}$ of $\msf{even}(p)$.}''

This difference is also reflected in the structure of the proof.
In response to a logic programming query we only use the
inference rules defining the predicates directly.  In the proof
of the theorem about addition, we instead use induction in order
to show that deductions of $\msf{plus}(m, n, p)$ and
$\msf{even}(p)$ exist.  If you carefully look at our proof, you
will see that it contains a recipe for constructing these
deductions from the given ones, but it does not construct them by
backward search as in the operational semantics for logic
programming.  As we will see later in the course, it is in
fact possible to represent the induction proof of our first
theorem also in logic programming, although it cannot be found
only by logic programming search.

We will make a strict separation between proofs using only the
inference rules presented by the logic programmer and proofs
\emph{about} these rules.  We will try to be consistent and write
\emph{deduction} for a proof constructed directly with the rules
and \emph{proof} for an argument about the logical or operational
meaning of the rules.  Similarly, we reserve the terms
\emph{proposition}, \emph{goal}, and \emph{query} for logic
programs, and \emph{theorem} for properties of logic programs.

\subsection{Inversion}

An important step in many induction proofs is \emph{inversion}.
The simplest form of inversion arises if have established that a
certain proposition is true, and that the proposition matches the
conclusion of only one rule.  In that case we know that this rule
must have been used, and that all premisses of the rule must also
be true.  More generally, if the proposition matches the
conclusion of several rules, we can split the proof into cases,
considering each one in turn.

However, great care must be taken with applying inversion.  In my
experience, the most frequent errors in proofs, both by students
in courses such as this and in papers submitted to or even
published in journals, are (a) missed cases that should have been
considered, and (b) incorrect applications of inversion.  We can
apply inversion only if we already know that a judgment has a
deduction, and then we have to take extreme care to make sure
that we are indeed considering all cases.

As an example we prove that the list difference is uniquely
determined, if it exists.  As a reminder, the definition of
append in rule form.  We use the Prolog notation $\nil$
for the empty list, and $\cons{x}{xs}$ for the list with
head $x$ and tails $xs$.
\[ \infer[\msf{apnil}]
         {\msf{append}(\nil, ys, ys)}
         {\mathstrut}
   \hspace{5em}
   \infer[\msf{apcons}]
         {\msf{append}(\cons{x}{xs}, ys, \cons{x}{zs})}
         {\msf{append}(xs, ys, zs)}
\]
We express this in the following
theorem.

\begin{theorem}
For all $xs$ and $zs$ and for all $ys$ and $ys'$,
if $\msf{append}(xs, ys, zs)$ and $\msf{append}(xs, ys', zs)$
then $ys = ys'$.
\end{theorem}
\begin{proof}
By induction on the deduction $\DD$ of
$\msf{append}(xs, ys, zs)$.  We use $\EE$ to denote the
given deduction $\msf{append}(xs, ys', zs)$.
\begin{description}
\item[Case:]
$\DD = \lowered{\infer{\msf{append}(\nil, ys, ys)}{\mathstrut}}$
where $xs = \nil$ and $zs = ys$.
\begin{tabbing}
$\msf{append}(\nil, ys', ys)$ \` Given deduction $\EE$ \\
$ys' = ys$ \` By inversion on $\EE$ (rule $\msf{apnil}$)
\end{tabbing}
\item[Case:]
$\DD = \lowered{\infer{\msf{append}(\cons{x}{xs_1}, ys, \cons{x}{zs_1})}
                      {\deduce{\msf{append}(xs_1, ys, zs_1)}{\DD_1}}}$
where $xs = \cons{xs}{xs_1}$, $zs = \cons{xs}{zs_1}$.
\begin{tabbing}
$\msf{append}(\cons{x}{xs_1}, ys', \cons{x}{zs_1})$ \` Given deduction $\EE$ \\
$\msf{append}(xs_1, ys', zs_1)$ \` By inversion on $\EE$ (rule $\msf{apcons}$) \\
$ys = ys'$ \` By ind.\ hyp. on $\DD_1$
\end{tabbing}
\end{description}
\end{proof}

\subsection{Operational Properties}

We do not yet have formally described the operational semantics
of logic programs.  Therefore, we cannot prove operational
properties completely rigorously, but we can come close by appealing
to the intuitive semantics.  Consider the following perhaps
somewhat unfortunate specification
of the predicate $\msf{digit}$ for decimal digits in unary
notation, that is, natural numbers between 0 and 9.
\[ \infer{\msf{digit}(\s(\s(\s(\s(\s(\s(\s(\s(\s(\z))))))))))}
         {\mathstrut}
   \hspace{5em}
   \infer{\msf{digit}(N)}
         {\msf{digit}(\s(N))}
\]
For example, we can deduce that $\z$ is a digit by using
the second rule nine times (working bottom up) and then closing
of the deduction with the first rule.  In Prolog notation:
\begin{code}
digit(s(s(s(s(s(s(s(s(s(z)))))))))).
digit(N) :- digit(s(N)).
\end{code}
While logically correct, this does not work correctly
as a decision procedure, because it will not terminate
for any argument greater than 9.

\begin{theorem}
Any query \cd{?- digit($n$)} for $n > 9$ will not terminate.
\end{theorem}
\begin{proof}
By induction on the computation.  If $n > 9$, then the first
clause cannot apply.  Therefore, the goal \cd{digit($n$)} must be
reduced to the subgoal \cd{digit(s($n$))} by the second rule.
But $\s(n) > 9$ if $n > 9$, so by induction hypothesis the subgoal
will not terminate.  Therefore the original goal also does not terminate.
\end{proof}

\subsection{Aside: Forward Reasoning and Saturation}

As mentioned in the first lecture, there is a completely
different way to interpret inference rules as logic programs than
the reading that underlies Prolog.  This idea is to start with
axioms (that is, inference rules with no premisses) as logical
truths and apply all rules in the forward direction, adding more
true propositions.  We stop when any rule application that we
could perform does not change the set of true propositions.
In that case we say the database of true propositions is
\emph{saturated}.  In order to answer a query we can now
just look it up in the saturated database: if an instance
of the query is in the database, we succeed, otherwise we fail.

In the example from above, we start with a database consisting
only of $\msf{digit}(\s(\s(\s(\s(\s(\s(\s(\s(\s(\z))))))))))$.
We can apply the second rule with this as a premiss to conclude that
$\msf{digit}(\s(\s(\s(\s(\s(\s(\s(\s(\z)))))))))$.  We can
repeat this process a few more times until we finally conclude
$\msf{digit}(\z)$.  At this point, any further rule applications
would only add facts with already know: the set is saturated.
We see that, consistent with the logical meaning, only the numbers
0 through 9 are digits, other numbers are not.

In this example, the saturation-based operational semantics
via forward reasoning worked well for the given rules, while
backward reasoning did not.  There are classes of algorithms
which appear to be easy to describe via saturation, that
appear significantly more difficult with backward reasoning and
vice versa.  We will therefore return to forward reasoning
and saturation later in the class, and also consider how it
may be integrated with backward reasoning in a logical way.


\subsection{Historical Notes}

The idea to mix reasoning \emph{about} rules with the usual logic
programming search goes back to work by Eriksson and
Halln\"as~\cite{Eriksson88} which led to the GCLA logic programming
language~\cite{Aronsson90}.  However, it stops short of supporting full
induction.  More recently, this line of development been revived by Tiu,
Nadathur, and Miller~\cite{Tiu05eshol}.  Some of these ideas are
embodied in the Bedwyr system currently under development.

Another approach is to keep the layers separate, but provide means to
express proofs of properties of logic programs again as logic programs,
as proposed by Sch\"urmann~\cite{Schurmann00phd}.  These ideas are
embodied in the Twelf system~\cite{Pfenning99cade}.

Saturating forward search has been the mainstay of the theorem proving
community since the pioneering work on resolution by
Robinson~\cite{Robinson65}.  In logic programming, it has been called
\emph{bottom-up evaluation} and has historically been applied mostly in
the context of databases~\cite{Naughton91} where saturation can often be
guaranteed by language restrictions.  Recently, it has been revisited as
a tool for algorithm specification and complexity analysis by Ganzinger
and McAllester~\cite{Ganzinger01ijcar,Ganzinger02iclp}.

\subsection{Exercises}

The proofs requested below should be given in the style presented
in these notes, with careful justification for each step of reasoning.
If you need a lemma that has not yet been proven, carefully state
and prove the lemma.

\begin{exercise}
Prove that the sum of two even numbers is even in the first
form given in these notes.
\end{exercise}

\begin{exercise}
\label{exc:plus}
Prove that $\msf{plus}(m, n, p)$ is a total function of
its first two arguments and exploit this property to prove
carefully that the two formulations of the property that
the sum of two even numbers is even, are equivalent.
\end{exercise}

\begin{exercise}
Prove that $\msf{times}(m, n, p)$ is a total function
of its first two arguments. 
\end{exercise}

\begin{exercise}
Give a relational interpretation of the claim that
``\textit{addition is commutative}'' and prove it.
\end{exercise}

\begin{exercise}
Prove that for any list $xs$, $\msf{append}(xs, \nil, xs)$.
\end{exercise}

\begin{exercise}
Give two alternative relational interpretations of the
statement that ``\textit{$\msf{append}$ is associative.}''
Prove one of them.
\end{exercise}

\begin{exercise}
Write a logic program to reverse a given list and prove
that when reversing the reversed list, we obtain the original
list. 
\end{exercise}

\begin{exercise}
Prove the correctness of quicksort from the previous lecture with
respect to the specification from Exercise 2.2: If \cd{quicksort($xs$,
$ys$)} is true then the second argument is an ordered permutation of the
first.  Your proof should be with respect to logic programs
to check whether a list is ordered, and whether one list is
a permutation of another.
\end{exercise}

\subsection{References}

\bibliographystyle{plain}
\bibliography{lp}

\end{document}