[Om3] Om3 Digest, Vol 18, Issue 5

[David Carlisle]

Chris

> And moreover, there is no difference between these since 'being an element
> of the domain' is a condition; and the other conditions are merely 'AND'ed
> with this condition to describe a new domain.

Yes this is exactly my objection to prodcond, prod already takes a
domain, so prodcond which takes a domain and a condition, is totally
unnecessary. 

> So it comes back to the question of how close to commonly used non-digital
> methods of describing 'mathematical semantics' should OM be?

I think I got as far as Phd level of education in mathematics without
ever being shown or thinking about explict binding operations. (Of course
you are aware that certain variable in certain constructions bind, but
never viewed binding itself as an explict construct in the sense of the
lambda calculus. I only met the (typed and untyped) lambda calculus
later, when I deserted my former colleagues and ended up in a Computer
Science department...

So while it's fun (and perhaps even useful) to argue the merits of typed
versus untyped foundational systems as being the correct basis for
Openmath, I don't really believe that any system that models
mathematical functions as the kind of formal term expression implied by
OM or MathML or any kind of lambda calculus is ever going to look
particularly natural to the man in the street (or even the mathematics
common room). Most people (XML geeks excepted) would say that any
encoding using XML looks pretty unnatural anyway. So I don't think this
is really a problem in practice, so long as there is a well defined
mechanism to go from what is meant to what must be encoded in OpenMath,
adding a few suchthat and lambda symbols at the same time as 
adding the XML markup is just "stuff" which needs to be done but
shouldn't affect the way you think or talk about or teach the original
expression.

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. 
________________________________________________________________________