[om] Proposed bug fix: deprecate Binding Object currying rule
Andreas Strotmann
strotman at cs.fsu.edu
Thu Sep 26 19:01:12 CEST 2002
Michael,
On Thu, 26 Sep 2002, Michael Kohlhase wrote:
> Could you please make clear what exactly you are poposing to delete?
> If you say "the two paragraphs", I frear that you are also throwing out
> parts of the alpha-conversion stuff, which we need to keep in the
> standard. Maybe you could just send around the proposed wording.
I did specify those paragraphs, by giving their beginning and ending. I
believe that I was careful not to touch the alpha conversion "stuff",
though it might look at first glance like I did. The discussion on the
meaning of binders with two occurrences of the same variable is clearly
part of the Currying rule, but the discussion of variable renaming
following it is not.
Anyway, here's a copy of the two paragraphs I propose to remove in
whichever way is deemed most appropriate:
Binding of several variables as in:
binding(B; v1; : : : ; vn;C)
is semantically equivalent to composition of binding of a single
variable,
namely
binding(B; v1; (binding(B; v2; (: : : ; binding(B; vn;C) : : :):
Note that it follows from this that repeated occurences of the same
variable in a binding
operator are allowed. For example the object
binding(lambda; v; v; application(times; v; v))
is semantically equivalent to:
binding(lambda; v; binding(lambda; v; application(times; v; v)))
so that the outermost binding is actually a constant function (v does
not
occur free in the
body application(times; v; v)))).
- Andreas
PS: I'm submitting this now because I can't come to Pisa myself to
present it to the meeting.
--
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