[Om] Om Digest, Vol 144, Issue 2
Richard Kaye
R.W.Kaye at bham.ac.uk
Thu Jun 7 17:55:53 CEST 2018
Dear all
Thank you for your help in clarifying these points for me. I am finding
this really helpful. I just hope my comments and questions are at least
vaguely helpful to some others too.
Yes I did misread the spec for the binding construct, and it is clear to
me now that a binder B can be at arbitrary expression. It's slightly
less clear what sort of things one might reasonably put in that place.
To my mind at least, there have been a number of issues raised, and
maybe if the spec even gets re-written it would be helpful to reconsider
these points. In particular, section 2.1.4 which is IMHO ambiguous.
The main points of ambiguity are that "MAY" in 2.1.4 (i-v) takes a
non-standard meaning that is not defined, "REQUIRES" in the sentence
following 2.1.4(vi) is not defined and "CONSTRUCT" in 2.1.4 (vi) should
be defined too. I honestly did my best to read these and failed to
guess the "correct" interpretation. Plenty of examples especially the
weird extreme cases and some idea of the thinking behind it would have
been helpful.
I have been trying to work out what I think of David's argument,
> Also you should be able to write nonsensical or incorrect expressions
<OMA><OMS cd="transc1" name="log"/><OMS cd="arith1" name="root"/></OMA>
> Is perfectly valid, perhaps one wants to encode the reasoning why it
> doesn't type check or have any sensible value, but to encode that
> reasoning you need to be able to encode the term.
I understand where this is coming from but there has to be a limit here,
and I don't see where this limit should be. It's a strange argument to
say that you have to be able to say anything because you may need to
express the idea that it is not mathematics. So OM needs to be able to
say "The moon is made out of green cheese" in order to express the fact
that '"The moon is made out of green cheese" is not mathematics'. But
the conclusion then is that OM needs to be able to express anything,
including all non mathematics.
"first class objects": The phrase isn't very accurate but the idea is
generally understood.
> You need to be able to use for example application symbols as
arguments
> rather than the first child, so that, as you say, you can treat
> functions as first class objects.
I still feel uncomfortable about this, and it doesn't fit with my
conception of mathematics. The problem is that "roles" give different
objects (which to me in maths would have been just plain objects at all
times on a completely egalitarian basis) different "abilities" and
*something* is therefore not "first class", or rather some symbols can
do more than (or different to) others, and this is a similar problem to
the classic "functions as first class objects" issue. But admittedly the
problem isn't so much about applying functions to other function
applications. One problem that arises is that ordinary objects cannot
easily behave as functions do, and another is that there is no obvious
natural place to specify how it is that functions (or objects behaving
as functions) actually behave. In other words I personally would expect
to see that plain constants and ordinary objects should be able to do
everything functions can, but this doesn't seem to be the case. The
current position in the OM spec as I now understand it looks like it is
a bit inconsistent in a way that is going to cause problems later.
For example if G is a group acting on a set X on the left, g in G and x
in X (both variables or symbols of the constant role) then by analogy
with sin(x) as in application(sin,x) it would be natural to write
application(g,x) (by which I mean <OMA><OMV name="g"/><OMV
name="x"/></OMA> of course) for the result of the action of g on x. But
that doesn't really work because there is no symbol or CD at all
describing this action and nowhere to say what g and x are without
additional attributes, so you should really attribute all your variables
all the time (something that is a real pain in the neck and not normally
required anyway) or (as I would prefer) write
application(groupaction,g,x) instead for some new documented symbol
"groupaction" and, for consistency, you really should have used
application(applyrealfunction,sin,x). Elsewhere in OpenMath this
"applyrealfunction" does not need spelling out, apparently, but this is
merely an arbitrary convenience that someone built in early on to be
helpful to some people but unhelpful to others. It's an unpleasant kind
of unconscious (mathematical) bias. I personally think explanation of
"applyrealfunction" really is needed, at least quite a lot of the
time.
For another example, if my OM compliant computer code were to be working
out functions such as sin, cos, etc, by means of power series by a
number of different algorithms (taking a different number of terms,
adding in a different order, rounding in a different way, estimating the
limit in some way etc.) I am encouraged to use symbols such as <OMS
cd="transc1" name="sin"/> etc for the functions, to preserve
interoperability. But then every instance of <OMS cd="transc1"
name="sin"/> needs a nasty bunch of attributes to say which algorithm is
to be used and what the parameters are. And then I have to attribute
"cos" and "log" and all the others all in exactly the same way even
though I am only using one particular algorithm in one particular
document, which results in code bloat and inelegant mathematics and a
huge amount of unnecessary repetition. The more elegant solution would
be to show in a more direct way that it is the kind of
*functionapplication* that is varying, not the *inputdata* to it.
The same applies to bindings, but this is a bit more complicated since
there is no clear idea in the standard of what kind of OM expressions
may reasonably appear in the first position of a "binding" construct and
no easy way to say "apply this kind of implementation of binding to this
binding with these variables and this matrix as body". (There is no
"symbol role" for the output of an application() for instance. That
does seem to be an issue.)
That's not to say this is a problem in OpenMath. It is such a general
system that you can always write your own CDs and choose to do your own
thing (at the expense of lack of interoperability of course). One
problem is that the syntax and examples and CDs seem to encourage what
is to me the wrong viewpoint of what maths is about, such as (for
example) the idea that everyone knows what a real number is (personally,
I don't) how best to represent one on a computer or even just in text
(ditto), and the global assumption is that there couldn't possibly be
any disagreement on these points let alone any underlying
mathematical/philosophical difficulty (there certainly is).
This isn't intended to be a rant or criticism, and I hope you don't take
it that way. It was only intended to show that different mathematical
viewpoints are not easily fitted onto the defaults suggested by openmath
(nor almost any computer algebra system, and definitely not content
mathml). The good thing is that openmath is big enough to do more and I
hope it will!
Richard
On Wed, 2018-06-06 at 13:31 +0200, om-request at openmath.org wrote:
> Send Om mailing list submissions to
> om at openmath.org
>
> To subscribe or unsubscribe via the World Wide Web, visit
> http://mailman.openmath.org/cgi-bin/mailman/listinfo/om
> or, via email, send a message with subject or body 'help' to
> om-request at openmath.org
>
> You can reach the person managing the list at
> om-owner at openmath.org
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Om digest..."
>
>
> Today's Topics:
>
> 1. Re: Om Digest, Vol 143, Issue 8 (David Carlisle)
> 2. Re: Om Digest, Vol 143, Issue 8 (David Carlisle)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Wed, 6 Jun 2018 11:22:27 +0100
> From: David Carlisle <davidc at nag.co.uk>
> To: Richard Kaye <R.W.Kaye at bham.ac.uk>, "'om at openmath.org'"
> <om at openmath.org>
> Subject: Re: [Om] Om Digest, Vol 143, Issue 8
> Message-ID: <edb42bf4-723e-0724-389f-bbe2fedf1339 at nag.co.uk>
> Content-Type: text/plain; charset="utf-8"
>
> On 05/06/2018 09:30, Richard Kaye wrote:
> > binding(B,v1..vn,C)
> >
> > can only have a symbol B in this position (and presumably the same: not
> > attributed)
>
> No B and C can be any openmath object which is what it says in 2.1.3 of
> the spec and also the relax schema, which allows "omel" as the first
> child of OMBIND (which is the same as the first (all) arguments of OMA.
>
> OMBIND = element OMBIND { compound.attributes, omel, OMBVAR, omel }
>
> David
>
> Disclaimer
>
> 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 and malware, and may have been automatically archived by Mimecast Ltd, an innovator in Software as a Service (SaaS) for business.
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://mailman.openmath.org/pipermail/om/attachments/20180606/6c8862a7/attachment-0001.html>
>
> ------------------------------
>
> Message: 2
> Date: Wed, 6 Jun 2018 12:37:45 +0100
> From: David Carlisle <davidc at nag.co.uk>
> To: <om at openmath.org>
> Subject: Re: [Om] Om Digest, Vol 143, Issue 8
> Message-ID: <262f3c33-a813-6b48-64aa-74e90a645ab5 at nag.co.uk>
> Content-Type: text/plain; charset="utf-8"
>
> On 05/06/2018 09:30, Richard Kaye wrote:
> > Naively perhaps, I rather assumed
> > that the allowed places for symbols other than as a "key" for binder
> > attribution semantic-attribution error and application REQUIRE the
> > constant role. (This is because of the "may only" interpretation and
> > the fact that the constant role is listed in parallel with all the other
> > roles in exactly the same way.)
> >
> > But now I see many different readings of "requires a different role" one
> > of which is that application arguments can be of ANY role and nothing
> > "requires" the constant role. That opens up a whole new kind of
> > mathematics, like taking the logarithm of the square root sign, and
> > taking the power set of Church's lambda operator. Is this really what
> > we want? (I had initially considered this and rejected it since I
> > thought it couldn't possibly be.)
>
> the latter reading is intended.
>
> You need to be able to use for example application symbols as arguments
> rather than the first child, so that, as you say, you can treat
> functions as first class objects.
>
> Also you should be able to write nonsensical or incorrect expressions
>
> <OMA><OMS cd="transc1" name="log"/><OMS cd="arith1" name="root"/></OMA>
>
> Is perfectly valid, perhaps one wants to encode the reasoning why it
> doesn't type check or have any sensible value, but to encode that
> reasoning you need to be able to encode the term.
>
> David
>
> Disclaimer
>
> 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 and malware, and may have been automatically archived by Mimecast Ltd, an innovator in Software as a Service (SaaS) for business.
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://mailman.openmath.org/pipermail/om/attachments/20180606/a55db855/attachment.html>
>
> ------------------------------
>
> _______________________________________________
> Om mailing list
> Om at openmath.org
> http://mailman.openmath.org/cgi-bin/mailman/listinfo/om
>
>
> End of Om Digest, Vol 144, Issue 2
> **********************************
More information about the Om
mailing list