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

[Christoph LANGE]

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

-------------- 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/20090509/935b7537/attachment.pgp