- From: Andreas Strotmann <strotman@cs.fsu.edu>
- Date: Tue, 19 Dec 2000 12:28:09 -0500 (EST)
- To: David Carlisle <davidc@nag.co.uk>
- cc: www-math@w3.org
David, thanks for your reply. I think there was a bit of bad and hurried phrasing in my previous message, so let me try to explain a bit more here about what I meant. > > - 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