\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}

The results above have been used to implement a rewriting system for LPF
in the Isabelle theorem prover.

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, 
which are not equalities, it is not possible to use
Isabelle's built-in rewriting.

The inference steps used include steps of (inter alia) the following forms 
\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 a binary propositional operator,
and 
\begin{equation} \label{repD}
\frac {\texttt{rep}(P,Q) \qquad P} Q 
\end{equation}

The Isabelle tactics select and combine these results
appropriately to give the
user the feel of a system based on standard (equality) rewriting.
Details are given in Appendix \ref{app:LPF-impl}.