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

Andreas Strotmann strotman at cs.fsu.edu
Wed Sep 25 21:56:35 CEST 2002


Hello all,

I have been pointing out for a while now some problems with the Currying
rule that the OM Standard document defines for OM Binding Objects.
However, I had always said that there may be more than one way out.

I believe now that there is actually only one solution to the problem I
will describe below, and that is to deprecate entirely the two paragraphs
in the OM Standard describing the Currying rule for OM Binding Objects.

(In terms of wording, this means re-typesetting those paragraphs in a
different style, and introducing them with something like "The following
is deprecated as of OpenMath version 1.1" or so. The two paragraphs start
at the bottom of page 11 ("Binding of several variables...") and end on
page 12 ("... v does not occur free in the body
application(times,v,v))))").)

Rationale:

1. As I noted at Nice, the Currying rules of Lambda Calculus come in
   pairs, namely for abstraction *and* for application.  Having
   one but not the other can lead to odd behaviour, to say the least.

2. The Currying rule in the standard is actually much more general
   than that of Lambda Calculus.  A type analysis quickly shows that
   it only works for what one might term "nassoc" binders:

    OMBind(Binder,x,y,expr) == OMBind(Binder,x,OMBind(Binder,y,expr))

   implies that the type of the result of the OMBind must be the same
   as the type of the embedded expression expr ("same" taken with a
   grain of salt, but close enough for our argument).

   This is true for binders such as quantifiers, for summation type
   operators, in short, for binders that generalize associative binary
   functions (forall/and, exists/or, sum/+,...).

   It is NOT true for potential binders that do not follow this pattern.
   A "set_of_all" binder would violate it, a "list_of_all" one would;
   even "lambda" would violate it except for the axiom saying it doesn't
   (provided both application and abstraction are Curryed). In general,
   binders that generalize "nary" rather than "nassoc" functions do not
   obey the currying rule.

In a nutshell, the Currying rule is the exception rather than the rule for
binders in that it "really" only applies to "nassoc" ones.  I therefore
move to enact the above-mentioned change to the OpenMath Standard as a
bug-fix.

Side effects:

- I don't think that anyone actually implemented the Binding rule in a
system except to the extent that it is applied in cases where the binders
themselves are known to obey it.  Deprecating the feature should therefore
not break any existing software.

- Expressions of the form

  forall p in P, k in Z_p. Q(p,k)

now become erroneous since no scoping rule within a Binding Object is
defined any more.  Personally, I believe that that is a good thing -- I
just taught my students today out of a standard text book that it should
in general be the case that

  forall x,y. P == forall x. forall y. P == forall y. forall x. P

Reasonably competent dependency analysis can serve to circumvent this
problem where it arises.

- The quantifier symbols can be classified as "nassoc binders" in their CD
entries to recapture their Currying property.  For lambda, care must be
taken when mentioning a Currying rule as a FMP in order not to state
something that OpenMath doesn't support (since application is not Curryed
in OpenMath -- see rationale 1. above).

Best regards,

  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