[SCL] scl:comment [was: Re: SCL spec question]

[Bill Andersen]

SCL-ers - {Pat},

For context, I asked Pat about identity conditions on formulas named 
inside (scl:comment ...) forms.

Pat..

See below...

On Sep 8, 2004, at 1113, Pat Hayes wrote:

> I was hoping we could use strict syntactic identity. In fact, for some 
> purposes, even token identity. So for example this would make sense:
>
> In BillsOntology:
>
> .....(forall (?x)(p ?x))
>
> In PatsOntology:
>
> .... (scl:comment "this is the same as the axiom in Bill's ontology" 
> (forall (?x) (p ?x)))
>
> BUt they are still different axioms as far as the syntax is concerned.
>
> BTW, this question of what constitutes identity is an open issue for 
> text with markup, as in XML, as far as I know. Som=eone needs to look 
> at this issue carefully, its on my stack somewhere....

Yeah, it's a tough one.  My natural tendency is to say it's an 
ontological question and try to bring some of that machinery to bear, 
but I think that's overkill for a standard like this and might well 
slow down progress towards ISO status.

I think a reasonable compromise might be a notion of identity that 
works within an SCL document.  It seems a reasonable assumption that if 
I say:

(scl:comment "bill likes this" (forall (?x) (p ?x)))
(scl:comment "pat doesn't like this" (forall (?x) (p ?x)))

in the same document, they pretty clearly refer to the same axiom.  
This does make for a problematic situation for collaborative 
development where I enter an axiom (with a comment) one day, and you on 
the next write another comment (intended to be) for the same axiom.

Another (I think reasonable) compromise, would be to introduce 
non-denoting constants to name axioms.  I say non-denoting because I'm 
trying to avoid quantification over formulas.  It has the additional 
advantage of not having to retype the axiom.  So I say something like:

(scl:formulaID a1 (forall (?x) (p ?x)))

This gives users (or collaborators in the development) of an ontology 
unambiguous access to the axiom for the purposes of documentation.  
Uses of such constants within a document need to be unique.  With this, 
you could say in the same file, e.g.:

(scl:comment "bill likes this" a1)

Or if Pat includes the "bill" ontology containing a1:

(scl:comment "pat disagrees" bill:a1)

This is, in general, a useful mechanism for commenting on any constant 
introduced.  I don't think it's a good idea to embed this in the term 
syntax, since there seems to be no principled place to put the comment. 
  What are the ramifications of doing it this way instead:

(scl:comment "biological fatherhood relation" bill:fatherOf)

One big difference could be that bill:fatherOf denotes, but for 
something as mundane and useful as making comments I think there's good 
cause to special case the function of scl:comment