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

[Tanel Tammet]

Pat Hayes wrote:

>>        b) We could axiomatise that Atom_2(P,x) is always
>>             equivalent to P(x). This is, of course, perfectly possible:
>>            it would be an axiom schema similar to what we have to
>>           use to define equality.
>>
>>           I suspect that this would be similar to the folding
>>           semantics (is it?) but would have an important advantage
>>           of - by virtue of being axiomatised - not changing the
>>           underlying semantics a bit.
>>
>>            I do not think that it makes sense to axiomatise this,
>>            but, well, we could do it if we really wanted to.
>>         
>> To summarise: I think you have made a good point,
>> but the folding semantics is not an answer.
>>
>> Instead, there is a trivial, correct answer
>
>
> I don't think that it is correct, is the point. None of your options 
> above seem acceptable, and all are more complex for a user than the 
> SCL logic we already have (which, as you say, is almost embarrassingly 
> simple, both in its syntax and its proof theory.)
>
Well, the trivial answer definitely is correct, but I agree that it has 
unpleasant side effects
in terms of syntax.

> Here's my current 'acid test'. If two people both want to use a symbol 
> P, but one wants to use it as an individual name and the other wants 
> to use it as a relation name, can they use the language to communicate 
> with one another? That is, can each of them use the symbol in their 
> way to draw arbitrary first-order inferences from information send to 
> them by the other, so that they can agree on the conclusions?

This is certainly crucial, I agree.

> And can they do this without having to negotiate, use syntax 
> declarations, or translate from one syntax into another? Right now, 
> SCL allows all of this. I don't think ECL does.
>
ECL does this, of course, but it does not allow to write conventional FOL.
It simply forces the Atom_N etc wrappers into the FOL translation.

Should we allow ECL to be used in the conventional FOL way,
without this App/Holds wrapping, then either the acid test fails or
we have to introduce extra syntax: both are bad. That is the reason
I did not allow the conventional FOL way, of course.

> Well, I tend to agree, but I don't think that your approach does 
> provide an answer, at least to my questions.
>
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).

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.

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 :)

Regards,
               Tanel