<html><head><style type="text/css">.style1 {font-family: "Times New Roman";}</style></head><body>On 05/06/2018 09:30, Richard Kaye wrote:<BR>
> Naively perhaps, I rather assumed<BR>
> that the allowed places for symbols other than as a "key" for binder<BR>
> attribution semantic-attribution error and application REQUIRE the<BR>
> constant role. (This is because of the "may only" interpretation and<BR>
> the fact that the constant role is listed in parallel with all the other<BR>
> roles in exactly the same way.)<BR>
> <BR>
> But now I see many different readings of "requires a different role" one<BR>
> of which is that application arguments can be of ANY role and nothing<BR>
> "requires" the constant role. That opens up a whole new kind of<BR>
> mathematics, like taking the logarithm of the square root sign, and<BR>
> taking the power set of Church's lambda operator. Is this really what<BR>
> we want? (I had initially considered this and rejected it since I<BR>
> thought it couldn't possibly be.)<BR>
<BR>
the latter reading is intended.<BR>
<BR>
You need to be able to use for example application symbols as arguments <BR>
rather than the first child, so that, as you say, you can treat <BR>
functions as first class objects.<BR>
<BR>
Also you should be able to write nonsensical or incorrect expressions<BR>
<BR>
<OMA><OMS cd="transc1" name="log"/><OMS cd="arith1" name="root"/></OMA><BR>
<BR>
Is perfectly valid, perhaps one wants to encode the reasoning why it<BR>
doesn't type check or have any sensible value, but to encode that <BR>
reasoning you need to be able to encode the term.<BR>
<BR>
David<BR>
<br /><br /><p style="font-family: Verdana; font-size:10pt; color:#666666;"><b>Disclaimer</b></p><p style="font-family: Verdana; font-size:8pt; color:#666666;">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. Please see our <A href="https://www.nag.co.uk/content/privacy-notice">Privacy Notice</A> for information on how we process personal data and for details of how to stop or limit communications from us.<br /><br />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.</p>
</body></html>