[m-dev.] Re: bug in scoping for higher order terms

[Fergus Henderson]

On 07-Mar-1999, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> 
> the intuitive rule (to me) is [...]: If there is a `:-' in a
> func closure, then variables appearing left of it are scoped to the
> closure; otherwise, variables appearing left of the `=' are scoped to
> the closure.
...
> > Perhaps we should just say that variables in a lambda expression
> > are *never* distinct from variables occurring outside; that would
> > mean that if you want a fresh variable, then you must use a
> > different variable name.
> 
> That's a pretty unnatural rule for both preds *and* funcs.  It'll
> probably bite people less often than the current rule (because people
> will naturally tend to use different variable names for head variables
> in closures), so perhaps it's an improvement.  Still, despite the
> greater complication, the second scoping rule for funcs I suggested
> just above seems more intuitive and less error prone.  If that rule
> seems too complicated to you, I suppose an alternative intuition is
> that, in a function, `:-' is pronounced `where', and so "the thing
> being defined" is always what's left of the `=', and everything right
> of the `=' is scoped to the enclosing clause.

The first rule (above) does seem too complicated to me, so
this second rule is the one that I propose to adopt.

Thus the rule is: in lambda expressions, any variables occuring
in the predicate or function arguments are lambda-quantified;
variables in the function result term (if any) or in the goal
use the normal rules for implicit quantification.

This means that for function lambda expressions, variables which
occur in the function result term are not lambda-quantified, unless
they also occur in the arguments.

I believe this is consistent with Lee's suggestions on this topic.

So, if anyone has any serious objections to this, please speak up (quickly).
Otherwise I will go ahead and implement this change.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.