[om] Proposed bug fix: deprecate Binding Object currying rule

Andreas Strotmann strotman at cs.fsu.edu
Thu Sep 26 19:01:12 CEST 2002


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
  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
  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