From 06b95f9bd95528bef9da2ac37473f614e4ec8185 Mon Sep 17 00:00:00 2001
From: Michael Kohlhase <michael.kohlhase@fau.de>
Date: Sun, 15 Apr 2018 15:23:40 +0200
Subject: [PATCH] draining
---
OM18-ole/.gitignore | 14 ++
OM18-ole/argseq.ocd | 59 +++++++++
OM18-ole/ext.rnc | 3 +
OM18-ole/omle.rnc | 60 +++++++++
OM18-ole/omseq.ole | 52 ++++++++
OM18-ole/openmath2.rnc | 89 +++++++++++++
OM18-ole/paper.tex | 289 +++++++++++++++++++++++++++++++++++++++++
OM18-ole/schemas.xml | 5 +
8 files changed, 571 insertions(+)
create mode 100644 OM18-ole/.gitignore
create mode 100644 OM18-ole/argseq.ocd
create mode 100644 OM18-ole/ext.rnc
create mode 100644 OM18-ole/omle.rnc
create mode 100644 OM18-ole/omseq.ole
create mode 100644 OM18-ole/openmath2.rnc
create mode 100644 OM18-ole/paper.tex
create mode 100644 OM18-ole/schemas.xml
diff --git a/OM18-ole/.gitignore b/OM18-ole/.gitignore
new file mode 100644
index 0000000..30fab50
--- /dev/null
+++ b/OM18-ole/.gitignore
@@ -0,0 +1,14 @@
+auto
+*-blx.bib
+*.aux
+*.bbl
+*.bcf
+*.log
+*.out
+*.run.xml
+*.synctex.gz
+*.blg
+*.sty
+*.zip
+*.cls
+*.bib
diff --git a/OM18-ole/argseq.ocd b/OM18-ole/argseq.ocd
new file mode 100644
index 0000000..eff1a6f
--- /dev/null
+++ b/OM18-ole/argseq.ocd
@@ -0,0 +1,59 @@
+<CD xmlns="http://www.openmath.org/OpenMathCD">
+ <CDComment>
+ This CD contains a (part of a) specification of argument sequences
+ for an OpenMath language extension.
+ </CDComment>
+ <CDName>argseq</CDName>
+ <CDBase>http://www.openmath.org/cd</CDBase>
+ <CDURL>http://www.openmath.org/cd/argseq.ocd </CDURL>
+ <CDReviewDate>2014-03-01</CDReviewDate>
+ <CDStatus>experimental</CDStatus>
+ <CDDate>2013-10-01</CDDate>
+ <CDVersion>0</CDVersion>
+ <CDRevision>1</CDRevision>
+
+ <Description>
+ This CD defines argument sequences for the use in an OpenMaht3
+ language extension.
+ </Description>
+ <CDDefinition>
+ <Name>nth</Name>
+ <Role>application</Role>
+ <Description>
+ This symbol represents the sequence selector. The first argument
+ is a natural number n and the second an argument sequence S.
+ The argument selector returns the n-th element in S, if it exits.
+ </Description>
+ </CDDefinition>
+ <CDDefinition>
+ <Name>nats</Name>
+ <Role>application</Role>
+ <Description>
+ Given a natural number n, this symbol returns the sequence of the
+ first n natural numbers (starting at zero).
+ </Description>
+ <CMP>
+ For any natural numbers n and m with m>n, the n-th component of nats(m) is n
+ </CMP>
+ <FMP>
+ <OMOBJ xmlns="http://www.openmath.org/OpenMath">
+ <OMBIND>
+ <OMS cd="quant1" name="forall"/>
+ <OMBVAR><OMV name="n"/><OMV name="m"/></OMBVAR>
+ <OMA>
+ <OMS cd="logic1" name="implies"/>
+ <OMA><OMS cd="relation1" name="gt"/><OMV name="m"/><OMV name="n"/></OMA>
+ <OMA>
+ <OMS cd="relation1" name="eq"/>
+ <OMA>
+ <OMS cd="argseq" name="nth"/>
+ <OMA><OMS cd="argseq" name="nats"/><OMV name="n"/></OMA>
+ </OMA>
+ </OMA>
+ <OMV name="n"/>
+ </OMA>
+ </OMBIND>
+ </OMOBJ>
+ </FMP>
+ </CDDefinition>
+</CD>
diff --git a/OM18-ole/ext.rnc b/OM18-ole/ext.rnc
new file mode 100644
index 0000000..731465e
--- /dev/null
+++ b/OM18-ole/ext.rnc
@@ -0,0 +1,3 @@
+ OMNATS = element OMNATS {omel}
+ OMNTH = element OMNTH {omel,omel}
+ omel |= OMNTH | OMNATS
diff --git a/OM18-ole/omle.rnc b/OM18-ole/omle.rnc
new file mode 100644
index 0000000..5cfb514
--- /dev/null
+++ b/OM18-ole/omle.rnc
@@ -0,0 +1,60 @@
+# *********************************************
+#
+# Relax NG Schema for OpenMath Language Extensions
+#
+# *********************************************
+
+default namespace = "http://www.openmath.org/OpenMathCD"
+
+## we include an encapsulated version of the OpenMath Schema
+omelorig = grammar {include "openmath2.rnc" {start=omel}}
+## and one we extend with the generated extension (extract from the LED in question)
+omelext = grammar{include "openmath2.rnc" {start=omel} include "ext.rnc"}
+
+## metadata analogous to the one of CDs.
+OLEComment = element OLEComment { text }
+OLEName = element OLEName { xsd:NCName }
+OLEUses = element OLEUses { OLEName* }
+OLEURL = element OLEURL { xsd:anyURI }
+OLEBase = element OLEBase { xsd:anyURI }
+OLEReviewDate = element OLEReviewDate { xsd:date }
+OLEDate = element OLEDate { xsd:date }
+OLEVersion = element OLEVersion { xsd:nonNegativeInteger }
+OLERevision = element OLERevision { xsd:nonNegativeInteger }
+OLEStatus = element OLEStatus { "official" | "experimental" | "private" | "obsolete"}
+
+Description = element Description { text }
+
+## the top-level element
+start = OMLangExt
+ OMLangExt =
+ element OMLangExt {
+ (OLEComment* & Description? &
+ OLEName & OLEURL? & OLEBase? &
+ OLEReviewDate? & OLEDate & OLEStatus &
+ OLEUses? &
+ OLEVersion & OLERevision),
+ schemaext, equality, translation}
+
+name.attrib = attribute name {xsd:NCName}?
+exprlist.attribs = name.attrib
+exprlist.model = headexp*
+exprlist = element exprlist {exprlist.attribs & exprlist.model}
+
+expr.attribs = name.attrib
+expr.model = empty
+expr = element expr {expr.attribs & expr.model}
+
+head.class = exprlist | expr
+headexp = grammar {include "openmath2.rnc" {start = omel}
+ include "ext.rnc"
+ omel |= parent head.class
+ omvar |= parent head.class}
+
+## and now the LED-specific elements
+schemaext = element schemaext {text}
+equality = element equality {omelext+}
+translation = element translation {attribute cd {text},rule+}
+rule = element rule {headexp,omelorig}
+
+
diff --git a/OM18-ole/omseq.ole b/OM18-ole/omseq.ole
new file mode 100644
index 0000000..6df15ea
--- /dev/null
+++ b/OM18-ole/omseq.ole
@@ -0,0 +1,52 @@
+<OMLangExt xmlns="http://www.openmath.org/OpenMathCD">
+ <OLEName>seq</OLEName>
+ <OLEDate>2014-04-22</OLEDate>
+ <OLEStatus>experimental</OLEStatus>
+ <OLEVersion>1</OLEVersion>
+ <OLERevision>1</OLERevision>
+ <schemaext>
+ OMNATS = element OMNATS {omel}
+ OMNTH = element OMNTH {omel,omel}
+ omel |= OMNTH | OMNATS
+ </schemaext>
+ <equality>
+ <OMBIND>
+ <OMS cd="quant1" name="forall"/>
+ <OMBVAR><OMV name="n"/><OMV name="m"/></OMBVAR>
+ <OMA>
+ <OMS cd="logic1" name="implies"/>
+ <OMA><OMS cd="relation1" name="gt"/><OMV name="m"/><OMV name="n"/></OMA>
+ <OMA>
+ <OMS cd="relation1" name="eq"/>
+ <OMNTH>
+ <OMI>n</OMI>
+ <OMNATS><OMI>m</OMI></OMNATS>
+ </OMNTH>
+ <OMI>n</OMI>
+ </OMA>
+ </OMA>
+ </OMBIND>
+ </equality>
+ <translation cd="argseq">
+ <rule>
+ <OMNTH>
+ <expr name="n"/>
+ <exprlist name="seq">
+ <expr name="elt"/>
+ </exprlist>
+ </OMNTH>
+ <OMA>
+ <OMS cd="seqs" name="nth"/>
+ <render name="n"/>
+ <iterate name="seq">
+ <render name="elt"/>
+ </iterate>
+ </OMA>
+ </rule>
+ <rule>
+ <OMNATS><expr name="n"/></OMNATS>
+ <OMA><OMS cd="seqs" name="nats"/><render name="n"/></OMA>
+ </rule>
+ </translation>
+</OMLangExt>
+
diff --git a/OM18-ole/openmath2.rnc b/OM18-ole/openmath2.rnc
new file mode 100644
index 0000000..2d07eb1
--- /dev/null
+++ b/OM18-ole/openmath2.rnc
@@ -0,0 +1,89 @@
+# RELAX NG Schema for OpenMath 2
+# $Id: openmath2.rnc 8959 2011-09-02 06:01:43Z kohlhase $
+# $HeadURL: https://svn.omdoc.org/repos/omdoc/branches/omdoc-1.3/schema/rnc/openmath2.rnc $
+# See the documentation and examples at http://www.openmath.org
+
+default namespace om = "http://www.openmath.org/OpenMath"
+
+start = OMOBJ
+
+# OpenMath object constructor
+OMOBJ = element OMOBJ { compound.attributes,
+ attribute version { xsd:string }?,
+ omel }
+
+# Elements which can appear inside an OpenMath object
+omel =
+ OMS | OMV | OMI | OMB | OMSTR | OMF | OMA | OMBIND | OME | OMATTR |OMR
+
+# things which can be variables
+omvar = OMV | attvar
+
+attvar = element OMATTR { common.attributes,(OMATP , (OMV | attvar))}
+
+
+cdbase = attribute cdbase { xsd:anyURI}?
+
+# attributes common to all elements
+common.attributes = (attribute id { xsd:ID })?
+
+# attributes common to all elements that construct compount OM objects.
+compound.attributes = common.attributes,cdbase
+
+# symbol
+OMS = element OMS { common.attributes,
+ attribute name {xsd:NCName},
+ attribute cd {xsd:NCName},
+ cdbase }
+
+# variable
+OMV = element OMV { common.attributes,
+ attribute name { xsd:NCName} }
+
+# integer
+OMI = element OMI { common.attributes,
+ xsd:string {pattern = "\s*(-\s?)?[0-9]+(\s[0-9]+)*\s*"}}
+# byte array
+OMB = element OMB { common.attributes, xsd:base64Binary }
+
+# string
+OMSTR = element OMSTR { common.attributes, text }
+
+# IEEE floating point number
+OMF = element OMF { common.attributes,
+ ( attribute dec { xsd:double } |
+ attribute hex { xsd:string {pattern = "[0-9A-F]+"}}) }
+
+# apply constructor
+OMA = element OMA { compound.attributes, omel+ }
+
+# binding constructor
+OMBIND = element OMBIND { compound.attributes, omel, OMBVAR, omel }
+
+# variables used in binding constructor
+OMBVAR = element OMBVAR { common.attributes, omvar+ }
+
+# error constructor
+OME = element OME { common.attributes, OMS, (omel|OMFOREIGN)* }
+
+# attribution constructor and attribute pair constructor
+OMATTR = element OMATTR { compound.attributes, OMATP, omel }
+
+OMATP = element OMATP { compound.attributes, (OMS, (omel | OMFOREIGN) )+ }
+
+# foreign constructor
+OMFOREIGN = element OMFOREIGN {
+ compound.attributes, attribute encoding {xsd:string}?,
+ (omel|notom)* }
+
+# Any elements not in the om namespace
+# (valid om is allowed as a descendant)
+notom =
+ (element * - om:* {attribute * { text }*,(omel|notom)*}
+ | text)
+
+# reference constructor
+OMR = element OMR { common.attributes,
+ attribute href { xsd:anyURI }
+ }
+
diff --git a/OM18-ole/paper.tex b/OM18-ole/paper.tex
new file mode 100644
index 0000000..300362b
--- /dev/null
+++ b/OM18-ole/paper.tex
@@ -0,0 +1,289 @@
+\documentclass{easychair}
+\usepackage{doc}
+\usepackage{makeidx}
+
+\usepackage{url,graphicx,wrapfig,subcaption}
+\usepackage{amsfonts,amstext}
+\usepackage{lstomdoc}
+\lstset{language=OpenMath}
+\lstset{columns=fullflexible,basicstyle=\sf}
+\usepackage{rotating}
+\usepackage{paralist,xcolor}
+\usepackage{calbf}
+\usepackage[hide]{ed}
+\usepackage[hyperref=auto,style=alphabetic,isbn=false,backend=bibtex]{biblatex}
+%\usepackage{bibtweaks}
+\addbibresource{kwarcpubs.bib}
+\addbibresource{extpubs.bib}
+\addbibresource{kwarccrossrefs.bib}
+\addbibresource{extcrossrefs.bib}
+\usepackage{stex-logo}
+\usepackage{hyperref}
+\def\KWARCslides#1{/Users/kohlhase/stc/slides/#1}
+
+\def\omdoc{OMDoc\xspace}
+\def\mathml{MathML\xspace}
+\def\openmath{OpenMath\xspace}
+\def\defemph{\textbf}
+\def\thmo#1#2{\mathsf{#1}\colon\kern-.15em{#2}}
+
+\title{\openmath Language Extensions}
+\titlerunning{\openmath Language Extensions}
+\author{Michael Kohlhase}
+\institute{Computer Science, Jacobs University\\\url{http://kwarc.info/kohlhase}}
+\authorrunning{Michael Kohlhase}
+
+\begin{document}
+\maketitle
+
+\begin{abstract}
+ We propose a language extension mechanism for \openmath that will allow us to introduce
+ new language features (as have been called for by the community) while keeping the
+ underlying core language intact so that we can maintain compatibility with MathML3 and
+ the upcoming ISO standard.
+ We exhibit the mechanism on the example of extending \openmath with sequences and
+ discuss other language extensions.
+
+ In a nutshell, we propose to establish OpenMath Language Extension Dictionaries (OLEDs)
+ as an OpenMath extension mechanism akin to Content Dictionaries, but at the language
+ level. OLEDs have three functions: They a) extend the syntax admissible in the extended
+ language, b) specify the meaning of the language extensions, and c) specify when two objects
+ of the extended language are equal. For a) OLEDs use an extension of the OM RelaxNG
+ schema, for b) a set of OM-represented rewrite rules into the OpenMath2 language, and
+ for c) a set of terminatig rewrite rules.
+\end{abstract}
+
+\section{Introduction}
+
+The \openmath society has decided to task a committee to assess the viability of extending
+the \openmath2~\cite{BusCapCar:2oms04} standard and bring in all the extension proposals
+out there. There are a variety of proposals that involve extending the set of \openmath
+objects, e.g. to introduce sequences in~\cite{HKR:sequences:11}. However, the recent
+synchronization of \openmath and content \mathml in the \mathml3
+recommendation~\cite{CarlisleEd:MathML3} and its imminent ISO standardization restrict
+the possible extensions severely.
+
+We propose a way to have our cake (minimize extensions to the \openmath objects) and eat
+it (get native syntax for often-used mathematical representational idioms). Instead of
+extending the \openmath language with a limited set of primitives we propose to extend
+\openmath by a syntax extension mechanism much like \openmath CDs constitute an extension
+mechanism for the mathematical vocabularies.
+
+This proposal is similar in spirit to the re-interpretation of the content \mathml format
+into a structurally regular core language (``strict content \mathml'') which is
+interpreted as \openmath objects and a more extensive language (``full content \mathml'')
+whose semantics is given by translation into strict content \mathml.
+
+In our proposal, \openmath2 is retained as a strict core language, but various
+``pragmatic'' language extensions can be introduced via \openmath \textbf{language
+ extension dictionaries} (LED). The \openmath society adopts and maintains a set of
+``standard LEDs'' alongside with the standard CDs. The \openmath3 format is then induced by
+the \openmath standard LEDs from the strict core given by the \openmath2 language. Other
+entities can standardize other extensions in LED format -- e.g. the Math working group at
+W3C could provide LEDs for full content MathML.
+
+\section{Language Extension Dictionaries}
+Language Extension Dictionaries have three functions: to
+\begin{compactenum}
+\item\label{n:schema} extend the syntax admissible in the extended language,
+\item\label{n:trans} specify the meaning of the language extensions, and
+\item\label{n:eq} specify when two objects of the extended language are equal.
+\end{compactenum}
+As the \openmath and \mathml specifications give a RelaxNG schema~\cite{CM:RELAXNG01} for
+the syntax, we do the same in the LED. Following the \mathml3 lead we give the semantics of
+the ``full language'' by translation into the strict core. Note that the first two
+functions are addressed at the user who wants to write meaningful expressions in the
+extended format. The third function is only addressed to phrasebook implementors of the
+extended objects.
+
+\section{An Example Language Extension: Argument Sequences}
+We now fortify our intuition with a small LED fragment that introduces two extension
+elements from~\cite{HKR:sequences:11}. Note that these have been chosen for expository
+reasons only, in particular, they do not constitute a concrete extension proposal, that
+would be based on~\cite{HKR:flexary:14}.
+
+\subsection{Example A Language Extension Dictionary for Sequences}\label{sec:omseq:led}
+
+\lstinputlisting[caption=A LED for sequences,label=lst:ledseq]{omseq.ole}
+
+The \lstinline|OMLangExt|\footnote{Note that the names of LED elements have been chosen
+ more or less randomly and should be carefully re-considered before this turns note into
+ a standards extension proposal.} element is the top-level element of language
+definitions. It contains metadata that is isomorphic to that of \openmath CDS and three
+children for the three functions mentioned above.
+
+\subsubsection{The Schema Extension}
+
+The \lstinline|schemaext| contains contains RelaxNG rules in compact form that extend the
+\openmath2 schema. In our example, the language of \openmath objects is extended by two
+new constructs:
+\begin{compactitem}
+\item the sequence constructor \lstinline|OMNATS| that (given a natural number $n$)
+ represents the sequence of the first $n$ natural numbers starting at zero.
+\item the sequence selector \lstinline|OMNTH| takes an \openmath object representing a
+ natural number $n$ and a sequence $S$ as arguments and represents the
+ $n$\textsuperscript{th} element of $S$ (if it exists).
+\end{compactitem}
+Correspondingly, the \lstinline|schemaExt| element contains a rule for both of the
+elements, an extension of the \openmath expressions by \lstinline|OMNTH| elements and a
+new syntactic category \lstinline|omseq| that contains \lstinline|OMNATS| elements. From
+the LED in Listing~\ref{lst:ledseq}, we can generate RelaxNG schema for the extended
+language in Figure~\ref{fig:omobj+seq}.
+
+We probably need to have an extension for OMCDs as well. Maybe we can use a dynamic
+extension mechanism, where an OMOBJ specifies what extensions it uses in a special
+attribute, which lists the extensions it uses. If we have a list of LEDs supported by OM,
+then we can probably compile such a RelaxNG schema from them.
+
+\begin{figure}[ht]\centering\lstset{aboveskip=0pt,belowskip=0pt}
+\begin{lstlisting}[language=RNC]
+input "openmath2.rnc"
+OMNATS = element OMNATS {omel}
+OMNTH = element OMNTH {omel,omseq}
+omseq = OMNATS
+omel |= OMNTH
+\end{lstlisting}%|
+\caption{The RelaxNG Schema \lstinline|omobj+seq|.}\label{fig:omobj+seq}
+\end{figure}
+
+\subsubsection{Equality}
+\def\nth{\text{nth}} \def\nats{\text{nats}}
+
+The \lstinline|equality| element contains equality rules that say when two elements in the
+extended language are equal expressed as \openmath elements. Here, we have the relation:
+\begin{equation}\label{nthnats}
+\forall n.n>m \Rightarrow \nth(\nats(n)) = n
+\end{equation}
+
+\ednote{MK: we have to think about this, maybe we can get by by importing equality
+ from the corresponding CD.}
+
+\subsubsection{Translation to \openmath2}
+And finally, the \lstinline|translation| element contains rules that allow to translate
+objects from the extended language into core \openmath2 objects.
+
+We propose the OMDoc presentation rewriting for translation since it is relatively
+restricted and declarative here. But arguably having XSLT for translation would be more
+standards-conformant and more powerful -- which might or might not be a good thing. In
+principle any translation mechanism would work, the concrete choice of a mechanism is an
+open design choice. The XSLT for our example is in Figure~\ref{fig:olexslt}.
+
+The \lstinline|translation| element gives objects in the extended language their meaning
+by translation into strict \openmath2 (with a special content dictionary
+\lstinline|argseq| specified in the \lstinline|cd| attribute of the
+\lstinline|translation| element\footnote{We probably need to allow multiple CDs here,
+ since we may need combinations. Unfortunately, we do not have inheritance in CDs, so we
+ need more. But on the other hand, the whole attribute is unnecessary, since we can just
+ pick up the necessary CDs from the translation objects themselves.}; see
+Listing~\ref{lst:ledocd}).
+
+\begin{figure}[ht]\centering\lstset{aboveskip=0pt,belowskip=0pt}
+\begin{subfigure}{6.5cm}
+\begin{lstlisting}
+<OMNTH>
+ <OMA>
+ <OMS cd="arith1" name="plus"/>
+ <OMI>1</OMI>
+ <OMI>2</OMI>
+ </OMA>
+ <OMNATS><OMI>7</OMI></OMNATS>
+</OMNTH>
+\end{lstlisting}
+\caption{A \openmath object with Sequences}\label{fig:omseq-src}
+\end{subfigure}\qquad
+\begin{subfigure}{7cm}
+\begin{lstlisting}
+<OMA>
+ <OMS cd="argseq" name="nth"/>
+ <OMA>
+ <OMS cd="arith1" name="plus"/>
+ <OMI>1</OMI>
+ <OMI>2</OMI>
+ </OMA>
+ <OMA>
+ <OMA>
+ <OMS cd="argseq" name="omnats"/>
+ <OMI>7</OMI>
+ </OMA>
+</OMA>
+\end{lstlisting}
+\caption{Its Translation}\label{fig:omseq-trans}
+\end{subfigure}
+\caption{Translating Extended \openmath Expressions}\label{fig:omseq}
+\end{figure}
+
+With the LED from Listing~\ref{lst:ledseq} we can express \openmath objects like the one
+in Figure~\ref{fig:omseq-src} with the new \openmath elements licensed by the language
+definition: The sequence selector \lstinline|OMNTH| expects an openmath object (denoting a
+natural number) as the first child and a sequence as the second. The latter is represented
+by the \lstinline|OMNATS| element that represents the sequence of the first seven natural
+numbers.
+
+\begin{figure}
+\begin{lstlisting}
+<xsl:template match="om:OMNTH">
+ <om:OMA>
+ <OMS cd="argseq" name="nth"/>
+ <xsl:apply-templates/>
+ </om:OMA>
+</xsl:template>
+<xsl:template match="om:OMNATS">
+ <om:OMA>
+ <OMS cd="argseq" name="nth"/>
+ <xsl:apply-templates/>
+ </om:OMA>
+</xsl:template>
+\end{lstlisting}
+\caption{An XSLT alternative to pattern-based translation}\label{fig:olexslt}
+\end{figure}
+\subsection{The Corresponding CD}\label{sec:omseq:cd}
+
+The translation in the LED above uses special symbols from the \lstinline|argseq| CD,
+which we give in Listing~\ref{lst:ledocd}. The CD introduces two symbols \lstinline|nth|
+and \lstinline|nats|\ednote{MK: maybe it should also introduce the set of sequences, which
+ corresponds to the new schema class?}. Note that a full development of argument
+sequences would contain more symbols and relations.
+
+The \lstinline|CMP| and \lstinline|FMP| elements state mathematical properties that
+specify the relations between the symbols, here the strict \openmath variant of
+\ref{nthnats}\footnote{Here it would be good to have an \lstinline|id| attribute on the
+ \lstinline|FMP|, so that we can reference it in the LED as a justification.}
+
+ \lstinputlisting[caption=The CD for the LED in \ref{lst:ledseq},
+language=omCD,label=lst:ledocd]{argseq.ocd}
+
+\section{Conclusion}
+
+We have sketched an extension mechanism for \openmath that allows to interpret pragmatic
+extensions in terms of a core language using specific CDs. That would allow use to obtain
+\openmath3 as a collection of language extensions while retaining \openmath2 as a strict
+core language -- which is important, since it is referenced as a semantic basis of
+\mathml3~\cite{CarlisleEd:MathML3}. The language extension mechanism might be interesting
+as a tool for formally recast the full \mathml3 language as a collection of extensions to
+strict content \mathml. This would be a nice test case for the extension mechanisms
+expressivity.
+
+\printbibliography
+
+\begin{appendix}
+\section{A RelaxNG Schema for LEDs}
+Here we have a RelaxNG schema for LEDs, note that OLEs are self-referential in the sense
+that they already contain the language extensions they introduce, so we have to include a
+sub-schema \lstinline|ext.rnc| that is the contents oft he \lstinline|schemaext|
+element. But with this little trick, we can validate quite nicely.
+\lstinputlisting[caption=The CD for the LED in \ref{lst:ledseq},
+language=RNC,label=lst:omle]{omle.rnc}
+\end{appendix}
+\end{document}
+%%% Local Variables:
+%%% mode: LaTeX
+%%% TeX-master: t
+%%% End:
+
+
+% LocalWords: maketitle mathml mathml3 printbibliography LDs eq lst ldseq th 2oms04 nats
+% LocalWords: lstinputlisting omseq.ole schemaext ednote compactitem omseq seq nats omCD
+% LocalWords: textsuperscript argseq centering lstset aboveskip belowskip omel nthnats
+% LocalWords: lstlisting arith1 qquad omnats ldocd argseq.ocd RELAXNG01 textbf ext.rnc
+% LocalWords: ledseq omobj openmath2.rnc ledocd forall Rightarrow compactenum omle
+% LocalWords: subsubsection omle.rnc
diff --git a/OM18-ole/schemas.xml b/OM18-ole/schemas.xml
new file mode 100644
index 0000000..1d9ad21
--- /dev/null
+++ b/OM18-ole/schemas.xml
@@ -0,0 +1,5 @@
+<?xml version="1.0"?>
+<locatingRules xmlns="http://thaiopensource.com/ns/locating-rules/1.0">
+ <uri resource="argseq.ocd" uri="../../../vc/svn/omdoc.org/omdoc/branches/omdoc-1.3/schema/rnc/omcd2.rnc"/>
+ <uri resource="omseq.ole" uri="omle.rnc"/>
+</locatingRules>
--
GitLab