wadtabstract.tex

\documentclass[orivec]{llncs}

\usepackage{graphicx,url,wrapfig,amsmath,amssymb}

\usepackage[show]{ed} %for ednotes

\usepackage{sembracket}
\usepackage{mytikz}
\usepackage{basics}
%\usepackage[llncs]{theorems} %only for now so that the environments are defined; replace with nice package for this later
\usepackage{local}

\setcounter{tocdepth}{3}
\usepackage[bookmarks,linkcolor=red,citecolor=blue,urlcolor=gray,colorlinks,breaklinks,bookmarksopen,bookmarksnumbered]{hyperref}

\setlength{\hfuzz}{3pt}
\hbadness=10001 %make box warning less strict

\begin{document}
\title{Structuring Theories with Implicit Morphisms}
\author{Florian Rabe$^{1,2}$ \and Dennis M\"uller$^2$}
\institute{LRI Paris \and FAU Erlangen-Nuremberg}
\maketitle

\begin{abstract}
We introduce \emph{implicit} morphisms as a concept in formal systems based on theories and theory morphisms.
The idea is that there may be at most one implicit morphism from a theory $S$ to a theory $T$, and if $S$-expressions are used in $T$ their semantics is obtained by automatically inserting the implicit morphism.
The practical appeal of implicit morphisms is that they hit the sweet-spot of being extremely simple to understand and implement while significantly helping with structuring large collections of theories.
\end{abstract}

Theory morphisms have proved an essential tool for managing collections of theories in logics and related formal systems.
They can be used to structure theories and build large theories modularly from small components or to relate different theories to each other \cite{asl,devgraphs,littletheories}.
Areas in which tools based on theories and theory morphisms have been developed include specification \cite{obj,hets}, rewriting \cite{maude}, theorem proving \cite{imps}, and knowledge representation \cite{RK:mmt:10}.

%The latter of these tools is our \mmt system.
%We use \mmt as both a theoretical framework and a concrete implementation of our results.
%But our ideas are independent of \mmt and can be transferred very easily to any other language using theory morphisms.

These systems usually use a logic $L$ for the fine-granular formalization of domain knowledge, and a diagram $D$ in the category of $L$-theories and $L$-morphisms for the high-level structure of large bodies of knowledge.
This diagram is generated by all theories/morphisms defined, induced, or referenced in a user's development.

\begin{wrapfigure}{r}{5.5cm}
\vspace{-3em}
\begin{tikzpicture}
\node (M) at (0,0) {$\cn{Monoid}$};
\node (G) at (-2,-2) {$\cn{Group}$};
\node (D) at (2,-2) {$\cn{DivGroup}$};
\draw[mono](M) -- (G);
\draw[arrow](G) to[out=30,in=150] node[above] {$\cn{G2DG}$} (D);
\draw[arrow](D) to[out=-150,in=-30] node[above] {$\cn{DG2G}$} (G);
\end{tikzpicture}
\vspace{-3.5em}
\end{wrapfigure}

For example, a user might reference an existing theory $\cn{Monoid}$, define a new theory $\cn{Group}$ that extends $\cn{Monoid}$, define a theory $\cn{DivGroup}$ (providing an alternative formulation of groups based on the division operation), and then define two theory morphisms $\cn{G2DG}:\cn{Group}\darr \cn{DivGroup}:\cn{DG2G}$ that witness an isomorphism between these theories.
This would result in the diagram on the right.
Note that we use the syntactic direction for the arrows, e.g., an arrow $m:S\to T$ states that any $S$-expression $E$ (e.g., a sort, term, formula, or proof) can be translated to an $T$-expression $m(E)$.
Crucially, $m(-)$ preserves typing and provability.

The key idea behind implicit morphisms is very simple:
We maintain an additional diagram $I$, which is commutative subdiagram of $D$ and whose morphisms we call \emph{implicit}.
The condition of commutativity guarantees that $I$ has at most one morphism $i$ from theory $S$ to theory $T$, in which case we write $\ipce{S}{T}$.
Commutativity makes the following language extension well-defined: if $\ipce{S}{T}$, then any identifier $c$ that is visible to $S$ may also be used in $T$-expressions; and if $c$ is used in a $T$-expression, the semantics of $c$ is $i(c)$ where $i$ is the uniquely determined implicit morphism $i:S\to T$.

Despite their simplicity, the practical implications of implicit morphism are huge.
For example, in the diagram above, we may choose to label $\cn{G2DG}$ implicit.
Immediately, every abbreviation or theorem that we have formulated in the theory $\cn{Group}$ becomes available for use in $\cn{DivGroup}$ without any syntactic overhead.
We can even label $\cn{DG2G}$ implicit as well if we prove the isomorphism property to ensure that $I$ remains commutative, thus capturing the mathematical intuition that $\cn{Group}$ and $\cn{DivGroup}$ are just different formalizations of the same concept.
While these morphisms must be labeled manually, any inclusion morphism like the one from $\cn{Monoid}$ to $\cn{Group}$ is implicit automatically.

In fact, this principle works so well that we have refactored our \mmt system (our long-standing implementation) in such a way that implicit morphisms are now more primitive than inclusion morphisms.
The semantics of inclusion morphisms is obtained by saying that inclusions are implicit morphisms that map all identifiers to themselves.
Even the fundamental property that a theory may reference its own identifiers is now just a consequence of the fact that all identity morphisms are implicit.
Therefore, surprisingly, adding implicit morphisms deep in the \mmt kernel has made its design more elegant.

\bibliographystyle{alpha}
\bibliography{../../../Program_Data/Latex/bib/rabe,../../../Program_Data/Latex/bib/systems,../../../Program_Data/Latex/bib/institutions,../../../Program_Data/Latex/bib/pub_rabe,../../../Program_Data/Latex/bib/historical}
\end{document}