🚀 go-pugleaf

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.