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

[Professor James Davenport]

On Wed, May 6, 2009 11:29 pm, Christoph LANGE wrote:
> 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
In detail, I am not sure I quite undertsnad the question, since the
semantics of the n-ary operator are defined (as far as STS is concerned: I
can see that there is a question as to whether STS is the right place to
dump this) by the fact that it is nassoc.
> 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.
This is indeed a general question, and one that I have run into eslewhere
(semantics of 'forallin', for example).
> 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).
I understand this, but isn't it sufficient to define intersectionOf(x1,x2).
Or is your problem that this won't work in OWL?

James Davenport
Visiting Full Professor, University of Waterloo
(but in Dubai for the next three hours)
Otherwise:
Hebron & Medlock Professor of Information Technology and
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009
IMU Committee on Electronic Information and Communication