
\documentclass{article}

\usepackage{isolatin1,xspace,url}
\usepackage{../../utils/hetcasl} 

\newcommand{\CASL}{\textsc{Casl}\xspace}
\newcommand{\CASLDL}{\textsc{Casl\_DL}\xspace}

\begin{document}
\author{Klaus Lüttich}

\title{Design and Notes for the \CASLDL Node in Hets}
\maketitle
\section{Issues (with implementation options)}

\textbf{Note:} The following issues very often mention the not jet
complete OWL DL logic (node) of Hets. Clearly the development of
\CASLDL and OWL DL support in Hets must be closely coupled.

\subsection{Each OWL DL-File is one Named Spec}

[and when translating to CASL-DL, 
the named spec is put into a file/CASL library that contains
only this named spec? Till] [No, if you parse an OWL DL file the
  resulting abstract syntax will include all imported
  specifications. This makes the handling of parsing and analysis
  between Hets and an external parser much easier. So we generate a
  development graph from this import structure. The parser already
  handles cyclic imports as it does not read a known OWL DL file
  again. Example: food.owl imports wine.owl and wine.owl imports
  food.owl. If you parse wine.owl the parser reads first wine.owl and
  second food.owl and it recognizes that it has read wine.owl already
  hence it skips the import in food.owl. This development graph has
  two nodes: food and wine where wine is an extension of
  food. \emph{while writing this I recognized that splitting an
    abstract syntax like this is not possible. There can be
    mutally recursive defined symbols.}  So circular imports lead to
  one theory in Hets and we have to split such a theory back into
  circular imports afterwards. Klaus]
[Although it seems to be the only way, it sounds a bit complicated.
Perhaps you could leave out the ``splitting back'' in a first
approximation. Till]

  Where do we get the name from:
  \begin{itemize}
  \item Name derived from URI of the OWL DL-File.
  \item Ontologies in OWL DL can be named. We should encourage people
    to do so and use that one.
  \item (Given as annotation to the Ontology in the OWL DL-File.)
  \end{itemize}

  But is every named theory (spec) an OWL DL-file?  [Yes, unless we
  have a way to distingiush several named specs with one OWL DL file,
  which seems not to be the case. Till ] Do we generate OWL DL-files
  for parametrised specifications? [Yes. Till] [This is not very
  useful. As there is no notion of parametrisation in OWL DL these
  ontologies can't be used. The formal parameter specification
  normally provides no meaning in terms of known concepts. Klaus]
  [The reulting theory is just a loose theory, which may be useful
  even without instantiation. Till] An
  Annotation should map specification names to URIs and only these
  theories are exported to OWL DL files. [But aren't auxilary specs
  needed as well? Till] (each of these URIs should have a Namespace
  abbrev for the disambiguation when an imported ontology is extended)

  How to treat circlar imports in the development graph. 
  [The development graph must be acyclic. Hence,
  cyclic imports are not supported, unless the theories
  are not really cyclic. Till]
  The OWL DL
  parser will parse each URI pointing to an OWL file importes or not
  only once. This even applies if an OWL DL file is not loaded form
  the document inherent base URI which is seen as the URI of the
  ontology in any case.

\subsection{Structuring an ontology inside an OWL DL-File}
  Annotations (on the OWL DL side) can point to parts that are
  extensions. \emph{not in the paper}

  So we could reflect some structuring made in \CASLDL. But 
  keeping track of parametrised specifications is not easy. 
  [I will implement some naming scheme for internal nodes soon.
   Perhaps that helps a little. Till] [What will this naming scheme
  look like? Can we discuss that before you start implementing it? Klaus]
  [I have already done this. Till]

\subsection{Structuring on the \CASLDL side}
  flattened into a set of named theories each resulting into one OWL
  DL file. After conversion back from spme genrated OWL DL files the
  structuring is lost. (or we have to add many Annotations to the
  generated OWL DL output)

\subsection{Cardinality Restrictions}

  \begin{itemize}
  \item An instantiation of GenCardinality must be traced. All
    renamings should end up in a table that could resemble a
    minCardinality[pred\_name] for translation to OWL DL. \emph{paper
    conforming}
  \item new FORMULA variants, that have directly the semantics of
    Cardinality Restrictions. No tracing is needed. Only the the
    embedding into \CASL is a little bit harder, as the instantiation
    has to be generated. \emph{Not paper conforming}
\end{itemize}

[don't know which one is better. Till] [Extendenting FORMULA seems
  easier to me. So I implement that. Klaus]
  
\subsection{Namespaces} (1) global to library or (2) local to a named
  specification or (3) to a basic specification?

  \begin{enumerate}
  \item means globally available but namespaces have to be
    unified. Only possible as gobal annotations. Are they available in
    the right place, need they still be in the \CASLDL-Signature?
    Namespaces of different OWL DL-files need to be integrated.
    (abbrevs should not collide, point to different URIs) The java
    parser may (/ will) do this.
  \item with annos this is not easy. Here it must be possible to
    have all annos available during the analysis. 
  \item with annos this is not easy. Here it must be possible to
    have all annos available during the analysis. 
  \end{enumerate}
  
[I vote for 1. Perhaps having only one DL spec per library
eases things? Other OWL tools also should have the problem
of name space integration w.r.t. imported files ?!? Till] [A
  unification is done by the parser we currently consider, but all
  imports become integrated into one abstract syntax. Klaus]

\subsection{Symbols in / from different OWL DL files}

 In OWL DL files symbols are unique in terms of URIs. But in \CASLDL
  we want shorter ids than URIs. So we could use the last part of each
  URI (\url{http://host/path#symbol}) but these symbols are no longer
  unique.  We could either use the name of the specification (OWL DL)
  that declares this name. But a redeclaration is allways allowed. Or
  the namespace abbrevs generated by the OWL DL parser could be
  used. For a set of theories (containing ontologies) developed in
  \CASLDL and translated to OWL DL the declaration of symbols is
  seperated into different OWL DL files if we translate a development
  graph into a set of OWL DL files.

  \begin{itemize}
  \item Namespace abbrevs go as first Id in compound
    Identifier. Collides a little bit with minCardinality[pred\_name],
    if this is an predicate Identifier obtained from an
    instantiation. \newline (maybe minCardinality[OWL,pred\_name])
  \item Namespace abbrevs are added as prefix to the Identifier with an
    underscore only if needed for distinction and the real mapping of
    identifiers into Namespaces (different OWL DL files) is written
    down after a new keyword.
  \end{itemize}

[I vote for the second possibility, because it keeps names shorter
whenever possible. Till] [I agree. Klaus]

\subsection{Renaming of predefined concepts}

During symbol map analysis it must be ensured that \Id{Thing} and
\Id{Nothing} are never renamed and that they are always associated
with \verb|owl:Thing| and \newline \verb|owl:Nothing|.

\subsection{AnnotationProperties}

On the OWL DL side so called AnnotionProperties can be declared and
used. One of them is used for \CASLDL sort marking. But what to do
with the other AnnotationProperties? 

Options:
\begin{enumerate}
\item keeping them as annotations in \CASLDL \ 
  this means providing a declaration and an application annotation for
  AnnotationProperties (see below).

\item declaring them as special binary relations, that could relate
  with every symbol (sort name, pred name, op name)
\end{enumerate}

[I vote for 1. Why should annotations be integrated into models
via predicates? Till] [These AnnotationProperties have to be declared
  on the OWL DL side like ordinary other properties. And they are
  applied like other properties. We have no place in the Signature yet
  for storing annotations that are passed over morphisms. Klaus]
  [Sounds strange to me. But if this the way OWL DL works, we have
   to support it. Till]

\section{Implementation decisions}

\subsection{Needed Annotations}

\begin{description}

\item[Namespaces] \ 

{\small"\KW{\%owl\_namespace(}" (QURI "=$>$" SIMPLE\_ID )+ "\KW{)\%}"}

mapping URIs to abbreviations that are kept during the translation
from and to OWL DL and that are used in compounds for the distinction
of symbols that would otherwise clash.

\item[Mapping of spec names to URIs (files)]\ 

{\small"\KW{\%owl\_export(}" (SIMPLE\_ID "=$>$" "(" QURI "," FILE\_PATH
  ")" )+ "\KW{)\%}"}

Each named spec that should be transformed to an OWL DL file must get
an URI and file path. The URI is used as the base URI of the xml (owl)
document. 

\item[Declaration and application of OWL Annotation Properties]\ 

OWL allows the declaration of untyped annotation properties. They can
be applied to all symbols / entities like the ontology as a whole and
to classes, properties and individuals. We will map them in \CASLDL to
\CASL annotations.  

{\small"\KW{\%owl\_annotation\_properties(}" SIMPLE\_ID + "\KW{)\%}"}

{\small"\KW{\%owl\_annotations(}" (SIMPLE\_ID "(" CID "," ANNO-LITERAL ")") + "\KW{)\%}"}

\end{description}

QURI ::= "\textbackslash"" URI "\textbackslash""

ANNO-LITERAL ::= DATA-LITERAL $|$ URI $|$ INDIVIDUAL-ID

CID is a \CASL Id that must be declared in the current specification (library).

DATA-LITERAL is a literal allowed for a subsort of \Id{Data}.

INDIVIDULA-ID is the Id of a declared constant operation.

\subsection{Needed Formula Extensions}

For Cardinality Restrictions three symbols are introduced which are
also reserved symbols then. They will be parsed as a predication of a
compound id with exactly one compound and two arguments: (1) a
variable quantified over Thing or a subsort of it and (2) a number
literal denoting the number of relations for each member of the
characterized class (type: \Id{nonNegativeInteger}).

\begin{hetcasl}
\Id{minCardinality}[PRED\_NAME](\Id{x}, NUMBER\_LITERAL)\\
\Id{maxCardinality}[PRED\_NAME](\Id{x}, NUMBER\_LITERAL)\\
\Id{cardinality}[PRED\_NAME](\Id{x}, NUMBER\_LITERAL)
\end{hetcasl}

\subsection{Needed Sign Extensions}

\begin{itemize}
\item Namespace abrreviation maps (maybe better as part of the
  GlobalAnnos record)
\item renamed symbols mapped to their real name (OWL DL name) with
  namespace abbrev (or URI)
\end{itemize}

\section{\CASLDL prelude}

A library of specifications in \CASLDL and \CASL named
\SId{CASL\_DL/Prelude}.

\subsection{\CASL specifications}

\SId{GenCardinality} from the WADT04 paper.

Theories of the known datatypes where all the opearations are hidden
except those needed for the construction of literals. These datatypes
are than collected under the supersort \Id{DATA}

\subsection{\CASLDL specifications}

Basic classes \Id{Thing} and \Id{Nothing} and their axiomatization.

A specification that embeds the \CASL specification of predefined
datatypes into \CASLDL (as predefined symbols that cannot be
changed). 

A combining specification that provides access to \Id{Thing},
\Id{Nothing} and \Id{DATA} including all subsorts of \Id{DATA} and all
``literals'' in one of these. This specification will be called
something like \SId{CASL\_DL\_prelude}

\noindent\textbf{-- OR --}

Maybe its better not to have this embedding specification at
all and apply something behind the scenes to get the mixfix and static
analysis working with the predefined stuff visible.

[I would vote for the first possibility. In CASL, there are no
predefined things, and we should keep this principle for
CASL-DL. Till] [This complicates checking the CASL\_DL language. Every
  renaming of the predefined OWL DL datatypes and Symbols must be
  rejected; every hiding, too. Klaus]  
  [But this can be implemented as an easy restriction on signature
   morphisms. Till]

\end{document}
