[SCL] Metalinguistic constructs

[Bill Andersen]

On Friday, Dec 20, 2002, at 14:16 US/Eastern, Chris Menzel wrote:
>
> Thus, "formula", "name", and "comment" all take names of syntactic
> thingies in the language as their values.

Chris is right here of course.  Anyway, coming up with some kind of 
practical mechanism for recording meta-info about formulas is certainly 
desirable.  One complication comes when you want to say something after 
the fact

> (formula (name pluscomm)
>          (comment "commutativity of plus")
>          (content
>             (forall (?x ?y)
>                 (equal (plus ?x ?y) (plus (?y ?x)) )))

And then I want to say:

   (bill-comment <formula> "another comment")

The question is, how can I refer to <formula> in such a way as to add 
the comment to the formula above if no name is supplied.  The name 
provides a nice way to beat the identity problem for formulas, but, for 
example, the following should be a legitimate way to refer to the above 
formula:

   (forall (?foo ?bar)
      (equal (plus ?foo ?bar) (plus (?bar ?foo))))

Or how about

   (not (exists (?foo ?bar)
        (not (equal (plus ?foo ?bar) (plus (?bar ?foo))))))

In sum, should it be a feature of SCL that one is required to name a 
formula, lest one lose all chance later of being able to say anything 
(additional) about it that wasn't said inside the (formula ...) form?

   .bill

--
Bill Andersen
Chief Scientist
Ontology Works, Inc.
1132 Annapolis Road, Suite 104
Odenton, Maryland 21113
United States
Office: 410-674-7600
Mobile: 443-858-6444