Re: quantifiers

Andreas,

> The draft of MathML3 specifies that at least one bvar needs to be
> present, in all cases of quantifiers. This needs to be fixed.

as I just mentioned in the case of lambda, I don't think the current
draft has this restriction. (Although if it looks as if it does, we
should make it clearer.)


> May I also suggest to change the current rewrite rule to one that
> restricts the quantifier to the domainofapplication, instead of
> embedding logical implication in the body. This would make its treatment
> consistent with the general case if my previous suggestion on the
> general rewrite rule is taken into account.

I was tempted to suggest this while these were being drafted, but it
requires that we don't use the existing forall and exists symbols in the
OM2 cds, or we extend OpenMath a bit.

in OM2 quant1:forall is used with OMBIND
so we could introduce a new CD which instead had forall as a symbol to
be used with application, taking a lambda term so

ombind
  quant1:forall
  bvar x
  oma
   P
   x

would be

oma
  fns1:lambda
  ombind
    quant1:forall
    bvar x
    oma
     P
     x



But this should really be true of _all_ uses of OMBIND.
I think personally that in Openmath we should allow 
OMBIND with no head term (meaning lambda abstraction) and
interpret the existing

OMBIND
  head
  bvars
  body

as

OMA
  head
  OMBIND <!-- lambda -->
   bvars
   body


Then the forall symbol (and other binders) is a normal function symbol
that could be gives STS types, etcand you could restrct its domain to
get qualifiers over a specific domain in the usual way, exatly as you
suggest.

However that would be for OM3, and we need to map to OM2 for MathML3 (as
OM3 will not exist in time). So changing OMBIND is out, but of course we
could do the first suggestion above of not using the existing forall and
exists symbols.

More discussion will be required on this one, I fear....

David




  



________________________________________________________________________
The Numerical Algorithms Group Ltd is a company registered in England
and Wales with company number 1249803. The registered office is:
Wilkinson House, Jordan Hill Road, Oxford OX2 8DR, United Kingdom.

This e-mail has been scanned for all viruses by Star. The service is
powered by MessageLabs. 
________________________________________________________________________

Received on Sunday, 7 June 2009 10:44:40 UTC