- From: Michael Kohlhase <m.kohlhase@jacobs-university.de>
- Date: Thu, 07 Jun 2007 06:14:08 +0200
- To: David Carlisle <davidc@nag.co.uk>
- Cc: r.muetzelfeldt@ed.ac.uk, www-math@w3.org
Dear all, I really like David's representation it seems the cleanest so far, because it highlights the 'bound variables' character of a and b (for instance they can be renamed without changing the meaning of the expression). To make things more explicit, it may be best to combine the two ideas and use a <csymbol > variant of lambda to make it clear that the beta-reduction David is talking about should maybe executed at different occasions than that for regular lambdas. Michael David Carlisle wrote: > I agree with Robert that csymbol is probably better than ci but that > otherwise that's a good encoding. > > An alternative viewpoint that I picked up in a previous life working in > formal systems that essentially viewed everything as a lambda expression > is that > 2*a+3*a^2+b+b^2 WHERE a=5+c*2, b=17-d > is syntactic sugar for > (lamda a b. 2*a+3*a^2+b+b^2)(5+c*2, 17-d) > > that is first create the anonymous function of two variables > representing the bound variables in your expression, then apply that > function to the two expressions which hold the definitions of the bound > variables. > > This could be encoded directly in mathml as > > <apply> > <lambda> > <bvar><ci>a</ci></bvar> > <bvar><ci>b</ci></bvar> > <apply> > <plus/> > <!-- mathml for 2*a+3*a^2+b+b^2 --> > </apply> > </lambda> > <apply> > <plus/> > <!-- mathml for 5+c*2--> > </apply> > <apply> > <plus/> > <!-- mathml for 17-d--> > </apply> > </apply> > > > This has the advantage of being coded in core mathml without needing any > csymbol defined operators, it has the possible disadvantages of being > possibly harder to read by humans, and possibly more likely to be > automatically "expanded out" by a system consuming the expression, just > as > <apply><plus/><mn>1</mn><mn>1</mn></apply> > might not be the best encoding of the concept 1+1 if you want it to > survive importing it into a CA system and not have it be seen as 2. > > David > > > > > ________________________________________________________________________ > The Numerical Algorithms Group Ltd is a company registered in England > and Wales with company number 1249803. The registered office is: > Wilkinson House, Jordan Hill Road, Oxford OX2 8DR, United Kingdom. > > This e-mail has been scanned for all viruses by Star. The service is > powered by MessageLabs. > ________________________________________________________________________ > > -- ---------------------------------------------------------------------- Prof. Dr. Michael Kohlhase, Office: Research 1, Room 62 Professor of Computer Science Campus Ring 12, School of Engineering & Science D-28759 Bremen, Germany Jacobs University Bremen* tel/fax: +49 421 200-3140/-493140 m.kohlhase@jacobs-university.de http://kwarc.info/kohlhase skype: m.kohlhase * International University Bremen until Feb. 2007 ----------------------------------------------------------------------
Received on Thursday, 7 June 2007 04:14:22 UTC