[om] OMBVAR and related question

jhd at cs.bath.ac.uk jhd at cs.bath.ac.uk
Wed Apr 24 18:21:52 CEST 2002


Dear Fellow OpenMath-ers,
            Cartesian Products and tuples
It occurred to me while writing a few CDs while on holiday that, while we
(and MathML) have a construct for (n-ary) Cartesian_product, we don't have
a construct for making elements of this cartesian product (nor does it seem
that MathML has). Hence I propose to introduce one. I recall that we had
debates about a record type (which might, for reasons a different e-mail
explains) be worth resurrecting, but i feel that mathematically a tuple
type is still necessary, to state (3,2) rather than [x-coord=3,y-coord=2].
This would seem like a logical candidate to go into the set2 CD.
     While trying to write an FMP for it, I realised that what I wanted
was, in TeX notation
$$
\forall n\in\N, (x_1\in A_1)\land\cdots\land(x_n\in A_n)=implies
(a_1,\ldots,a_n)\in A_1\times\cdots\times A_n.
$$

It seems to me that I can only write this in OpenMath by stretching the
semantics of OMBIND somewhat, as attached. Other than the fact that
subscript has yet to be written (and any errors inthe OpenMath, which I am
sure David will point out), what do people this?
           James

<FMP>
<OMOBJ>
  <OMBIND>
    <OMS name="forall" cd="quant1"/>
    <OMBVAR>
      <OMV name="n"/>
    </OMBVAR>
    <OMA>
      <OMS name="implies" cd="logic1"/>
      <OMA>
        <OMS name="in" cd="set1"/>
        <OMV name="n"/>
        <OMS name="N" cd="setname1"/>
      </OMA>
      <OMBIND>
        <OMBVAR>
          <OMA>
            <OMS name="make_list" cd="list2"/>
            <OMI> 1 </OMI>
            <OMV name="n"/>
            <OMBIND>
              <OMBVAR>
                <OMV name="i"/>
              </OMBVAR>
              <OMA>
                <OMS name="subscript" cd="to=be=written"/>
                <OMV name="a"/>
                <OMV name="i"/>
              </OMA>
            </OMBIND>
          </OMA>
          <OMA>
            <OMS name="make_list" cd="list2"/>
            <OMI> 1 </OMI>
            <OMV name="n"/>
            <OMBIND>
              <OMBVAR>
                <OMV name="i"/>
              </OMBVAR>
              <OMA>
                <OMS name="subscript" cd="to=be=written"/>
                <OMV name="A"/>
                <OMV name="i"/>
              </OMA>
            </OMBIND>
          </OMA>
        </OMBVAR>
        <OMA>
          <OMS name="implies" cd="logic1"/>
          <OMA>
            <OMS name="and" cd="logic1"/>
            <OMA>
              <OMS name="make_list" cd="list2"/>
              <OMI> 1 </OMI>
              <OMV name="n"/>
              <OMBIND>
                <OMBVAR>
                  <OMV name="i"/>
                </OMBVAR>
                <OMA>
                  <OMS name="in" cd="set1"/>
                  <OMA>
                    <OMS name="subscript" cd="to=be=written"/>
                    <OMV name="a"/>
                    <OMV name="i"/>
                  </OMA>
                  <OMA>
                    <OMS name="subscript" cd="to=be=written"/>
                    <OMV name="A"/>
                    <OMV name="i"/>
                  </OMA>
                </OMA>
              </OMBIND>
            </OMA>
          </OMA>
          <OMA>
            <OMS name="in" cd="set1"/>
            <OMA>
              <OMS name="apply_to_list" cd="list2"/>
              <OMS name="tuple" cd="set2"/>
              <OMA>
                <OMS name="make_list" cd="list2"/>
                <OMI> 1 </OMI>
                <OMV name="n"/>
                <OMBIND>
                  <OMBVAR>
                    <OMV name="i"/>
                  </OMBVAR>
                  <OMA>
                    <OMS name="subscript" cd="to=be=written"/>
                    <OMV name="a"/>
                    <OMV name="i"/>
                  </OMA>
                </OMBIND>
              </OMA>
            </OMA>
            <OMA>
              <OMS name="apply_to_list" cd="list2"/>
              <OMS name="Cartesian_product" cd="set1"/>
              <OMA>
                <OMS name="make_list" cd="list2"/>
                <OMI> 1 </OMI>
                <OMV name="n"/>
                <OMBIND>
                  <OMBVAR>
                    <OMV name="i"/>
                  </OMBVAR>
                  <OMA>
                    <OMS name="subscript" cd="to=be=written"/>
                    <OMV name="A"/>
                    <OMV name="i"/>
                  </OMA>
                </OMBIND>
              </OMA>
            </OMA>
          </OMA>
        </OMA>
      </OMBIND>
    </OMA>
  </OMBIND>
</OMOBJ>
</FMP>





_____________________________________________________________________
This message has been checked for all known viruses by Star Internet
delivered through the MessageLabs Virus Scanning Service. For further
information visit http://www.star.net.uk/stats.asp or alternatively call
Star Internet for details on the Virus Scanning Service.


----- End forwarded message -----

_____________________________________________________________________
This message has been checked for all known viruses by Star Internet
delivered through the MessageLabs Virus Scanning Service. For further
information visit http://www.star.net.uk/stats.asp or alternatively call
Star Internet for details on the Virus Scanning Service.
--
om at openmath.org  -  general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems



More information about the Om mailing list