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

Christoph LANGE ch.lange at jacobs-university.de
Thu May 7 10:58:25 CEST 2009


On Thursday 07 May 2009 03:59:36 Professor James Davenport wrote:
> 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


-- 
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/e1096d94/attachment.pgp 


More information about the Om mailing list