1\documentclass[11pt]{article}
2
3\usepackage{charter}
4
5\title{Isabelle-Style Overloading for HOL}
6\author{Michael Norrish}
7\date{8 May 2006}
8
9\begin{document}
10\maketitle
11\begin{abstract}
12  An attempt to detail what changes would be required to HOL systems
13  (HOL4, HOL~Light and ProofPower) to implement Isabelle-style
14  overloading.  Each section below describes successive changes that
15  might be made to the existing HOL systems.  Later changes require
16  previous changes, but we might choose adopt a prefix of the three
17  changes.
18\end{abstract}
19
20\section{Deferred Definition}
21\label{sec:deferred-definition}
22
23\begin{description}
24\item[Summary] Add two theory operations: constant \emph{declaration}
25  and constant \emph{definition}.
26\end{description}
27
28A constant declaration specifies a constant name and type.  Performing
29a declaration reserves the given name.  After declaration, the
30constant exists in the theory signature, and the parser should treat
31it as if it were a full-blown constant.
32
33After a declaration has been made, a constant can be defined.  Such a
34definition must be for a term of the same type and name of an existing
35declaration.\footnote{Clearly ``declare-and-define'' could be provided
36  as a derived principle.} The rules for validity of definitions
37should be unchanged, except possibly to require equational definitions
38to have the now already existing constant on the LHS rather than a
39variable.  The result of a definition is to add a new theorem to the
40theory.
41
42To prevent circular definitions, the implementation must record the
43dependency graph for constant definitions and prohibit loops.  In an
44equational definition, the new constant depends on those constants
45that appear on the right-hand side of the equation.  In a definition
46made by \texttt{new\_specification}, the new constants depend on those
47constants that appear within the (existential) theorem.
48
49\begin{description}
50\item[Advantages] Allows a nice presentation style which separates
51  constants and their types from the details of their definition.
52  Also, allows a style of work where a constant starts out completely
53  under-specified, but is later given a definition.  One might have
54  different refinements of the same constant in different branches off
55  the same root.  This can be emulated in our existing systems by
56  calls to \texttt{new\_constant} and \texttt{new\_axiom} (or their
57  equivalents), but forcing the user to assert axioms is painful.
58\item[Disadvantages] Implementation must track the dependency graph, a
59  rather more complicated object than existing theory-signature code
60  deals with.
61\end{description}
62
63
64\section{Monomorphic Definitions at Different Types}
65\label{sec:defin-at-diff}
66
67\begin{description}
68\item[Summary] Allow a definition to cover a monomorphic part of a
69  declaration's type-scheme.
70\end{description}
71
72When a definition is made, the type of the constant does not have to
73be exactly the same as that given in the constant's declaration.
74Instead, the \emph{defined type} can be an instance of the
75(polymorphic) \emph{declared type}.  However, the instance must be
76monomorphic.  Any references to other, possibly overloaded, constants
77will therefore be monomorphic as well (otherwise the definition would
78fall foul of the rule forbidding extra type variables). As before, the
79resulting equation is added to the evolving theory.
80
81Now the situation is effectively that there are multiple constants of
82the same name but different types.  Without the monomorphism
83restriction, the dependency graph checking becomes more complicated.
84For example, while it's OK to have
85\begin{verbatim}
86  declare c1 : 'a -> bool
87          c2 : 'a -> bool
88
89  define  c1 (n:num) = ~c2(n)
90          c2 (b:bool) = c1 b
91\end{verbatim}
92it's clearly \emph{not} OK to have
93\begin{verbatim}
94  declare c1 : 'a -> bool
95          c2 : 'a -> bool
96
97  define  c1 (x:'a) = ~c2(x)
98          c2 (b:bool) = c1 b
99\end{verbatim}
100
101To figure out whether the latter is safe or not is the problem of
102determining if a rewriting system is strongly normalising.  It is this
103problem that Steven Obua's paper~\cite{Obua-RTA06} solves.  If we
104force definitions at different instances to be monomorphic then we
105avoid this problem because we can just check each monomorphic
106constant's dependency graph independently.
107
108\begin{description}
109\item[Advantages] Allows a simple emulation of type classes, such that
110  it becomes possible to prove a rewrite (\emph{e.g.}, left-identity
111  for groups) that applies to slew of different types (such as
112  \texttt{:real}, \texttt{:int} and \texttt{:word}).  Rather than have
113  type-classes, the emulation mimicks them with predicates and
114  conditional rewrite rules.
115\item[Disadvantages] Is even more complicated, and doesn't even allow
116  full emulation of Isabelle type-classes.
117\end{description}
118
119
120\section{Type-Recursive Definitions}
121\label{sec:type-recurs-defin}
122
123\begin{description}
124\item[Summary] Allow definitions to be recursive on types, subject to
125  some sort of soundness guarantee.
126\end{description}
127
128It's not clear quite what should be done here.  We need an
129easy-to-implement approximation to proof of termination.  One helpful
130fact is that because definitions do not overlap, any given definition
131can only expand to one reduct.  Nor is it necessary to worry about the
132real term structure in the definition.  Instead the rewrite system is
133really one from name-type pairs to lists of the same.
134
135The restriction we thought would work in our discussion via e-mail was
136to require all recursion to occur on smaller types ``structurally''.
137But this wouldn't directly prevent the second (unsound) scenario
138above.  Instead, some sort of circular dependency test would have to
139reject it.  But this same circular dependency test would probably
140reject a legitimate recursion via an intermediate constant.  To
141construct a correct test seems as if it would be trying to be a
142general (though conservative) solution for the rewriting termination
143problem.
144
145\begin{description}
146\item[Advantages] Would allow, for example, the definition of addition
147  on a polymorphic type like \texttt{:'a~matrix} in terms of addition
148  on \texttt{:'a}.
149\item[Disadvantages] We don't have a known-to-be-sound restriction
150  other than Steven Obua's, which is a very complicated piece of code
151  to be putting into a kernel.
152\end{description}
153
154\bibliographystyle{plain}
155\bibliography{overloading-extension}
156
157\end{document}
158
159%%% Local Variables:
160%%% mode: latex
161%%% TeX-master: t
162%%% End:
163