# Re: a content question/suggestion

From: Andreas Strotmann <strotman@cs.fsu.edu>
Date: Tue, 19 Dec 2000 12:28:09 -0500 (EST)
To: David Carlisle <davidc@nag.co.uk>

Message-ID: <Pine.GSO.4.10.10012191145420.7778-100000@xi.cs.fsu.edu>
David,

phrasing in my previous message, so let me try to explain a bit more here

> >  - bvar introduces a bound variable
> this is certainly the intent. Where "bound variable" has to be
> interpreted with some care

My intent here was to set the stage for the following points.  I realize
that that is its intent.
>
>  x is expressed using a bvar in \int x dx even though x is free
> there. This could be rationalised by saying that \int x dx is syntactic
> shorthand for
> ( \int  (\lambda x. x) dx) (x)
> (which is how it would be encoded in OpenMath) and the inner use of x is
> bound.

I know - didn't I write one or two articles on this?   ;-)

Still, my analysis in those articles was that the *variable* x is actually
a *bound* variable in this context - it's only its *name* (the string "x")
that is global (roughl the same as free) in this context, denoting the
x-axis space, and linking outer and inner occurrences of "x" as denoting a
common function space.

I'm not sure if explaining this nicety in the spec would help implementors
do this correctly, but I'm tempted to suggest that some explanation like
this be added to the spec just to make sure that everybody gets it right
in the same way :-)

This is of course a common phenomenon, and in all cases (I wager)
analysable in this way, making all <bvar>s *bound*.  My point here is that
it should be analysed (and more importantly, used) only in ways consistent
with this usage, even if new symbols (such as <csymbol>s) are used as
operators (heads).  To ensure that, these things need to be specifically
exempted from the rule that the meaning of qualifiers depends on context.

> >  - that variable's scope is the surrounding apply
> This is also the intent.
I know.. just repeating here to set the context again for this:

>  - except for <interval> qualifiers as immediate children of the
>    surrounding apply

I think I didn't explain well enough what I meant here - bad, hurried
phrasing (sorry).  I meant that the entire immediately surrounding apply
is the scope of the bound variable *except* those <interval> qualifiers
that are direct children of that surrounding apply.  (I believe I
explained a couple of times before here and in the OpenMath community that
those are outside the bvar's scope).

The main point that I wanted to make here is that this latter scoping
issue needs to be explained, and again made independent of the concrete
operators that set the context, so that this scoping issue is resolvable
even for <csymbol> operators (say, using a specific Lebesgue integral
semantics via <csymbol> instead of the generic "integral" of MathML).

<interval> was also meant to serve as an example for the other qualifiers
that are used in specific meanings inthe integral and other generalized
quantifier contexts.  In all cases, it needs to be specified *generally*
(that is, for that qualifier independent of the head symbol) how it
behaves wrt scoping of the sibling bvars.  Otherwise, correct
interpretation is left to the implementors, and I'm not sure they would
all make the same choice ;-)  And the way I see it, MathML usage is
sufficiently consistent to allow such general scoping rules at least, and
indeed more general usage guidelines.

In short, variable scoping is quite special, and should be treated that
way if we really want machine-understandable Content-MathML.

> 4.2.3.2 (Operators taking qualifiers)
> says:
> > Qualifiers always follow the operator and precede the argument if it is
> > present. If more than one qualifier is present, they appear in the order
> > bvar, lowlimit, uplimit, interval, condition, domainofapplication,
> > degree, momentabout, logbase. A typical example is:
>
> which does constrain qualifiers to being immediate children of the apply
> doesn't it?

Sure -- I meant that <interval> qualifiers in embedded expressions don't
count (a triviality of course, but still... in formal contexts youneed to
be formal).
>
> The description of bvar in 4.4.5.6 does say
>
> > Discussion
> > The bvar element is the container element for the bound variable' of an
> > operation
>
> so I think it is clear that use of bvar with other newly introduced
> constructs should not change that. It does go on to say
>
> > The meaning of the bvar element depends on the context it is being used
> > in. For further details about how qualifiers are used in conjunction
> > with operators taking qualifiers, consult Section 4.2.3.2 [Operators
> > taking Qualifiers].
>
> I'm not sure if that can really be made any more constrained given
> existing differences in the use of bvar between the various elements.

I suppose you're right, except for the discussion we had above of how some
bound variables are at the same time "free".
>
>
> Do you have any explicit example in mind that you think would be a) bad
> and b) allowed by the current spec. (It's getting too close to Christmas
> to consider problems in the abstract, need concrete examples:-)

I'll think about it -- but I think I already pointed out that the scoping
issues for neighboring qualifiers of a bvar need to be specified globally
and independently of those other operators.

Example:  What is the scoping of the degree variable "n" in (d^n f / dx)
wrt to the variable x?  It's outside the bvar's scope if you think about
it for just a moment!
>

Were you planning to add a note about the meaning of these qualifiers when
used with an "nassoc" operator (in James' Simple Type System parlance)?
There was a discussion on that on this list, and this could also serve as
an interesting example.

Hope this helps!

Andreas
`
Received on Tuesday, 19 December 2000 12:28:14 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:27:31 UTC