[Om] Accessing arguments of an n-ary operator as indexed list items (in a definition)

[Christoph LANGE]

Dear OpenMath users,

  we are wondering how the semantics of an n-ary operator in some CD can be
defined (e.g. in an FMP).  Suppose there is an n-ary left-associative operator
nop, which is defined in terms of a binary operator op, i.e.

a nop b nop c := (a op b) op c

Given that the number n of arguments to nop is not known initially and that in
an OMBIND we cannot look into the term structure of bound variables (consider
"forall x . x = nop(arg1, ..., argn) => ..."), how can we access the arguments
of nop like an indexed list?  See below for an incomplete idea using the list*
CDs.

So much for the question that has a general impact.  Our actual use case is
that we are formalizing the translation of OWL ontologies from OMDoc (using
OpenMath formulas) to RDF.  We invented CDs that resemble the abstract syntax
of OWL, and we implemented a translation from that to RDF according to the
OWL specification.  However, we'd also like to formalize this translation as
axioms in our CD.  The problem introduced above occurs again more concretely
when translating certain n-ary OWL set constructors to RDF, where they are
broken down into linked lists, e.g.

<OMA>
  <OMS cd="owl" name="intersectionOf"/>
  x1
  ...
  xn
</OMA>

translates to the RDF triples

_:some-id owl:intersectionOf _:list1 .
_:list1   rdf:first          x1 .
_:list1   rdf:rest           _:list2 .
_:list2   rdf:first          x2 .
_:list2   rdf:rest           ...
...
_:listn   rdf:first          xn .
_:listn   rdf:rest           rdf:nil .

... for which we also have an OpenMath representation like

<OMA>
  <OMS cd="rdf" name="first"/>
  list1
  x1
</OMA>

(Don't pay too much attention to the _:node-names, they are arbitrary and will
be generated automatically, it's just their interlinking that matters for
representing the linked list.)

So how can we formalize something like the following in OpenMath:

1 let x = intersectionOf(x1, ..., xn)
2 forall i, 1 <= i <= n . rdf:first(list$i, x$i)
3     and forall i, 1 <= i < n . rdf:rest(list$i, list${i+1})
4     and rdf:rest(list$n, rdf:nil)
     
My question is about line 1; lines 2 to 4 are not a problem in OpenMath.  I
don't consider it negotiable that we want to have an easy-to-use input
representation like intersectionOf(x1, ..., xn).

There is the list1#list n-ary list constructor, and the list3#length and
list3#entry functions.  (My source of information is
https://svn.openmath.org/www/cdfiles2/cd/list3.ocd.)  They have not been
formalized via FMPs, but don't worry, we're first interested in writing down
our axiom _at all_ and would take a bit of hard-coded "magic" into account.
So what we'd need is a generalization of list1#list to n-ary operators (or
call them constructors for this purpose), and of the length and entry
functions.  Or would it make sense to implicitly treat an n-ary operator as
equivalent to a unary operator with a list argument -- e.g.

<OMA>
  <OMS cd="owl" name="intersectionOf"/>
  <OMA>
    <OMS cd="list1" name="list"/>
    x1
    ...
    xn
  </OMA>
</OMA>

What would you suggest?  Thanks in advance for any feedback!

Cheers,

Christoph

-- 
Christoph Lange, Jacobs Univ. Bremen, http://kwarc.info/clange, Skype duke4701

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part.
Url : http://openmath.org/pipermail/om/attachments/20090507/d2f4b3b7/attachment.pgp