From: Andreas Strotmann <Andreas.Strotmann@ualberta.ca>

Date: Mon, 25 May 2009 11:17:08 -0600

To: Andrew Miller <ak.miller@auckland.ac.nz>

Cc: David Carlisle <davidc@nag.co.uk>, www-math@w3.org

Message-Id: <1243271828.6600.11.camel@ubuntu.ubuntu-domain>

Date: Mon, 25 May 2009 11:17:08 -0600

To: Andrew Miller <ak.miller@auckland.ac.nz>

Cc: David Carlisle <davidc@nag.co.uk>, www-math@w3.org

Message-Id: <1243271828.6600.11.camel@ubuntu.ubuntu-domain>

Thank you, Andrew, for a beautiful real-life example of context determining the meaning of variables in a MathML expression. All I ask is that MathML *continue* to leave variable names untouched so that context can reliably refer to them for its own needs - regardless how local (as in your example) or global (in mine) that context may be. It might be a good idea, come to think of it, for a <math> element to be able to declare such global context - for symbols, this is already the case, but is it also for variables? Such a declaration could then link explicitly (via "share") to those symbols and variables that it affects - hence my earlier cryptic earlier on using "share" to resolve the bound/free paradox in integration. On Mon, 2009-05-25 at 13:03 +1200, Andrew Miller wrote: > Andreas Strotmann wrote: > > On Fri, 2009-05-15 at 23:12 +0100, David Carlisle wrote: > >>> The only reason why this argument applies to MathML at all is that you made > >>> the grave mistake of importing alpha-conversion from OpenMath into > >>> MathML. > >> It seems to me that alpha conversion is just another name for binding To > >> say a variable is bound is to say that it only has local scope, and that > >> consequently its name can be changed consistently in that scope, ie > >> alpha conversion. > > > > That's what I thought you thought. It is, however, true only under very > > specific conditions: the extensional semantics (in the famous example, > > "the planet Venus") of an expression does not change under alpha > > conversion, as a theorem of an appropriate semantic mapping would state. > > > > The intensional semantics (in that famous example, "the morning star was > > already visible in the sky" does not make any sense, despite being > > extensionally true), however, does change when variable names are > > changed. Recall that across all of maths, variable names are carefully > > chosen to carry what one might call type information - x stands for > > *the* x-axis, changing it to y or even z would change the meaning > > drastically, even if the final result is the same. V is volume, A area, > > etc. > > > > Projects like WebALT, which use languages like OpenMath and MathML to > > represent meaning, and to provide universal access to that meaning in a > > host of human languages, need to be able to rely on that use being > > preserved, e.g. in order to translate "x" to the correct Arabic > > equivalent. alpha conversion violates this trust. > > > I'm not sure that capturing intensional semantics should be within the > scope of what MathML aims to do. > > I think that the solution is, where appropriate, to annotate / wrap > MathML in sufficient context to provide necessary information about the > link between the mathematics and the 'real world', and the intensional > semantics (and interpretation of the identifiers) associated with it. > > CellML (http://www.cellml.org) and SBML (http://www.sbml.org) are > examples of domain specific XML formats which use MathML to represent > relations between mathematical objects (currently, they exclusively use > MathML on real numbers, although I am working on extensions for CellML > to make this more generic). However, CellML and SBML have other elements > in the XML which refer to the variables in the MathML, and these > variables can in turn be annotated using RDF to link them to ontologies > which provide semantic information on the entities being described. > > Essentially, MathML with no context has no inherent semantic meaning, > and so any trust in the variable names having a particular meaning > without supporting context is misplaced. If supporting context is > present, and alpha-conversion is performed, the supporting context may > need to be adjusted; however, that is again beyond the scope of the > MathML specification. > > > > > There is no need to adopt a theorem of a semantics as an axiom, either, > > so that mentioning alpha-conversion in MathML is quite superfluous even > > when it does work. > > The same could be said of most constructs in MathML; this is essentially > a result of the fact that MathML has a high degree of generality, but > still provides constructs which are specific (but commonly used). > > Best regards, > Andrew Miller >Received on Monday, 25 May 2009 17:17:14 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Saturday, 20 February 2010 06:13:04 GMT
*