Comments to [[SCL] new version improved slightly]

[pat hayes]

>pat hayes wrote:
>
>>Re: Comments to [[SCL] new version improved slightly]
>>
>>>
>>>3) Comments and headers and topsentences etc.
>>>
>>>There is no talk about how comments and metainfo should be given.
>>>Comments have to be put back into the core, preferrably into
>>>the kernel.
>>>
>>
>>I have a suggestion, which is that they are not in the kernel 
>>(since they have no semantics) but that any dialect may include 
>>material which does not parse to the kernel, and that is 
>>'invisible' to SCL. THis allows any dialect to include comments and 
>>meta-info freely, using any non-SCL syntax. Do you think the 
>>core/kernel should provide an explicit comment syntax also?
>>
>Yes. The comments and metainformation (for SCL they are the same!

No, I don't think they are.

The motivation for the header is as a place to put stuff that someone 
wants to be true, but does not want as part of their universe. This 
may sound odd but it has been a constant issue in the SW designs: it 
surfaced there for a while as 'dark triples' in OWL-RDF, and also in 
the design of datatyped literals. Thre was a long-running  dispute 
about whether things like arity assertions should be allowed in an 
ontology or not; one can see arguments both ways.  In general, there 
seems to be a widespread utility for being able to segregate some 
parts of an ontology from the other parts.  The header syntax is a 
small, simple device which I think can be used to solve a lot of 
these problems at least well enough to let people coexist.

It also provides a way to licence a more efficient holds/app 
translation. You argued forcefully for having a uniform translation 
here, rather than trying to be clever and only using holds/app when 
'necessary', so that a FO SCL ontology would translate directly as 
is.  I agreed with you, because one never knows when another sentence 
might come along which uses some FO syntax in a non-FO way, requiring 
a revision.  But consider the case where a FO ontology is provided 
with an explicit header which forces it to be FO, and suppose we 
require that merging of ontologies is allowed only when they have 
consistent headers. Then it would be safe to translate this 
'cleverly' by rendering it directly, without the holds/app mapping 
being invoked. This enables SCL to represent GOFOL directly, and have 
it processed as GOFOL, while still supporting the general embedding 
for all the rest of SCL.  And since the header can consist simply of 
an importation of a 'standard' header describing the signature, the 
extra overhead for this can be made very small. Notice that the 
header defining GOFOL is not itself written in GOFOL (necessarily, 
since it has to quantify over relations in order to express the 
requirement that they are not individuals.)

In terms of files, think of an ontology with a header as a linked 
pair of files. Merging two of these is done by checking the header 
parts for compatibility, then concatenating the headers and 
concatenating the bodies. More simply, if coarsely: check the headers 
for identity , then if so, concatenate the bodies and pass the header 
along unchanged.

>) are extremely important. Better
>not push them to some obscure corner.

OK, I have put them back into the core in the form ('commentstring' 
<term.|<sentence>) and plain ('commentstring') at the top level as an 
option for 'global' comments.

>
>For example: the reason why you introduced ontology and header 
>special names was IMHO that
>you forgot the comments:

No, that wasn't the reason.

>if you had had them in the core or kernel, the'yd have sticked out as
>a suitable machinery to use instead of inventing new names for 
>special-purpose metainformation.
>
>I know you claim otherwise, but I am not so sure yet that these 
>mysterious headers are a necessity.

They are not necessary for many purposes, and can always be 
eliminated (if necessary by simply eliminating the header 
boundaries), but I want to retain them for SW applications.

>
>>>Although I understand the principal need for headers, the current
>>>talk about headers (unavoidably) stops too early. There is no 
>>>indication about
>>>what and how should be put there, and as such, one cannot use the
>>>headers.
>>>
>>
>>I am writing that stuff now.
>>
>Waiting with interest.
>
>>>
>>>I'd rather see the headers and comments merged into one. Comments
>>>should have no semantics for SCL (they should have semantics at the
>>>level outside the scope of SCL). Since any headers can be written 
>>>as comments,
>>>
>>
>>No: headers *do* play a semantic role. That is the reason for the 
>>distinction.
>>
>Perhaps, we'll see.
>
>>>I think we should not separate them. Comments are IMHO enough.
>>>
>>>If/where they are not enough, then I am afraid that headers will
>>>work neither.
>>>
>>>As an example, consider http. The type of a body part of a http response
>>>(gif, jpg, html, txt, doc etc) is NOT given as part of the body. It is
>>>given as content-type in the http headers, which is on a _different_ level
>>>than the http body itself. Similarly, any "headers" should IMHO be either
>>>given as comments or they should not be at the SCL syntax level at all.
>>>
>>>As another example, you just cannot declare
>>>in XML text itself that now we are going to have something in arbitrary
>>>NON-XML: this non-xml might contain less-than etc symbols, breaking the XML
>>>syntax of the whole text.
>>>
>>>I am also not sure we should use topsentence and allow imports at 
>>>top level only.
>>>IMHO we could allow import in any place, not just top level. This would
>>>make the kernel more flexible while syntax is actually simplified.
>>>
>>
>>I cannot make semantic sense of
>>
>>(not (import <ontology:foo>) )
>>
>>If you can, I would be grateful for an explanation. (Also inside 
>>disjunctions, for example.)
>>
>Sure there is the ordinary, trivial procedural meaning: replace the 
>(import ....) substring with the contents
>of a file with this URL. This is a simple macro operation.

I don't want it to mean that.

However, I now see that such an assertion makes perfect sense, 
although I cannot think of any point in being able to do that (in 
effect, it is a denial of the ontology foo: it asserts it to be 
false. )

>
>Observe that:
>
>- there is no semantics of (import ...) in SCL: it is a different 
>language level, as macros always are

No, there is a semantics (which is why its in the core).

>
>- it is completely up to the person who wrote the (import ...) to 
>guarantee that the content and syntax
>   in the included file will suit the context.
>
>- in case you restrict (import ....) to top level only, nothing will 
>get cleaner or get more semantics:
>    it is still a macro operation without SCL semantics.

No, it has a semantics. It is kind of trivial, but it is there. It is 
not a procedural macro.

>
>Hence, in case we prefer to put (import ....) into SCL, then I'd be 
>all for removing any restrictions:
>let it occur wherever the writer wants to write it.
>
>Of course, I prefer NOT putting (import ...) into core SCL at all. 
>This kind of thing should be
>implemented on a different level. For example, should we put XML 
>namespaces into SCL?
>No? If not, then let us avoid putting XLINK into SCL, for similar reasons!

YOu have lost me here completely. I wasn't suggesting having anything 
to do with XLINK.

>
>>>
>>>5) Equality
>>>
>>>The current presentation avoids equality issues.
>>>
>>
>>It defines equality: what issues did you have in mind (apart from 
>>those that arise in your previous point)? Semantically and 
>>syntactically, equality gives rise to no problems.  Computationally 
>>it is very tricky, I know.
>>
>I had in mind the problems we get from equality in connection to 
>TFOL<->SCL translations.
>
>>I'll try to get a sketch of this done in the next few days. It will 
>>be based on these observations:
>>
>>0. A GOFOL SCL ontology is one with a 'standard FO header' which 
>>asserts not(scl:Ind(x) & scl:Rel(x)) and assigns the appropriate 
>>category to every name in the lexicon.
>>
>>1. It is always possible to merge a header into the body and have a 
>>blank header, but the universe is enlarged; so to retain the old 
>>body quantifiers, one needs to restrict all quantifiers to a class 
>>called 'ind' (not scl:ind) which represents what scl:Ind meant in 
>>the previous ontology.
>>
>>2. scl:Ind used in a body can be rendered as scl:Ind(x) iff (x=x), 
>>ie using equality.
>>
>>3. For a headerless ontology, the hold/app translation for the 
>>logic without equality is kind of obvious
>>
>>4. Putting these observations together, with a bit of care, the 
>>quantifier restrictions for the holds/app translation (which is a 
>>very particular kind of translation, obeying a very regular 
>>pattern) can be captured exactly by (a) mapping equality to 
>>equality' (*not* using holds/app) where (b) equality' is equality 
>>but restricted to apply only to things not in the first position 
>>(since the others would fail the quantifier restriction - which can 
>>now be rendered as (x =' x) - and for these it would be the trivial 
>>restriction x=x.)
>>
>>This can all be stated by adapting the 'position' terminology to 
>>the holds/app translation: the things in the first position after 
>>the holds or app are those that map from relation/function position 
>>in the original ontology, so the original fitting requirements 
>>(which were pretty trivial for GOFOL, but still were there as 
>>lexical restrictions) translate into conditions on those new 
>>positions.
>>
>>Im sure you grok this, since I learnt it from you, though the 
>>terminology may be different. If you feel like writing it up, that 
>>would be great.
>>
>No, I do not grok this yet.
>
>What you wrote here seems to be strongly related to these headers 
>you are planning to describe
>in the near future.
>
>Since you have not described them yet, I have no idea why they are 
>there or what exactly they do,
>and hence I cannot really understand what you mean  by the paragraph above.

Well, they actually are totally defined by the model theory, which 
you do have.  What is now partly written is an exposition of some 
uses for them.  Unfotunately, Xmas is now starting to interfere with 
my writing speed.

>
>Naturally, I am rather sceptical about the whole idea of suddenly 
>bringing in the header concept
>nobody has discussed or heard of before. Sounds like either 
>complicating things up or acting
>as a special kludge.

Its an option, remember. All the above isnt really to do with 
headers, its to do with moving from a FO SCL into the holds/app case, 
and the need to restrict the quantifiers to the 'individuals', and 
the fact that in the h/a translation, one can capture this 
restriction by invoking a special equality which is restricted to the 
non-first arguments of holds and app. The headers language is just a 
convenient way to express all this.

Pat


>But, as said: any sensible discussion of the header concept will just have to
>wait until you write a description.
>
>Tanel


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes