[SCL] Suggestion for SCL extension module

[Tanel Tammet]

Chris,

Hopefully we can get your version very soon now:
we'll have some work to do on full SCL modules
and SCL concrete syntaxes, which cannot be really
started before.

Meanwhile I have a proposal about a full SCL
module, which we could include. We have spoken
about it before, but IMHO too little.

I'll give the proposal in the short and informal
manner here.

The goal of the module would be to allow SCL
to be extended with operators which are NOT
defined in SCL and have no meaning for SCL.

Examples could be modal operators, negation-as-failure,
default rules, etc etc. All of these have their
own semantics and we cannot describe this
semantics in SCL spec.

However, we could provide a clear slot
to put these operators into SCL.

Why would that be good? Because:

- they are crucial for various specific applications
- the specific logical languages using them tend to
    contain FOL
- hence the designers of these specific languages
   could take adavante of SCL spec as a component
   of their own language spec
- systems not understanding anything out of SCL
   could still understand PARTS of the extended
   language.

Let me bring an example.

Suppose we have a file containing two assertions
in a nonmonotonic logic, one of them a simple default
rule:

==============
ostrich(dave).
forall X. default-implies(bird(X),flies(X)).
=============

Now, the first of these has perfectly clear
semantics in FOL, while the second one does
not.

Hence, an SCL-understanding system could
perhaps understand this file by keeping
only these TOP-LEVEL parts which it can
understand (first sentence) and throw away the
not-understood ones (second).

What would it mean semantically:

The top-level sentence containing unknown
operators cannot be given a concrete
truth value in the SCL-based system,
since this would probably misinterpret
the sentence.

However, FOL (and prop logic) can represent
an unknown logical truth value simply as
a propositional variable not occurring anywhere
else, ie a new propositional variable.
"New" here means the same as a "new" function
symbol for Skolemization: when we give a sentence
forall X. exists Y. P(X,Y).
then, as we know, we can Skolemize it into
forall X. P(X,f(Y)).
where "f" is a new function symbol not
occurring anywhere in the full formula
which is interpreted.

Skolemization does not change satisfiability,
as we know, although it brings in the
new symbol.

The example we had before could hence be
"pseudo-skolemized" to

=============
ostrich(dave).
p1.
============

where "p1" is a new propositional variable
not occurring anywhere else.

After this "pseudo-skolemization" an SCL
understanding system could still infer
"ostrich(dave)"
from the file above, which is a correct
inference also in the context of default
logic (or ANY interpretation of
"default-implies" in any sensible
extended logical system).

In order to allow this we should:

a) give a syntactic slot for such
    operations, for example, by adding
    an operator "extended_i" to the language,
    where any "extended_i" tuple would be
    analogous to the "formula_i" tuple.

==============
ostrich(dave).
forall X. extended_3(default-implies,bird(X),flies(X)).
=============

b) give semantics for "extended_i" tuples.
    This is certainly harder than giving a
    syntactic slot.

    One way to do that would be to define
    that any tuple "extended_n(f1,...,fn)"
    would will have  a new propositional variable
    as a value (ie the pseudo-skolemization described above).

    Then the example would be interpreted as

==============
ostrich(dave).
forall X. p1.
=============

    where "p1" is this new prop variable
    (we could also have "forall X. Atom_1(p)."
    where "p" is a new constant, essentially
    a predicate).

    Another (probably worse) way to do that
    would be to  take advantage of the "sequence" construction
    (file top level constructions) and define
    that any element of the sequence containing
    an operator "extended" anywhere will have
    a new propositional variable as a value.

    Then the example would be interpreted as

==============
ostrich(dave).
p1.
=============

Finally, perhaps the same goals could be achieved
using the annotations module in the SCL.
Remember: "formula_3(annot,something,f1)"
is equivalent to "f1"
and "term_3(annot,something,t1)"
is equal to "t1".

I have not really thought yet whether
the annotation module would be enough
or not.

Any thoughts on this theme?

Regards,
          Tanel Tammet