[SCL] Re: (SCL) Getting a move on

[Tanel Tammet]

Hi,

pat hayes wrote:

> OK, lets agree on that. I think we can make a simple start on this by 
> having a way to attach SCL-meaningless (ie no logical semantics) text to 
> any piece of SCL syntax. Then we, or others, can come along later and 
> make subtler distinctions between different kinds of attachments and 
> what they mean.
> 
> I think the key issues we need to decide at present are
> 
> 1. to actually do this (I vote yes)
> 2. deciding what level to break out the attachments (lexically distinct, 
> syntactically distinct?)
> 3. what level(s) the attachments can be made to SCL expressions
> 4. Do we need at this stage to consider different 'types' of attachment 
> or can we put that off until later?
> 
> then later we will need to get detailed:
> 
> 5. deciding on a workable syntax which doesn't break existing syntactic 
> constraints. This might need to be done differently for each concrete 
> syntax, so we might want to defer this until later, but it ought to be 
> as simple as possible, for sure.
> 
> 6 (Part of 3) deciding what lexical/syntactic constraints there might be 
> on the text OF an attachment, and whether these are going to be a 
> problem or not. For example, can SCL itself appear inside an SCL 
> attachment? and if it does, should it get parsed or ignored by the SCL 
> parser?


I'll give a draft of how these kinds of information
attachments could be given in SCL. The draft is a small
toy example which might well a part of larger realistic
example.

I am quite sure it won't be OK the way I present it, but
I hope that the needs are visible and we get an example
to work on for devising a better syntax for the attachments.

I'll try to keep the syntax as simple as I can. It really
looks trivial, unrestrictive and almost devoid of predefined
meanings. Opposite to clever.

First, I assume that the SCL file is a flat sequence of data objects.


Data objects: formulas or declarations
---------------------------------------

Some of the data objects are formulas which do have built-in
logical semantics.

Some of the data objects are declarations with no built-in
logic.

At the end of the example I'll suggest two additional
data objects: file inclusion and connective syntax declarations.

Formulas
--------

Data objects which are formulas may be assigned:
  a name
  a comment
  content
and probably nothing more.

Any of these three may be lacking.

Here is a toy example:

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

(formula (name pluszero)
          (comment "plus of zero and int")
          (content
             (forall (?x)
                 (equal (plus zero ?x) ?x) )))

(formula (name plussucc)
          (comment "plus of successor int and int")
          (content
             (forall (?x ?y)
                 (equal (plus (succ ?x) ?y)
                        (succ (plus ?x ?y)) ))))

(formula (name mynegatedgoal)
          (comment "the formula we want to refute")
          (content
             (forall (?x ?y)
                 (equal (plus ?x (succ (succ 0)))
                        (succ (succ ?x)) ))))


Declarations
------------

Essentially, data objects which are declarations either:


- attach SCL-meaningless text to the WHOLE file (problem name,
   author, suggested strategies, etc)

- attach SCL-meaningless text to functions, predicates, constants,
   formulas and sets of all of these.

I think that allowing attachments to term constructor symbols
and formula name sets is enough. I cannot immediately
see a need to give attachments to arbitrary subterms.

Literal level might be an exception. You might want to say
that one specific equality literal in a larger formula is oriented well.
I do not know how to do it nicely with declarations, though.
Often people just use a special name for equality in this case.

This attached text normally has meaning for some implementations.
It does not necessarily have any meaning to other implementations.
SCL ignores any meanings of text given by declarations.

Declarations refer either to formula names or term constructors:
predicates, functions, constants. Observe that we need to
distinguish referring to different types of objects in case
the names may be overloaded.

I'll give some decidedly dirty, nonelegant example declaration objects
you might want to use in practice as additions to the previous
example:


; The first four declarations say something about the whole file.
; NB! The later example declarations will say things about functions,
; formulas, etc, but not the whole file.
;
; The first four declarations probably mean for some
; implementations that:
; - the name of the problem is "example problem"
; - the author of the problem is "John Doe"
; - the file is probably unsatisfiable
; - the suggested strategies are hyperresolution and "binary resolution"
;
; NB! "name", "author" etc have no predefined meanings in SCL!

(declare (name "example problem"))
(declare (author "John Doe"))
(declare (guessvalidity false))
(declare (trystrategies hyperresolution "binary resolution"))



; probably means for some implementations that:
; - procedural attachments should be enabled for plus and succ
; - plus and succ take integers and return integers
;
; NB! "function", "hasproperty", etc have a meaning in SCL in the
; context of "declare"


(declare (function succ plus)
          (hasproperty computable int2int) )

; probably means for some implementations that:
; - procedural attachments should be enabled for zero,
;   for example simply replacing "zero" with integer rep.
; - zero has integer type

(declare (constant zero)
          (hasproperty computable int) )

; probably means for some implementations that:
; - formula set {pluscomm,pluszero,plussucc} is
;   known to be satisfiable
; - formula set {pluscomm,pluszero,plussucc} is
;   a theory call "myinttheory" and known to the
;   system under this name.

(declare (formula pluscomm pluszero plussucc)
          (hasproperty satisfiable myinttheory) )

; probably means for some implementations that:
; - formula "mynegatedgoal" is a goal to be
;   refuted


(declare (formula mynegatedgoal)
          (hasproperty goal) )


; probably means for some implementations that
; formula set {pluszero,plussucc} is such that:
; - is confluent
; - is terminating
; - equalities are ordered in right direction


(declare (formula pluszero plussucc)
          (hasproperty knuthbendix terminating ordered) )


Inserting files
----------------

This example does not concentrate on file insertions and such,
but I'll just throw an example file insertion in.

Essentially we need a THIRD kind of top level data object for
file insertion:

; the following ALWAYS means that files at two given locations should
; be physically inserted into the current file, replacing the
; insert data object

(insert "http://wewe.www.cdd/dddd.csl" "../nicetheory.txt")



Declaring connective syntax
---------------------------

This example does not concentrate on connective syntax declarations and 
such, but I'll just throw an example connective syntax declaration in.

Essentially we need a FOURTH kind of top level data object for
syntax declarations:

; The following ALWAYS means that "negationasfailure" and
; "tlexist" can syntactically be used as ordinary logical
; connectives.
;
; Probably means for some implementations that:
; - negationasfailure is a negation symbol in the CWA sense
; - tlexist is an existential quantifier in some terminological
;   reasoning syntax
;
; Probably means for all the other implementations that
; formula objects containing connctives "negationasfailure" or
; "tlexist" should be discarded as ununderstandable.
;
; NB! Observe that if something additional needs to be
; said about "negationasfailure" or "tlexist" (URI-s or such)
; then the (declare ...) data objects above can be nicely used.

(connective negationasfailure tlexist)




Regards,
           Tanel Tammet