% File:         /home/jrl/doc/RecFuns/recfuns.tex
% Author:       Simon Finn, Michael Fourman, John Longley
% Date:         17th August 1992
% Revised:      29 Jan 1996
% Description:  LaTeX source for article on recursive function definitions
%               (paper for Journal of Automated Reasoning?).


%%%%%%%%%%%%%%%%%%%%
%  Kluwer stuff    %
%%%%%%%%%%%%%%%%%%%%

\documentstyle[numreferences]{kluwer}    

\newcommand{\BS}{$\backslash$}
\let\oldverbatim\verbatim
\renewcommand{\verbatim}{\expandafter\small\oldverbatim}

% This document needs the KLUWER.STY file to create a document with 
% font size 11pts. 
% The title, subtitle, authors' names and institutes and date 
% are handled by the `opening' environment.


\runningtitle{Partial Functions in a Total Setting}
\runningauthor{Finn, Fourman, and Longley}

\begin{opening}

\title{Partial Functions in a Total Setting}

% You can split the title and subtitle by putting 
% two backslashes at the appropriate place.            
\author{Simon \surname{Finn}({\tt simon@ahl.co.uk})}
\institute{Abstract Hardware Limited, Uxbridge, Middlesex.}
\author{Michael P. \surname{Fourman}\thanks{Also of Abstract Hardware Limited} ({\tt M.Fourman@ed.ac.uk})}
\author{John \surname{Longley} ({\tt jrl@lfcs.ed.ac.uk})
 }
\institute{The University of Edinburgh, Edinburgh, UK. \thanks{We are grateful to SERC and DTI for support (grants GR/F31199 and GR/F35890).}}

%\date{}

% Gives you the possibility to enter a date. If you leave the
% space between the curly braces empty, no date is printed.

\end{opening}

\begin{ao}
  Abstract Hardware Limited,\\
  Building 2,
  Brunel Science Park,\\
  Uxbridge UB8 3PQ\\
  \\
  Laboratory for the Foundations of Computer Science,\\
  The University of Edinburgh, James Clerk Maxwell Building,\\
  King's Buildings, Mayfield Road,\\
  Edinburgh EH9 3JZ
\end{ao}

\setcounter{secnumdepth}{2}
%\renewcommand{\theenumi}{\it (\roman{enumi})}


% typewriter text:
\newcommand{\fm}[1]{\mbox{\tt #1}}
% Old: \newcommand{\fm}[1]{{\tt #1}}

\newcommand{\emph}[1]{{\em #1\/}}
\newcommand{\texttt}[1]{\mbox{\tt #1}}

% my environments for producing numbered lists:
\newcounter{mycount}

\newenvironment{romanlist}%
{\begin{list}%
       {(\roman{mycount})}%
       {\usecounter{mycount}} }%
{\end{list}}

\newenvironment{spacyromanlist}%
{\begin{list}%
       {(\roman{mycount})}%
       {\usecounter{mycount}
        \setlength{\itemsep}{2.0\itemsep}
} }%
{\end{list}}

% horizontal space used in quoted formulae:

\newcommand{\spc}{\hspace*{3.0em}}

% environment used for definition of <<_>>:
\newenvironment{clause}%
{\begin{tabbing} \samepage
 \fm{$\ll $ f $e_{1}~\ldots ~e_{k} \gg \; $} 
 \=  $= \; $ \= \kill}%
{\end{tabbing}}


% the tokens /\, \/ in typewriter font
\newcommand{\And}{\fm{/\char`\\ } }
\newcommand{\Or}{\fm{\char`\\ /} }


% true, false etc. in math mode
\newcommand{\true}{\mbox{\em true\/}}
\newcommand{\false}{\mbox{\em false\/}}
\newcommand{\bool}{\mbox{\em bool\/}}
\newcommand{\chose}{\mbox{\em choose\/}}


% semantic brackets (for use within math environments)
\newcommand{\lsem}{[\hspace{-0.13em} [\,}
\newcommand{\rsem}{\, ]\hspace{-0.13em} ]}
\newcommand{\sem}[1]{\lsem #1 \rsem}
% Old:
% \newcommand{\lsem}{[\! [\,}
% \newcommand{\rsem}{\, ]\! ]}


% total and partial arrows
\newcommand{\arrow}{\rightarrow}
\newcommand{\parrow}{\rightharpoonup}
\newcommand{\isdef}{\downarrow}

\newcommand{\thetainf}{\theta_{\infty}}

% turnstile formerly used for semantic rules (forcing turnstile)
\newcommand{\turnstile}{\|\hspace{-0.45em}-}
% Previously: \newcommand{\turnstile}{\|\!\!-}


% semantic judgements
\newcommand{\interpret}[4]%
   {#1\: ; #2\:\vdash\: #3 \, \Rightarrow \, #4}

% Old version:
% \newcommand{\interpret}[4]{#1 ; #2~\;\turnstile~\lsem #3 \rsem \; = \; #4}


% semantic rules (with side-condition)
\newcommand{\semrule}[3]%
   {\raisebox{-1.7ex}{\( \displaystyle \frac{#1}{#2}~~~#3\)}}


% gap between premises of a rule
\newcommand{\gap}{~~~~~}


% empty context
\newcommand{\emptycon}{\langle \rangle}


% definedness judgements
\newcommand{\defined}[3]%
  {#1\: ; #2\:\vdash\: #3 \isdef}


% theorem-like environments
\newtheorem{proposition}{Proposition}
\newtheorem{definition}[proposition]{Definition}
\newtheorem{lemma}[proposition]{Lemma}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}


\begin{abstract}  

We discuss a scheme for defining and reasoning about partial recursive
functions within a classical two-valued logic in which all terms
denote.
%Our approach is motivated by considerations relevant to mechanical 
%theorem-proving.
We show how a total extension of the partial function introduced by a
recursive declaration may be axiomatised within a classical logic, and
illustrate by an example the kind of reasoning that our scheme
supports.  By presenting a naive set-theoretic semantics, we show that
the system we propose is logically consistent.
%We discuss some of the
%practical advantages and limitations of our approach in the context of
%mechanical theorem-proving.
Our work is motivated largely by the pragmatic issues arising from
mechanical theorem-proving---we discuss some of the practical benefits
and limitations of our scheme for mechanical verification of software and
hardware systems.
%We discuss the practical advantages that our scheme offers in the context
%of mechanical theorem-proving---our work is motivated largely by these
%pragmatic considerations.

\end{abstract}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}


% various approaches to recursive fn defs in thm provers

Partial functions appear ubiquitously in formal descriptions of computer
systems. They arise, for example, in connection with non-terminating programs
or programs that terminate exceptionally, and in situations where we are
interested in the behaviour of a function only on some restricted set of 
argument values. 
Partial functions also arise frequently in specification formalisms such as
the `Z' notation \cite{zed}. 
%Moreover, widely-used specification formalisms such as `Z' \cite{zed} 
%admit the definition of partial functions.
Partial functions arise because we want to declare functions using
general recursive definitions, which don't automatically guarantee
totality.  So an important problem is to find a logic in which we can
reason about these functions conveniently but safely.
%
This turns out to be surprisingly hard---if 
$x$ denotes a value outside the intended domain of a function $f$, then
the treatment of the term $f(x)$ is problematic.
Several approaches to this problem have previously been proposed---%
for a useful survey see \cite{cliff}.

%Finding a suitable logic for partiality becomes a particularly important issue
%in the design of mechanical theorem-provers or proof-assistants.
%We would like a theorem-prover to satisfy the competing requirements 
%of logical soundness, expressive power and ease of reasoning---these factors
%all depend to a large extent on the logic we choose to implement.
%Existing theorem-provers display a wide variety of approaches,
%each with their strengths and weaknesses. 
%For example:

The choice of a logic is a crucial issue in the design of mechanical
theorem-provers or proof assistants: we would like a logic that satisfied the
competing requirements of logical soundness, expressive power and ease of 
reasoning.
The logics used in existing theorem-provers exhibit various strengths and
weaknesses, and display a range of attitudes towards the problem of partial
functions.
For example:

\begin{romanlist}

\item
We can restrict ourselves to reasoning about {\em total\/} functions, and so
ignore the problem completely.
% this bypasses the logical difficulties completely. 
In the HOL system \cite{hol}, for instance, only primitive recursive
definitions are allowed---a function declaration will thus be legal only if 
it can be shown by a simple syntactic check to define a total function.
This certainly makes the logic simple, but we might hope for greater 
expressive power.
Some other theorem-provers, such as the Boyer-Moore
\cite{boyer} and LEGO \cite{lego} systems, allow more general
function definitions, but the user is required to prove theorems 
guaranteeing their totality.
%This is a useful facility, though one may argue that the need to
%prove such a theorem in advance imposes an undesirable methodological
%constraint on the user.


\item
We can incorporate {\em subtyping\/} into our type discipline---given
a partial function on some type $\tau$, we can regard its domain as a
subtype $\sigma$ of $\tau$.  Elements of $\sigma$ may then be
construed also as elements of $\tau$.  This is the approach taken in
the EHDM proof environment \cite{ehdm}, \cite{pvs}.  This approach
offers considerable expressive power, though it has the disadvantage
that our type system will become undecidable if the allowed function
definitions are sufficiently general.  In the EHDM system, for
instance, the user sometimes has to discharge a proof obligation in
order to show that a term is well-typed.

\item  
We can incorporate the notion of partiality into the logic itself, by using
a logic that takes account of possibly non-denoting terms. 
Examples of such logics include 
\begin{itemize}
\item
Scott's Logic of Computable Functions, used as the basis of the LCF proof 
system \cite{lcf};
\item
the three-valued Logic of Partial Functions, LPF \cite{lpf}, 
used in VDM \cite{vdm}
and implemented in the Mural system \cite{mural};
\item
the Logic of Partial Elements, LPE \cite{scott}, used in earlier versions 
of the LAMBDA theorem-prover \cite{lambda3.2};
\item
the partial functions version, PF, of Church's simple type theory used
in the IMPS proof system \cite{farmer}.
\end{itemize}
These logics are all very expressive, and they all have in common the notion
that only certain well-formed terms or formulae are ``defined''. 
However, in each of them, some of the familiar logical rules are
complicated by extra ``definedness'' premises. 
Much time and effort may be expended in propagating and discharging these, 
even when we are reasoning only about total functions. 
For instance, in LPE there is a special
{\em existence predicate\/} E\,; and we need to prove that E $t$ holds 
in order to deduce $P(t)$ from $\forall x.\,P(x)$.
%\begin{quote} \begin{verbatim}
%forall x. P(x)  |-  P(f 0)
%\end{verbatim} \end{quote}
%unless we know that \fm{E(f 0)} holds.

%One candidate for this is
%the Logic of Partial Elements \cite{scott}. 
%(This was used as the basis of earlier versions of the LAMBDA theorem-prover
%\cite{lambda3.2}.) The main feature of this logic is a special {\em existence
%predicate}\, \fm{E x}, to be thought of as meaning ``\fm{x} exists'' 
%or ``\fm{x} is defined''. This system is extremely expressive, 
%but rather cumbersome to use in practice---much time and
%effort is expended in discharging and propagating tedious existence 
%conditions, even when we are dealing only with total functions.
%Besides, this particular logic has a somewhat unfamiliar feel:   
%for example, we cannot prove the theorem
% is this example strictly relevant?
% ? mention LCF, the ``classical counterpart'' to LPE.

\end{romanlist}

% we suggest another approach - analogy with @ in HOL

In this article we discuss yet another approach, one that combines the
practical benefits of a familiar logic, expressive flexibility, and
decidable type-checking. The basic idea is as follows: we regard a
function application $f(x)$ as {\em always defined\/}, but if $x$ is
outside the intended domain of $f$ we will not be able to prove
anything about its value.  In this case we may think of $f(x)$ as an
arbitrary or ``random'' value of the appropriate type.  There is an
analogy here with the Hilbert choice operator $\epsilon$, familiar to
users of HOL and LAMBDA as \fm{@} and \fm{any} respectively: if $\tau$
is any inhabited type, then $\epsilon x\! :\! \tau.\, \false$
represents an arbitrary value of type $\tau$. Similarly, in our
treatment, \fm{hd~[ ]}, (where \fm{hd} takes the head of a list),
represents an arbitrary value of the appropriate type.  However, this
expression has the same logical status as any other
expression---hence, for example, the theorem
\[ \vdash \fm{hd~[ ]} = 5 \; \vee \;  \fm{hd~[ ]} \neq 5 \]
is provable, even though neither 
$\vdash  \fm{hd~[ ]} = 5$ nor $\vdash  \fm{hd~[ ]} \neq 5$ is provable.

% structure of rest of article etc.

This approach to the semantics of partiality has been proposed previously by
Abrial, in the context of `Z' (see \cite{zed}, Section~4.3). 
Our goal in this paper is to develop this idea to give a semantics for 
recursively defined functions, and to show how such functions can be 
axiomatised within a conventional classical logic. 
Our motivation is pragmatic rather than philosophical---our aim is not to
offer the most satisfactory ``ontology'' of partial terms, but to address some
of the issues that arise in the implementation and use of theorem-provers.
We believe our approach has several practical advantages over the others 
outlined above.

%Our motivation is pragmatic rather than philosophical---we 
%do not claim that this approach provides the most natural ``ontology''
%of partial terms, but merely that it offers a simple
%treatment of general function declarations that has many practical advantages.

The rest of the article is structured as follows.
%
In Section~\ref{sec-examples} we introduce the basic idea with the help of 
examples, and illustrate the kind of reasoning that our scheme supports.
This section presents the scheme as it would appear to the user 
of a theorem-prover.
Such a user should also be aware of the
limitations highlighted in Section~\ref{sec-remarks}.
%
In Section~\ref{sec-axioms} we give the formal details of how, given a
general (partial) function definition, we may syntactically generate
logical rules to axiomatise a total extension of the function.  (From
a formalist point of view, such axioms specify the ``meaning'' of the
function definition in that they determine precisely what can and
cannot be proved about the function.)  This section contains what the
builder of a theorem-prover would need to know in order to implement
our scheme, (which has been implemented in LAMBDA theorem-prover
\cite{lambda4.0}).
%
In Section~\ref{sec-semantics} we present a naive and intuitive 
set-theoretic semantics for our function definitions and axioms.
This section is addressed to the logician who seeks assurance 
that the scheme is logically consistent.
Furthermore, such a semantics helps to clarify
the ``intended meaning'' of the function definitions, and provides
reassurance that the axioms say the things one would expect.
In Section~\ref{sec-remarks} we mention some advantages, subtleties,
and potential pitfalls associated with our scheme.
%,we draw together a few loose ends, and discuss
%some of the advantages and limitations of our approach.
%we mention some possible pitfalls
%associated with our scheme, and briefly indicate some 
%areas where there is scope for further work. % wait and see!


% LAMBDA implementation


% acknowledgements

The authors would like to thank Matt Fairtlough and Wesley Phoa for their
valuable input during discussions on this work, and Cliff Jones for his
perceptive and helpful comments.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Examples}
\label{sec-examples}

We begin with some concrete examples.  These should convey the basic
ideas, and should help to motivate the more technical discussions of
Sections~\ref{sec-axioms} and \ref{sec-semantics}.

Our goal is to show how general function definitions can be
incorporated into a theorem-prover for classical higher-order logic.
For the kind of theorem-prover we have in mind, a user may enter a
function declaration,\footnote{Throughout this paper we use an
ML-style syntax compatible with LAMBDA v 4.2.1.}  and the system will
respond by introducing logical theorems or rules axiomatising its
behaviour. Primitive recursive functions are unproblematic; we can
introduce a function constant satisfying the recursion equations.

Consider the following definition of the sorting function
{\em quicksort\/}:

\begin{quote} \samepage \begin{verbatim}
fun quicksort [ ]       = [ ]
  | quicksort (h :: t)  =
      case partition h t of
        (before, after) => 
          quicksort before @ [h] @ quicksort after;
\end{verbatim} \end{quote}
%
Here we are assuming that we have already defined a suitable function 
\fm{partition} (this is primitive recursive and hence total), 
and that we have managed to prove the following theorem:

\begin{quote} \samepage \begin{verbatim}
partition h t = (before, after)  |- 
   length before <= length t  /\  length after <= length t
\end{verbatim} \end{quote}
%
Given the \fm{quicksort} definition, the system will introduce a
constant \fm{quicksort} to denote the function defined, \emph{plus} an
auxiliary predicate \fm{DOM'quicksort}.  The expression
\fm{DOM'quicksort x} will be used to mean that \fm{x} lies within the
intended domain of \fm{quicksort} -- the declaration determines the
value of \fm{quicksort x} for such \fm{x}, or (more loosely) the
function application \fm{quicksort x} is guaranteed to ``terminate''.
The system will then generate axioms stipulating that, for arguments
satisfying \fm{DOM'quicksort}, the function \fm{quicksort} obeys its
defining clauses.  For arguments not satisfying \fm{DOM'quicksort} we
say nothing about the result.

Each clause of the definition will in fact generate one axiom for 
\fm{quicksort} and one for \fm{DOM'quicksort}. 
The first clause will generate the two axioms:

\begin{quote} \begin{verbatim}
DOM'quicksort([ ])  |-  quicksort [ ] = [ ]

|-  DOM'quicksort([ ]) = TRUE
\end{verbatim} \end{quote}
%
and the second clause will generate the axioms:

\begin{quote} 
{\samepage \begin{verbatim}
DOM'quicksort(h :: t)  |-
    quicksort(h :: t)  =
      case partition h t of
        (before, after) => 
          quicksort before @ [h] @ quicksort after
\end{verbatim} } 
%
{\samepage \begin{verbatim}
|-  DOM'quicksort(h :: t) =
      forall before, after.
        (before, after) = partition h t ->>
          DOM'quicksort(before) /\ DOM'quicksort(after)
\end{verbatim} } \end{quote}
%
% theorems provable
%
In this particular case it so happens that the function we have defined is 
{\em total\/}---the quicksort algorithm always terminates.
The above axioms (together with the theorem for \fm{partition}) 
are enough to allow a user to prove the following theorem:

\begin{quote} \begin{verbatim}
|-  forall k. DOM'quicksort(k)
\end{verbatim} \end{quote}
%
Once we have proved this theorem, we can use it to ``prune'' the
above axioms, so that we need never refer to the \fm{DOM} predicate again.
We could also prove theorems asserting that the list returned by
\fm{quicksort} is indeed sorted, or that the function \fm{quicksort} is
identical to the function defined by some other sorting algorithm:

\begin{quote} \begin{verbatim}
|-  forall k. sorted (quicksort k)

|-  forall k. quicksort k = othersort k
\end{verbatim} \end{quote}

% advantage over E predicates. Perhaps improve/revise if e.g. LPF is above.

Of course, we do not expect the machine to be able to deduce this
automatically from the syntactic form of the declaration -- although
there is scope for tactics to automate such reasoning for common
patterns of recursion.

Our scheme also allows us to declare genuinely partial functions in
exactly the same way. For example, declaring the difference function
\begin{quote} \begin{verbatim}
fun diff x y = if x = y then 0 else 1 + diff (x + 1) y;
\end{verbatim} \end{quote}
generates the axioms
\begin{quote} \begin{verbatim}
DOM'diff#(x,y) |-
    diff x y = if x = y then 0 else 1 + diff (x + 1) y

|- DOM'diff#(x,y) = (x = y = false ->> DOM'diff#(x + 1,y))
\end{verbatim} \end{quote}
We can then prove that
%
\begin{quote} \begin{verbatim}
|-  DOM'diff#(x,y) = x <= y
\end{verbatim} \end{quote}
%
and that
%
\begin{quote} \begin{verbatim}
x <= y |- x + diff x y = y
\end{verbatim} \end{quote}


Of course, there are simpler ways to tackle this example. A more
experienced proof hacker might define \fm{diff} as follows:
%
\begin{quote} \begin{verbatim}
fun diff 0 y         = y
  | diff (S x) (S y) = diff x y 
\end{verbatim} \end{quote}
%
Our scheme then gives the more immediately useful axioms
%
\begin{quote} \begin{verbatim}
|- diff 0 y = y

|- diff (S x) (S y) = diff x y
\end{verbatim} \end{quote}
%
Because we use primitive recursion, all \fm{DOM} predicates can be optimised
away automatically.

The \fm{DOM} predicate does duty for the \fm{E} predicate of LPE (for
instance), and in the case of a genuinely partial function we would
still expect to have to spend time propagating and discharging
\fm{DOM} conditions.  Notice the gains, however: for total functions
we can prove totality once for all and then forget about the \fm{DOM}
predicates (as above); and even for partial functions we only need the
\fm{DOM} predicates for reasoning that depends specifically on the
{\em value\/} of a function application.  Thus, for instance, we can
prove the theorem
%
\begin{quote} \begin{verbatim}
forall x. P(x)  |-  P(f 0)
\end{verbatim} \end{quote}
%
without mentioning the predicate \fm{DOM'f} at all. Moreover, we have retained
the familiarity and simplicity of (two-valued) classical logic. (For a
discussion of some possible drawbacks of our approach, see Section~5.3.)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Axiomatising partial functions}
\label{sec-axioms}
% (distilled from the description in the LAMBDA logic manual.)

In this section we describe in detail the general procedure whereby
the axiomatisation of a function can be derived syntactically from its
declaration (we want the theorem-prover to be able to do this
automatically). We here assume that, as in HOL or LAMBDA, we are
reasoning only about non-empty {\em well-founded\/} datatypes, which
may be modelled semantically as free algebras -- thus we exclude from
consideration certain ML types such as

\begin{quote} \begin{verbatim}
datatype d = D of d -> d
\end{verbatim} \end{quote}

% new paragraph?
Suppose the general form of a legal function declaration to be
%
\begin{quote} \samepage
\begin{tabbing}
\fm{fun}   \=  \fm{f $pat_{11}~\ldots ~pat_{1n}~$} \= $=~exp_{1}$      \\
\verb.  |. \>  \fm{f $pat_{21}~\ldots ~pat_{2n}~$} \> $=~exp_{2}$      \\
           \>  $\cdots $                                               \\
\verb.  |. \>  \fm{f $pat_{m1}~\ldots ~pat_{mn}~$} \> $=~exp_{m}$
\end{tabbing}
\end{quote}    % perhaps columns would be better?
%
where the $pat_{ij}$ are ML-style patterns (which may contain
variables), and the $exp_{i}$ are expressions of higher-order logic.
There is no notion of sequential execution here, so the order of the
clauses should not matter; hence we stipulate that no two clauses may
possess overlapping patterns. However, we do {\em not\/} require that
the patterns should be exhaustive. Moreover, there is no restriction
on the ways in which \fm{f} can occur in the $exp_{i}$. (This is in
contrast to primitive recursion, for instance, where \fm{f} may only
take arguments that are syntactically ``smaller'' than the
corresponding LHS patterns.) We permit all partial recursive function
definitions.
% question re incompleteness.

% introducing DOM'f 

Given a declaration of this form, we introduce an auxiliary predicate
\fm{DOM'f}. We then use each of the $m$ clauses of the definition to
produce one axiom for \fm{f} and one axiom for \fm{DOM'f}.  We can
think of \fm{DOM'f $x_{1}\ldots x_{n}$} as meaning (very
roughly)\footnote{This informal interpretation of \fm{DOM'f} is
reasonable only when all calls to previously-defined functions also
terminate.  The semantics of Section~4 gives a precise
interpretation for \fm{DOM'f}. See Section~5.3 for further discussion
of the differences between our \fm{DOM} predicates and termination in
Standard ML.}  that the function application \fm{f $x_{1}\ldots
x_{n}$} is guaranteed to terminate. A better intuition is that the
\fm{DOM} predicate characterises those arguments for which the value
of the function is determined.  Our axiomatisation of \fm{f} is
incomplete in that we say nothing about the values of the function for
other arguments.  Providing the predicate \fm{DOM'f} holds, we can
reason about the value of the function call by using the corresponding
clause of the definition. By contrast, if the function call does {\em
not\/} terminate then it is not possible to reason about the value;
our semantics assigns an arbitrary value to the result. This is how we
avoid paradox in the case of functions such as
%
\begin{quote} \begin{verbatim}
fun g x = g x + 1
\end{verbatim} \end{quote}

% form of the axioms

The axioms for \fm{f} simply say that the function obeys its defining clause
on all arguments for which it is known that the function call terminates:
for each $1 \leq i \leq m$ we have an axiom
%
\begin{quote} \begin{tabbing}
\fm{DOM'f($pat_{i1}, \ldots ,pat_{in}$)~~|-~
        f $pat_{i1}~\ldots ~pat_{in}$ = $exp_{i}$} \` (\dag)
\end{tabbing} \end{quote}
%
The axioms for \fm{DOM'f} give conditions on $x_{1},\ldots ,x_{n}$ that are 
sufficient to guarantee that \fm{f $x_{1}~\ldots ~x_{n}~$} will terminate. 
To specify how the form of these axioms is determined, 
we need to give a syntactic way of transforming an expression $exp$ into 
a formula $\ll exp \gg $ -- informally, we think of $\ll exp \gg $ as meaning 
``the evaluation of $exp$ is guaranteed to terminate''.
We then take as our axioms for \fm{DOM'f} the equations

\begin{quote} \begin{tabbing}
\fm{|-~~DOM'f($pat_{i1}, \ldots  ,pat_{in}$) = 
        $\ll exp_{i} \gg $} \` (\ddag)
\end{tabbing} \end{quote}
for $1 \leq i \leq m$.
\footnote{In both these sets of axioms, all atoms occurring in the 
$pat_{ij}$ are considered as free variables. For simplicity, we assume that the
theorem-prover is able to distinguish these from {\em constants\/} 
which may have the same name.} We choose to use equality here, rather than the
implication
\begin{quote} \begin{tabbing}
\fm{|-~~$\ll exp_{i} \gg~ \rightarrow$~DOM'f($pat_{i1}, \ldots  ,pat_{in}$)}
\end{tabbing} \end{quote}
for pragmatic reasons: we want to use rewriting to eliminate \fm{DOM}
predicates.

%  (OLD:)
%where $\ll exp_{i} \gg $ means the result of processing $exp_{i}$ 
%according to the rules given below---it may be loosely translated as the
%predicate ``all calls to \fm{f} within the expression $exp_{i}$ terminate''.

% freedom in defining <<_>>

There are many different ways in which $\ll \_ \gg $ could be defined,
depending on how we wished to interpret the phrase ``is guaranteed
to terminate''. Firstly, whether a given call terminates might 
depend on semantic choices---for instance,
on whether we are thinking of call-by-name or call-by-value semantics.
Secondly, we must decide how to interpret
``termination'' for non-executable logical constructs such as quantifiers.
Finally, we do not insist that the \fm{DOM} predicate represents a
{\em necessary\/} condition for termination---%
we thus have some freedom in deciding how much of the termination behaviour
we want to capture. (We discuss this point more fully in Section~5.3.)
%\footnote{In the case of higher-order functions, for instance, 
%necessary and sufficient \fm{DOM} predicates seem hard to axiomatise.}
The definition below illustrates one way of responding to these issues.
However, the same idea applies to other variants, 
and indeed to logical constructs other than those we consider here.

% OLD:
%In Section~\ref{sec-semantics} we make explicit the particular semantic we
%have chosen to work with. But there is nothing special about this choice,
%nor about the particular selection of logical constructs we consider---the 
%same idea applies to other extensions and other variants.

We define the operator $\ll \_ \gg$ inductively on terms of our logic
as follows:\footnote{In applying these clauses to generate the axioms
for the examples in Section~\ref{sec-examples}, we have taken the
liberty of ``optimising out'' a few redundant conjuncts.}

% definition of <<_>>

\begin{spacyromanlist} 

\item
Atomic expressions other than occurrences of \fm{f} always terminate.
Thus if $x$ is any atom other than \fm{f}:%
%
\begin{quote}
$ \ll x \gg~=~\fm{TRUE} $
\end{quote}
%
% old:
%\begin{eqnarray*}
%  \ll x \gg  & = & \fm{TRUE}
%\end{eqnarray*}


\item
For each occurrence of \fm{f}, we generate a call to \fm{DOM'f}. If the
occurrence of \fm{f} is not ``fully applied'', then we introduce extra,
universally quantified, variables for the missing arguments. Thus for
$0 \leq k \leq n$:%
%
\begin{quote}
$ \ll \fm{f } e_{1}~\ldots~e_{k} \gg~= \\
\spc \ll e_{1} \gg~\And \ldots\ \And~\ll e_{k} \gg~\And \\
\spc \fm{forall}\; x_{k+1}, \ldots ,x_{n}.\;
          \fm{DOM'f(}e_{1}, \ldots ,e_{k},x_{k+1}, \ldots ,x_{n}\fm{)} $
\end{quote}
%
% old:
%\begin{eqnarray*}
%  \ll \fm{f } e_{1}~\ldots~e_{k} \gg  & = & 
%      \ll e_{1} \gg~\And \ldots\ \And~\ll e_{k} \gg~\And     \\
%  & & \fm{forall}\; x_{k+1}, \ldots ,x_{n}.\;
%         \fm{DOM'f(}e_{1}, \ldots ,e_{k},x_{k+1}, \ldots ,x_{n}\fm{)}
%\end{eqnarray*}


\item
Other function applications are treated ``structurally''.% 
\footnote{One case deserves special mention: if $e'$ is \fm{f},
the condition we obtain here is stricter
than, say, termination of the corresponding ML program.} 
Thus, for $e$ not of the form \fm{f $e_{1}~\ldots~e_{k}$} for $k<n$:
%
\begin{quote}
$ \ll e~e' \gg~=~\ll e \gg~\And~\ll e' \gg $
\end{quote}
%
% old:
%\begin{eqnarray*}
%  \ll e~e' \gg  & = & \ll e \gg~\And~\ll e' \gg
%\end{eqnarray*}


\item
Case expressions are treated in a way which takes account of the ``flow of
control'' within the expression. (Here, for simplicity, the patterns in a 
\fm{case} construct are assumed to be non-overlapping and exhaustive.%
\footnote{Exhaustiveness is not essential and is not required in the LAMBDA
implementation. We impose it since it simplifies our presentation of the 
semantics.})
%
\begin{quote}
$ \ll \fm{case } e \fm{ of } p_{1} \fm{ => } e_{1} 
                   \fm{ |\ldots | } p_{k} \fm{ => } e_{k} \gg~= \\
\spc \ll e \gg~\And  \\
\spc \fm{(forall}\;\overline{x_{1}}.~
                   p_{1}~=~e \fm{ ->> } \ll e_{1} \gg \fm{)}~\And  \\
\spc \cdots  \\
\spc \fm{(forall}\;\overline{x_{k}}.~
                   p_{k}~=~e \fm{ ->> } \ll e_{k} \gg \fm{)} $
\end{quote}
%
% old:
% \begin{eqnarray*}
%  \lefteqn{\ll \fm{case } e \fm{ of } p_{1} \fm{ => } e_{1} 
%                    \fm{ | \ldots | } p_{k} \fm{ => } e_{k} \gg~~=}
%  \hspace{9.0em}                                                     \\
%   & & \ll e \gg~\And                                                \\
%   & & \fm{(forall}\;\overline{x_{1}}.~
%            p_{1}~=~e \fm{ ->> } \ll e_{1} \gg \fm{)}~\And           \\
%   & & \cdots                                                        \\
%   & & \fm{(forall}\;\overline{x_{k}}.~
%            p_{k}~=~e \fm{ ->> } \ll e_{k} \gg \fm{)}
%\end{eqnarray*}
% 
where $\overline{x_{i}}$ stands for all the variables occurring in the
pattern $p_{i}$.


\item
A variable-binding expression is considered to terminate iff the body of
the expression terminates for all values of the bound variable. Thus:%
%
\begin{quote}
$ \ll Q\, x.~e \gg~=~\fm{forall }x.~\ll e \gg $
\end{quote}
%
% old:
%\begin{eqnarray*}
%  \ll Q\, x.~e \gg  & = & \fm{forall }x.~\ll e \gg
%\end{eqnarray*}%
%
where $Q$ is any binder (i.e.\ \fm{forall}, \fm{exists}, \fm{fn}, \fm{any}).
(Note that this corresponds to a very strict interpretation of the binders.
More generous versions are also possible, see Section~5.1.)

\item
Other expressions are treated structurally---we simply conjoin together the
\fm{DOM} calls from the various subexpressions. For example:%
%
\begin{quote}
$ \ll \; \fm{(} e \fm{,} e' \fm{)} \; \gg~=~\ll e \gg~\And~\ll e' \gg $
\end{quote}
%
% old:
%\begin{eqnarray*}
%  \ll \; \fm{(} e \fm{,} e' \fm{)} \; \gg  & = & \ll e \gg~\And~\ll e' \gg
%\end{eqnarray*}

\end{spacyromanlist}


% PS on mutual recursion

\vspace{0.5ex}
Note that clauses (ii) and (iii) embody the choice of {\em
applicative-order\/} (call-by-value) semantics.  The above scheme can
be extended in an obvious way to cover {\em mutually\/} recursive
functions---% we have one \fm{DOM} predicate for each function, and
each mutually recursive function call generates a call to the
corresponding \fm{DOM} predicate.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Set-theoretic semantics}
\label{sec-semantics}

% two reasons for wanting semantics

We now outline a semantics for our system. As mentioned earlier, there are
at least two reasons for wanting to do this---to establish the consistency
of our scheme, and to provide a framework for thinking about our functions
and axioms in an intuitive way. The consistency is by no means obvious---%
there certainly are some logical principles that do apply to non-terminating
function calls, and we might be worried that these might allow us to deduce
more than we really intend in the case of some pathological function 
definition.
% OLD:
% there are certainly some modes of reasoning that do apply to
% non-terminating function calls, so we may worry that for
% some subtle kinds of ``paradoxical'' function definition it might be possible
% to prove more about them than we intend. 
%
We prove that our system actually is consistent by interpreting
our function definitions in some model, and checking that the corresponding
axioms are valid under this interpretation (and that our rules of inference
are sound).

% naivety of model

Our model is very elementary and purely set-theoretic---it allows us
to think of a type simply as a set, and a term of that type as a
member of the set. A function definition is then interpreted by just
an ordinary function between sets---the \fm{DOM} predicate is modelled
by (the characteristic function of) a subset of its domain.  In our
view, it is a virtue of our logic that it can be modelled without
using any domain theory or category theory. Our contention is that
such a logic will be more easily grasped by a non-specialist than a
logic for which the models are necessarily mathematically abstruse.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Interpretation of types}

The interpretation $\lsem \_ \rsem $ for the types
of our logic is defined inductively as follows.

\begin{romanlist}

\item
The basic types are interpreted as sets in the obvious way, e.g.\
\begin{quote} \samepage \begin{tabbing}
$ \lsem t\, \fm{->} \, t' \rsem~$ \= $=~$ \=  \kill
$ \lsem \! \fm{bool} \! \rsem $ \> $=$ \> $\{ \true , \false \}$  \\
$ \lsem \! \fm{nat}  \! \rsem $ \> $=$ \> $\{ 0,1,2,\ldots \}$
\end{tabbing} \end{quote}

\item
Function types are interpreted by set-theoretic {\em total\/} function spaces:
\begin{quote}
$ \lsem t\, \fm{->} \, t' \rsem~=~\sem{t} \arrow \sem{t'} $
\end{quote}

\item
Product types are interpreted by cartesian products:
\begin{quote} \begin{tabbing}
$ \lsem t\, \fm{->} \, t' \rsem~$ \= $=~$ \=  \kill
$ \lsem t\, \fm{*} \, t' \rsem $ \> $=$ \> $ \sem{t} \times \sem{t'} $
\end{tabbing} \end{quote}
Similarly for other
ways of forming new non-empty types (sums, quotients, 
non-empty subtypes etc.)

\item
Inductive datatypes are interpreted by sets constructed as free algebras---%
we omit the easy details. (In fact, we can allow any ways of defining 
types that have natural interpretations as non-empty sets, e.g.\ inductive
types modulo equational constraints.)

\end{romanlist}


% bool = om

Henceforth we will identify the booleans with the truth-values in
our (classical) meta-logic, so that for instance we write \mbox{$(u=v)$}
in place of the expression
\[ \left \{ \begin{array}{ll}
              \true  & \mbox{if $u=v$} \\
              \false & \mbox{otherwise}
            \end{array}
   \right. \]


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Interpretation of terms}

% explain use of judgements. Envt E, extra envt F.

We will define the interpretation of a term $e$ in an environment $E$ (that is,
a finite function that assigns interpretations to all the constants and
free variables appearing in $e$).
For convenience, we assume here that our logic is {\em explicitly typed\/}---%
all constants and free variables have some specific type, and
all variable-bindings carry explicit type annotations.
We say that an environment $E$ is {\em well-typed\/} if for all
\mbox{$x \in \mbox{dom}~E$} we have \mbox{$E(x) \in \lsem t \rsem $},
where $t$ is the type of $x$.

In fact, for the interpretation of function
definitions, we need both an environment $E$ and a 
{\em function-environment\/} $F$,
whose role is explained in Section~4.3. We use the notation
\[ \interpret{E}{F}{e}{v} \]
to mean ``$v$ is the interpretation of $e$ in environment $E$ 
and function-environment
$F$''. This notation allows us to present the semantics in an ``operational''
style by means of inference rules.
The following rules define interpretations for all well-typed expressions 
other than those occurring as part of a function definition.
(Note that $F$ plays no active role in any of these rules.)


% semantic rules for terms

\begin{spacyromanlist}

\item
\( \interpret{E}{F}{\overline{n}}{n} \gap (n = 0,1,2,\ldots )
\) 
% or n \in {\Bbb N} using amssymb style option.

\noindent where $\overline{n}$ is the numeral for $n$.
Similarly for the other basic types.

\item
\( \interpret{E}{F}{x}{E(x)} \gap (x \in \mbox{dom}~E;~x \notin \mbox{dom}~F) 
\)

\item
\semrule{\interpret{E}{F}{e}{v} \gap \interpret{E}{F}{e'}{v'}}%
        {\interpret{E}{F}{\fm{(} e \fm{,} e' \fm{)}}{(v,v')}}{}

\vspace{0.5ex}
\noindent and similarly for the term constructors for other 
type-forming operations.

\item 
\semrule{\interpret{E}{F}{e}{u} \gap \interpret{E}{F}{e'}{v}}%
        {\interpret{E}{F}{e~e'}{u(v)}}{(v \in \mbox{dom}~u)}

\vspace{0.5ex}
\noindent (we will see later that the side-condition is redundant)

\item   % compressed format to fit in such a big rule!
\semrule{\interpret{E}{F}{e}{u} ~~\interpret{E'}{F}{p_{i}}{u}
                                ~~\interpret{EE'}{F}{e_{i}}{v}}%
        {\interpret{E}{F}{\fm{case } e \fm{ of } p_{1} \fm{=>} e_{1}
                          \fm{|}\ldots \fm{|} p_{k} \fm{=>} e_{k}}{v}}%
        {\!\!\! (\mbox{dom}\,E'\! =\! FV(p_{i}))}

\vspace{0.5ex}
\noindent where $1 \leq i \leq k$, and $EE'$ means the environment in which
the bindings in $E$ are enriched (and possibly overwritten) by those in
$E'$.

\item
\semrule{\interpret{E}{F}{e}{v} \gap \interpret{E}{F}{e'}{v'}}%
        {\interpret{E}{F}{e\,\fm{=}\,e'}{(v=v')}}{}

\item
\semrule{\interpret{E}{F}{e}{v} \gap \interpret{E}{F}{e'}{v'}}%
        {\interpret{E}{F}{e\, \And \,e'}{v \wedge v'}}{} 

\vspace{0.5ex}
\noindent and similarly for the other propositional connectives.

\item
\semrule{\interpret{E(x , v)}{F}{e}{u(v)} \gap
         \mbox{for each $v \in \sem{t}$}}%
        {\interpret{E}{F}{\fm{fn }x \fm{:} t\,\fm{=>} e}{u}}%
        {(\mbox{dom}~u = \sem{t} )}
% Old:  {(\fm{x:}t~,~\mbox{dom}~u = \sem{t} )}

\item
\semrule{\interpret{E(x , v)}{F}{e}{u(v)} \gap
         \mbox{for each $v \in \sem{t}$}}%
        {\interpret{E}{F}{\fm{any }x \fm{:} t.\; e}{\chose_{t}~u}}%
        {(\mbox{dom}~u = \sem{t} )}

\vspace{0.5ex}
\noindent where for each type $t$ we have a semantic choice function 
$\chose_{t}$
% \[ \chose_{t} : (\sem{t} \arrow \bool) \arrow \sem{t}  \]
satisfying $u(choose_{t}~u) = \true $ for all $u \neq \lambda v.\false $.

\item
\semrule{\interpret{E(x , v)}{F}{e}{u(v)} \gap
         \mbox{for each $v \in \sem{t}$}}%
        {\interpret{E}{F}{\fm{forall }x \fm{:}t.\; e}{(u = \lambda v.\true)}}
        {(\mbox{dom}~u = \sem{t} )}

\vspace{0.5ex}
\noindent and dually for \fm{exists}.

\end{spacyromanlist}

% remarks and observations

\vspace{0.5ex}
% Note that in rule~(iv) the side-condition ensures that the application
% $u(v)$ always denotes.
Note that in general (viii), (ix) and (x) will be {\em infinitary\/} rules,
so our derivation trees may be infinite. (However, they will always have 
finite depth, by induction on the size of $e$.)
The following are now easy observations.

\begin{proposition}
\label{exactly-one}
\hspace*{1.0em} \\ \indent
(i) Given any well-typed environment $E$, function-environment $F$ 
and expression $e$,
where {\em dom~}$E$ contains all constants and free variables appearing 
in $e$, there is a unique value $v$ such that 
\mbox{$\; \interpret{E}{F}{e}{v} \; $}
is derivable using the above rules. \\
\indent 
(ii) If \mbox{$\; \interpret{E}{F}{e}{v} \; $} is derivable and 
$e$ has type $t$, then $v \in \sem{t} $.
\end{proposition}

\noindent {\em Proof.~~} By simultaneous induction on the structure of $e$.
If $e$ is a \fm{case} expression, then rule~(v) applies for
some unique value of $i$, since the patterns are exhaustive and 
non-overlapping. If $e$ is an application, then the side-condition in 
rule~(iv) automatically holds since, by the induction hypothesis, $u$ 
belongs to the appropriate total function space. $\Box $

\begin{definition}

If \mbox{$\; \interpret{E}{F}{e}{v} \; $} is derivable, 
we write \mbox{$\; \sem{e}_{E;F} = v\;$}.
We also write $\; \sem{e}_{E} \;$
in place of   $\; \sem{e}_{E;\emptycon}\;$, 
and           $\; \sem{e} \;$ 
in place of   $\; \sem{e}_{\emptycon ; \emptycon} \;$.

\end{definition}

\noindent
Note that, by Proposition~\ref{exactly-one}{\em (i)\/}, this defines 
$\sem{e}$ for all {\em closed\/} terms $e$.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Interpretation of functions}

% the goal

We now give the interpretation of \fm{fun} definitions. As in Section 2
we consider just a single declaration of the form
%
\begin{quote} \samepage
\begin{tabbing}
\fm{fun}   \=  \fm{f $pat_{11}~\ldots ~pat_{1n}~$} \= $=~exp_{1}$      \\
\verb.  |. \>  \fm{f $pat_{21}~\ldots ~pat_{2n}~$} \> $=~exp_{2}$      \\
           \>  $\cdots $                                 \>            \\
\verb.  |. \>  \fm{f $pat_{m1}~\ldots ~pat_{mn}~$} \> $=~exp_{m}$
\end{tabbing}
\end{quote} 
%
(mutual recursion can be dealt with similarly).
We will find it convenient to distinguish notationally between this
declaration and the function \fm{f} it declares---we thus use $\Delta$
to denote the piece of syntax constituting the above declaration.

Our goal is to give definitions of $\sem{\fm{f}}$ and $\sem{\fm{DOM'f}}$.
We regard the ``meaning'' of $\Delta$ as being given by these two components:
$ \sem{\Delta} = ( \sem{\fm{f}}\, ,\, \sem{\fm{DOM'f}} ) $.
Suppose that the $pat_{ij}$ are patterns of type $s_{j}$ and the $exp_{i}$ 
are expressions of type $t$.
Then we expect to obtain
%
\begin{quote} \begin{tabbing}
$ \sem{\fm{DOM'f}}$ \= $\, \in \,$ \=  \kill
$ \sem{\fm{f}} $    \> $\, \in \,$ \>  $ \sem{s_{1}} \arrow \ldots \arrow 
                                   \sem{s_{n}} \arrow \sem{t} $        \\
$ \sem{\fm{DOM'f}}$ \> $\, \in \,$ \>  $ (\sem{s_{1}} \times \ldots \times 
                                   \sem{s_{n}}) \arrow \bool $
\end{tabbing} \end{quote}

%\begin{eqnarray*}
%\sem{\fm{f}}     & \in & \sem{s_{1}} \arrow \ldots \arrow
%                         \sem{s_{n}} \arrow \sem{t}                 \\
%\sem{\fm{DOM'f}} & \in & (\sem{s_{1}} \times \ldots \times
%                          \sem{s_{n}}) \arrow \bool
%\end{eqnarray*}


% reducing higher-order to first-order

The first step in defining these is to transform the declaration syntactically
into a form that we call {\em first-order}. We say the declaration $\Delta$
is first-order provided every occurrence of \fm{f} in the $exp_{i}$ is
fully applied (i.e.\ occurs at the head of some subexpression 
\mbox{\fm{f}$\, e_{1} \ldots e_{n}$} ).
A general declaration $\Delta$ may be translated into a first-order one 
by eta-expanding occurrences of \fm{f} in the $exp_{i}$, i.e.\
replacing every subexpression
  \mbox{\fm{f}$\, e_{1} \ldots e_{k}$} $(0 \leq k < n)$ 
that is not itself an applicand by
%
\[ \fm{(fn }x_{k+1},\ldots ,x_{n} \fm{ => f}~e_{1}~\ldots ~e_{k}~
   x_{k+1}~\ldots ~x_{n} \fm{)}  \]
%
We write $\hat{\Delta}$ to denote the transformed declaration---we also write
$\widehat{exp_{i}}$ for the translations of the $exp_{i}$.
(Note that these depend implicitly on the atom \fm{f} and the value of $n$).
We define the meaning of a general declaration to be the same as the meaning 
of its first-order expansion: $\sem{\Delta} = \sem{\hat{\Delta}}$.%
\footnote{Thus, our semantics is as strict for \fm{fn}-expressions as it is
for their eta-reducts. This is not the case for the semantics of Standard ML,
for instance.}
For the rest of this subsection we will therefore assume that $\Delta$ 
is first-order.



% deferred explanation of function-environment

We now explain the role of the function-environment $F$ introduced earlier.
Let us write $S = \sem{s_{1}} \times \ldots \times \sem{s_{n}}$
and $T = \sem{t}$;
suppose now that we are given a set-theoretic {\em partial\/} function
\mbox{$\theta : S \parrow T$}.
We can regard $\theta$ as an ``approximation'' to (an uncurried form of) 
\fm{f}.
We express this intention by putting the pair $(\fm{f},\theta)$ in 
the function-environment.
A function-environment is thus a finite map taking function-names to partial
functions between the appropriate sets.%
\footnote{In fact, since here we are not handling mutual recursion,
we never require  $F$ to contain more than one entry.}
The idea is now to ``interpret'' \fm{f} by $\theta$.
To do this, we augment the inference rules of Section~4.2 with the rule

\vspace{0.5ex}
\[ ( \star )~~~
   \frac{\interpret{E}{F}{e_{1}}{v_{1}}~~~ \cdots ~~~
         \interpret{E}{F}{e_{n}}{v_{n}}}%
        {\interpret{E}{F}{\fm{f}~e_{1}~ \ldots ~e_{n}}%
                                    {\theta (v_{1}, \ldots ,v_{n})}} ~~~~
        (\fm{f},\theta) \! \in \! F;~~
        (v_{1}, \ldots ,v_{n}) \! \in \! \mbox{dom}\,\theta
\] 

% remarks and observations

\vspace{0.5ex}
This is the only rule that ``introduces'' partiality into the semantics---%
it assigns meanings to certain fully applied occurrences of \fm{f}
but not to others. 
There is no clash here with rule~4.2(iv) for application,
since there is no value $v$ such that 
$\interpret{E}{F}{\fm{f}~e_{1}~ \ldots~e_{n-1}}{v}\;$
because we have not assigned any independent meaning to \fm{f}. 
We can now prove the following properties:

\begin{proposition}
\label{at-most-one}
\hspace*{1.0em} \\ \indent
(i) Given any well-typed environment $E$, function-environment $F$, 
and expression $e$
(possibly containing occurrences of\/ \fm{\em f}),
there is\/ {\em at most one} value $v$ such that 
\mbox{$\; \interpret{E}{F}{e}{v} \; $} 
is derivable using the rules of 4.2 together with the rule $( \star )$. \\
\indent
(ii) If \mbox{$\; \interpret{E}{F}{e}{v} \; $} is derivable in this system, and
$e$ has type $t$, then $v \in \sem{t}$. \\
\indent
(iii) If \mbox{$\; \interpret{E}{F(f,\theta )}{e}{v} \; $} is derivable and
\mbox{$\theta ':S \parrow T$} extends $\theta $, then also
\mbox{$\; \interpret{E}{F(f,\theta ')}{e}{v} \; $} is derivable.
\end{proposition}

\noindent {\em Proof.~~}
{\em (i)\/} and {\em (ii)\/} are proved by simultaneous induction, as in
Proposition~\ref{exactly-one}. For {\em (iii)\/}, just observe that 
any valid derivation remains valid when $\theta $ is replaced everywhere 
by $\theta '$. $\Box$


% defining the operator \cal F

\vspace{2.5ex}
We now show how, given an approximation $\theta $ 
to \fm{f}, we can construct a ``next approximation'' ${\cal F}\theta $.
We suppose here that $D$ is an environment giving interpretations for all the
constants already in scope at the point of declaration of \fm{f}.

\begin{definition}
\label{F-def}
Let ${\cal F} : (S \parrow T) \arrow (S \parrow T)$ 
be defined as follows.
Given $\theta : S \parrow T$ and $(v_{1},\ldots v_{n}) \in S$,
define ${\cal F}\theta (v_{1},\ldots ,v_{n}) = w$ iff,
for some clause,
\[\fm{f} pat_{i1}~\ldots ~pat_{in}~=~exp_{i}\]
in $\Delta$, where $1 \leq i \leq m$,\\
and some environment $E$ with 
{\em dom~}$E = FV(pat_{i1},\ldots ,pat_{in})$, we have \\
\hspace*{1.5em}
(a) $\sem{pat_{ij}}_{E} = v_{j} \;$ for each $1 \leq j \leq n$;
and moreover \vspace{0.2ex}  \\
\hspace*{1.5em}
(b) $\interpret{DE}{(\fm{\em f},\theta)}{exp_{i}}{w} \;$.


%\begin{itemize}
%\item
%take ${\cal F}\theta (v_{1},\ldots ,v_{n})$ to be defined iff,
%for some $1 \leq i \leq m$ and some environment $E$ with 
%{\em dom~}$E = FV(pat_{i1},\ldots ,pat_{in})$, we have \\
%\hspace*{1.5em}
%(a) $\sem{pat_{ij}}_{E} = v_{j} \;$ for each $1 \leq j \leq n$;
%and moreover \vspace{0.2ex}  \\
%\hspace*{1.5em}
%(b) $\interpret{DE}{(\fm{\em f},\theta)}{exp_{i}}{w} \;$ for some $w \in T$;
%\item
%in this case, define ${\cal F}\theta (v_{1},\ldots ,v_{n}) = w$.

% OLD:
% \hspace*{1.5em} 
% (a) $\interpret{E}{\emptycon}{pat_{ij}}{v_{j}} \;$
% for each $1 \leq j \leq n$; and moreover \\
% \hspace*{1.5em}
% (b) $\interpret{E}{(\fm{\em f},\theta )}{exp_{i}}{w} \;$ for some $w \in T$;

\end{definition}

% Remarks justifying definition.

\noindent
Note that, in the above definition, the value of $i$ is necessarily
unique since the patterns are non-overlapping.  We think of $E$ here
as the environment generated by the pattern-matching---% the
pattern-matching process determines $E$ uniquely for the free algebras
we use to model datatypes.  Given this, it follows from
Proposition~\ref{at-most-one}{\em (i)\/} that $w$, if it exists, is
unique.

% The crucial lemma: existence of lfp.

\begin{proposition}
\hspace*{1.0em} \\ \indent
(i) If $\theta \subseteq \theta '$ then 
${\cal F}\theta \subseteq {\cal F}\theta '$, where $\subseteq$ is the
inclusion ordering on $S \parrow T$. \\
\indent
(ii) $\cal F$ has a least fixed point $\thetainf = {\cal F}\thetainf$.
\end{proposition}

\noindent {\em Proof.~~}
{\em (i)\/} follows immediately from Definition~\ref{F-def} and 
Proposition~\ref{at-most-one}{\em (iii)\/}.
{\em (ii)\/} is then an application of Tarski's fixed point theorem. 
Note that since $S \parrow T$ is not a complete lattice, we need to use
transfinite iteration to construct the least fixed point. Note also that
iteration up to $\omega$ will not in general suffice,
because of the presence of the infinitary rules. $\Box$

% Semantics of f and DOM'f

\begin{definition}
Suppose the declaration $\Delta$ is first-order. 
Then, with $\thetainf$ as above,  \\
\indent
(i) let $\sem{\fm{\em f}}$ be (the curried form of) any total function
$S \arrow T$ extending $\thetainf$;
\indent
(ii) let $\sem{\fm{\em DOM'f}} : S \arrow \mbox{bool}\;$
be the characteristic function of\/ {\em dom} $\thetainf$.
\end{definition}
%
Note that we have used only the graph ordering on $S \parrow T$
rather than any sophisticated domain ordering. Furthermore, we have not
used any notion of {\em continuity\/}---indeed the operator $\cal F$ will
not in general be continuous!


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Validity of axioms}
% also need soundness of inference rules.
% Rules for f are easy, rules for DOM harder.
% Just do a few examples?
% Do first-order first, then higher-order(?)

We must now check that the axioms discussed in Section~\ref{sec-axioms} 
are valid under the interpretation we have given. 
Recall that for each $1 \leq i \leq m$
we have an axiom (\dag) for \fm{f} and an axiom (\ddag) for \fm{DOM'f}.
We sketch the proofs that these are valid, omitting some of the details.
We use identifiers such as $\Delta$ and $\thetainf$ with the same
meanings as in Section~4.3.
Throughout this section, $F$ will denote the function-environment 
$\langle (\fm{f},\thetainf) \rangle$, and $D$ will denote the ``current
environment'' at the point of declaration.

We begin by restricting our attention to first-order declarations---later
we show that the results for the general case may be reduced to those for
the first-order case. The axioms for \fm{f} are easily shown to be valid:

%We now restrict our attention to first-order declarations. The axioms for
%\fm{f} are easily shown to be valid:

% validity of axioms for f

\begin{proposition}
Suppose $\Delta$ is first-order. Then the axioms

\begin{quote} \begin{tabbing}
\fm{\em DOM'f($pat_{i1}, \ldots ,pat_{in}$)~~|-~
        f $pat_{i1}~\ldots ~pat_{in}$ = $exp_{i}$} \` {\em (\dag)}
\end{tabbing} \end{quote}
%
for\/ \fm{\em f} are valid under the given 
interpretations of\/ \fm{\em f} and\/ \fm{\em DOM'f}.
\end{proposition}

\noindent {\em Proof.~~}
It is easily seen from the definitions of $\sem{\fm{f}}$ and $\sem{\fm{DOM'f}}$
that (\dag) is valid iff, for any environment $E$ giving interpretations 
to the pattern-variables, we have

\begin{quote}
$ (\sem{pat_{i1}}_{E}, \ldots ,\sem{pat_{in}}_{E}) 
    \;\in\; \mbox{dom}~\thetainf~~ \Longrightarrow \\
\hspace*{2.0em} \thetainf \,(\sem{pat_{i1}}_{E}, \ldots ,\sem{pat_{in}}_{E}) 
    \;=\; \sem{exp_{i}}_{DE;F} $
\end{quote}
%
But this assertion is indeed true in our model, since from 
Definition~\ref{F-def} (and the remark following it) it is easy to see that
% 
\begin{quote}
$ \sem{exp_{i}}_{DE;F}~=~
     {\cal F}\thetainf \;(\sem{pat_{i1}}_{E}, \ldots ,\sem{pat_{in}}_{E}) $
\end{quote}
(where if either side is defined then so is the other). 
$\Box$

% notation for ``[[_]]E;F is defined''

\vspace{2.5ex}
The corresponding theorem for the \fm{DOM'f} axioms is somewhat harder. 
Let us write $\;\defined{E}{F}{e}\;$ to mean
``$\,\sem{e}_{E;F}$ is defined'' (i.e.\
$\interpret{E}{F}{e}{v} \;$ for some $v$).
The following lemma says that this property 
behaves formally like the operator $\ll \_ \gg$ defined in Section~2.


% LEMMA on <<_>> and \downarrow

\begin{lemma}\label{defdom}
Let $e$ be any first-order expression (relative to \fm{\em f} and $n$),
and suppose $E$ is any environment giving interpretations to all the 
constants and free variables of $e$ (other than \fm{\em f}). 
Then $\;\defined{E}{F}{e}\;$  iff\/ $\;\sem{\ll e \gg}_{E;F} = $true.
\end{lemma}

\noindent {\em Proof.~~} By induction on the structure of $e$. We consider
only a selection of the cases.

\begin{itemize}

\item
If $e$ is an atom other than \fm{f}, then 
$\sem{\ll e \gg}_{E;F} = \true$ always; 
likewise $\;\defined{E}{F}{e}$ always since $\;\sem{e}_{E;F} = E(e)$.

\item
If $e$ is of the form $\fm{f}~e_{1}~\ldots~e_{k}$ with $k \leq n$, then $k=n$
by the assumption that $e$ is first-order. But now
\begin{eqnarray*}
\defined{E}{F}{\fm{f}~e_{1}~\ldots~e_{n}}
  & \mbox{~iff~}
    & \defined{E}{F}{e_{i}} \mbox{~~for $1 \leq i \leq n$~~and}       \\
  & & (\sem{e_{1}}_{E;F} ,~\ldots~,\sem{e_{n}}_{E;F}) \in 
      \mbox{dom}~\thetainf                                            \\
  & \mbox{~iff~}
    & \sem{\ll e_{i} \gg} = \true \mbox{~~for $1 \leq i \leq n$~~and} \\
  & & \sem{\fm{DOM'f}(e_{1},\ldots,e_{n})} = \true                    \\
% & & \hspace{2.0em} \mbox{using induction hypothesis}                \\
  & \mbox{~iff~}
    & \sem{\ll \fm{f}~e_{1}~\ldots~e_{n} \gg} = \true                 \\
  & & \hspace{2.0em} \mbox{by definition of $\ll \_ \gg$}
\end{eqnarray*}

\item
If $e$ is of the form $e'~e''$, where $e'$ is not of the form
$\fm{f}~e_{1}~\ldots~e_{k}$ with $k<n$, then by rule~(iv) of Section~4.2
we have
\begin{eqnarray*}
\hspace*{1.1em} 
\defined{E}{F}{e'~e''}
  & \mbox{~iff~}
    & \defined{E}{F}{e'}~~and~~\defined{E}{F}{e''}                    \\
  & \mbox{~iff~}
    & \sem{\ll e' \gg} = \sem{\ll e'' \gg} = \true                    \\
  & \mbox{~iff~}
    & \sem{\ll e'~e'' \gg} = \true
\end{eqnarray*}

\item
If $e$ is of the form $Q\, x.~e'$ ($Q$ a binder), then by rules~(viii) and (ix)
of Section~4.2 we have
\begin{eqnarray*}
%
% dummy line to homogenise formatting
%\defined{E}{F}{\fm{f}~e_{1}~\ldots~e_{n}}
%  & \mbox{~iff~}
%    & \sem{\ll e_{i} \gg} = \true \mbox{~~for $1 \leq i \leq n$~~and} \kill
%
\defined{E}{F}{Q\, x:t.~e'}
  & \mbox{~iff~}
    & \defined{E(x,v)}{F}{e'} \mbox{~~for all $v \in \sem{t}$} 
                                                \hspace*{0.6em}       \\
  & \mbox{~iff~}
    & \sem{e'}_{E(x,v);F} = \true \mbox{~~for all $v \in \sem{t}$}    \\
  & \mbox{~iff~}
    & \sem{\ll Q\, x:t.~e' \gg} = \true
\end{eqnarray*}

\end{itemize}

\noindent
The other cases are handled similarly using the appropriate clauses in the
definition of $\ll \_ \gg$. $\Box$

% validity of axioms for DOM'f

% \vspace{2.5ex}
\begin{proposition}
Suppose $\Delta$ is first-order.
Then the axioms

\begin{quote} \begin{tabbing}
\fm{\em |-~~DOM'f($pat_{i1}, \ldots  ,pat_{in}$) = 
        $\ll exp_{i} \gg $} \` {\em (\ddag)}
\end{tabbing} \end{quote}
%
for\/ \fm{\em DOM'f} are valid under the given
interpretations of\/ \fm{\em f} and\/ \fm{\em DOM'f}.
\end{proposition}

\noindent {\em Proof.~~}
Clearly (\ddag) is valid provided, for any environment $E$ giving 
interpretations to the pattern-variables, we have

\begin{quote}
$ (\sem{pat_{i1}}_{E}, \ldots ,\sem{pat_{in}}_{E}) 
    \;\in\; \mbox{dom}~\thetainf~~\mbox{~iff~}~~
  \sem{\ll exp_{i} \gg}_{DE;F} = \true $
\end{quote}
%
But this holds in our model, since
%
\begin{eqnarray*}
\hspace*{1.8em}
\sem{\ll exp_{i} \gg}_{DE;F} = \true
  & \mbox{~iff~}
    & \defined{DE}{F}{exp_{i}}  \hspace{1.0em} \mbox{by Lemma~\ref{defdom}}    \\
  & \mbox{~iff~}
    & (\sem{pat_{i1}}_{E}, \ldots ,\sem{pat_{in}}_{E})
      \;\in\; \mbox{dom}~{\cal F}\thetainf                            \\
  & & \hspace{2.0em} \mbox{by definition of $\cal F$}
\end{eqnarray*}
%
and $\mbox{dom}~{\cal F}\thetainf = \mbox{dom}~\thetainf$. $\Box$


% reducing general to first-order case:

\vspace{2.5ex}
Finally we need the following proposition, which says that the general case 
may be reduced to the first-order case:


\begin{proposition}
Let $\Delta$ be a general declaration. 
If the axioms generated from $\hat{\Delta}$ 
are valid under the given interpretation for $\; \sem{\fm{\em f}} \;$ and
$\; \sem{\fm{\em DOM'f}} \;$,
then the axioms generated from $\Delta$ are likewise valid.
\end{proposition}

\noindent {\em Proof.~~}
Note first that $\Delta$ and $\hat{\Delta}$ yield the same values for
$\sem{\fm{f}}$ and $\sem{\fm{DOM'f}}$ by definition.
For the axioms (\dag) for \fm{f}, we need the fact that
\begin{quote}
$  \sem{\widehat{exp_{i}}}_{D'}~=~\sem{exp_{i}}_{D'} $
\end{quote}
where $D'$ is the ``updated'' environment $\; D \: (\fm{f},\sem{\fm{f}}) \;$.
But this follows easily by induction from the fact that the eta-rule is
valid in our model:
\begin{quote}
$   \sem{\fm{f}~e_{1}~\ldots~e_{k}}_{D'}~=~
    \sem{\fm{fn }x_{k+1},\ldots ,x_{n} \fm{ => f}~e_{1}~\ldots ~e_{k}~
                 x_{k+1}~\ldots ~x_{n} }_{D'} $
\end{quote}

For the axioms (\ddag), it suffices to note that the predicates
$\ll exp_{i} \gg$ and $\ll \widehat{exp_{i}} \gg$ are syntactically
identical---this follows by induction from the fact that
\begin{tabbing}
\hspace*{2.0em}
$   \ll \fm{f}~e_{1}~\ldots~e_{k} \gg~=~
    \ll \fm{fn }x_{k+1},\ldots ,x_{n} \fm{ => f}~e_{1}~\ldots ~e_{k}~
                 x_{k+1}~\ldots ~x_{n} \gg $
\` $\Box$
\end{tabbing}


% Soundness of inference rules.

\vspace{2.5ex}
This completes the proof that our axioms are valid. In order to show that
our system was consistent, we would also need to check that the inference
rules of our logic were {\em sound\/} for our model. For any reasonable
formulation of higher-order logic, this would be completely routine.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Further remarks}
\label{sec-remarks}

We conclude with some miscellaneous remarks concerning the strengths, 
subtleties and weaknesses of our approach. We also mention some areas
where there is scope for further work.

\subsection{Bound variables}

Our treatment of the binding operators in Section~3(v) deserves
further comment.  The behaviour of \fm{any} in combination with
recursion is especially subtle.

For the quantifiers \fm{forall} and \fm{exists} we could have given a more 
generous interpretation---for instance, in Section~3 we could have defined
\begin{quote}
\begin{eqnarray*}
\ll \fm{exists }x.~e \gg &= &(\fm{forall }x.\, \ll e \gg )~~\Or\\
      && (\fm{exists }x.\, \ll e \gg \And~e\, )
\end{eqnarray*}
\end{quote}
(with corresponding changes to the semantic clauses in Section~4.2).

However, in the case of \fm{any} we are forced to take a very strict
interpretation. If in the semantics of Section~4 we allowed 
$\sem{\fm{any }x.e}_{E;F}$ to have a value when not all $\sem{e}_{E(x,v);F}$
were defined, then this value might change as the recursion unwound and new
values of $\sem{e}$ ``arrived''. This would cause the operator ${\cal F}$ to be
non-monotonic and we would not be able to obtain a fixed point.

Hence, although the following function definition is legal in our scheme,
we cannot prove it defines the identity function (even though the identity
is the only total function satisfying its two clauses):
\begin{quote} \begin{verbatim}
fun f 0     = 0
  | f (S n) = (any x. f x = n) + 1
\end{verbatim} \end{quote}

There are other uses of \fm{any} in function definitions that behave 
more as one would expect. 
For instance, the reader is invited to check that the following function
{\em can\/} be shown to be the identity:
\begin{quote} \begin{verbatim}
fun id 0     = 0
  | id (S n) = any x. (id n < x) = true /\ (x <= S n) = true
\end{verbatim} \end{quote}


\subsection{Advantages of our scheme}

As mentioned in Section~2, one advantage of our approach is
that it does not impose unnecessary proof obligations on users who 
wish to work only with total functions. 
Once we have proved a theorem asserting totality of a function, we can
forget about the \fm{DOM} predicates completely. Indeed, if our theorem-prover
detects that some function definition is primitive recursive (for instance),
the \fm{DOM} predicates need not even be generated, and simpler forms of the
axioms will suffice.%
\footnote{The LAMBDA system incorporates this feature.
The axioms generated in this case are similar to the theorems generated 
by a HOL package.}

Moreover, even when reasoning about non-total functions, it seems that proofs
in our logic involve fewer definedness conditions than proofs in other systems
(see Section~2).
This suggests that proofs in our logic may be less time-consuming. 
The gain stems from the fact that the \fm{DOM} predicates do not feature 
at all in the rules of the pure logic---they are no more than 
particular object-level constants.
%Moreover, definedness conditions do not feature at all
%in the rules of the pure logic---the \fm{DOM} predicates are no more than 
%particular object-level constants---and so automated proof tactics 
%may be 
%able to proceed further before getting stuck on conditions that cannot be 
%discharged automatically.

Of course, users will still need to prove \fm{DOM} conditions sometimes.
But the analogy with ``termination'' of the corresponding program suggests 
a way in which automated assistance for proving \fm{DOM} conditions 
might be provided, at least for the ``executable'' fragment of the logic. 
A machine could try to prove \fm{|- DOM'f }$e$ by simulating
the execution of \fm{f }$e$---if this terminated then the
course of computation would yield a proof of \fm{DOM'f }$e$. Even if $e$ is not
a concrete value but an expression containing variables, it might still be
possible to achieve a similar result by running the computation 
``symbolically''. Of course, this would give us at best a {\em semi-decision\/}
procedure, since such a proof tactic would diverge if applied to an
unprovable goal. Also, there are limitations to the analogy between
\fm{DOM} predicates and termination (see below).
Nevertheless, we feel that proof tactics along these lines
might be of some benefit to users.

\subsection{Limitations of our scheme}

In Section~4 we gave a proof of the logical consistency of our system.
However, in practice we are interested in more than this---%
we would like to know that there is a ``good fit'' between our formalism 
and the real-world situations that we are using it to describe. 
If this relationship has been misunderstood by the user, 
theorems generated using the theorem-prover may be misinterpreted 
as expressing false (or unproven) statements about the real world. 
In this subsection we seek to explain more fully the ``intended use'' of
our logic, and to point out some of the possible pitfalls.

There are essentially two different ways in which partial function 
declarations can be understood: 
as definitions of genuinely partial functions between the relevant domains, 
or as loose specifications of {\em total\/} functions. 
Logics such as LPF \cite{lpf}, which has a three-valued semantics,
fit well with the former interpretation, 
whereas our scheme fits more comfortably with the latter,
as will be clear from the semantics we have given. 

The distinction between these interpretations does not matter much to us 
if we adhere to the principle of writing function applications only in contexts
where they are ``guarded'' by conditions ensuring their well-definedness. 
For instance, the predicate
\begin{quote} \begin{verbatim}
(y > 0) = true  /\  x div y = 1
\end{verbatim} \end{quote}
has the same truth-value in our scheme as in LPF for any assignment of values
to \fm{x} and \fm{y}.
It seems likely that there is a metatheorem asserting that the two
interpretations agree for certain ``guarded'' formulae.
In specification languages such as `Z', writing such formulae
would seem to be good practice in any case.
%In writing a specification in a language such as Z, it would seem sensible 
%in any case to adopt such a principle, if only for the sake of clarity. 
%The meaning of a specification should not depend on esoteric uses of
%undefinedness.

The ``loose specification'' interpretation 
may also be appropriate in the context of hardware verification.
Suppose we wish to reason about a hardware component whose behaviour is
only specified for certain input values. 
Typically, the design of such a component will ensure that it still
exhibits {\em some\/} determinate behaviour even on ``incorrect'' inputs, 
though what this behaviour is may not be specified.
In this case, our scheme would be particularly suitable---the conclusions
derived in the logic would be correct for {\em any\/} component satisfying
the specification.

However, there are problems if we try to use our logic to reason about
the behaviour of programs.  Although in Sections~2 and 3 we used
program termination as an analogy to help motivate our scheme, this
analogy should not be pressed too far.  A non-terminating program is
not the same as a program returning an unknown value, but our
semantics is not capable of reflecting this distinction.  Here LPF
reflects the real-world situation perhaps more faithfully.
We now give some examples of predicates that are misleading if
interpreted as statements about Standard ML programs.

The first kind of discrepancy arises in connection with functions of
higher type.  Consider the following declarations:
\begin{quote} \begin{verbatim}
fun apply f x = f x

fun id  0    = 0
  | id (S n) = S (apply id n)
\end{verbatim} \end{quote}
In Standard ML, \fm{id} will behave as an identity function.  By
contrast, in our scheme the theorem \fm{|- id 1 = 1} is not provable
(although \fm{|- id 0 = 0} is).  The problem is that we cannot, in
general, keep track of how a higher-order function, such as \fm{apply}
will choose to apply its argument. To be safe, we take (in
Section~3(ii)) the pessimistic view, and universally quantify the
missing arguments. The resulting \fm{id} is thus ``under-defined''
relative to ML. This example is artificial, but similar remarks apply
to the following natural code for summing the nodes of a labelled tree:
\begin{quote} \begin{verbatim}
fun sumNodes (Tree(n, ts)) = n + sum (map sumNodes ts);
\end{verbatim} \end{quote}
%
We can strengthen such examples. Consider
\begin{quote} \begin{verbatim}
fun hal  0       = 0
  | hal  1       = 1 + (hal 1)
  | hal (S(S n)) = S (apply hal n)
\end{verbatim} \end{quote}
(\fm{hal} is almost \fm{half}). In ML, $\fm{hal}~n$ will terminate for
all even $n$. However, because, in our axiomatisation of \fm{DOM}
predicates ($\ddag$ in section~3), we chose to use equality rather
than implication, we can prove that
\begin{quote} \begin{verbatim}
|- DOM'hal(x) = (x = 0)
\end{verbatim} \end{quote}

On the other hand, a function application may (provably) have some concrete
value in our scheme when the corresponding ML program diverges. This
is perhaps the more serious problem.  Consider for instance
\begin{quote} \begin{verbatim}
fun f x = f x;
fun g x = x * f x
\end{verbatim} \end{quote}
The resulting function \fm{g} is ``over-defined'' relative to ML -- we
can prove the theorem \fm{|- g 0 = 0} even though \fm{g 0} diverges
in ML. 

These examples illustrate the differences between regarding \fm{f x}
as having an unknown value and as having no value.  In particular, the
role of the \fm{DOM} predicates in our system is purely auxiliary -- we
introduce them to provide a formal means for reasoning about the
values of function-calls. It is tempting but misleading to think of
them expressing ``definedness'' -- \fm{DOM'g x}~really only means
``the function \fm{g} obeys its defining equation for the value
\fm{x}''. In our final example, \fm{|- g x = x * f x}~ independently of
whether we can prove anything about \fm{f x}.

We have described the details of our scheme as it has been implemented
in the LAMBDA theorem-prover. However, as we discussed in Section~3,
variants of the scheme are certainly possible -- in particular, there
is scope for variation in our definition of the syntactic operator
$\ll \_ \gg $.  It seems that there amay be other definitions that avoid
some of the above problems, in particular the ``over-definedness''
phenomenon mentioned above.  For such alternative definitions, we
expect to obtain metatheorems guaranteeing certain relationships
between our logic and the behaviour of programs in Standard ML.  We
have not yet worked out all the details, however; and it is not yet
clear to us what the trade-offs are between competing definitions of
$\ll \_ \gg $.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{thebibliography}{99}

\bibitem{lpf} H. Barringer, J.H. Cheng and C.B. Jones, \ because we chose, to use equality rather than
implication in our axiomatisation of \fm{DOM} predicates ($\ddag$ in
section~3),
A logic covering undefinedness in program proofs. \
{\it Acta Informatica\/} 21, 251--269, 1984.

\bibitem{boyer} R.S. Boyer and J.S. Moore, \
{\it A Computational Logic.} \
ACM Monograph Series, Academic Press, 1979.

\bibitem{cliff} J.H. Cheng and C.B. Jones, \
On the usability of logics which handle partial functions.\
In C. Morgan and J. Woodcock (eds.), \
{\it Proceedings of the Third Refinement Workshop}, Springer-Verlag, 1990.

\bibitem{lambda3.2} S. Finn and M.P. Fourman, \
{\it Logic Manual for the Lambda System.} \
Abstract Hardware Limited, version 3.2, 1990.

\bibitem{lambda4.0} S. Finn and M.P. Fourman, \
{\it Logic Manual for the Lambda System.} \
Abstract Hardware Limited, version 4.2.1, 1992.

\bibitem{farmer} W.M. Farmer, \
A Partial Functions Version of Church's Simple Theory of Types. \
{\it Journal of Symbolic Logic\/} 55, 3, 1269--1291, 1990.
\bibitem{hol} M.J.C. Gordon, \
HOL: A proof generating system for higher-order logic.\
In G. Birtwistle and P.A. Subrahmanyam (eds.),\
{\it VLSI Specification, Verification and Synthesis,\/} 73--128, \
Kluwer Academic Publishers, 1987.

\bibitem{lcf} M. Gordon, R. Milner and C. Wadsworth, \
{\it Edinburgh LCF.} \
Volume 78 of {\it Lecture Notes in Computer Science,\/} Springer-Verlag, 1979.

\bibitem{vdm} C.B. Jones, \
{\it Systematic Software Development Using VDM.\/}\
Prentice Hall International, 1986.

\bibitem{mural} C.B. Jones et al.,\ eds.,\
{\it Mural: A Formal Development Support System.\/}\
Springer-Verlag, 1991.

\bibitem{lego} Z. Luo and R. Pollack, \
LEGO proof development system: User's manual. \
LFCS Report Series ECS-LFCS-92-211, Department of Computer Science, \
University of Edinburgh, 1992.

\bibitem{pvs} S. Owre, J.Rushby, {\em et. al.}, \
Formal Verification for Fault-Tolerant Architectures: Prolegomena to
the Design of {PVS}. \
{\em IEEE Transactions on Software Engineering\/} 21, 2, 107--125, 1995.

\bibitem{ehdm} J. Rushby, F. von Henke and S. Owre, \
An Introduction to Formal Specification and Verification using EHDM. \
Technical Report SRI-CSL-91-02, SRI International, 1991.

\bibitem{scott} D.S. Scott, \
Identity and existence in intuitionistic logic.
In {\it Lecture Notes in Mathematics\/} Volume 735, 661--696, \
Springer-Verlag, 1979.

\bibitem{zed} J.M. Spivey, \
{\it Understanding Z---A Specification Language and its Formal Semantics.}\
Cambridge Tracts in Computer Science 3, CUP, 1988.


\end{thebibliography}

\end{document}
