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

[pat hayes]

>Hi,
>
>Pat Hayes wrote a fairly detailed answer to the mini-agenda. Thanks!
>
>I'll give brief explanations of two issues which were a bit foggy
>in my agenda:
>
>>>- Additional conceptual information for functions and predicates.
>>>
>>>   It should be possible to declare that some functions, predicates
>>>   etc have some properties (for example, by saying something like
>>>   (hasproperty f (uri "http:/asasas.asa.aa/")).
>>>
>>>   For example, an application might want to say that f is a computable
>>>   function and it has a built-in extralogical function to compute f
>>>   in some circumstances.
>>>
>>>   An application might also want to say that f is a special
>>>   answer-predicate.
>>
>>
>>Hmmm. I'd like to know more about what kinds of property and in 
>>what sorts of ways those properties can be defined.
>
>The properties I am thinking about are extralogical. I would rather NOT
>declare in some specific way that f or P are commutative etc, since
>we have ordinary formulas for declaring that.

Right.

>
>However, suppose you have a function plus in your language. You may 
>well axiomatize plus, but after a while you may decide to implement 
>plus of two integers directly, with an extralogical program. You may 
>still keep the axiomatisation. The intention of the program attached 
>to plus is to
>speed up term normalisation. Of course, it may (and normally does) 
>also create its own additional semantics for plus.

There is a delicate issue about what exactly 'extra semantics' is 
supposed to mean, but lets agree to be firm about that.

>
>These kinds of attached programs often give a huge improvement in 
>speed and usability for automated theorem provers optimised for some 
>application domain.
>
>Hence an implementor may well expect the user of the system to indicate
>which functions and predicates have such extralogical attachments.
>
>It is very clumsy to do this with special names like $f, etc.
>
>A declaration possibility is better. A declaration may also declare
>other things besides the procedural attachment.
>
>One simple example is the ans-predicate used in theorem proving to
>capture the substitution created by the proof (essentially the same
>machinery as used by Prolog for giving answers).
>
>The fact that some predicate is used as ans-predicate is somewhat 
>extralogical. You cannot define it in logic. Yet you badly need to
>say that you do have such a special predicate. Again, the general 
>declaration possibility would help. Systems could use the mechanism
>(if they please) to these kinds of purposes I outlined here.
>
>Yet another example is term rewriting. You may want to say that an 
>equality is oriented in a specific way. You may want to say that 
>some unit equalities should always be treated as term rewriting 
>rules, and some others should not.
>
>The important issue is that (IMHO) no kind of semantics should be 
>given by the SCL to these declarations. They are there to be given a 
>special semantics by the particular implementations.

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?

>
>In some sense it is bad, since this semantics would not be understood
>by other systems.
>
>On the other hand the possibilities like these are absolutely necessary
>in practice. Also, people could, in fact, design and explain 
>"standard" collections of URI-s for indicating popular kinds of 
>information conveyed by these URIS about properties of functions, 
>predicates, etc.

I agree with all of this.

>
>
>>>
>>>- Additional conceptual information for sequences of formulas
>>>   in the file.
>>>
>>>   It should be possible to declare that a sequence of formulas
>>>   in the file has some properties (for example, by saying something like
>>>   (hasproperty (uri "http:/asasas.asa.aa/")
>>>       (forall (?x) (p ?x))
>>>       (forall (?x) (r ?x))) )
>>>
>>>   It is crucial for making it clear that some formulas represent
>>>   a particular theory for which an implementation might know something
>>>   about.
>>
>>
>>? similar comments to previous.
>
>For example, take the classical set-of-support strategy.
>
>You may want to split the formula C1 & C2 & ... & Cn to be refuted 
>into two parts, C1 & ... & Ci   and  Ci+1 &... & Cn so that you know 
>beforehand that the first part, say, is consistent. This knowledge 
>gives
>you several very nice and efficient proof search strategies.
>
>A typical situation where this occurs: you want to check that a 
>formula F is derivable from the theory T. Normally you know 
>beforehand that T is
>consistent. You may also want to tell the prover that it is namely F
>which needs to be derived, ie F is the question to be focused on.
>
>You may also want to indicate that a certain group of equalities is
>known to be oriented in a nice way and forms a complete and terminating
>reduction system.
>
>Knowing that some theory is present in the file may be advantageous 
>to the prover also in other respects.
>
>Such knowledge does not normally introduce semantics other than 
>suggesting a suitable search strategy for the prover.
>
>On the other hand, writing this knowledge into the file may capture
>pretty important information from a human user about the theories
>used and questions asked.

OK, what these examples suggest is that we need a level of scoping in 
the syntax *above* that of a 'top-level' axiom, and we need to be 
able to attach things to that level.

Question: would it be enough to just say that a group of expressions 
(call it a theory) is a syntactic unit, or do we need to allow 
recursion (theories containing theories containing.....) ?

My instincts suggest that allowing recursion is less likely to cause 
problems, but its only a weak instinct.

>
>Obviously, this information is semantical in nature, just
>that I do not think we will succeed in formalising this kind of
>semantical information for SCL or CL in some generic way.
>
>So I propose forgetting the semantics of "metalogics" and
>using a syntactical declaration mechanism, where concrete
>semantics is given by the implementations.

I agree. We don't have time to get into metalogics in any case.

Pat
-- 
---------------------------------------------------------------------
IHMC					(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola              			(850)202 4440   fax
FL 32501           				(850)291 0667    cell
phayes at ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu   for spam