Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!uwm.edu!gem.mps.ohio-state.edu!tut.cis.ohio-state.edu!snorkelwacker!bloom-beacon!eru!luth!sunic!bmc!kuling!mattias
From: mattias@emil.CSD.UU.Se (Mattias Waldau)
Newsgroups: comp.lang.prolog
Subject: Semantics of type checking (was "extralogical")
Keywords: usage
Message-ID: <1213@kuling.UUCP>
Date: 20 Oct 89 13:20:33 GMT
References: <2204@munnari.oz.au> <786@ecrcvax.UUCP> <2390@munnari.oz.au>
Sender: news@kuling.UUCP
Reply-To: mattias@emil.CSD.UU.Se (Mattias Waldau)
Organization: Uppsala University, dept. of Computer Science
Lines: 40
In-reply-to: ok@cs.mu.oz.au (Richard O'Keefe)
Posting-Front-End: Gnews 2.0

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.