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

Arjeh Cohen amc at win.tue.nl
Sat May 9 16:43:02 CEST 2009


In the good old day, I used sequence rather than list
for the same purpose. See http://www.win.tue.nl/~amc/oz/om/cds/sequence1.xml.

The reason for choosing this slight variation of list is that
I thought of a list as [x1,x2,....,xn]
and of a sequence as x1,x3,...,xn.
So, in accordance with
f(x1,x2,...,xn) we write f(a) where
a is the sequence x1,x2,...,xn rather than the correspondinglist.
There are operators to go back and forth from one to the other.

I tried to see what exists of this on the openmath website, but that
one seems down.


Best regards, Arjeh Cohen



On Sat, May 09, 2009 at 04:12:00PM +0200, Christoph LANGE wrote:
> On Saturday 09 May 2009 15:31:46 Professor James Davenport wrote:
> > What I meant is that you say "assuming the existence of such a function
> > x(i) ...". I've always assumed we meant list_selector from list2, but we
> > haven't made that as clear as we should.
> >
> > Incidentally, I've noticed a missing FMP there: will fix.
> 
> I see!  Well, I hadn't even been aware of the list2#list_selector symbol when
> writing my previous mails.  I had mentioned list3#entry, though, which seems
> redundant with the former.  (So shouldn't we actually deprecate one of them
> and declare it equivalent with the other one? -- Do you want me to file a
> ticket on that?)
> 
> In any case, I think using such a symbol does not apply in my case.  (But
> correct me if I'm wrong!)  When I mentioned that symbol in my previous mails,
> I was not referring to decomposing the _given_ list of n arguments of the
> given operator (which I'm now doing using David's approach), but to
> _generating_ the nodes of the linked-list data structure as which I'd like to
> represent the n arguments in RDF.  I think that their "linked list nature"
> needs not be explicated by using the list* OpenMath CDs, but it is made
> explicit by using the corresponding RDF vocabulary rdf#first and rdf#rest.  So
> actually I simply wanted to generate n existentially qualified variables out
> of nothing (one for each node of the linked list), which I'd then link into
> such a data structure using rdf#first and rdf#rest -- and there is no default
> way of generating n existentially qualified variables at once for a given n.
> 
> So I generated one existentially quantified function variable f (which is not
> further specified), and then asserted something about f(i) for i=1,...,n.  In
> my implementation, I took the freedom to implement f(i) by generating n random
> identifiers (cf. https://trac.omdoc.org/OMDoc/ticket/1506).
> 
> Technically, it would also be _possible_ to instead generate one existentially
> quantified variable L, saying that that is a list of length n, and then
> asserting something about list2#list_selector(L, i), for all i=1,...,n.  But I
> think it is not necessary, as the linked list data structure that I need has
> to be established by other means anyway.
> 
> Cheers,
> 
> Christoph
> 
> -- 
> Christoph Lange, Jacobs Univ. Bremen, http://kwarc.info/clange, Skype duke4701
> 



> _______________________________________________
> Om mailing list
> Om at openmath.org
> http://openmath.org/mailman/listinfo/om



More information about the Om mailing list