Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!allegra!princeton!caip!lll-crg!seismo!munnari!moncskermit!basser!elecvax!cheops!alan
From: alan@cheops.OZ (Alan Tonisson)
Newsgroups: net.lang.prolog
Subject: Re: Standard behavior?
Message-ID: <498@cheops.OZ>
Date: Thu, 19-Jun-86 04:24:02 EDT
Article-I.D.: cheops.498
Posted: Thu Jun 19 04:24:02 1986
Date-Received: Wed, 25-Jun-86 04:57:17 EDT
References: <6500005@uicsl> <29700028@uiucdcs> <768@aimmi.UUCP>
Organization: Computer Science, Uni of NSW, Aust.
Lines: 35

> In article <29700028@uiucdcs> reddy@uiucdcs.UUCP writes:
> >
> >To rggoebel@watdragon:
> >
> >You can try explaining cut, var and nonvar logically.  If you do it
> >successfully, you could become a star of the logic programming community.
> 
> In all humility, and with a strong chance of getting it all wrong here I
> go:
> 
> var(X) = All t in Term: can_unify(t,X)
> 
> where can_unify is true if a most general unifier can be found for both
> its arguments.
> 
> nonvar(X) = Exists t in Term: NOT(can_unify(t,X))
> 
> Dirty structures like lists with uninstantiated tails (as in the unit
> time queue trick) are nonvar under these definitions.
> 
> I've had minimal training in Logic, so I don't know if the set of all
> Terms is an ok construct. Seems ok to me. 
> 
> This leaves cut, which is definitely meta-logical.

	It is not possible to talk about the SET of all terms within
first order predicate calculus, but it is possible to state that some
property holds for all things (i.e. it is true of all terms) e.g.
forall X: p(X) says that p holds for all things and hence p(t) is
true for any term t.
	The real problem with the above definitions is that one cannot
define can_unify within first order predicate calculus. can_unify is
just as nasty a beast as var and nonvar are.

						Alan Tonisson.