Quoting of OMOBJs as part of an OMOBJ

[jbs1]

migrated from Trac, where originally posted by lars_h on 16-May-2014 10:10am

In mathematical logic, from Gödel and forth, it is a very important trick that mathematical formulae can be encoded as actual mathematical objects, and thus operated on or made claims about. Most of the time, it doesn't matter how you encode things as long as the encoding is effective and faithful, so most authors tend to express their proofs using an abstract "the encoding of the formula ..." notation. It traditionally looks like

$$
  \ulcorner f(x) \urcorner
$$

for "the constant term encoding the formula $f(x)$".

The "OMOBJs as mathematical objects" extension is to add an equivalent of the $\ulcorner ... \urcorner$ quoting mechanism to OM -- an element that, when placed around a valid omel yields a new omel that semantically is as atomic as an OMV or OMI. The element name I find most natural for this is OMOBJ, so my proposed schema extension would be

omel |= element OMOBJ {omel}

For example the formula

$$
  6 < \ulcorner f(x) \urcorner
$$

(possibly "6 is less than the Gödel number of f(x)") would become

<OMOBJ>
  <OMA>
    <OMS cd="relation1" name="lt"/>
    <OMI>6</OMI>
    <OMOBJ>
      <OMA>
        <OMV name="f"/>
        <OMV name="x"/>
      </OMA>
    </OMOBJ>
  </OMA>
</OMOBJ>

in which neither f nor x occurs freely; an embedded OMOBJ is a constant.

An advantage of having this at the language level is that it can then interact sensibly with references. Concretely, one could have a formula

<OMOBJ>
  <OMA>
    <OMS cd="foo" name="evaluates_to"/>
    <OMOBJ>
      <OMA id="twoplustwo">
        <OMS cd="arith1" name="plus"/>
        <OMI>2</OMI>
        <OMI>2</OMI>
      </OMA>
    </OMOBJ>
    <OMR href="#twoplustwo"/>
  </OMA>
</OMOBJ>

that by referential transparency is equivalent to

<OMOBJ>
  <OMA>
    <OMS cd="foo" name="evaluates_to"/>
    <OMOBJ>
      <OMA id="twoplustwo">
        <OMS cd="arith1" name="plus"/>
        <OMI>2</OMI>
        <OMI>2</OMI>
      </OMA>
    </OMOBJ>
    <OMA>
      <OMS cd="arith1" name="plus"/>
      <OMI>2</OMI>
      <OMI>2</OMI>
    </OMA>
  </OMA>
</OMOBJ>

If quoted formulae are instead expressed using explicit constructor operations, then it would be syntactically different from the same formula not quoted, and thus references could not be used to share common parts.

That far the Standard Extension Proposal, now for a discussion of how that could be realised using kohlhase's sketched Language Extension Dictionaries. We want a translation back to something strictly OM2, which boils down to having a bunch of constructor operations. Basically, all one needs is a content dictionary with application symbols for every OM element. The interpretation of one of these should be that it constructs the encoding of an omel from any pieces involved. Concrete rules could be

<rule>
  <OMOBJ>
    <OMA>
      <exprlist name="seq"> <expr name="whatever"/> </exprlist>
    </OMA>
  </OMOBJ>
  <OMA>
    <OMS cd="openmath" name="application"/>
    <iterate name="seq">
      <OMOBJ> <render name="whatever"/> </OMOBJ>
    </iterate>
  </OMA>
</rule>

<rule>
  <OMOBJ>
    <OMV  ??? >
    <!-- Don't know how to match against an attribute value here. -->
  </OMOBJ>
  <OMA>
    <OMS cd="openmath" name="variable"/>
    <OMSTR><render name="name"/></OMSTR>
  </OMA>
</rule>

What I suspect is the trickiest issue here is making sure that the translations apply recursively as intended. It is in these kinds of fine details that the small homegrown language tends to lose against the big established standard; the latter has had many pairs of eyes looking at the corner cases and ironing out the messy parts.

But the conclusion is that this is a language extension that could be handled purely using this kind of translation mechanism.

[kohlhase]

moved to OpenMath/OMSTD#17