mattias@emil.CSD.UU.Se (Mattias Waldau) (10/20/89)
In article <2390@munnari.oz.au>, ok@cs (Richard O'Keefe) writes: >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. What is the semantics of type checking? Should a ill-typed program fail or is it an error? Expressed formally corresponds the following HCMT program (1) to the logical formula (2) or (3)? (Syntax: -> implication, <-> iff, or or, & and) (1) :- pred q(type) q(X) :- r1(X). q(X) :- r2(X). (2) q is a partial relation, only defined for type's. type(X) -> [q(X) <-> {r1(X) or r2(X)}] (3) q is a total relation, false if type is false q(X) <-> [(type(X) & r1(X)) or (type(X) & r2(X))] If the HCMT program corresponds to (2) type checking is used to assure that all calls of q during the execution are defined. If the HCMT program corresponds to (3) type checking is just partial evalutation, we are moving execution to compile-time. P.s. I have used the completed form. If we are reasoning about programs we can either use the Horn clauses and SLD-resolution together, or use the completed form and first order logic. SLD-resolution completes the program since it can only use the currently known clauses.
ok@cs.mu.oz.au (Richard O'Keefe) (10/21/89)
In article <1213@kuling.UUCP>, mattias@emil.CSD.UU.Se (Mattias Waldau) writes: > What is the semantics of type checking? There are two basic observations. (a) Some built-in predicates may report an error if called with inappropriate arguments. For example, arithmetic comparisons in DEC-10 Prolog print an error message if any variable in them is bound to something other than a number. Precisely which predicates report errors and which fail quietly is, alas, implementation dependent. But at the very least "well-typed programs do not go wrong" means that calls to built in predicates in well-typed programs never report type errors. (b) Some predicate definitions are really not intended as what they appear to be. The standard example of this is append/3, which is not intended to be used on anything other than lists. Every non-trivial program I have checked is riddled with predicates whose definitions are only correct under certain implicit assumptions (this argument is non-zero, that argument occurs in this other, and so on). My interest in type checking was that Leon Sterling had written a small Boyer-Moore-style theorem prover for Horn Clause programs, and most of the theorems I wanted it to prove turned out to be non-theorems because of (b). > Should a ill-typed program fail or is it an error? Why should I define it? The only behaviour of an ill-typed query is "rejected as ill-typed"; what _would_ happen if it was allowed to run is unobservable. In a *well*-typed program, neither type failure nor type error can occur. > If the HCMT program corresponds to (2) type checking is used to assure > that all calls of q during the execution are defined. That is one purpose for using a type checker. > If the HCMT > program corresponds to (3) type checking is just partial evalutation, > we are moving execution to compile-time. As I was interested in "supplementing" the bare rules with further constraints which ensured that the theorems I wanted to be true were in fact true, that is the view I took. It's worth noting that the Mycroft/O'Keefe paper only considers Horn Clauses and SLD; it does _not_ consider negation nor yet SLDNF. I imagine that the choice between (2) and (3) does matter if you are handling negation. Lee Naish has found that some problems in that case; adding type declarations to a Horn Clause program causes at most a monotonic decrease in the model, but this is not so for programs with negation. I have no idea (yet) what to do about that.
lee@munnari.oz.au (Lee Naish) (10/23/89)
In article <1213@kuling.UUCP> mattias@emil.CSD.UU.Se (Mattias Waldau) writes: > >(Syntax: -> implication, <-> iff, or or, & and) > >(1) >:- pred q(type) >q(X) :- r1(X). >q(X) :- r2(X). > >(2) >q is a partial relation, only defined for type's. >type(X) -> [q(X) <-> {r1(X) or r2(X)}] > >(3) >q is a total relation, false if type is false >q(X) <-> [(type(X) & r1(X)) or (type(X) & r2(X))] I have argued that the semantics should be defined as (and the intended semantics generally is) (3). See my paper in LNCS 287. > Should an ill-typed program fail or is it an error? It depends. As Richard pointed out, in the Mycroft/O'Keefe scheme the program should never be run (it should get a compile time error). In the Dart/Zobel scheme it would fail (runtime type checks are added where they are needed). There are several different notions of "an ill-typed program", by the way, and they can't all be bundled together. > Richard writes >It's worth noting that the Mycroft/O'Keefe paper only considers Horn >Clauses and SLD; it does _not_ consider negation nor yet SLDNF. I >imagine that the choice between (2) and (3) does matter if you are >handling negation. Lee Naish has found that some problems in that >case; adding type declarations to a Horn Clause program causes at >most a monotonic decrease in the model, but this is not so for programs >with negation. I have no idea (yet) what to do about that. If you give the semantics of type declarations in terms of incomplete definitions then you will certainly run into problems with negation. Even with the other semantics there are problems. For example, I think the Mycroft/O'Keefe scheme can be extended trivially so that it is sound for programs containing negation when SLDNF is used. If a different (but sound) implementation of negation is used, the scheme is unsound. It is a shame that there is so much work on types for logic programming but nearly all of it ignores negation. Negation is vital for logic programming and can interact with types to produce unsoundness. lee
mattias@emil.CSD.UU.Se (Mattias Waldau) (10/26/89)
In article <2497@munnari.oz.au>, lee@munnari (Lee Naish) writes: >In article <1213@kuling.UUCP> mattias@emil.CSD.UU.Se (Mattias Waldau) writes: >> >>(Syntax: -> implication, <-> iff, or or, & and) >> >>(1) >>:- pred q(type) >>q(X) :- r1(X). >>q(X) :- r2(X). >> >>(2) >>q is a partial relation, only defined for type's. >>type(X) -> [q(X) <-> {r1(X) or r2(X)}] >> >>(3) >>q is a total relation, false if type is false >>q(X) <-> [(type(X) & r1(X)) or (type(X) & r2(X))] > >I have argued that the semantics should be defined as (and the intended >semantics generally is) (3). See my paper in LNCS 287. Could you please give some of these arguments? In your paper in LNCS 287 you say that specification=types+program. In some cases this is true but not generally. merge below is an example of an untyped specification and a typed program. For this case the semantics (2) above is the correct one. The untyped specification of merge: merge(x,y,z)<->(forall e)[{(e in x) or (e in y)}<->(e in z)] One merge program is the program that merges ordered lists. It is a partial program that assumes that its argument are ordered lists. The program is undefined for other types of arguments, but we may later add more clauses, e.g. for merging unordered lists (also called union). ordlist(x)&ordlist(y)&ordlist(z) -> [ merge([],X,X). merge(X,[],X). merge([X|Xs],[Y|Ys],[X|Zs]) :- X<Y, merge(...... ]