[Om] Om Digest, Vol 143, Issue 8
Richard Kaye
R.W.Kaye at bham.ac.uk
Tue Jun 5 10:30:17 CEST 2018
Thanks James !
> I think you've misread the standard: it says ""application: the symbol
may appear as the first child of an OpenMath application object", but
that certainly doesn't preclude it from appearing elsewhere.
OK: this is important, maybe I misread or maybe it doesn't actually say
what you think it does .. see below
> I don't understand what you mean by ""application(apply,sin,x)", which
seems to have two layers of application - how do they differ?
In my post I was advocating a slightly stricter form for the OM
application construct in which the first item in the application MUST be
a plain symbol of role "application". This massively helps in the
application I am currently writing (for one reason because the form the
expression takes can be deduced from the role of the main symbol). To
interoperate between the two I would suggest a new generic symbol called
"apply" of role "application". Its description (in its CD) should say
something like
The "apply" symbol represents function application and should be used
at the first position in an OM application when the item in the second
position is to be understood as a function to be applied to the
remaining items. This "apply" symbol should only be used when no
semantically more precise notion of function application is available,
and makes no further guarantees as to its behaviour beyond what has
already been said and any details in the CDs for the symbols used.
Authors should consider providing and using more precise function
application symbols, such as "apply-real-valued-function-to-real" or
"apply-lambda-term-to-lambda-expression" or
"apply-recursive-procedure-to-natural-number-on-machinemodel-X".
One of the reasons for suggesting this was to encourage people to regard
functions as first class objects. Another is to encourage people to
realise there is not just one but many ways to understand and implement
function application, and another is to ensure that the spec contains
"all bets are off" warnings in the obvious places.
> "application: the symbol may appear as the first child of an OpenMath
application object"
OK... this is about the reading of the standard, in particular sections
2.1 and 2.2 of version 2.0r1/June2017. I read this many many times!
To clarify, my reading of 2.1.3 is that
application(A1,...,An)
can currently have any object as A1 (this is the point I was just
discussing)
attribution(A,S1 A1,...,Sn An)
can only have symbols S1 .. Sn in those places, and in particular
attributed symbols are not allowed (TMK, nowhere does it explicitly say
these are not allowed, but nowhere does it say that they are allowed
either).
binding(B,v1..vn,C)
can only have a symbol B in this position (and presumably the same: not
attributed) but v1..vn can be attributed variables
error(S,A1..An)
can only have a symbol in the position for S
Then in the very very tricky section 2.1.4 "OpenMath Symbol Roles", we
have additional restrictions. (Or that's how I read them.) For indeed
if these are not restrictions then surely you (the document's authors)
would have said something quite different, to wit: "To facilitate
interpretation of the symbols CDs provide *suggested* roles for their
symbols and use. These suggested roles need not be adhered to but are
strongly encouraged at all times."
Indeed, the current text says, "The role of an OpenMath symbol is a
restriction on how it may be used to construct a compound OpenMath
object..." so it is a restriction.
So now, to take "application" as an example (the same applies to all
symbol roles) the *restriction* on a symbol of role "application" is (I
quote)
(v) application The symbol may appear as the first child of an OpenMath
application object.
Since this is a restriction and not a permission, I read "may" as "may
only". I know that is not the usual use of "may" in such documents but
it is common parlance and I see no alternative. You also say "A symbol
cannot have more than one role and cannot be used to construct a
compound OpenMath object in a way which requires a different role" which
seems to back this up.
That's where I was when I wrote my last piece... there is an inclusive
specification and what you may do that allows any symbols anywhere
(2.1.3) and then a later restriction based on roles (2.1.4). I don't
know where the definition of "requires" in "requires a different role"
is. That would seem to be important. 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.)
Incidentally, suppose I really want to consider the binding "lambda" as
a function. I could use an identity function application symbol
"id" (sorry I don't know if there is one in the standard CDs... I would
have thought there ought to be one) and do
application( application(id,lambda) , arguments-to-lambda ). So the
"restrictions" on the role of symbols is hardly any restriction at all
and my first reading (that for symbols other than as a "key" for binder
attribution semantic-attribution error and application REQUIRE the
constant role) is rather more sensible! (This takes us back to my first
point.)
Sorry if I misunderstood :( Maybe some more precision or more examples?
Richard
PS. While I remember there is an error in the discussion of
alpha-conversion in section 2.2. The substitution must not introduce
new variables into the scope of existing bindings over those variables.
As currently written it might. No doubt others have pointed this out.
On Wed, 2018-05-30 at 22: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: Comments on applications in OpenMath (James Davenport)
> 2. Re: Call for Discussion: CD editing process (technical)
> (James Davenport)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Wed, 30 May 2018 19:49:11 +0000
> From: James Davenport <J.H.Davenport at bath.ac.uk>
> To: Richard Kaye <R.W.Kaye at bham.ac.uk>, "om at openmath.org"
> <om at openmath.org>
> Subject: Re: [Om] Comments on applications in OpenMath
> Message-ID:
> <63895728d89d4ae793effc4ac7b5adaf at exch04.campus.bath.ac.uk>
> Content-Type: text/plain; charset="us-ascii"
>
> My apologies - this landed in my Spam bucket, and I've only just seen it.
> I think you've misread the standard: it says ""application: the symbol may appear as the first child of an OpenMath application object", but that certainly doesn't preclude it from appearing elsewhere.
>
> I don't understand what you mean by ""application(apply,sin,x)", which seems to have two layers of application - how do they differ?
>
> -----Original Message-----
> From: om-bounces at openmath.org [mailto:om-bounces at openmath.org] On Behalf Of Richard Kaye
> Sent: 04 May 2018 13:27
> To: om at openmath.org
> Subject: [Om] Comments on applications in OpenMath
>
> I am a big fan of the OpenMath standard. It seems to get an awful lot of things right or very nearly right and pushes the user/designer into thinking in the right directions and putting down ideas in correct
> (relevant) places. The built-in redundancy (e.g. including functions of zero arguments as well as constants) is there for good reason and this part is well thought out. The flexibility of CDs allows extremely subtle semantic points to be expressed, points that (as a mathematician) I regard as necessary options - unlike all other systems I can think of, none of which allows me to express semantically the mathematics I actually do.
>
> There are a couple of issues, however. I am coming up against them whist writing some (hopefully OM compliant) software. (More on this
> later.)
>
> This post concern applications, with some queries on these that I have come across in my work. (I also have some issues to do with attributions but this is a tad more complicated and I haven't got my questions straight there yet.)
>
> Sorry if some of this has been raised before. I didn't know where to look.
>
> ---
>
> To start with, it is a bit of a pity that the way the standard is documented, and in particular the CD files themselves are written, seem to discourage functions as first class objects. This is not a problem with the standard, just how it is used. I certainly would prefer to work with, for example, "application(apply,sin,x)" for some appropriate symbol "apply" rather than application(sin,x). (Here, sin is from "transc1" but the same remarks apply to all the others.)
>
> I understand from 2.1.4, "the role ... is a restriction on how [the symbol] may be used" and "application: the symbol may appear as the first child of an OpenMath application object", that symbols with the application role are restricted to only appear as the first child of an object. (In other words "may" is being used in the restrictive sense "may only".) In which case "application(fnplus,sin,cos)" is not possible because "sin" and "cos" have the wrong roles.
>
> This is not an essential point, because I can write my own CDs and redefine everything all over again but it very much limits the utility of the current CDs.
>
> In any case, the fact that "application" is the exception to the rule that says that all the derived constructs are informed by literal symbols acting as "keys" (to attributions, binder symbols, errors) is rather odd. If there was a possibility to reconsider I would very much suggest a standard "apply" symbol as above in a standard CD, and insist that applications like all the other constructs must take a literal symbol with the application role as the first argument. This would make for (a) more consistency and (b) encourage users to provide functions such as "sin" as first class objects (symbols with the "constant" role).
>
> This change would also signal to any user of the standards the correct place to look up specific details. As things stand, an expression such as "application( f , 21.3 )" is allowed where f is one of a number of arbitrary OM expressions. So where does someone look up how to interpret these expressions, especially when f is somewhat complicated?
> In the OM standard itself, of course, because the key notion to understand here is "application(". And unfortunately the details are not explained there. However, to understand "application( apply, f , 21.3 )"
> the user will of course look to the CD for the "apply" symbol in the first instance, which is the correct place to look. (Ideally users will specialise "apply" to give better semantic information as well.)
>
> If there were to be a revision of the OM standard and you were to provide a standard generic "apply" symbol (and give the CD of course) and say that all previously allowed "application(f,21.3)" are deprecated but to be regarded as semantically equivalent to "application(apply,f,21.3)" I don't think anything much would be lost and a lot might be gained. Just my suggestion :)
>
> Richard
>
>
> _______________________________________________
> Om mailing list
> Om at openmath.org
> http://mailman.openmath.org/cgi-bin/mailman/listinfo/om
>
>
> ------------------------------
>
> Message: 2
> Date: Wed, 30 May 2018 20:36:37 +0000
> From: James Davenport <J.H.Davenport at bath.ac.uk>
> To: Michael Kohlhase <michael.kohlhase at fau.de>
> Cc: "om at openmath.org" <om at openmath.org>
> Subject: Re: [Om] Call for Discussion: CD editing process (technical)
> Message-ID: <1527712599687.69467 at bath.ac.uk>
> Content-Type: text/plain; charset="windows-1252"
>
> Certainly a good idea in general - I am not sure I myself can make OM yet - my schedule is hectic.
>
>
> James Davenport
> Hebron & Medlock Professor of Information Technology, University of Bath
> National Teaching Fellow 2014
> OpenMath Content Dictionary Editor
> Former Fulbright CyberSecurity Scholar (at New York University)
> Chair, IMU Committee on Electronic Information and Communication
> Vice-President and Academy Chair, British Computer Society
> ________________________________
> From: Michael Kohlhase <michael.kohlhase at fau.de>
> Sent: Wednesday, May 30, 2018 4:38 PM
> To: James Davenport
> Cc: om at openmath.org
> Subject: Re: [Om] Call for Discussion: CD editing process (technical)
>
>
> Probably a good discussion topic for the OpenMath workshop.
>
> Michael
>
> On 30.05.18 17:34, Michael Kohlhase wrote:
>
> Dear James, dear all,
>
> On 29.04.18 11:15, James Davenport wrote:
> Thanks for starting this debate: a useful corollary to the decision to go GitHub. I propose that ?CD Editor? becomes plural, and we start having a team.
> I second that, that would get us around the "single-point-of-failure/delay" problem.
> I have no immediate intention of stepping down, but Michael?s Post has made me realise how ad hominem the current system is. Presumably the editors should essentially (I.e. apart from sysadmins) be those with push rights to this repository.
> I would suggest a new "team" of CD Editors at the GithHub level, and have three editors and James as Editor-in-chief. a
> A change log would be necessary.
> I think the GitHub log should be sufficient, if people give good commit messages.
>
> Michael
> I wonder (no real views either way - what do those with experience of larger/longer lasting projects think) whether a simple text (probably actually HTML) file will suffice.
>
> James
>
> Sent from my iPhone
>
> On 29 Apr 2018, at 09:42, Michael Kohlhase <michael.kohlhase at fau.de<mailto:michael.kohlhase at fau.de>> wrote:
>
>
> Dear all,
>
> as you know, we have been reorganizing the OpenMath resources and web site as multiple repositories at [1]
>
> In particular we have the new CDs repository [2], which has the CD resources and feeds the CD web site [3]
>
> The idea is that [2] should facilitate CD development by providing public source access, issues, pull requests, and notifications. Now, the first outside user (Jacob Beal) has taken advantage of this first by raising an issue [4], and then providing a pull request [5] which is currently being discussed. In a nutshell the proposal is to add negated binary connectives nor, nand, and nxor to logic1.ocd.
>
> So far so good, but this raises the question of how the CD approval process should be organized (technically).
>
> The OpenMath Standard [6] only says
>
> > 4.5 Content Dictionaries Reviewing Process
>
> > The OpenMath Society is responsible for implementing a review and referee
> > process to assess the accuracy of the mathematical content of Content Dictionaries.
> > The status (see CDStatus) and/or the version number (see CDVersion ) of a Content |
> > Dictionary may change as a result of this review process.
>
> which leaves the process open and the OpenMath Society delegates the responsibility to its CD Editor (James Davenport).
>
> James and I have started discussing the technical process of approving CD revisions. We propose that we make the GitHub-supported process we have started with Jacob's proposal the standard and document it in the README of [2].
>
> Here is what we think the process should be.
>
> 1. An extension proposal is made via a GitHub issue at [2] and discussed there.
> 2. The discussion is concretized into a pull request (PR) to [2] that is discussed further on the PR (including inline comments) until all issues are resolved.
> 3. James explicitly approves the PR and someone with push rights merges it.
> 4. the changes are announced and added to a changelog.
>
> We would like your input on this proposal (in particular what we should do for 4.)
>
> James & Michael
>
>
> [1] https://github.com/OpenMath
>
> [2] https://github.com/OpenMath/CDs
>
> [3] http://openmath.org/cd/
>
> [4] https://github.com/OpenMath/CDs/issues/32
>
> [5] https://github.com/OpenMath/CDs/pull/34
>
> [6] http://www.openmath.org/standard/om20-2017-07-22/omstd20.html#cdapprove
>
> [7]
>
> --
> ----------------------------------------------------------------------
> Prof. Dr. Michael Kohlhase, http://kwarc.info/kohlhase, skype: mibein42
>
> Professur f?r Wissensrepr?sentation & -verarbeitung
> Informatik, FAU Erlangen N?rnberg, Martensstr. 3, D-91058 Erlangen, Room 11.139,
> tel/fax: (49) 9131-85-64052/55, michael.kohlhase at fau.de<mailto:michael.kohlhase at fau.de>
> ----------------------------------------------------------------------
>
>
> _______________________________________________
> Om mailing list
> Om at openmath.org<mailto:Om at openmath.org>
> http://mailman.openmath.org/cgi-bin/mailman/listinfo/om
>
>
> --
> ----------------------------------------------------------------------
> Prof. Dr. Michael Kohlhase, http://kwarc.info/kohlhase, skype: mibein42
>
> Professur f?r Wissensrepr?sentation & -verarbeitung
> Informatik, FAU Erlangen N?rnberg, Martensstr. 3, D-91058 Erlangen, Room 11.139,
> tel/fax: (49) 9131-85-64052/55, michael.kohlhase at fau.de<mailto:michael.kohlhase at fau.de>
> ----------------------------------------------------------------------
>
>
>
> --
> ----------------------------------------------------------------------
> Prof. Dr. Michael Kohlhase, http://kwarc.info/kohlhase, skype: mibein42
>
> Professur f?r Wissensrepr?sentation & -verarbeitung
> Informatik, FAU Erlangen N?rnberg, Martensstr. 3, D-91058 Erlangen, Room 11.139,
> tel/fax: (49) 9131-85-64052/55, michael.kohlhase at fau.de<mailto:michael.kohlhase at fau.de>
> ----------------------------------------------------------------------
>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://mailman.openmath.org/pipermail/om/attachments/20180530/64f0e2b9/attachment.html>
>
> ------------------------------
>
> _______________________________________________
> Om mailing list
> Om at openmath.org
> http://mailman.openmath.org/cgi-bin/mailman/listinfo/om
>
>
> End of Om Digest, Vol 143, Issue 8
> **********************************
More information about the Om
mailing list