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 > [email protected] > http://openmath.org/mailman/listinfo/om _______________________________________________ Om mailing list [email protected] http://openmath.org/mailman/listinfo/om
