Re: on alpha conversion

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 UTC