\documentclass{article}
\usepackage[a4paper]{geometry}
\usepackage{url}
\usepackage[sort&compress]{natbib}
\begin{document}
\title{Research Proposal: Relating Formal Theories}
\author{Ramana Kumar}
\maketitle
Mechanically formalising mathematics is an activity with decades of history and some established tools.
At a high level, mechanical formalisation means proving theorems in a formal system as implemented by a piece of software, a theorem prover or proof assistant.
But there are many theorem provers, all different.
Diversity has advantages, but so would effective communication between systems.
I propose to research how such communication is best achieved, and to create tools for doing so.
\subsection*{Why relate formalisations?}
\subsubsection*{Pragmatically}
\begin{itemize}
\item
To make duplicate work unnecessary.
Theories of the same content are found duplicated in the libraries of various proof assistants.
Basic definitions, of say numbers or relations, perhaps do have different natural forms in different logics.
But higher-level theorems, like the fundamental theorem of algebra, shouldn't depend so much on the exact details of the underlying logic, and should only have to be proved once or twice.
There are reasons to maintain multiple proofs of the same theorem (see \cite{DBLP:conf/aisc/GrabowskiS10}).
But often someone who is familiar with one system wants to prove something that first requires some supporting formalisation, and the support only exists in another system.A translation mechanism enabling library reuse would be helpful in these situations.
\item
To enable collaboration.
The more complex the mathematics, the more practical it is to formalise it in pieces.
But these pieces might be done by different teams, working with different systems.
The Flyspeck project \cite{DBLP:journals/dcg/HalesHMNOZ10} is one example of a substantial formalisation that is currently across three proof assistants.
Aside from reducing the number of systems one needs to trust to believe a formalised result, translating between systems helps teams on the same project share work.
\item
Since some things are more easily expressed in certain systems.
For example, natural formalisations of abstract algebra would arguably use dependently typed records, which are only available in some proof assistants.
Also, most proof assistants are based on type theory, but sometimes the expressivity of untyped set theory is desirable.
Literature on set theory versus type theory, and the advantages of translating between them, includes \cite{DBLP:conf/tphol/Gordon96,Gordon:HOLST94,DBLP:journals/toplas/LamportP99}.
\item
Since some systems provide better tools.
Theorem provers vary on level of automation, number of users, quality of documentation, user interface, suitability for software verification versus traditional mathematics, code generation facilities, and size or contents of the library of formalised results.
These, along with familiarity, are all good reasons for someone to choose one system over another, and someone else to choose differently.
Good translations would reduce the cost of this choice, by making the existing library less of an issue, and by making it easier to switch systems during development.
\end{itemize}
\subsubsection*{Theoretically}
\begin{itemize}
\item
To find out how to make efficient translations.
Interpreting one logic in another usually results in a blowup in proof/term size and a slowdown in proof checking \cite{holl2coq}.
Developing good translations between systems means finding ways to mitigate or avoid this problem.
The mechanism of an efficient translation would be theoretically interesting.
\item
To find out how to make usable translations.
This is another engineering problem whose solutions would be interesting.
A translation accomplished by, say, embedding the source logic in the target logic, would look unnatural to a user of the target system, who would have formalised the results directly in the target logic.
But it might be possible to make the equivalence of isomorphic structures transparent to the user.
\item
To explore a philosophical question.
Can two formalisations (or two formal models) be about the same thing, if they are in different logics, or even in the same logic but with different definitions?
What makes them formalisations of the same theorem (or models of the same system)?
Whatever it is ultimately grounds any hope of a translation between them, so writing the translation can help us see it.
\item
To investigate language and foundations.
Ideas used in translating between theorem provers may also be useful for making mechanical formalisations more appealing to mainstream mathematicians.
Work in the other direction, extracting the formal content from mathematical language, can be found in \cite{GanesalingamThesis}.
The needs of translation may point to particularly weak formal systems as container languages, perhaps in the style of Metamath \cite{metamath}, or like Primitive Recursive Arithmetic suggested in the QED Manifesto \cite{DBLP:conf/cade/Anonymous94}, and the interplay with stronger systems is interesting.
\end{itemize}
\subsection*{Existing translations between systems}
There are several implementations of translations between different proof assistants, for example \cite{DBLP:conf/cade/ObuaS06,DBLP:conf/itp/KraussS10,holl2coq,DBLP:conf/cade/McLaughlin06,DBLP:conf/fmcad/GordonRHK06,DBLP:conf/lpar/SchurmannS06,DBLP:conf/tphol/NaumovSM01}.
In each case, we may ask three questions:
\begin{itemize}
\item
Are proofs translated?
Finding a good translation between statements in different logics can be hard enough, but a complete translation will also deal with proofs.
Advantages of translating proofs include: the source system does not become part of the trusted code base, and the soundness of the translator doesn't need to be checked.
Naumov \cite{Naumov:1999:IIF:867021}, for example, discusses this issue.
\item
Is the translation usable by a native of the target system?
\item
Is the translation maintained over time?
A particular formalisation can be ported manually on a one-off basis.
Sometimes a more general translator from one prover to another will be written.
But it is rare for a translator to be maintained alongside new versions of the source and target proof assistants.
A related issue here is coverage of the source language, in other words, restrictions on what can be translated.
\end{itemize}
We would like all three answers to be ``yes''.
Achieving that for many pairs of systems is a good goal.
There has also been some work on ``theory management'', akin to package management, in particular Hurd's OpenTheory project \cite{hurd2009,hurd2010b}.
One main point here is to make the dependencies (required results) and provisions of a formal theory explicit, so that theories can be composed, sometimes with one standing in for another.
The second main point is to design theories so that they fit nicely into this environment of composable theories.
Theory management, especially if it is theorem prover-neutral, would make translations between systems much easier, and would shape the design of and requirements for such translations.
Related ideas include a ``standard library'' of formalised results \cite{mathstdlib,mathstdlib2}, and the notion of ``high-level theories'' \cite{DBLP:conf/aisc/CaretteF08}.
My aim is to tackle the problem of translation between proof assistants directly.
Rather than implementing a separate translation for each pair of systems, I hope to find a workable ``hub'' language to which each system needs only one two-way link.
Lessons both from existing translations and from theory management are relevant to the design of such a language.
\subsection*{First year goals}
\begin{itemize}
\item
Deliverable: A map of existing translations between theorem provers, indicating what they accomplish and how.
The goal here is to see what works well out of the approaches taken so far, so that good ideas can be reused in a more comprehensive translation scheme.
A secondary goal is to assess the state of interoperability, in other words, how many pairs of systems can already share results.
The map would extend the second part of this research proposal, and thus is within my capacity.
\item
Deliverable: A design of a language for capturing the content of formal theories and emitting it back in particular logics.
Goals for the language include the ability to capture any formal content, and the support for making isomorphic structures easily interchangeable.
\item
Deliverable: A working prototype of the OpenTheory project tools.
The aim is to get experience with theory engineering, and tools to experiment with theory design.
A working prototype is arguably already available, or close to it, so this item should not involve as much work as it would seem.
My experience as a developer of the HOL4 proof assistant \cite{HOL4} will be of use here.
\end{itemize}
\bibliographystyle{plain}
\bibliography{bib}
\end{document}