[Om] Om Digest, Vol 143, Issue 8

[David Carlisle]

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-0001.html>