Path: utzoo!utgpu!watserv1!watmath!att!att!dptg!ulysses!andante!alice!pereira
From: pereira@alice.att.com (Fernando Pereira)
Newsgroups: comp.lang.prolog
Subject: Re: Standards question: behavior of arg/3
Keywords: ANSI, standard
Message-ID: <11528@alice.att.com>
Date: 23 Oct 90 15:42:47 GMT
References: <9888@bunny.GTE.COM> <3992@goanna.cs.rmit.oz.au> <1753@ecrc.de>
Reply-To: pereira@alice.UUCP ()
Organization: AT&T, Bell Labs
Lines: 57

In article <1753@ecrc.de> micha@ecrc.de (Micha Meier) writes:
>[...]
>At ECRC, we were faced with the same problems when designing Sepia. Our solution
>was in a way 'maximal', as opposed to the 'minimal' one of C-Prolog.
>Sepia raises an event each time the predicate is not sufficiently
>instantiated, an argument has a wrong type (where the type does not depend
>on the value of other arguments, so functor(1.2, A, 1) fails)
>or when the arguments that have to be the input ones
>are not in the required domain.

The deeper issue that is lurking here is that of types in logic programs.
Straight FOL has nothing to say about types. In programming based on
the lambda calculus, two main typing paradigms have been used:

	1. The underlying semantics is untyped, and type judgments are
	compile-time provable constraints on the domains and ranges of
	functions (for example, the identity function \x.x maps any
	set of values to itself, therefore it has type /\A.A->A). This
	is the approach used by Milner for the ML type system

	2. The underlying semantics is typed, and type judgments are
	well-formedness judgments on expressions given the meanings
	of the constants in them. This is the usual view of typed
	lambda calculi in logic.

Following the first view, the typing + : int * int -> int just states that
when given two ints + delivers an int. To account for typing failures one
needs to add to this that + will produce a special distinguished "bad"
valund 'wrong' when given anything else. Then typing failure corresponds to
not being able to show that an expression never yields 'wrong'. We could
adopt a version of this for Prolog. Any builtin would be seen as a
convenient proxy for some relation, *except* that Prolog does not know
how to compute the relation for arguments outside the intended domain.
That is, it is not that

	(foo, bar(a), a)

is not in the relation arg/3, but rather that Prolog has no way of knowing
whether it should be or not, and thus it issues a domain fault. This
is analogous to the instantiation fault on

	?- arg(X, foo(a), Y)

where Prolog (assuming no delaying) has no way of determining the
truth value of the query. Thus, my addition to Richard's design principles
is:

	Each builtin comes with an intended domain of applicability.
	Prolog has no way of knowing whether the builtin holds of
	argument values outside that domain, and will therefore
	issue a domain fault.

Fernando Pereira
2D-447, AT&T Bell Laboratories
600 Mountain Ave, Murray Hill, NJ 07974
pereira@research.att.com