🚀 go-pugleaf

In article <2204@munnari.oz.au>, ok@cs.mu.oz.au (Richard O'Keefe) writes:
> The reason that I ask is that I was stunned to find a paper which
> described the Mycroft/O'Keefe type system as ``extralogical''.  Now,
> we're talking about a type system where type declarations are
> syntactic sugar for certain Horn clauses, and where a predicate declaration
> 	pred p(T1, ..., Tn)
> is interpreted as saying that
> 	p(X1, ..., Xn) :- Body
> is to be read declaratively as
> 	p(X1, ..., Xn) :- isa(X1, T1), ..., isa(Xn, Tn), Body.
> (in essence, the type checks are ``factored'' out into the declaration.)
> I really can't see any side effects there, nor can I see how to simulate
> var/1 with this stuff, nor yet does it seem to me to lie outside the
> logic programming model.  Is there some other sense of ``extralogical''
> which does apply?  Did presenting the system in proof theoretic rather
> than model theoretic terms damn it to extralogicality?
> 
> So, what DOES ``extralogical'' mean?

Okay, I am the one who is most responsible for that paper. To Richard,
I have explained a lot in my response to your mail, but have not seen
any reply from you. Let me repeat my argument in that mail:

---------------------
About your comment on our claim that "types in M&O scheme is extra-logical",
I do not see any ambiguity here. In your paper you wrote "type checking
does not change the semantics of Prolog", does that mean a program has the
same semantics no matter whether there are type declarations existing?
If yes, does that mean the type declarations have no semantics?
I am not saying the type declarations have no semantics at all,
their semantics is not related to (first-order or higher-order) logic.
In the sentence following above, you wrote that the type checking
"merely discourages the execution of ill-typed programs", but 
"ill-typed programs" are defined by mimicing traditional procedural
languages.
--------------------

Now, you claim your type declaration is just a "syntactic sugar for 
certain Horn clauses". Are you telling me that

 	p(X1, ..., Xn) :- isa(X1, T1), ..., isa(Xn, Tn), Body.

_does not change the semantics of_

 	p(X1, ..., Xn) :- Body.

Yes, of course you can _give_ a semantics to type declarations in this
way, and in fact this is almost exactly what we did in our LP'88 paper
(for other readers, the paper "a type inference system in Prolog",
by Jiyang Xu and David S. Warren, Proc. of Fifth ICLP, pp 604-619),
and a paper by Lee Naish in 1987. The point is you did not think
this way, or at least you did not claim you thought this way.
There are several other works that give semantics to type declarations,
for example typed unification by Michael Hanus (something similar to
typed lambda calculus), order-sorted logic by Gert Smolka and etc.,
and our partial logic semantics. The discussions and references are
all included in our paper which you read.
How can one tell _which_ semantics you had in mind?
As you can see, all these methods give different semantics to types.
Giving semantics to type declarations is not a piece of
cake that you can simply _left out_ from your paper as you said
in your previous mail.

-- Jiyang Xu
==========================================
   ECRC, Munich, West Germany
   jiyang%ecrcvax.uucp@pyramid.pyramid.com 
   or jiyang@ecrcvax.uucp
==========================================