Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!uunet!munnari.oz.au!cs.mu.oz.au!ok From: ok@cs.mu.oz.au (Richard O'Keefe) Newsgroups: comp.lang.prolog Subject: Re: What does "extralogical" mean? Keywords: usage Message-ID: <2390@munnari.oz.au> Date: 11 Oct 89 15:34:55 GMT References: <2204@munnari.oz.au> <786@ecrcvax.UUCP> Sender: news@cs.mu.oz.au Lines: 275 In article <786@ecrcvax.UUCP>, jiyang@ecrcvax.UUCP (Jiyang Xu) writes: In article <2204@munnari.oz.au>, ok@cs.mu.oz.au (Richard O'Keefe) writes: > 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: I have received other mail from Jiyang Xu and replied to it. I have not, however, received any mail which clarifies this point. : 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? I say that claim is _wrong_, not that it's _ambiguous_. As I recall it, Alan Mycroft wrote that (he wrote most of the paper). It is an essential property of ML-like type systems that type checking serves only to accept or reject entire programs; once a program has been accepted as well-typed the types are not used at run time. A recent paper on this subject is The Essence of ML John C. Mitchell & Robert Harper POPL 15, 1988 The point is that you have two related languages, a typed language and an untyped language. BOTH languages have a semantics; the point of a type checking theorem is to show that a formula in the typed language can be evaluated correctly by the untyped interpreter. In the case of the Mycroft/O'Keefe system, it is again the case that there are two languages, ***EACH*** with a logical semantics. One of them is the language with type information in it, call it HCMT (for Horn Clauses with ML Types). The other is HC (Horn Clauses simpliciter). The central theorem of the paper is that a program in HCMT can be interpreted by SLD resolution as an HC program, just by erasing the types, and that this preserves the semantics of HCMT programs. To repeat, the essence of the idea is that type checking is a compile time operation whose effect is to reject entire programs, and that the types have no run-time role at all. The type system described in the Xu and Warren paper has exactly the same property! "The type of a predicate [is an] abstract semantics of the regular program semantics". If the fact that types play no role at run time is what makes a type system "extralogical", then the Xu and Warren system is also extralogical. : If yes, does that mean the type declarations have no semantics? No, the type declarations have a first-order logical semantics. The point is that type checking shows that the type goals are redundant, so that they do not need to be executed at run time. It is possible to do this precisely *because* the type declarations have a first-order logical 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. Here is what a type declaration looks like in the Mycroft/O'Keefe scheme. :- type t(T1,...,Tn) --> c1(X11,...,X1n1) | ... | ck(Xk1,...,Xknk). where the Ti are distinct type variables, the ci/ni are distinct constructor functions, and the Xij are terms made up of type variables (which must appear in the head; this is important for technical reasons that I'll not go into) and type constructors, possibly including t/n. Here is the semantics of such a declaration: isa(c1(A1,...,An1), t(T1,...,Tn)) :- isa(A1, X11), ... isa(An1, X1n1). ... isa(ck(A1,...,Ank), t(T1,...,Tn)) :- isa(A1, Xk1), ..., isa(Ank, Xknk). For example, here are two of the predefined types and their meanings: :- type pair(K,V) --> K-V. :- type list(T) --> [] | .(T,list(T)). isa(A-B, pair(K,V)) :- isa(A, K), isa(B, V). isa([], list(T)). isa([A|B], list(T)) :- isa(A, T), isa(B, list(T)). If a compositional mapping from declarations to Horn clauses does not constitute a first-order logical semantics for those declarations, I don't know what does. It's true that the Mycroft/O'Keefe paper doesn't present exactly this mapping, but it does say "Our approach is to consider type specifications as restrictions on arguments to predicates (and functors). ... We do not test for violation of such restrictions at run time, but by statically forbidding all programs which may lead to a type error. ... the well-typing rules ... are essentially Horn clauses." A predicate declaration in the Mycroft/O'Keefe scheme looks like :- pred p(X1,...,Xn). where each of the Xi is a type term. This is "a restriction on arguments to predicates". The semantics is again compositional; every clause p(A1,...,An) :- Body is to be read AS IF p(A1,...,An) :- isa(A1, X1), ..., isa(An, Xn), Body had been written. The net effect is that the combination of - type declarations, - predicate declarations, and - Horn clauses is another set of Horn clauses. The meaning of the declarations and clauses is defined to be the meaning of the Horn clause program which results. For example, consider the HCMT program :- type list(X) --> [] | [X|list(X)]. :- pred append(list(X), list(X), list(X)). append([], L, L). append([H|T], L, [H|R]) :- append(T, L, R). This program has a well defined first-order meaning; which is the same as the meaning of isa(X, integer) :- integer(X). /* other built-in types */ isa([], list(_)). isa([A|B], list(X)) :- isa(A, X), isa(B, list(X)). append([], L, L) :- isa([], list(X)), % drop, because true isa(L, list(X)), isa(L, list(X)). % drop, because redundant append([H|T], L, [H|R]) :- isa([H|T], list(T)), % reduce isa(L, list(T)), isa([H|R], list(T)), append(T, L, R). The clauses for append/3 simplify to append([], L, L) :- isa(L, list(_)). append([H|T], L, [H|R]) :- isa(H, X), isa(T, list(X)), isa(L, list(X)), isa(R, list(X)), append(T, L, R). the last clause of which simplifies to append([H|T], L, [H|R]) :- isa(H, X), isa(L, list(X)), append(T, L, R). Now there is another HC program which can be obtained from the same HCMT program, by discarding the declarations. That's just the append/3 we know and love. That predicate has a DIFFERENT meaning: append(1, 2, [1|2]) is in the meaning of the usual definition of append/3, but it is ***NOT*** in the meaning of the HCMT program *with* the declarations. So we have two different ways of turning an HCMT program into a set of Horn clauses: one which inserts isa/2 goals, and one which just discards the declarations, and these two methods yield DIFFERENT meanings. The type declarations *DO* make a semantic difference. The point is that if you have a well-typed program (a static check) then well-typed *queries* can't DETECT the difference; any query which could detect the difference will be rejected by the type checker. Because of that, you can use (the type checker to screen out ill- typed queries followed by) the untyped program to find the same answers that the typed program would have done. I repeat, the Xu and Warren type inference system appears to have the same character: the types which are inferred do not have any run-time effect. : 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. What Alan Mycroft wrote was "Due to the type checker being a separate program, type checking does not change the semantics of Prolog, but merely discourages the execution of ill-typed programs." That is, the type checker was not built into DEC-10 Prolog, so although the type checker could say "this program or query is not well-typed" (and thus change the semantics of the program or query to "no"), it could not prevent you running the program in straight DEC-10 Prolog anyway. I don't see how anyone can get from that to '"ill-typed programs" are defined by mimicking traditional procedural languages'. Alan Mycroft didn't say that, I didn't say it, and it isn't true. Traditional procedural languages don't allow ill-typed programs, and the ill-typed nature of the query ?- append(1, 2, X). has nothing to do with 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. No. I'm saying that it ***DOES*** change the semantics (in a compositional first-order way), but that for well-typed programs and well-typed queries you can't DETECT the difference. : The point is you did not think this way So now he reads minds. Brilliant. : How can one tell _which_ semantics you had in mind? Reading the paper is a good way. The point is tht Xu CLAIMED TO KNOW what our semantics was and to know that it was "extralogical". Given that the abstract of the paper says explicitly "we observe that the type resolution problem for a Prolog program is another Prolog program" it was obvious that we had _some_ sort of logical semantics in mind. : Giving semantics to type declarations is not a piece of : cake that you can simply _leave out_ from your paper as you said : in your previous mail. I did not say that giving a semantics to type declarations is a piece of cake. Neither did we simply leave it out. The key point, the very most important thing, about the Mycroft/O'Keefe type system, is that it is not original. We didn't have to define the semantics of our polytypes, because we stole them from Milner. The paper was quite explicit that declarations for predicates were to be viewed as restrictions on their solution sets. Re-reading the Mycroft & O'Keefe paper, I have to agree that it doesn't spell things out much. Unfortunately, both of us were PhD students who were supposed to be doing other things, and we thought that everyone understood the ML type system (or if they didn't, would read the Milner paper we cited). We also thought that the idea of applying it to Prolog was fairly obvious, and that our main contribution was showing that it worked. If someone wants to say that it is not a well-written paper, I'll not gainsay them. But it is one thing to say (for example) that the Mycroft/O'Keefe paper describes the syntax of types and type declaration without spelling out their semantics (a true statement, alas). It is quite another to say in print that you know that the semantics is extralogical! I'm not defending the Mycroft/O'Keefe scheme as being especially wonderful (I repeat that the point of it was to be UNoriginal). My point is to defend it as _logical_. The irony is that, far from being extralogical, the presentation in the paper showed only that the scheme was sound for Horn clauses; we failed to show that it worked for full Prolog. For example, it turns out that cuts can be ignored, but we didn't _prove_ that. Come to that, the Xu and Warren paper doesn't discuss cuts or negation any more than ours did.