W3C home > Mailing lists > Public > www-math@w3.org > May 2009

Re: on alpha conversion

From: David Carlisle <davidc@nag.co.uk>
Date: Tue, 26 May 2009 16:07:21 +0100
Message-Id: <200905261507.n4QF7Lgd006201@edinburgh.nag.co.uk>
To: www-math@w3.org

> If one carefully creates new MML3 markup using <bind> and <lambda/>,
> then it is possible in Strict markup to be formal enough so that
> alpha-conversion holds.  But as in MML2, that won't ordinarily be the
> case in MML3.

what Robert says is true, but also in the case where you do use strict
markup (or general markup that is defined in terms of strict markup
using bound variables) the fact that alpha coversion applies is simply a
mechanism for describing the meaning, it doesn't imply any conversion is
automatically applied.
Saying  lambda x . f(x) is the same as lambda y. f(y) and both mean f,
is the same as saying 1 + 1 = 2. The last example does not imply that 
a mathml processor should normalise
to <cn>2</cn> these are dfferent MathML expressions with different
properties, although of course some systems will evaluate them to the
same object on import.

The situation with alpha conversion is entirely similar.
lambda x . f(x) and lambda y. f(y)  both mean the same thing (f)
and you may choose to use "alpha conversion" terminology to say that
but it doesn't mean that they are the same mathml expression (in
particular they have different default renderings). The language in the
spec has hopefully been clarified, but I am not aware of any mathml 2
expressions whose meaning has changed by this clarification, if you have
found some please report them.


The Numerical Algorithms Group Ltd is a company registered in England
and Wales with company number 1249803. The registered office is:
Wilkinson House, Jordan Hill Road, Oxford OX2 8DR, United Kingdom.

This e-mail has been scanned for all viruses by Star. The service is
powered by MessageLabs. 
Received on Tuesday, 26 May 2009 15:22:23 UTC

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