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