[om] Re: [om-a] Draft version of OpenMath 1.1 available

Andreas Strotmann strotman at cs.fsu.edu
Thu Oct 24 01:44:53 CEST 2002



On Wed, 23 Oct 2002, David Carlisle wrote:
> Michael: [redirected the discussion to om at openmath.org instead of om-announce]
> Yes a good idea. Here's a reply to Andreas that I just sent to om-announce..

I agree.  Sorry for missing that bit myself and posting to the wrong list.

>
> >
> > In particular, why not just make repeated variables ``erroneous'' in the
> > CLtL sense (undefined, but not an error) instead of this arbitrary rule?
>
> I think mainly as this effectively keeps all existing reasonable OM
> objects valid, and with the same interpretation as before. This seems a
> good objective for a "point" release. For an OM 2 (or if we'd got it
> right in OM 1) then maybe error would be a possibility but I didn't want
> to suggest invalidating such objects in OM 1.1.

Actually, that's why I suggest "erroneous" instead of "error".  That way,
applications are not required to catch it, and are allowed to interpret it
any way they like (from false infer anything at all...).  Applications
would be *allowed* to catch it as an error, though.

It's just another way of saying "deprecated".  And I think it is close
enough to the current status.

> > what's more, it contradicts the variable-renaming rule in the
> > preceding
>
> er that would be bad. I just read the text and don't see a conflict
> If you have an expression with repeated variables teh preceding alpha
> renaming rule would just give you an expression with a new repeated
> variable and then the new paragraph would still apply wouldn't it (it's
> maybe too late in teh evening to be thinking about this:-)

Well, it's a matter of , well, taste.  The rule appears to say that all
variables should be replaced - including the repeated ones. So you would
get an expression with *all* v's replaced by v*, say. Then, all v*'s by
v**, and so on ad infinitum.

Anyway, that's one possible interpretation.

Another possible interpretation of the generalized rule would be that you
could make *any* of the variables repeated in the binding be the one that
gets used in the body, not just the last one.  It just depends on which
one you rename first, and the generalized alpha conversion rule should not
specify an order.

Either way, the rule for repeated variables is not 100% compatible with
the (generalized version of) alpha conversion.  The reason why it used to
be was because of the currying rule, and that is gone.

Does this make sense?

 -- Andreas


--
om at openmath.org  -  general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems



More information about the Om mailing list