[SCL] Re: Folding unnecessary [was: Re: Update to SCL-related work]

[Tanel Tammet]

Pat Hayes wrote:

>> Pat Hayes wrote: It does provide an answer (which is correct but not 
>> ideal)
>> but your explanations made me hope that perhaps the folding stuff
>> is not so horrendous as it initially seemed.
>>
>> If it can be presented in an understandable and simple way and
>> really has all the nice effects you describe, would be really neat.
>>
>> BTW, could you briefly comment on whether the following approach
>> is exactly folding or is there something different:
>>
>> Suppose we normally convert P(x) in SCL
>> to Atom_2(P,x) in abstract syntax, which is really
>> just traditional FOL.
>>
>> Then we want to have completely conventional
>> FOL in SCL as well (without forcing these Atom_N or App etc
>> to be used in FOL translation) so we also allow to write P(x) in 
>> abstract
>> syntax, i.e traditional FOL.
>>
>> The P in the first abstract syntax expression
>> Atom_2(P,x) is, of course, completely different from
>> P in the second abstract syntax expression P(x).
>
>
> If you write it this way, yes. But they should not be independent, is 
> the point, because they are punned from a single symbol which should 
> play the same role when it occurs in the same kind of position (as a 
> relation name, in this case.)
>
>> In order to make these two P-s equivalent in some sense,
>> we axiomatise explicitly that for any two abstract syntax expressions
>> Atom_2(P,x) and P(x),  it always holds that they are equivalent.
>>
>> This is simply my intuitive hypothesis of how to understand
>> folding on top of conventional FOL semantics,
>> but I am a bit unsure whether it is a correct reading.
>
>
> I think it is right, yes.  Its easy (trivial) for relations, but 
> functions introduce new complications because one has to guarantee 
> that any constructible term will have a denotation even if the term is 
> not explicitly exhibited in the text.  There are cases where the 
> conditions have to be applied to things that are themselves denoted by 
> terms but not directly by names in the vocabulary, eg the case like
>
> ((((f a) b) c)
>
> where f has to be a function whose value is a function whose value is 
> a relation, but there need be no actual name for this relation. 
> Nevertheless we have to somehow guarantee that it exists in any 
> interpretation. 


I'll try to make it clearer for myself here.

First I'll write SCL: (((f a) b) c) in FOL with
app/holds:

(1)  (holds2 (app2 (app2 f a) b) c)

Now I write the "folding axiom" for f:

(foreach (x y) (= (f x) (app2 f x)))

Once we have that axiom, the formula (1)
is equivalent to

(2) (holds2 (app2 (f a) b) c)

and there seems to be nothing more left to be done.

BTW, it seems that the need for two equalities still persists.

Let us take a horrocks sentence again.

(forall (x y) (and (P x) (not (Q y)) (= x y)))

We now add "folding axioms" for P and Q:

(forall (x) (iff (holds2 P x) (P x)))
(forall (x) (iff (holds2 Q x) (Q x)))

and from these two axioms the (conventional FOL) equality
in the horrocks sentence allows us to derive that

(forall (x) (iff (P x) (Q x)))

thus making the horrocks sentence unsatisfiable.

Should we use weak equality instead (axiomatised in
a way that does not make first arguments of  holdsN
replacable, even if they are (weakly) equal), then
the horrocks sentence is satisfiable.

What this seems to indicate is that we still need the
"abstract syntax", which is FOL with appN and holdN.
This allows us to axiomatise the weak equality in an
understandable way.

Now, if we forget the equality for a moment,
it still appears that once the two folding axioms
are present, the "simplified horrocks sentence"

(forall (x y) (and (P x) (not (Q y)))

does NOT have a one-element domain,
differently from the conventional FOL
formula, which does.

The folding axioms

(forall (x) (iff (holds2 P x) (P x)))
(forall (x) (iff (holds2 Q x) (Q x)))

introduce two constants, which have to
be mapped to two different domain
elements in order to get a model for

(forall (x y) (and (P x) (not (Q y)))

Now, perhaps you want to say that since
we have not used variables or terms in the
predicate position, we do not need to
introduce the folding axioms. But then
we fall into the traditional trap:
the moment somebody adds a formula
(forall (x) x(.....)) we have to introduce
the folding axioms and the example
formula suddenly requires a two-element
domain. I.e., expected meaning of subformulas
starts to change when new, seemingly
irrelevant formulas are added.

Hence: IMHO we cannot avoid
adding the folding axioms in the
examples above.

>>
>> If it is (maybe?) then the folding stuff is explainable with just
>> this schema, without changes to underlying semantics, which
>> would make it eatable for a complex-semantics-hater
>> like me :)
>
>
> Well, indeed, one can often express a semantic constraint is a 
> requirement that a schema be true. I tend to think it is easier to 
> just state the semantic condition directly, but every man to his 
> taste. I'll think hard about restating the simplified version in this 
> style.

It would be great if you could do this. It does not mean that you cannot 
give standalone
semantics without axioms like the ones above: in principle, one could 
include both.

However,  I think that "ordinary people" would feel much
more comfortable if the semantics is exactly conventional
FOL semantics, and all the extra stuff is axiomatised on
top of it. Otherwise you could still claim that your semantics
is FOL, but anybody who looks at it sees folding maps and
all kinds of unconventional stuff, which makes people
suspicious. At least this is what happens to me: just claiming
that something is FOL does not help much unless I recognise
that the semantics really is conventional FOL with no
strange devices built in.

To summarize: this far my impression is that

(a) The folding idea is nice, if it can be presented with
     axioms.

(b) The semantics of SCL formulas in some concrete syntax
      is still different from the FOL formulas looking exactly
      the same (see the examples above).

(c) The abstract syntax with appN/holdsN is still necessary
      for clear presentation and axiomatisation of various
      operations (folding axioms and equality).

It is of course possible that I am still misunderstanding
the folding stuff and the axioms above are not right
(even though you said they seem to be right).


Regards,
              Tanel