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

Date: Mon, 25 May 2009 13:03:52 +1200

Message-ID: <4A19EE78.6090905@auckland.ac.nz>

To: Andreas Strotmann <andreas.strotmann@ualberta.ca>

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

Date: Mon, 25 May 2009 13:03:52 +1200

Message-ID: <4A19EE78.6090905@auckland.ac.nz>

To: Andreas Strotmann <andreas.strotmann@ualberta.ca>

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

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 MillerReceived on Monday, 25 May 2009 01:04:53 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:27:41 UTC
*