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
signature.asc
Description: This is a digitally signed message part.
_______________________________________________ Om mailing list [email protected] http://openmath.org/mailman/listinfo/om
