Re: on alpha conversion

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 01:04:53 UTC