It is proposed that the restriction in the OpenMath standard that an OMBIND element must have exactly three children should be lifted, to support more general binder symbols. The case of logics with generalised quanti ers is described in some detail, since these turn out to not have a natural encoding within OpenMath 2.0, because of precisely this restriction. That restricting quanti ers to a single body should have such consequences is not trivial, but follows from a theorem in the Logic branch of Philosophy.
in place switch to the more colloquial `de nite integral Rab f (x) dx of an expression'; the former is an application, the latter is a binder, but the mathematical content is the same.
There is however one factor in the OpenMath standard that prevents viewing an OMBIND
simply as an OMA beefed-up with the additional power to bind variables, namely that an OMA
can have any number of children, whereas an OMBIND must have exactly three: the head, an
OMBVAR containing the variables to be bound, and one body object; a structural analogy with
OMA would rather require that there could be zero or more body objects. Not having that
freedom becomes a noticeable restriction quite soon beyond the most elementary integral and
sum concepts, since it is quite common in calculations that these carry conditions (involving
the bound variables) which are as important as the integrand itself for how one should proceed.
These conditions are not natively part of the integrand (even if it can be useful to introduce
devices that let one so incorporate them [
Not surprisingly, this problem has been noticed and discussed before [
This view represents a feasible way of formalising concepts such as sums with conditions, but whether it also provides a faithful representation of these symbols with respect to the practices for how they are manipulated is quite a di erent matter. In for example i=0 k=i Xn Xn k xiyk = i
X i;k2Z 06i6k6n k xiyk = Xn Xk k xiyk = i i k=0 i=0 n X(x + 1)kyk k=0 (1) the key idea is that the left double sum mechanically translates to a combined sum with condition 0 6 i 6 n ^ i 6 k 6 n whereas mechanical translation of the right double sum yields the condition 0 6 k 6 n ^ 0 6 i 6 k|both of which are neatly summarised as 0 6 i 6 k 6 n. With the view that the condition sum is technically
X (i;k)2f(i;k)2Z2j06i6k6ng k i
i k x y or even arith1#sum set1#suchthat Z2; i; k: (0 6 i 6 k 6 n) ; i; k: ki xiyk (2) the step grows longer, mostly because it becomes necessary to reverse the introduced ordering of the bound variables. It likewise becomes much less straightforward to argue that a summand may be rewritten subject to some piece of information expressed in a condition when that condition is two steps further away from the sum.
Still, it will likely remain dependent on point of view whether the conditioned sum in (1) is technically an expression of the form (2) or rather just something equivalent to it. Because K{14 mathematics undeniably provides for these kinds of binding-reduced presentations, it is hard to argue within that context that a more general OMBIND is necessary. Therefore, if one wishes to drive home such a point of necessity, one should rather look beyond the K{14 horizon, and in particular at contexts that do not have set theory and lambda calculus built in. Such contexts exist, and one may even add the prerequisite that they have practical applications, but they are probably not what one would call \part of mainstream mathematics", since the relevant literature tends to rather be classi ed as computer science or philosophy. (But then again, so is much of lambda calculus and set theory.)
Next, Section 2 gives an introduction to a body of theories where generalised binders are common and important. Section 3 then details the enhancements of the OpenMath standard here proposed, and nally Section 4 discusses some objections that have been raised in the past.
Quanti ers are concepts of which di erent mathematicians seem to have unusually varied
understandings. A very striking example of this is provided by the Encyclopaedia of Mathematics
Hellstrom
entry [
Part of the di erence in views may be due to that the contexts in which one tends to
encounter quanti ers other than the basic 8 and 9 (and \shorthand" variants of these, such
as the unique existence quanti er 9!) are not that of mathematics in general, but rather some
specialised subsets of mathematics. The best-known example of such a subset is probably the
use of Monadic Second-Order (MSO) logic within formal language theory, where several classes
of languages have been characterised using MSO logic (see for example [
In second-order logic, one may quantify over predicates (\relation symbols") as well as variables, but the `monadic' imposes the restriction that the predicates being quanti ed may only have one argument. Since a relation with one argument is essentially a set (P (a) () a 2 P ), this means MSO logic gives one the power to quantify over sets of atoms (but not over for example sets of pairs of atoms) without introducing any primitives of set theory as such, since that would let the logic express far too much for these purposes. The point is not to build a formal theory and start deriving theorems stated in MSO logic, but to use that logic to describe classes of models. For suitably weak logics, truth may well be an algorithmically decidable property.
Quite a lot can be done in MSO logic with just the (possibly second order) universal and existential quanti ers, but the fact that these bind \set variables" suggests a range of additional conditions that can be imposed. One might quantify with respect to the nite sets, the sets of even cardinality, or the sets of prime cardinality. Having the same quanti er bind several variables, one can quantify with respect to pairs of sets of equal cardinality. None of these things are beyond what OpenMath 2 supports, but they are mentioned here to give a hint of how useful expressive power can be built into the quanti ers of a language, rather than provided via predicates or functions.
What OpenMath 2 does not support is Lindstrom quanti ers,1 since these bind variables in several subformulae simultaneously; if Q is a Lindstrom quanti er and '1(x); : : : ; 'k(x) are well-formed formulae, then
Q x '1(x); : : : ; 'k(x) (3) is a well-formed formula in which there are no free occurrences of x. The natural encoding of this formula in OpenMath (XML) would be <OMBIND> hencoding of Q i <OMBVAR>
<OMV name="x"/>
1There seems to be some disagreement about terminology here. In [
.
hencoding of 'k(x)i </OMBIND> but this is currently not allowed, since the number of children of the <OMBIND> is 2 + k rather than exactly 3.
The matter of how an interpretation is assigned to such a quanti er Q is admittedly
somewhat involved; for a fully rigorous de nition see [8, Ch. 5], [6, Ch. 12], or [
v(y) otherwise, R'A(;xx);v = n a 2 A
A; v[x=a] j= '(x) o , i.e., the set of values for x that render this formula satis ed. The rule for Q is then that (A; v) j= Q x '1(x); : : : ; 'k(x) i 3
A; R'A1;x(x;v); : : : ; R'Ak;x(x;v) , that is, is essentially a table of those combinations of domain elements and corresponding truth values for argument formulae that satisfy this quanti er. (The reason the domain A is included in the tuples of is that when the quanti er is de ned in this generality, the \relational system" is required to be closed under isomorphism; if (A; R1; : : : ; Rk) 2 and f : A ! B is a bijection, then B; f (R1); : : : ; f (Rk) 2 as well.)
As an example of this, consider the Hartig quanti er QH for which the rule is (A; v) j= QH x '1(x); '2(x) i
R'A1;x(x;v) = R'A2;x(x;v) , i.e., QH x '1(x); '2(x) if and only if there are as many x satisfying '1(x) as there are x satisfying '2(x) (which is quite di erent from '1(x) and '2(x) being satis ed by the same x). As a relational system,
H = (A; P; Q)
P
A; Q
A; jP j = jQj .
Another such quanti er is Qmost , where most = (A; P; Q)
P
A; Q
A; jP \ Qj > jP n Qj , i.e., Qmost x '1(x); '2(x) could be read as `most x such that '1(x) satisfy '2(x)' or in less formulaic language `most '1 are '2' (compare `most continuous functions are nowhere di erentiable'). By [11, Th. 19.4], this Qmost quanti er is not de nable in terms of any set of quanti ers of type h1i (i.e., acting upon only one subformula)! Hence it is not expressible using present OpenMath with less than that one introduces the primitives of set theory, which however throws all hope of something like algorithmic decidability out the window. 3
As hinted at above, the Proposal is that the restriction on a binding OpenMath object that it must have exactly one body subobject should be lifted. In the normative Relax NG schema for the OpenMath XML encoding, that corresponds to the change It is not clear that there are any use-cases for the `no bodies' edge case, but it should not hurt to allow it, and it could conceivably turn up as a base case for some sort of \n-ary binder".
Note that the proposed change, both for the XML encoding and for the binary encoding, is strictly a matter of relaxing the syntax; it does not require any new delimiters or separators for disambiguating. In the XML encoding, this is because the list of variables being bound is already bundled into one OMBVAR element. In the binary encoding, token identi ers 28 and 29 similarly delimit the sequence of variables being bound.
What would require new delimiters is however the informal function-style syntax used to de ne OpenMath objects in Chapter 2 of the standard, since this presently employs a at list of head, variables, and body as in Subsection 2.1.3 Clause (iv):
binding(B; v1; : : : ; vn; C) It is thus further proposed that the punctuation before and after the list of variables in a binding is changed to a semicolon, like so:
binding(B; v1; : : : ; vn; C) and binding(B; v1; : : : ; vn; C1; : : : ; Cm) This places the semicolons in the same positions as the tokens 28 and 29 in the binary encoding. The second semicolon is of course necessary to mark the boundary between the two variablelength sections. The rst semicolon has the merit of highlighting the boundary between the head|where occurrences of the variables v1; : : : ; vn are not bound by this binding|and the rest of the binding object|where these variables are bound by it (in the sense of participating in -conversion). Since the latter is a somewhat subtle point, highlighting this boundary should enhance readability. Introducing semicolons as a new punctuation mark is furthermore not a very dramatic step, since these formulae already employ spaces as the secondary punctuation mark separating attribution symbols from their attribute value; commas never were the only punctuation marks around. 4
Since there has been a previous enhancement proposal [
What the latter part of this argument overlooks is that the brackets in (3) are a purely notational device|much like the parenthesis in `f (x; y; z)'. Content-wise, the problem with the above argument is that it introduces into the formula an OpenMath object which is a purely syntactic device; a theory encompassing the generalised binder B will have interpretations for all of C1, C2, . . . , Cm, and (4) as a whole, but there will not in general be anything that semantically corresponds to the application(D; C1; : : : ; Cm) (even if there can be in speci c cases). Hence this approach would prevent formulae from having a native expression in OpenMath, rather requiring them to be encoded into OpenMath (just like OpenMath in turn tends to be encoded into XML).
The dummy helper argument|that a multiplicity of objects can instead be encoded as a single application object|also begs the question of why error should be allowed to take an arbitrary number of non-heads, when binding is not. If minimality is the argument against generalised binders, then it should apply equally much against the present errors. 4.2
Another line of reasoning holds that fns1#lambda is the only binder anyone really needs| that every other binder can be rewritten to a combination of lambda and an application|and moreover that doing so is The Future. Therefore any changes made in this area should rather be in the direction of deprecating all binders that are not fns1#lambda.
It is di cult to view this argument as being anything but primarily ideological: a statement of what one would like people to do, possibly for aesthetic reasons, rather than a conclusion founded in utility. It is quite true that binders are awkward to formalise (and I for one have much a nity for variable-free formalisms), but what is awkward about binders is the binding of variables as such rather than the concepts that the binder seeks to encode. Therefore the `one lambda ts all' approach succeeds rather in combining the worst of both worlds: none of the conceptual unity that a specialised binder can bring, but all of the formal complications that are inherent in binding variables! Perhaps it is rationalised by viewing phrasebooks mostly as thin wrappers over an implementation language having lambda (but no other binders) as a primitive, since in that case having no other binders around makes life easier for the phrasebook implementor, but that would be a narrow-minded view. It cannot be the role of a general standard such as OpenMath to say that some styles of doing math (e.g. the functional style) are good and others (e.g. using binders) are bad, even if individual phrasebooks of course may choose to support the symbols of one style but not those the other.
More down to earth, the `one lambda ts all' approach to binding has several problems. One
is that using a separate single-body lambda for each Ci of a generalised binding like (4) weakens
the connection between occurrences of the same variable in di erent bodies, as remarked in [
A third line of reasoning could be that the proposed enhancement in principle is correct, but cannot be implemented because it is not in MathML 3. In other words, this amounts to saying \this can't be xed, because the Other Standard is broken in this regard too."
However, since (Strict Content) MathML 3 only claims to be in alignment with OpenMath 2.0, there is no particular reason why OpenMath could not advance. To preserve interoperability, one could adapt a variation on the work-around from Subsection 4.1 to the conversion of generalised OpenMath bindings to Content MathML 3; this is well on par with other code transformations that such a conversion must perform, at least if viewed at the XML level.
A
While writing about the suggested modi cations to the informal syntax for OpenMath binding objects, it occurs to me that this also opens up for unambiguously giving several subobjects before the list of variables. Could that be useful? Very much so, since it is hard to imagine a more straightforward encoding than
binding R ; a; b; x; f (x) of the binding de nite integral Rab f (x) dx than that! (With the physicist notation Rab dx f (x) the match is even closer.) The trick here is that since variables do not get bound before the rst semicolon (i.e., before the OMBVAR child), that will be the correct place to include subobjects that should not be subjected to such binding, for example integral bounds. In the Relax NG schema, the corresponding change would be @@ -144,9 +144,13 @@ <!-- binding constructor --> <define name="OMBIND"> <element name="OMBIND">
<ref name="compound.attributes"/> - <ref name="omel"/> + <oneOrMore> + + + + +
<ref name="omel"/> </oneOrMore> <ref name="OMBVAR"/> <ref name="omel"/> <zeroOrMore>
<ref name="omel"/> </zeroOrMore> </element> </define> which is again an unambiguous relaxation.
The reason I do not up-front propose this slightly more general enhancement is that I have thought about it too late to be comfortable that I have given all consequences a reasonable consideration. It does for example seem plausible that it would be more disruptive to existing phrasebooks than the proposed enhancement, since it should often have seemed natural to hardwire the knowledge that the OMBVAR is the second child of an OMBIND. The workaround by means of a helper application is also slightly less wasteful than for the bodies, since one can write
binding application(R ; a; b); x; f (x) and still get by with only one symbol (even if that is a weird application symbol in returning a binder, and moreover vulnerable to several of the arguments in Section 4).
This possibility is probably best discussed at the workshop.
B
Generalising the binders might also require a generalisation of their declarations in the Small
Type System [