[SCL] Metalinguistic constructs

[Tanel Tammet]

Hi,

Chris Menzel wrote:
> On Fri, Dec 20, 2002 at 08:29:08PM +0200, Tanel Tammet wrote:
> 
>>Here is a toy example:
>>
>>(formula (name pluscomm)
>>         (comment "commutativity of plus")
>>         (content
>>            (forall (?x ?y)
>>                (equal (plus ?x ?y) (plus (?y ?x)) )))
> 
> 
> The form here is really a metalinguistic template for introducing terms
> and their axiomatizations into a theory.  It's good to have examples
> that illustrate the need for a metatheory extension to SCL to motivate
> its design and definition.
> 
> It seems to me there are a couple of use/mention issues here as it
> stands.  If, as it appears, 'formula' is a predicate true of formulas
> and auxiliary info (maybe 'term' or 'termdef' would be better, if the
> idea is to have a mechanism for introducing new terms and corresponding
> axioms for them), then we need some sort of quotation device that forms
> names for formulas out of formulas, or else the result is not
> well-formed; or at any rate, it won't mean what it is supposed to mean.
> Using a single quote as the quoting mechanism then, it seems to me that
> the proper would be something like this:
> 
> (formula '(name 'pluscomm)
>           (comment "commutativity of plus")
>           (content
>             '(forall (?x ?y)
>                  (equal (plus ?x ?y) (plus (?y ?x)) ))))
> 
> Thus, "formula", "name", and "comment" all take names of syntactic
> thingies in the language as their values.

You are of course right in that IF we treat "formula" as a predicate
in a meta-language, then the content formula could be considered to be 
in a simpler language, quoted.


Then you would not need the tags "name", "comment" and "formula" in
the example above. You could write:

(formula pluscomm
          "commutativity of plus"
          '(forall (?x ?y)
               (equal (plus ?x ?y) (plus ?y ?x)) )

However, I have several doubts about this way to express information
in SCL. I still think a tagged and unquoted (in some sense, but read
on) expression is better. There are two separate reasons:

- Trying to use "real" metalogic here may lead us to serious
   complexities. IMHO the scl focus is on practical possibilities
   to present, extend, modify, annotate and connect formula-representing
   data.

   I'd prefer viewing SCL as a vehicle where we can convey data in
   various logical languages: FOL, intuitionistic logic, TR, default
   logic, etc. Of course we cannot, in practice, give connectives with
   predefined meanings for all these logics (and more) in SCL standard.

   Hence we should perhaps:
   - make it possible to use SCL base language for various logics
   - give at least one standard set of connectives with an exact
     semantics (ie implement one particular logic, and leave other
     logics to others). This one preferred logic should probably be
     FOL, of course.

   In case we try to treat "formula" as being a predicate in logic,
   then the TOP LEVEL, the base language of SCL suddenly becomes
   logic. What logic should that be? How do we define exact semantics?
   These questions are of course extremely hard and we will drown
   if we try to attack them.

   To summarize, it would be easier to:
    - not treat SCL base language ("formula", "declaration", "include"
      kinds of tags) as logic.
    - give slots in the base language where the logic goes (in the
      example I had a (formula (content ..)) slot).
    - give one standard logic (FOL) as one possible filler of the slot,
      concretely defining SCL representation of FOL.
    - make it possible for people to use their own exotic
      logics in the slot as well.

- Even if you would prefer to treat "formula" as a logical predicate,
   you still would not need quotes. Why? Because the tags
   "name" "comment" and "content" etc ARE quotes, with different names.

   In lisp the quote symbol in the second example above actually gives
   us the following term (as we know, tick is just a macro character):

(formula pluscomm
          "commutativity of plus"
          (quote
              (forall (?x ?y)
               (equal (plus ?x ?y) (plus ?y ?x)) ))

    Now, the "quote" function here is not really different from the
    "content"  function I had in the example.
    The "content" function is better since it conveys more information:
    it is a typed quote. What happens is that the order of arguments
    for "formula" becomes irrelevant, since the three different quote
    symbols "name" "comment" and "content" indicate the type of
    the quoted term just as well as the position would.

    The original example is exactly what you would get from the last
    "quote" function example once you introduce typed quote functions
    "name" "comment" and "content" in order to make the argument order
    of "formula" irrelevant ("formula" would then rather be a set
    constructor, which is IMHO more suited to the nonlogical XML
    ideology):

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


The following discussions concerns names, not the quote
issue:

An issue which was overlooked in my previous example of attaching
SCL-meaningless information to formula, function, etc names and
their sets:

- sometimes we want to say something about particular names
   separately, like:

(declare (formulas f1 f2 f3)
          (hasproperty orderedequality) )

- sometimes we want to say something about a WHOLE SET as one
   entity, like:

(declare (formulas f1 f2 f3)
          (hasproperty satisfiable) )

There is nothing hard or bad there, of course. We will

- either use different versions of "formula" or "hasproperty" tags (or a
   special "set" or "bag" tag to group) to differentiate between the two
   meanings.

- in case each of the "(formulas f1 f2 f3)" element separately has
   an indicated property (for example, "orderedequality"), we could
   give separate declarations for each (single element and set of a
   single element not distinguished: dirty and excessive
   but probably usable):


(declare (formulas f1)
          (hasproperty orderedequality) )
(declare (formulas f2)
          (hasproperty orderedequality) )
(declare (formulas f3)
          (hasproperty orderedequality) )


Any suggestions?


Another not-too-hard issue stems from the names of formulas. In case
we include other files or point to them, we need to make sure that
the names do not become ambiguous. To achieve this we could say
that each name is actually automatically prefixed with the file URI as a 
namespace, BEFORE any inclusions or pointings to external data are
carried out.

Then you can also refer to names in other files, just by using the URI
of the file (sometimes you do need to refer to the names in included
files).

We should explicitly disallow ambiguous names.




Regards,
           Tanel Tammet