Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!uunet!mcsun!sunic!bmc!kuling!mattias
From: mattias@emil.CSD.UU.Se (Mattias Waldau)
Newsgroups: comp.lang.prolog
Subject: Re: Semantics of type checking (was "extralogical")
Message-ID: <1218@kuling.UUCP>
Date: 25 Oct 89 19:48:42 GMT
References: <2204@munnari.oz.au> <786@ecrcvax.UUCP> <2390@munnari.oz.au> <1213@kuling.UUCP> <2497@munnari.oz.au>
Sender: news@kuling.UUCP
Reply-To: mattias@emil.CSD.UU.Se (Mattias Waldau)
Organization: Computing Science Department, Uppsala Univ, Sweden
Lines: 44
In-reply-to: lee@munnari.oz.au (Lee Naish)
Posting-Front-End: Gnews 2.0

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(......
]