\section{Relations with FOC}
\label{cont_thorey:section:Foc}

Foc is a certified computer algebra library. That means a strong
enphasys is made in providing certification of correctness for its
algorithms. Developers of Foc start by building a stratification of
mathematical universes, called {\em species}. The inhabitants of these
universes are called {\em entities}. Each species define methods.
Those methods may define computational properties, theorems, axioms,
etc, of the universes. Species can inherit from other species: most in
the same way a class inherits form a superclass in object oriented
programming languages.  Methods of a specie could be redefined in a
sub-specie but the type of a method must not change along the line of
inheritance. That defines a tree of universes. The root of this tree
is a unique specie called Basic (or similar name). Each species has a
unique method called the carrier that defines the type of the entities
in that universe. The Basic species defines three methods, inherited
by all descendants, the carrier (empty), parse and unparse (or
toString?). Foc possesses a system of types ( $\rightarrow$, $*$) and
basic data types (int, float, list(), string). Proofs for theorems
(methods defined with the theorem construct) must be provided (in Coq
language).  Computational methods are defined in a language with
strong fuctional programming flavour (Foc compiler translates Foc
programs into OMCAL syntax). Species may be parameterized by basic
types, and collections.  A collection is a species with all its
methods completely defined.

What do we currently have?

Type-templates: A type template defines:
\begin{itemize}
\item a reference to a CD where a type is defined for variables of that type 
 (that could change and the type to be defined in the type template itself). 

\item a constructor that specifies how to build a variable of that type (this is the 
 equivalent of the parse method in a specie). 
 
\item One or more display methods in a species (equivalent ot the
  toString()).
  
\item No inheritace yet between type-templates.

\end{itemize}

\begin{table}[htbp]
  \centering
\begin{tabular}{|l|l|}
\hline\\
Type-Template   &       Species. \\
display         &       toString()\\
constructor     &       parse\\
??              &       methods\\
??              &       inheritance\\
??              &       Types.\\
Variables       &       Entities? \\
\hline
\end{tabular}
  \caption{Type-Templates vs Species.}
  \label{tab:comparison}
\end{table}




\subsection{New setting}
\label{sec:new}


Type-template.

\begin{itemize}
\item Defines a type for variables inhabiting that Type-template.  No
  reference to a CD will be made. Own type language?  All our types
  are derived from an OpenMath type. Integer, String, Float,
  parameterized list(*), they are all represented in OpenMath. We need
  a product of types, funtional types, etc.
\item Each type template has one or several constructors. For
  instance, an Integer can be constructed from an ordinary Integer, an
  OpenMath Integers, and so forth. When assigning a value to a
  variable all the constructors are tried in the order they were
  defined till one succed. If no constructor succeeded then an error
  is stored in the variable.
  
\item Constructors define promotions (or casting operations). For
  instance an integer should be promoted to a polynomial where one is
  needed.  This solves the casting problem.

\end{itemize}

Examples:

     \begin{description}
     \item[DMP Polynomials] they can be constructed from an integer,
       list of, pairs of integers, a expression $122*x^12$, a
       recursive polynomial, etc.
     \item[Matrices] a list of list, a list and two integers representing the 
        dimensions.
     \end{description}


Define a Mathematical Universe (think of other name, AGExtructure): 

\begin{itemize}
\item each Mathematical universe makes reference to a Type-Template
  where the type for an entity, or variable containing an entity of
  that universe, is defined.  That will be the carrier of that
  Universe. As the carrier refers to a type-template we already have
  methods to parse entities (variables) inhabiting that universe (via
  the constructors of the Type-Template).  For instance, a Universe
  Integers will refer as carrier to the Type-Template for Integers.

\item Methods will define computational methods, theorems, axioms,
  etc. For instance, a Universe Integer may define a methods called
  {\em plus}, {\em times}, etc. The same for a universe monoid, etc.
 
\item Computational methods will have a return type (a Type-template)
  and specify a list of arguments (possibly a variable list of
  arguments).  Arguments will be typed.  In method's body some
  computations may be specified involving the arguments. In order to
  specify the computations we plan to use an XML scripting language.
  Jelly, see http://jakarta.apache.org/commons/jelly/, is a good
  candidate for such a language. It is extensible an supports a
  superset of the JSP scripting language.

\end{itemize}
     

     Theorems and axioms may state formal properties about the Universe.
     \begin{itemize}
     \item We should allow multiple inheritance. Methods in a Universe
       are inherited and possible redefined in sub-Universes. Methods
       defined in more than one super-Universe will have to be
       explicitly inherited (that is we will have to specify which one
       to inherit).
       
     \item Computational methods could be virtual. That is they may be
       defined at a Universe but no implementation is provided in that
       Universe. A sub-Universe may redefine and provide an
       implementation for that method.

      NOTE: For each Universe there will be a type with the same name.

     \end{itemize}


REMARK: One possible application of previous setting is for the creation of 
        smart phraseebook services (or computational services). 
        
        Our current implemenation of phrasebooks is CD oriented that
        is there is a CDCodec for each CD and when we encounter an
        expression like
\begin{verbatim}
<OMA>
    <OMS name="pkus".../>
    <OBJECT1/>
    <OBJECT2/>    
</OMA>
\end{verbatim}
        Then for most sytems we have to check that are the types of
        \verb|<OBJECT1/>| and \verb|<OBJECT2/>| in order to provide thet
        good translation (if any is available).  That makes CDCodec
        implementation rather complicate. Othe problem we encounter is
        casting the results to the appropiate type.


        Now, suppose we have created a system with a hierarchy of Universes like

\begin{verbatim}
                    setoid
                      | 
                    monoid
                      |
                    Ring----Integer-Complex
                      |
                    Matrices(n,m,Integer)-Matrices(n,m,Complex)

\end{verbatim}
                    
        (there are some arrows missing). Then you get an expression
        like the one above to evaluate. Each Universe has its own plus
        defined (from monoid on). Furthermore we asume that, somehow,
        we have a binding from arith1.plus to all these plus methods.
        Then an evaluator engine will traverse the tree till it find
        (a completely defined) Universe in which the expresion could
        be evaluated (that is a universe where \verb|<OBJECT1/>| and
        \verb|<OBJECT2/>| are inhabitants apply the corresponding plus
        method. The correcponding plus method will take care of the
        necessary casting operations. For instance, if we were doing
        matrix computations then that method will force a casting to a
        matrix.  Which would be trivial because it would have only to
        apply one of the constructor methods on the Matrix-Type
        template (for example from a list of lists to a matrix).

        
        This service could work with several backengines at the time
        (taking advantages of the best feature of all the systems).

      
