on alpha conversion

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. 

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.

In summary, alpha conversion is dangerous for projects like WebALT, and
not particularly useful when an appropriate semantic interpretation
would say so much more about it. If you have to talk about it, do so in
an appendix, and mention potential problems like the above.

Received on Monday, 25 May 2009 00:19:23 UTC