\def\I{{\cal I}}
\def\Z{{\bf Z}}
\def\Q{{\bf Q}}
\def\C{{\bf C}}
\def\R{{\bf R}}
\def\CL{\mathop{\rm CL}}
\def\IDA{{}_{\rm DA}\int}
\def\DDA{D_{\rm DA}}
\def\cDA{constant${}_{\rm DA}$}
\def\fracDDA#1#2{\frac{{\rm d}#1}{{\rm d}_{\rm DA}#2}}
\def\Ied{{}_{\epsilon\delta}\int}
\def\Ded{D_{\epsilon\delta}}
\def\fracDed#1#2{\frac{{\rm d}#1}{{\rm d}_{\epsilon\delta}#2}}
\documentclass{article}   % Without notes
\usepackage{verbatim}
\usepackage{url}

\title{Conditions in MathML}
\author{James Davenport\\\url{J.H.Davenport@bath.ac.uk}}

\begin{document}
\maketitle
\begin{abstract}\noindent
JHD's attempt (currently very incomplete) to look at the uses of 
\verb+condition+ in the MathML2 specification.
\end{abstract}
\section{Introduction}
This note follows from the OpenMath tele-conference at 15:00
GMT\footnote{16:00 BST, 17:00 CET.} on 10/10/2008. See
Michael Kohlhase (\url{m.kohlhase@jacobs-university.de})'s mail
\url{48F05077.7010004@jacobs-university.de}.
%Date: Sat, 11 Oct 2008 09:06:31 +0200
\par
The summary reads as follows.
\begin{quotation}\noindent
James was tasked to make sense of the integration/differentiation
examples from the MathML2 spec and make concrete suggestions for the
expression-based calculus CD.
\end{quotation}
The detailed record shows that it should be a wider look at {\it all\/} uses
of condition, and this version is an attempt to look at all occurrences of
\verb+condition+ in the MathML2 specification.
\section{Appendix C}
\subsection{C.2.2.4 MMLdefinition: {\tt interval}}
This contains the following example.
\begin{verbatim}
<interval>
  <bvar><ci>x</ci></bvar>
  <condition>
    <apply><lt/><cn>0</cn><ci>x</ci></apply>
    </condition>
</interval>
\end{verbatim}
Presumably this represents $(0,\infty)$. Equally, this is presumably intended
to close over \verb+<interval>+, i.e. $x$ is bound in this expression, and
freely $\alpha$-convertible. However, it seems to JHD to be purely ``luck''
that this defines an interval. What about the following?
\begin{verbatim}
<interval>
  <bvar><ci>x</ci></bvar>
  <condition>
    <apply><lt/><cn>1</cn>
       <apply> <power/>
         <ci>x</ci>
         <cn>2</cn>
         </apply>
      </apply>
    </condition>
</interval>
\end{verbatim}
By the same logic, this is $(-\infty,-1)\cup(1,\infty)$.  As far as JHD can
see, this use of \verb+interval+ is basically a declaration of a set, coupled
with an assertion that that set is in fact an interval, which assertion is, in
fact, true in the first case, but not the second.
\subsection{C.2.2.5 MMLdefinition: {\tt inverse}}
This contains the following example.
\begin{verbatim}
<apply><forall/>
  <bvar><ci>y</ci></bvar>
  <bvar><ci type="function">f</ci></bvar>
  <condition>
    <apply><in/>
      <ci>y</ci>
      <apply><csymbol definitionURL="domain"><mtext>Domain</mtext></csymbol>
        <apply><inverse/><ci type="function">f</ci></apply>
      </apply>
    </apply>
  </condition>
  <apply><eq/>
    <apply><ci type="function">f</ci>
      <apply><apply><inverse/><ci type="function">f</ci></apply>
        <ci>y</ci>
      </apply>
    </apply>
    <ci>y</ci>
  </apply>
</apply>
\end{verbatim}
The associated textual description is 
\begin{verbatim}
ForAll( y, such y in domain( f^(-1) ), f( f^(-1)(y) ) = y
\end{verbatim}
which does not include the fact that $f$ is in the scope of $\forall$.
\par
This usage seems to be basically a ``typed quantifier'', and as such could
look like the following.
\begin{verbatim}
<OMBIND>
  <OMA>
    <OMS name="forallrestricted" cd="quantifier2"/>
    <OMA>
      <OMS name="domain" cd="fns1"/>
      <OMA>
        <OMS name="inverse" cd="fns1"/>
        <OMV name="f"/>
      </OMA>
    </OMA>
  </OMA>
  <OMBVAR> <OMV name="y"/> </OMBVAR>
  <OMA>
    <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMV name= "f"/>
      <OMA>
        <OMA>
          <OMS name="inverse" cd="fns1"/>
          <OMV name= "f"/>
        </OMA>
        <OMV name= "y"/>
      </OMA>
    </OMA>
    <OMV name= "y"/>
  </OMA>
</OMBIND>
\end{verbatim}
This resembles the ``vernacular'', and does not bind $f$. If we wanted to do
so, along the lines of the MathML, we would have to wrap the whole thing in
another \verb+forall+. The two cannot be combined, as we want to be able to
$\alpha$-convert $f$ in the argument of \verb+forallrestricted+, and, as MK's
note of the tele-conference reads:
\begin{quotation}\noindent
In particular, we do not
      want to accept the occurrence of the bound variable in the
      (complex) binding operator. In particular, the OpenMath2 standard
      restricts alpha-conversion to the second and third children of the
      OMBIND, which is consistent with this view.
\end{quotation} 
See section \ref{sec:defintcond} below for an example of where this rule
bites.
\subsection{C.2.2.7 MMLdefinition: {\tt condition}}
This section contains two examples.
\subsubsection{C.2.2.7(1) MMLdefinition: {\tt condition}}
\begin{verbatim}
<condition>
  <apply><lt/>
    <apply><power/><ci>x</ci><cn>5</cn></apply>
    <cn>3</cn>
  </apply>
</condition>
\end{verbatim}
It is hard to understand the meaning of this fragment in isolation (and
presumably the reader was not intended to do so). If it was intended to be
part of an encoding of a set (mathematically, representing the interval
$(-\infty,3^{1/5})$, or possibly $[0,3^{1/5})$), then \verb+suchthat+ from
\verb+set1+ is appropriate. Here is the example from \verb+set1+ reworked to
match the MathML example (as $(-\infty,3^{1/5})$: if one wanted $[0,3^{1/5})$
one would have to add $x\ge0$, or change from $\bf R$ as the base set).
\begin{verbatim}
<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0"
       cdbase="http://www.openmath.org/cd">
  <OMA>
    <OMS cd="set1" name="suchthat"/>
    <OMS cd="setname1" name="R"/>
    <OMBIND>
      <OMS cd="fns1" name="lambda"/>
      <OMBVAR>
        <OMV name="x"/>
      </OMBVAR>
      <OMA>
        <OMS cd="relation1" name="lt"/>
        <OMA>
          <OMS cd="arith1" name="power"/>
          <OMV name="x"/>
          <OMI> 5 </OMI>
        </OMA>
        <OMI> 3 </OMI>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
\end{verbatim}
We should note that the OpenMath makes it clear that $x$ is bound by the
(\verb+OMBIND+ whose first child is the)
\verb+lambda+, whereas the MathML, being only a fragment, does not state the
scope.
\subsubsection{C.2.2.7(2) MMLdefinition: {\tt
condition}}\label{sec:defintcond}
\begin{verbatim}
<apply><int/>
  <bvar><ci>x</ci></bvar>
  <condition><apply><in/><ci>x</ci><ci type="set">C</ci></apply></condition>
  <apply><ci type="function">f</ci><ci>x</ci></apply>
</apply>
\end{verbatim}
This seems, to JHD, to be typical of the confusion that can arise over
\verb+condition+s. Let us look at this expression in the vernacular: 
\begin{equation}\label{defintcond}
\int_{x\in C}f(x){\rm d} x,
\end{equation}
and observe that this is probably equivalent to $\int_{C}f(x){\rm d} x$.
\par
In terms of \verb+calculus1+ (calculus with functions \cite{JHD})
this can be expressed as 
\begin{verbatim}
<OMA>
  <OMS cd="calculus1" name="defint"/>
  <OMV name="C"/>
  <OMV name="f"/>
</OMA>
\end{verbatim}
and $x$ doesn't appear at all. If one wants it to, then one writes
\begin{verbatim}
<OMA>
  <OMS cd="calculus1" name="defint"/>
  <OMV name="C"/>
  <OMBIND>
    <OMS cd="fns1" name="lambda"/>
    <OMBVAR>
      <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMV name="f"/>
      <OMV name="x"/>
    </OMA>
  </OMBIND>
</OMA>
\end{verbatim}
as in the example in \verb+calculus1+.
\par
MK's note \cite{MK} on \verb+calculus3+ (calculus with expressions \cite{JHD}), suggests (in MathML syntax)
\begin{verbatim}
<bind>
  <apply>
    <csymbol cd="calculus3">defintset</csymbol>
    <ci>C</ci>
  </apply>
  <bvar><ci>x</ci></bvar>
  <apply><ci>f</ci><ci>x</ci></apply>
</bind>
\end{verbatim}
which is a precise translation of the previous one from the language of
functions to expressions.
In OpenMath syntax it would be the following.
\begin{verbatim}
<OMBIND>
  <OMA>
    <OMS cd="calculus3" name="defintset"/>
    <OMV name="C"/>
  </OMA>
  <OMBVAR>
    <OMV name="x"/>
  </OMBVAR>
  <OMA>
    <OMV name="f"/>
    <OMV name="x"/>
  </OMA>
</bind>
\end{verbatim}
MK's note also suggests an alternative way of expressing (\ref{defintcond}),
which in MathML syntax would be the following.
\begin{verbatim}
<bind>
  <apply>
    <csymbol cd="calciulus3">defintcond</csymbol>
    <apply><in/>
      <ci>x</ci>
      <ci>C</ci>
    </apply>
  </apply>
  <bvar><ci>x</ci></bvar>
  <apply><ci>f</ci><ci>x</ci></apply>
</bind> 
\end{verbatim}
In OpenMath syntax it would be the following.
\begin{verbatim}
<OMBIND>
  <OMA>
    <OMS cd="calculus3" name="defintcond"/>
    <OMA>
      <OMS name="in" cd="set1"/>
      <OMV name="x"/>
      <OMV name="C"/>
    </OMA>
  </OMA>
  <OMBVAR>
    <OMV name="x"/>
  </OMBVAR>
  <OMA>
    <OMV name="f"/>
    <OMV name="x"/>
  </OMA>
</bind>
\end{verbatim}
This, however, falls foul of %OpenMath's rule that 
\begin{quotation}\noindent
the OpenMath2 standard restricts alpha-conversion to the second and third
children of the OMBIND
\end{quotation}
and hence JHD does not see how \verb+defintcond+ as postulated can make its
way into OpenMath.
\subsection{C.2.2.14 MMLdefinition: {\tt image}}
This section contains the following example.
\begin{verbatim}
<apply><forall/>
  <bvar><ci>x</ci></bvar>
  <condition>
    <apply><in/>
      <ci>x</ci>
      <apply><image/><ci>f</ci></apply>
    </apply>
  </condition>
  <apply><in/>
    <ci>x</ci>
    <apply><codomain/><ci>f</ci></apply>
  </apply>
</apply>
\end{verbatim}
The following remarks could be made.
\begin{enumerate}
\item This cries out for \verb"forallrestricted".
\begin{verbatim}
<OMBIND>
  <OMA>
    <OMS name="forallrestricted" cd="quantifier2"/>
    <OMA>
      <OMS name="image" cd="fns1"/>
      <OMV name="f"/>
    </OMA>
  </OMA>
  <OMBVAR> <OMV name="x"/> </OMBVAR>
  <OMA>
    <OMS name="in" cd="set1"/>
    <OMBVAR> <OMV name="x"/> </OMBVAR>
    <OMA>
      <OMS name="codomain" cd="fns1"/>
      <OMV name= "f"/>
    </OMA>
  </OMA>
</OMBIND>
\end{verbatim}
\item It is a pretty good case for the ``forall with implies'' trick.
\begin{verbatim}
<OMBIND>
  <OMS name="forall" cd="quantifier1"/>
  <OMBVAR> <OMV name="x"/> </OMBVAR>
  <OMA>
    <OMS name="implies" cd="logic1"/>
    <OMA>
      <OMS name="in" cd="set1"/>
      <OMBVAR> <OMV name="x"/> </OMBVAR>
      <OMA>
        <OMS name="image" cd="fns1"/>
        <OMV name= "f"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS name="in" cd="set1"/>
      <OMBVAR> <OMV name="x"/> </OMBVAR>
      <OMA>
        <OMS name="codomain" cd="fns1"/>
        <OMV name= "f"/>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
\end{verbatim}
\item Why use quantifiers at all?
\begin{verbatim}
<OMA>
  <OMS name="subset" cd="set1"/>
  <OMA>
    <OMS name="image" cd="fns1"/>
    <OMV name= "f"/>
  </OMA>
  <OMA>
    <OMS name="codomain" cd="fns1"/>
    <OMV name= "f"/>
  </OMA>
</OMBIND>
\end{verbatim}
\end{enumerate}
\begin{thebibliography}{9}
\bibitem{JHD}
Davenport,J.H.,
OpenMath and MathML:
Differentiating between analysis and algebra.
\url{http://staff.bath.ac.uk/masjhd/differentiate.html},
October 4, 2008.
\bibitem{MK}
Michael Kohlhase
OpenMath3 without conditions: A Proposal for a
MathML3/OM3 Calculus Content Dictionary.
\url{http://svn.openmath.org/OpenMath3/doc/blue/noconds/note.tex},
September 6, 2008.
\end{thebibliography}
\end{document}
\pause
\begin{itemize}
\end{itemize}
\begin{verbatim}
\end{verbatim}