\section{Logic of Partial Functions} \label{lpf}

\subsection{Introduction}

Partial functions --- which can yield ``undefined'' results -- are
common in computing, and proving results about programs requires
a method of handling undefined terms.
In \cite{CJ} and \cite{TANSTAAFL} various methods of either avoiding or coping
with them are discussed.
The Logic of Partial Functions, described in \cite{BCJ},
is one of these methods.
It is a three-valued logic, where propositional terms can be true, false or
undefined.
The title of \cite{TANSTAAFL} 
expresses the conclusion that every method has disadvantages;
in relation to LPF, in \cite[page~264]{BCJ} the authors state 
``Even given the basic set of axioms, it was not immediately apparent how to
avoid clouding proofs with case distinctions concerning undefined''.
In this section we show how this complication may often be avoided.

LPF is described in \cite{BCJ}, where its semantics are given,
together with a sound and complete Hilbert-style axiom system.
Briefly,
\begin{itemize}
\item the semantics are based on three truth-values,
true ($t$), false ($f$) and undefined ($\bot$).
\item $p \lor q$ is true if either $p$ or $q$ is true, false if both
$p$ and $q$ are false, and undefined otherwise.
\item $\sim p$ is defined precisely when $p$ is;
$\sim t$ is $f$ and $\sim f$ is $t$.
\item the other logical connectives can be defined by the usual identities,
ie, $p \land q$ is $\sim (\sim p \lor \sim q)$ and
$p \to q$ is $\sim p \lor q$.
\item the quantifiers $\forall x$ and $\exists x$ mean ``for all defined $x$''
and ``there exists a defined $x$''.
\item $\Delta x$ means ``x is defined''; $\Delta x$ can only be true or false.
\item a related operator is $\delta$, where $\delta x$ is $x \lor \sim x$;
thus $\delta x$ is undefined exactly when $\Delta x$ is false.
\item a valid derivation gives a conclusion which is true when the premises are
all true; it may give any conclusion when a premise is undefined or false
(in particular, an \emph{undefined} premise may give a \emph{false} conclusion).
\end{itemize}

Our $\to$ is written $\Rightarrow$ in \cite{BCJ}.
We use $\to$ to avoid confusion with the Isabelle convention, 
which we use,
where $P \Longrightarrow Q$ means ``$P$ can be derived from $Q$''
(for which \cite{BCJ} uses $\vdash$).
We also use $P \longrightarrow Q$ to mean the rule ``rewrite $P$ to $Q$''.

Thus all the logical operators behave as in classical logic 
when their operands are defined.
Furthermore, many usual identities of classical logic, such as the
associativity and commutativity of $\lor$, and that $\sim \sim p$ is 
identical to $p$, hold.
Many others, involving $\land$ and $\to$, hold since these operators 
can be defined in terms of $\lor$ and $\sim$.

We now introduce the partial order $\sqsubseteq$
in which $\bot \sqsubset f$ and $\bot \sqsubset t$,
$t$ and $f$ being incomparable.
This is the domain-theory partial order
(see \cite{Manna}, Ch. 5, in which $\omega$ is used for $\bot$).
All the operators above, except $\Delta$,
are ``monotone'' relative to this partial order.
Other types, such as numbers $\mathbb N$, are augmented with
an undefined element $\bot_{\mathbb N}$, and
$\sqsubseteq$ can be defined on each such type.

If we further define $p \leftrightarrow q$ to be $(p \to q) \land (q \to p)$,
as usual, we get that $p \leftrightarrow q$ is undefined whenever either
$p$ or $q$ (or both) is undefined.
Thus $p \leftrightarrow p$ is undefined whenever $p$ is.
In LPF, `$=$' denotes ``weak equality'' (whose operands may be
non-logical terms, such as numbers), which behaves similarly to 
$\leftrightarrow$;
that is, $x = x$ is true only if $x$ is defined, and is undefined otherwise.
With ``strong equality'', denoted by `$==$',
$x == y$ is also true if both $x$ and $y$ are undefined.
A definition (``let $x$ equal $y/z$'') is
necessarily interpreted as strong equality.

If the undefined value is taken, intuitively, to mean ``unknown''
(may be true, may be false), then the truth tables for the monotone operators
are consistent with this intuition.
This is the basis of the notion of ``replaceability'' described below.
However, because the values of expressions are determined by calculation using
the truth tables, the expressions 
$p \leftrightarrow p$ and $\sim p \lor p$ (equivalently, $p \to p$)
may be undefined (which is \emph{not} consistent with this intuition,
since under it both these examples are ``known'' to be ``true'').
In fact, taking an undefined term as referring to a real but unknown quantity
is one of the other approaches described in 
\cite{CJ} and \cite{TANSTAAFL}.

\subsection{Rewriting subterms}

The fact that a valid derivation may
give a false conclusion from undefined premises
is the key to the results of this section.
(In \cite{BCJ} this is called the weak interpretation of the semantic
turnstile).
It means that if we take a premise, and apply to it transformations which 
\begin{itemize}
\item transform true propositions to true propositions
\item transform undefined or false propositions to anything
\end{itemize}
then we have an inference which is valid in LPF.
In fact we will use a sub-class of such transformations,
namely those which 
\begin{enumerate}
\renewcommand\labelenumi{(\alph{enumi})}
\item ``behave nicely'' on defined propositions, 
ie, transform them to equivalent propositions
\item may ``misbehave'' on undefined propositions, 
ie, transform them to anything
\end{enumerate}
The value of this approach is that we can use a transformation 
(or rewrite rule) which does ``misbehave'' on undefined propositions, 
and yet avoid the need to check whether a proposition is defined.

We give an example based on division by zero,
$x/0$ being undefined.
At this point we treat $x * 0$ as undefined if $x$ is undefined.
Then the derivation 
$1/0*0 = 1/0*0 \Longrightarrow 1 = 0$ is valid in LPF,
because the premise is undefined.
(This may be thought a disadvantage of LPF, and is commented upon later).
We obtain this derivation using the methods of this section as shown in 
\fig{ex}:
we apply the rewrite rule
$x/y*y \longrightarrow x$ to the left-hand side,
and apply the rewrite rule
$z * 0 \longrightarrow 0$ to the right-hand side.
These rewrite rules are applied \emph{without} having to check 
which terms are defined.

\begin{figure} \normalsize
\vpf
\begin{center} 
\bpf
\A "$1/0*0 = 1/0*0$"
\U "$1 = 1/0*0$" "($x/y*y \longrightarrow x$)"
\U "$1 = 0$" "($z * 0 \longrightarrow 0$)"
\epf
\end{center}
\caption{A Valid Derivation in LPF}
\label{fig:ex}
\end{figure}

In the usual theory of numbers, the first rule above,
if expressed as an equality, $x/y*y = x$, would not be valid;
the second rule $z * 0 \longrightarrow 0$ looks all right, but
we apply it in a case where $z$ is undefined.
We now look at the justification for proceeding this way.

We say a term $x$ is ``replaceable'' by another term $y$ 
either if $x$ is undefined or if $x$ is (defined and) equal to $y$.
That is (in terms of the domain ordering) $x \sqsubseteq y$.
Note that, if $x$ and $y$ are propositional term, this means that a 
transformation satisfying the description in (a) and (b) above
may take $x$ to $y$.

Now, if $f$ is an operator monotone in its first argument,
then, by definition,  $f(x, \ldots) \sqsubseteq f(y, \dots)$.
We extend this to the following result.

\begin{lemma} \label{lpflem}
Let $x \sqsubseteq y$, and let
$g(x, \ldots)$ be a propositional expression made up from $x$ 
(and other operand terms) using only monotone operators.
Then the inference $g(x, \ldots) \Longrightarrow g(y, \dots)$ is valid.
\end{lemma}

\begin{proof}
Omitting reference to operands other than $x$,
we let 
$g(x) = f_n (f_{n-1} ( \ldots (f_1(x)) \ldots )$,
where each operator $f_i$ is monotone.
As $x \sqsubseteq y$ and $f_1$ is monotone,
$f_1(x) \sqsubseteq f_1(y)$;
generally, if 
$f_i (f_{i-1} ( \ldots (f_1(x)) \ldots ) \sqsubseteq
f_i (f_{i-1} ( \ldots (f_1(y)) \ldots )$
and $f_{i+1}$ is monotone,
then
$f_{i+1} (f_i (f_{i-1} ( \ldots (f_1(x)) \ldots ) \sqsubseteq
f_{i+1} (f_i (f_{i-1} ( \ldots (f_1(y)) \ldots )$.
Therefore, by induction,
$f_n (f_{n-1} ( \ldots (f_1(x)) \ldots ) \sqsubseteq
f_n (f_{n-1} ( \ldots (f_1(y)) \ldots )$; that is, 
$g(x, \ldots) \sqsubseteq g(y, \dots)$.
Finally, as $g(x, \ldots)$ is a proposition,
then $g(x, \ldots) \sqsubseteq g(y, \dots)$
means that either they both have the same
truth-value, or $g(x, \ldots)$ is undefined.
A fortiori, if $g(x, \ldots)$ is true then so is $g(y, \dots)$.
Thus the inference $g(x, \ldots) \Longrightarrow g(y, \dots)$ is valid.
\qed
\end{proof}

Note that every operator which is ``strict'' 
or ``naturally extended''
(ie, an undefined operand produces an undefined result)
is monotone (\cite{Manna}, p. 361).

Thus, when $x \sqsubseteq y$,
this result allows
rewriting $x$ by $y$
without checking whether $x = y$, 
ie without checking whether $x$ is defined.
However the example shown in \fig{ex}
% $1/0*0 = 1/0*0 \Longrightarrow 1 = 0$,
illustrates points at which one must beware of the issue of
undefinedness.

%There remain some practical cautions about LPF, which we illustrate by
%reference to the earlier example,
%$1/0*0 = 1/0*0 \Longrightarrow 1 = 0$.

Firstly, it is important to remember that some axioms (such as $x = x$)
and inference rules (such as implication-introduction)
do require that some term be defined.
(Otherwise one could use the valid rule 
$1/0*0 = 1/0*0 \Longrightarrow 1 = 0$ 
to deduce $1 = 0$).
Secondly, care is needed in formulating the definitions of operators and the
replacement rules.  
For example, if we chose to define $x * 0$ to be $0$ whether or not 
$x$ is defined (which would be quite sensible, since `$*$' would still
be monotone), then the premise of the example in \fig{ex} would be true.
However, with this definition the rewrite rule
$x/y*y \longrightarrow x$ would \emph{not} be valid, since 
$x/y*y$ and $x$ could be both defined but not equal,
in which case $x/y*y \not \sqsubseteq x$.

\subsection{Implementation in Isabelle} \label{LPF-impl}

Although Isabelle has a built-in rewriting capability, 
it is limited to the case where terms are equal (actually,
related by Isabelle's meta-equality operator).
Since the rewriting described here ultimately uses instead inference steps
of the form of (\ref{repD}) below, it is not possible to use
Isabelle's built-in rewriting.

The implementation of this technique was motivated by the manner in which 
the HOL theorem prover permits the user to specify a strategy for 
navigating through a term and rewriting rewritable subterms where they 
are found.
In HOL, this is done by specifying conversions and conversionals.
A full description of these is in \cite[Chapter~13]{HOLdesc}.
A \emph{conversion} is a function of type \texttt{term -> thm},
which takes a term $t$ to a theorem $t = t'$ (which can be used to  
rewrite $t$ to $t'$).
A \emph{conversional} is a function which acts on or modifies conversions.
For example, if 
$\textit{conv}\ t$ is $t = t'$ (to rewrite $t$ to $t'$), and 
$\textit{conv}'\ t'$ is $t' = t''$ (to rewrite $t'$ to $t''$)
then $(\textit{conv}\ \texttt{THENC}\ \textit{conv}')\ t$ is $t = t''$
(to rewrite $t$ to $t''$).
Another example is the \texttt{REPEATC} conversional, 
which repeatedly applies a conversion until there is no further change
to the term.
These are described in \cite[\S13.1]{HOLdesc}.
The conversional \texttt{SUB\_CONV}
applies a conversion to the immediate subterms of a term.
These conversionals may be used to program various more complex
strategies for rewriting (where possible) subterms of a term,
as described in \cite[\S13.2]{HOLdesc}.
A conversion \textit{conv} that ``fails'', in the sense that 
$\textit{conv}\ t$ finds no $t'$ such that $t = t'$,
can be programmed either to return $t = t$ or to raise an exception,
and there are functions to change one sort of conversion to the other.

Any conversion can be converted to either a forward proof rule or a tactic for
backwards proof by the functions \texttt{CONV\_RULE} and \texttt{CONV\_TAC},
see \cite[\S13.1]{HOLdesc}.
The conversions form the basis of \texttt{REWRITE\_RULE} and 
\texttt{REWRITE\_TAC}, used in forward proof and backward proof respectively.

Implementation of the simulated rewriting technique for LPF relies
heavily on the concepts of the HOL implementation, though the details differ.

In Isabelle, we implemented the axioms and rules of \cite{BCJ}
as a theory.
In addition, we defined a function 
$\texttt{rep} (t,t')$ to mean that $t$ is replaceable by $t'$,
(ie, $ t \sqsubseteq t'$) and we proved,
from the LPF axioms, 
results of the form 
\begin{equation} \label{rep-cong}
\frac {\texttt{rep}(P,P') \qquad \texttt{rep}(Q,Q')}
{\texttt{rep}(P \textit{ op } Q,P' \textit{ op } Q')} 
\end{equation}
where \textit{op} stands for each of the binary propositional operators,
and corresponding results for the unary propositional operators.
We also proved the reflexivity and transitivity of \texttt{rep},
and the following result 
\begin{equation} \label{repD}
\frac {\texttt{rep}(P,Q) \qquad P} Q 
\end{equation}

We define a new datatype which provides a way
(other than by using exceptions)
to indicate whether or not a term is unchanged,
$$ \texttt{datatype crep = Unc | Rep of thm ; }$$
A \emph{rep-conversion}, of type \texttt{cterm -> crep},
is given a term \textit{t}
% which is a proposition (without "Trueprop")
and produces a theorem.
In the case of a rep-conversion used for forwards (resp. backwards) proof,
the theorem is $\texttt{rep} (t,t')$ (resp. $\texttt{rep} (t',t)$)
for some $t'$.
This is analogous to a HOL conversion, except
that because \texttt{rep} is a preorder, not an equivalence, 
different rep-conversions are needed for forwards and for backwards proof.
A related function which helps in the implementation 
(in particular, it makes composition straightforward) is
a \emph{rep-transformation}, of type \texttt{thm -> crep};
a {rep-transformation} takes a theorem
$\texttt{rep} (s,t)$ and transforms it to
the theorem $\texttt{rep} (s,t')$ (for forwards proof)
or $\texttt{rep} (s',t)$ (for backwards proof).
It does this by discovering the theorem 
$\texttt{rep} (t,t')$ or $\texttt{rep} (s',s)$
% for forwards or backwards proof
respectively,
and using the transitivity of \texttt{rep}.
In either case the resulting theorem is prefixed by \texttt{Rep};
if the function does not find $t'$ ($s'$) distinct from $t$ ($s$)
then \texttt{Unc} is returned
(in which case we say the function \emph{fails}).
The transitivity and reflexivity of \texttt{rep} 
enables direct translation between rep-conversions and rep-transformations;
the detailed implementation uses both.

We then define operators on these as follows:
\begin{description}

\item[\texttt{THENtt : (thm -> crep) * (thm -> crep) -> thm -> crep}] (infix)
applies two rep-transformations (of which the first need not succeed)
in sequence.

\item[\texttt{SUBcr : (cterm -> crep) -> cterm -> crep}] 
applies a rep-conversion to the immediate subterms of a term.
It uses previously proved rules of the form of (\ref{rep-cong})
to ``join'' the results of applying the rep-conversion 
to the subterms.

\item[\texttt{SUBtt : (thm -> crep) -> thm -> crep}]
corresponds to \texttt{SUBcr}, but is in terms of rep-trans\-formations.

\item[\texttt{REPtt : (thm -> crep) -> thm -> crep}]
repeats a rep-trans\-formation one or more times until it fails.

%\item[\texttt{TDtt, BUtt : (thm -> crep) -> thm -> crep}]
%These (and many others) can be defined easily, using the above operators.
%\texttt{TDtt} \textit{tt} 
%applies the rep-transformation \textit{tt} repeatedly wherever possible,
%proceeding through the term ``top-down'', 
%first dealing with the whole term, then the immediate subterms, and so on 
%down to the smallest subterms.
%\texttt{BU} is similar, but ``bottom-up'';
%it tries to rewrite the smallest subterms first.
%These are defined by 
%\begin{center}
%\texttt{ \noindent
%\mbox{fun TDtt tt th = (REPtt tt THENtt SUBtt (TDtt tt)) th ;} \\
%\mbox{fun BUtt tt th = (SUBtt (BUtt tt) THENtt REPtt tt) th ;}
%}
%\end{center}

\end{description}

These operators are for forward proof;
of them, \texttt{SUBtt} %, \texttt{TDtt} and \texttt{BUtt}
needs to be programmed differently for backwards proof.
%(In fact, \texttt{SUBcr} does not;
%we chose to work in terms of rep-transformations rather than rep-conversions
%because the rep-conversion analogues of
%\texttt{THENtt} and \texttt{REPtt} do require different versions for
%backward proof).

Various search strategies can now be defined easily, using the above operators.
For example, 
\texttt{TDtt} \textit{tt},
given by 
\begin{center}
\texttt{fun TDtt tt th = (REPtt tt THENtt SUBtt (TDtt tt)) th ;} 
\end{center}
applies the rep-transformation \textit{tt} repeatedly wherever possible,
proceeding through the term ``top-down'', 
first dealing with the whole term, then the immediate subterms, and so on 
down to the smallest subterms.

The following functions make rep-transformations:
\begin{description}
\item[\texttt{rep\_tt : thm -> thm -> crep}]
From a theorem $\texttt{rep} (A, B)$, \texttt{rep\_tt}
gives the rep-transformation
which transforms a theorem
$\texttt{rep} (X, A')$ to $\texttt{rep} (X, B')$,
where $A'$ and $B'$ are instantiations of $A$ and $B$.

\item[\texttt{rep\_tt\_rev : thm -> thm -> crep}]
is the corresponding function for backward proof.
%from a theorem $\texttt{rep} (A, B)$, it gives the rep-transformation
%which transforms the theorem
%$\texttt{rep} (B', X)$ to $\texttt{rep} (A', X)$,
%where $A'$ and $B'$ are instantiations of $A$ and $B$.

\end{description}

Finally, these rep-transformations can be applied in forwards or backwards
proof.
There are functions to 
apply a rep-trans\-formation to a theorem, in performing forward proof,
and to 
apply a rep-trans\-form\-ation to a subgoal as a tactic in backwards proof.
\comment{
\begin{description}
\item[\texttt{reprule : (thm -> crep) -> thm -> thm}]
applies a rep-trans\-formation to a theorem, in performing forward proof.
If $t$ is the conclusion of the theorem \textit{th},
and \textit{tt} transforms the theorem $\texttt{rep}(t, t)$ to
$\texttt{rep}(t, t')$,
then \texttt{reprule}~\textit{tt~th} gives
the theorem \textit{th} with the conclusion $t$ replaced by $t'$.
\item[\texttt{rep\_prem\_tac : (thm -> crep) -> int -> int -> tactic}]
In the course of a backwards proof,
\texttt{rep\_prem\_tac} \textit{tt pn sg}
does a similar forward inference on premise number \textit{pn}
in subgoal number \textit{sg}
using rep-trans\-form\-ation \textit{tt}.
\item[\texttt{rep\_rew\_tac : (thm -> crep) -> int -> tactic}]
applies a rep-trans\-form\-ation to a subgoal as a tactic in backwards proof.
If $s$ is the \textit{sg}'th subgoal,
and \textit{tt} transforms the theorem $\texttt{rep}(s, s)$ to
$\texttt{rep}(s', s)$,
then \texttt{rep\_rew\_tac}~\textit{tt~sg} 
gives a new proof state in which subgoal $s$ is replaced by $s'$.

\end{description}
}