From: David Carlisle <davidc@nag.co.uk>

Date: Sun, 7 Jun 2009 11:44:08 +0100

Message-Id: <200906071044.n57Ai8ZT019789@edinburgh.nag.co.uk>

To: andreas.strotmann@ualberta.ca

Cc: www-math@w3.org

Date: Sun, 7 Jun 2009 11:44:08 +0100

Message-Id: <200906071044.n57Ai8ZT019789@edinburgh.nag.co.uk>

To: andreas.strotmann@ualberta.ca

Cc: www-math@w3.org

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

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