Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!tut.cis.ohio-state.edu!cs.utexas.edu!uunet!munnari.oz.au!lee
From: lee@munnari.oz.au (Lee Naish)
Newsgroups: comp.lang.prolog
Subject: Re: Semantics of type checking (was "extralogical")
Keywords: usage
Message-ID: <2497@munnari.oz.au>
Date: 23 Oct 89 06:56:46 GMT
References: <2204@munnari.oz.au> <786@ecrcvax.UUCP> <2390@munnari.oz.au> <1213@kuling.UUCP>
Sender: news@cs.mu.oz.au
Reply-To: lee@munmurra.UUCP (Lee Naish)
Organization: Comp Sci, University of Melbourne
Lines: 50

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