\documentclass[11pt]{article}

\usepackage{charter}

\title{Isabelle-Style Overloading for HOL}
\author{Michael Norrish}
\date{8 May 2006}

\begin{document}
\maketitle
\begin{abstract}
  An attempt to detail what changes would be required to HOL systems
  (HOL4, HOL~Light and ProofPower) to implement Isabelle-style
  overloading.  Each section below describes successive changes that
  might be made to the existing HOL systems.  Later changes require
  previous changes, but we might choose adopt a prefix of the three
  changes.
\end{abstract}

\section{Deferred Definition}
\label{sec:deferred-definition}

\begin{description}
\item[Summary] Add two theory operations: constant \emph{declaration}
  and constant \emph{definition}.
\end{description}

A constant declaration specifies a constant name and type.  Performing
a declaration reserves the given name.  After declaration, the
constant exists in the theory signature, and the parser should treat
it as if it were a full-blown constant.

After a declaration has been made, a constant can be defined.  Such a
definition must be for a term of the same type and name of an existing
declaration.\footnote{Clearly ``declare-and-define'' could be provided
  as a derived principle.} The rules for validity of definitions
should be unchanged, except possibly to require equational definitions
to have the now already existing constant on the LHS rather than a
variable.  The result of a definition is to add a new theorem to the
theory.

To prevent circular definitions, the implementation must record the
dependency graph for constant definitions and prohibit loops.  In an
equational definition, the new constant depends on those constants
that appear on the right-hand side of the equation.  In a definition
made by \texttt{new\_specification}, the new constants depend on those
constants that appear within the (existential) theorem.

\begin{description}
\item[Advantages] Allows a nice presentation style which separates
  constants and their types from the details of their definition.
  Also, allows a style of work where a constant starts out completely
  under-specified, but is later given a definition.  One might have
  different refinements of the same constant in different branches off
  the same root.  This can be emulated in our existing systems by
  calls to \texttt{new\_constant} and \texttt{new\_axiom} (or their
  equivalents), but forcing the user to assert axioms is painful.
\item[Disadvantages] Implementation must track the dependency graph, a
  rather more complicated object than existing theory-signature code
  deals with.
\end{description}


\section{Monomorphic Definitions at Different Types}
\label{sec:defin-at-diff}

\begin{description}
\item[Summary] Allow a definition to cover a monomorphic part of a
  declaration's type-scheme.
\end{description}

When a definition is made, the type of the constant does not have to
be exactly the same as that given in the constant's declaration.
Instead, the \emph{defined type} can be an instance of the
(polymorphic) \emph{declared type}.  However, the instance must be
monomorphic.  Any references to other, possibly overloaded, constants
will therefore be monomorphic as well (otherwise the definition would
fall foul of the rule forbidding extra type variables). As before, the
resulting equation is added to the evolving theory.

Now the situation is effectively that there are multiple constants of
the same name but different types.  Without the monomorphism
restriction, the dependency graph checking becomes more complicated.
For example, while it's OK to have
\begin{verbatim}
  declare c1 : 'a -> bool
          c2 : 'a -> bool

  define  c1 (n:num) = ~c2(n)
          c2 (b:bool) = c1 b
\end{verbatim}
it's clearly \emph{not} OK to have
\begin{verbatim}
  declare c1 : 'a -> bool
          c2 : 'a -> bool

  define  c1 (x:'a) = ~c2(x)
          c2 (b:bool) = c1 b
\end{verbatim}

To figure out whether the latter is safe or not is the problem of
determining if a rewriting system is strongly normalising.  It is this
problem that Steven Obua's paper~\cite{Obua-RTA06} solves.  If we
force definitions at different instances to be monomorphic then we
avoid this problem because we can just check each monomorphic
constant's dependency graph independently.

\begin{description}
\item[Advantages] Allows a simple emulation of type classes, such that
  it becomes possible to prove a rewrite (\emph{e.g.}, left-identity
  for groups) that applies to slew of different types (such as
  \texttt{:real}, \texttt{:int} and \texttt{:word}).  Rather than have
  type-classes, the emulation mimicks them with predicates and
  conditional rewrite rules.
\item[Disadvantages] Is even more complicated, and doesn't even allow
  full emulation of Isabelle type-classes.
\end{description}


\section{Type-Recursive Definitions}
\label{sec:type-recurs-defin}

\begin{description}
\item[Summary] Allow definitions to be recursive on types, subject to
  some sort of soundness guarantee.
\end{description}

It's not clear quite what should be done here.  We need an
easy-to-implement approximation to proof of termination.  One helpful
fact is that because definitions do not overlap, any given definition
can only expand to one reduct.  Nor is it necessary to worry about the
real term structure in the definition.  Instead the rewrite system is
really one from name-type pairs to lists of the same.

The restriction we thought would work in our discussion via e-mail was
to require all recursion to occur on smaller types ``structurally''.
But this wouldn't directly prevent the second (unsound) scenario
above.  Instead, some sort of circular dependency test would have to
reject it.  But this same circular dependency test would probably
reject a legitimate recursion via an intermediate constant.  To
construct a correct test seems as if it would be trying to be a
general (though conservative) solution for the rewriting termination
problem.

\begin{description}
\item[Advantages] Would allow, for example, the definition of addition
  on a polymorphic type like \texttt{:'a~matrix} in terms of addition
  on \texttt{:'a}.
\item[Disadvantages] We don't have a known-to-be-sound restriction
  other than Steven Obua's, which is a very complicated piece of code
  to be putting into a kernel.
\end{description}

\bibliographystyle{plain}
\bibliography{overloading-extension}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: