RE: on alpha conversion

Hi.

I expect you did see that there is a warning about alpha conversion in
the text.  But in case you missed it, note that MML3 does add a warning
about alpha conversion.  In 4.3.2 Bindings with <apply>, the text now
goes to some effort to point out that backward-compatible MML2 uses of
<bvar> in <apply> may or may not be true variable binding.  It says 

"Because expressions using bound variables with qualifiers are idiomatic
in nature, and do not always involve true variable binding, one cannot
expect systematic renaming (alpha-conversion) of variables "bound" with
apply to preserve meaning in all cases. An example for this is the diff
element where the bvar term is technically not bound at all."

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.

--Robert


> -----Original Message-----
> From: www-math-request@w3.org [mailto:www-math-request@w3.org] On
> Behalf Of David Carlisle
> Sent: Tuesday, May 26, 2009 4:11 AM
> To: Andreas.Strotmann@ualberta.ca
> Cc: www-math@w3.org
> Subject: Re: on alpha conversion
> 
> 
> 
> 
> > 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.
> 
> Andreas, I'm not at all sure what you think has changed here in
MathML.
> the amount to which MathML changes (or more to the point) doesn't
> change
> variable names has not changed in any draft of MathML as far as I am
> aware.
> 
>
<lambda><bvar><ci>x</ci><bvar><apply><ci>f</ci><ci>x</ci></apply></lamb
> da>
> 
> Is fairly unambiguously (in all versions of MathML) the lambda
> expression
> L x. f(x) and as such it means the same thing as L y. f(y) or just f.
> But
>
<lambda><bvar><ci>y</ci><bvar><apply><ci>f</ci><ci>y</ci></apply></lamb
> da>
> and
> <ci>f</ci>
> 
> are not the same MathML expression, there is no automatic
> lambda-calculus equivalence applied to mathml terms. The only
specified
> equivalence, other than just literal string identity is the
> normalisation of white space.
> 
> David
> 
> 
> 
>
_______________________________________________________________________
> _
> 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 14:54:30 UTC