Joe, I also think that you might need a new CD - unless you find something in the new ones from the interGeo efforts: http://i2geo.net/xwiki/bin/view/Main/About
(if it is geometry you are interested in) I do not think the Pair-Tuple symbols from ecc is what you want to use for a coordinate system. --olga On Fri, Feb 19, 2010 at 6:04 AM, Michael Kohlhase <[email protected]> wrote: > Dear Joe, > > On 18.02.10 18:56, Joe Collins wrote: >> Dear Michael, >> >> Most of what you write is roughly consistent with what I have understood, and >> helps a little more with the OpenMath flavor. >> I was a little thrown by "Semantics of OpenMath and MathML3", Kohlhase& >> Rabe, >> where: >> >> Definition 3 (OM Context). An OM context C is an n-tuple of variables >> which we will write as<x1 , . . . , xn>. We will use + for tuple >> concatenation and $\in$ for tuple membership. >> >> implies tuple concatenation is normal. >> > Ha, nice answer, >> (Sorry, I didn't mean to knock you for inconsistency). >> > this definition was actually written by my (formalist) co-author, who > was aware of the same isomorphism you were enquiring about. Indeed we > were talking about argument sequences there where lists and tuples are > equally far from the "real intuition", therefore I went along with this. > > BTW, I consider the representation of argument sequences as one of the > remaining problems of OpenMath, as we do not have a real means to > represent equations like f(a,x_1,...,x_n) = g(x_1,...x_n)-a. Mathematica > has a good way of doing this which OM lacks. >> Let me, however, get straight to my real concern. >> I want to represent a coordinate variable tuple like (X, Y, Z) or >> (r, theta, phi). I do NOT consider these "vectors" in general. >> I was considering using tuple to construct them, but then needed a >> means of indexing them. Either adding a "tuple_selector" symbol or using the >> existing list symbols seemed to be the two best options, with my preference >> towards the "tuple_selector" symbol. >> After this feedback on the OpenMath flavor of things, my preference has >> increased in that direction. >> >> If you ask "Why not 'vectors'?", I'll ask >> "What does it mean to add >> (r1, theata1, phi1) + (r2, theata2, phi2) ?". >> >> (Things aren't sufficiently interesting if you stay in Cartesian >> coordinates!) >> > I think that in this case you really are nearer to "vectors". But you > can always make your own tuples CD that does what you want. I am pretty > sure that you do not want to use ECC, since with the tuple constructor > you would "buy" all the rest of a (very complex) lambda calculus that > most people would probably consider a Meta-Logic. > > I encourage you to make a CD and contribute it to OM. > > Michael >> >> Regards, >> Joe >> >> Michael Kohlhase wrote: >> >>> Dear Joe, >>> >>> there are at least two possible answers to this question: >>> >>> Mathematical: >>> >>> generally spoken, tuples and lists are isomorphic as data raw >>> structures, but support conceptually different operations. Tuples are >>> usually thought of as having fixed length and operations are between >>> tuples of same length. Operations are mostly from linear algebra. In the >>> ecc CD we have dependent tuples that are mostly used for defining >>> functions. >>> >>> Lists are thought of as of variable length, and the operations are >>> mostly constructing lists from the empty list by prepending, appending >>> lists, mapping functions over lists,.... Moreover, lists typically only >>> have members of the same "type". >>> >>> So, even though everything you do with tuples, the mathematical, >>> operational intuitions are quite different. >>> >>> Formally: >>> >>> The levels of formality in the descirption of ecc and list1/2 are vastly >>> different. ECC (Extended Calculus of Construction) is a logical system, >>> where tupling has a very well-defined role. list1/2 is a (intendedly) >>> vague description of a vocabulary of lists without going into too much >>> detail, so that it can be universally used. >>> >>> hope this helps, >>> >>> Michael >>> >>> On 17.02.10 14:51, Joe Collins wrote: >>> >>>> The OpenMath ecc CD defines Tuple and the list1 CD defines list. >>>> >>>> Is there any essential distinction between Tuple and list? >>>> If so, what? >>>> >>>> Some of the definitions in list1, list2 suggest (to me) that the order >>>> of the >>>> list elements are arbitrary. Is this actually the case? >>>> >>>> Joe >>>> >>>> >>> >> > > -- > ---------------------------------------------------------------------- > Prof. Dr. Michael Kohlhase, Office: Research 1, Room 62 > Professor of Computer Science Campus Ring 1, > Jacobs University Bremen D-28759 Bremen, Germany > tel/fax: +49 421 200-3140/-493140 skype: m.kohlhase > [email protected] http://kwarc.info/kohlhase > ---------------------------------------------------------------------- > > _______________________________________________ > Om mailing list > [email protected] > http://openmath.org/mailman/listinfo/om > > _______________________________________________ Om mailing list [email protected] http://openmath.org/mailman/listinfo/om
