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

[Richard Fateman]

I have not been able to understand the object to the currying
rule, though the lack of currying in lisp has not been a
problem for me, so I'm not going to raise a fuss either way.

   Common Lisp does however have a very elaborate
mechanism for optional, default, keyword  arguments. The Common
Lisp Object System (CLOS) provides a mechanism whereby the
argument types, and perhaps numbers,
  determine the meaning of a function  (generic
functions), and this may provide currying.

  I suspect that the OM documents would benefit by running
them through a spelling checker.  Occurrence  is spelled wrong
in the paragraphs slated for deletion.  Where else?
RJF


Andreas Strotmann wrote:

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


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