Skip to content
GitLab
Commit 06b95f9b authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

draining

parent 64d69ecd
Hide whitespace changes
Inline Side-by-side
OM18-ole/.gitignore 0 → 100644
View file @ 06b95f9b
auto
*-blx.bib
*.aux
*.bbl
*.bcf
*.log
*.out
*.run.xml
*.synctex.gz
*.blg
*.sty
*.zip
*.cls
*.bib
OM18-ole/argseq.ocd 0 → 100644
View file @ 06b95f9b
<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>
OM18-ole/ext.rnc 0 → 100644
View file @ 06b95f9b
OMNATS = element OMNATS {omel}
OMNTH = element OMNTH {omel,omel}
omel |= OMNTH | OMNATS
OM18-ole/omle.rnc 0 → 100644
View file @ 06b95f9b
# *********************************************
#
# 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}
OM18-ole/omseq.ole 0 → 100644
View file @ 06b95f9b
<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>
OM18-ole/openmath2.rnc 0 → 100644
View file @ 06b95f9b
# 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 }
}
OM18-ole/paper.tex 0 → 100644
View file @ 06b95f9b
\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
OM18-ole/schemas.xml 0 → 100644
View file @ 06b95f9b
<?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>
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment