Department of Artificial Intelligence

University of Edinburgh

Title: Draft Proposed Standard for Prolog Evaluable Predicates
Author: R. A. O'Keefe.

Abstract

There are several different implementations of Prolog which resemble Dec-10 Prolog closely enough that it is worth trying to move programs from one version to another. To facilitate this, it is important to have a clear specification of the semantics of the standard predicates (syntax is comparatively unimportant). This paper presents such a specification for term classification, construction, and comparison, for arithmetic, and for control structures. the term classification and construction and the arithmetic evaluable predicates of a Prolog system. The proposed standard extends Dec-10 Prolog in the interests of portability between future systems.

This is a draft, published for comments.

This work was supported by a Commonwealth Scholarship. Computing was done on the Edinburgh ICF KL-10 under SERC grant GR/C/06226.

Draft Proposed Standard for Prolog Evaluable Predicates

Introduction

	atom(A) & name(A, S) & name(X, S) -> X = A

Error Reporting

Simple Failure

Undefined Predicates

	! Undefined predicate: pljs/3
	! pljs(3, 17, _273)

	! <error phrase>: <detail>
	! <the culprit goal>

	current_predicate(Name, Goal)

	:- data F/N.

	declare_data(F, N) :-
		functor(Goal, F, N),
		(   current_predicate(F, Goal)
		;   assert(Goal), retract(Goal)
		), !.

Type Failure

	! Type Error: argument 2 of plus/3 is not an integer:
	! plus(_273, a, _275)

Overflow

	handle overflow in plus(X,Y,Z) where nonvar(X)
	and nonvar(Y) by calling eval(Z is X+Y).

domain errors, such as sqrt(-1). These should be handled in the same way as integer division by 0.

overflows. These should be handled like integer overflows, that is, they must be detected, and must not be continuable.

underflow. It is common practice to replace an underflowed result by 0. There are two problems with this. The first is the fact that the ordered field laws

X > 0 & Y > 0 => X*Y > 0
X < 0 & Y > 0 => X*Y < 0
X*Y = 0 => X = 0 or Y = 0

and so on can be falsified. In a language allegedly based on logic this would be a pity. The second is that underflow represents a complete "loss of precision" and indicates a poor formulation of a calculation problem. As there is a vast literature on numerical analysis, and a good deal is known about coping with the defects of floating point, it would be a great pity if this indication of a badly expressed algorithm were not brought to the programmer's notice.

Instantiation Faults

	gen_nat(N) :-			% gen-erate nat-ural
		nonvar(N),		% if we aren't to generate it
		!,			% demand that it is an integer
		integer(N), N >= 0.	% and non-negative.
	gen_nat(N) :-			% otherwise, generate an
		gen_nat(0, N).		% integer >= 0


	gen_nat(L, L).
	gen_nat(L, N) :-		% generate natural > L
		succ(L, M),		% M = L+1
		gen_nat(M, N).		% generate natural >= M


	gen_int(I) :-			% gen-erate int-eger
		nonvar(I),		% if we aren't to generate it
		!,			% demand that it is an integer.
		integer(I).
	gen_int(0).			% generate 0
	gen_int(I) :-			% generate +/- N for N > 0
		gen_nat(1, N),
		(   I = N
		;   plus(I, N, 0)	% I+N = 0
		).

Unimplemented data types

A Design Principle

	length([], 0).
	length([_|Tail], N) :-
		length(Tail, M),
		succ(M, N).

	length(List, Length) :-
		nonvar(Length),
		!,
		length_gen(Length, List).
	length(List, Length) :-
		length_chk(List, Length).

	length_chk([], 0).
	length_chk([_|Tail], N) :-
		length_chk(Tail, M),
		succ(M, N).

	length_gen(0, []).
	length_gen(N, [_|Tail]) :-
		succ(M, N),
		length_gen(M, Tail).

if there is sufficient information in a question to determine that it has a unique answer, the implementation should yield that answer.

if there is sufficient information in a question to determine that it has NO answer, the implementation should fail.

If neither of these cases holds, but the implementation can tell that there is a finite number of solutions, it may enumerate them. But it need not.

If the implementation cannot tell that there is a finite number of solutions, or if it doesn't check, it should either adopt some other control strategy (such as delaying) or it should report an instantiation fault. It must NOT backtrack over an infinite set of solutions.

Some Naming Conventions

	D_size(D, Size) :-
		bind Size to the number of elements in D, or
		if D is a mapping, to the number of elements in 
		the domain of D.

	D_member(Element, D) :-
		recognise or enumerate elements of the collection.

	D_memberchk(Element, D) :-
		recognise elements of the collection, do not
		enumerate.  May delay if Element is unbound,
		but need not.

	check_D(Pred, D) :-
		check that Pred(X) is true for each element X of D.

	part_D(Pred, D, TrueD, FailD) :-
		distribute the elements of D into two objects
		TrueD/FailD of the same type according as
		Pred(Elem) succeeds/fails.

	map_D(Pred, Input_D, Output_D) :-
		construct a new object of type D,
		where corresponding elements I and O of
		Input_D and Output_D are related by Pred(I,O).

	some_D(Pred, D) :-
		D_member(Element, D),
		Pred(Element),
		!.

	each_D(Pred, D) :-
		forall(D_member(Element,D), Pred(Element)).

	check_list(divisible_by(Y), [72,6,30,1296])

	each_list(divisible_by(Y), [5,3,7])

	for all D_obj there is a unique R_obj such that
	    D_R(D_obj, R_obj)

*	for all R_obj there is a unique D_obj such that
*	    D_R(D_obj, R_obj)

	?- cp "*zeelunk*".

Determining the Type of A Term

			true
			  |
		+---------+---------+
		|		    |
	     nonvar		   var
		|
      +---------+--------------------------+
      |					   |
  compound			     atomic=constant
					   |
		+----------------+---------+---------+
		|		 |		     |
	     number	      string		 atom=symbol
		|
	+-------+-------+
	|		|
    rational	     complex
	|		|
     integer	      float

proper_rational(Q) :-
	rational(Q),
	\+ integer(Q).

proper_complex(F) :-
	complex(F),
	\+ float(F).

Var, nonvar

	...
	\+ number(X),
	...
	number(X)

simple, compound, atomic

compound(Term) -> exists N. exists A. arg(N, Term, A).

simple(Term) :-
	\+ compound(Term).

	atomic(Term) :-
		nonvar(Term),
		\+ compound(Term).

structure(X):-compound(X).

Atoms and Strings

    8-bit ASCII to EBCDIC		    EBCDIC to 8-bit ASCII

00  00   40  7c   80  20   c0  76	00  00   40  20   80  c3   c0  7b
01  01   41  c1   81  21   c1  77	01  01   41  a0   81  61   c1  41
02  02   42  c2   82  22   c2  78	02  02   42  a1   82  62   c2  42
03  03   43  c3   83  23   c3  80	03  03   43  a2   83  63   c3  43
04  37   44  c4   84  24   c4  8a	04  9c   44  a3   84  64   c4  44
05  2d   45  c5   85  15   c5  8b	05  09   45  a4   85  65   c5  45
06  2e   46  c6   86  06   c6  8c	06  86   46  a5   86  66   c6  46
07  2f   47  c7   87  17   c7  8d	07  7f   47  a6   87  67   c7  47
08  16   48  c8   88  28   c8  8e	08  97   48  a7   88  68   c8  48
09  05   49  c9   89  29   c9  8f	09  8d   49  a8   89  69   c9  49
0a  25   4a  d1   8a  2a   ca  90	0a  8e   4a  d5   8a  c4   ca  e8
0b  0b   4b  d2   8b  2b   cb  6a	0b  0b   4b  2e   8b  c5   cb  e9
0c  0c   4c  d3   8c  2c   cc  9b	0c  0c   4c  3c   8c  c6   cc  ea
0d  0d   4d  d4   8d  09   cd  9c	0d  0d   4d  28   8d  c7   cd  eb
0e  0e   4e  d5   8e  0a   ce  9d	0e  0e   4e  2b   8e  c8   ce  ec
0f  0f   4f  d6   8f  1b   cf  9e	0f  0f   4f  7c   8f  c9   cf  ed

    8-bit ASCII to EBCDIC		    EBCDIC to 8-bit ASCII

10  10   50  d7   90  30   d0  9f	10  10   50  26   90  ca   d0  7d
11  11   51  d8   91  31   d1  a0	11  11   51  a9   91  6a   d1  4a
12  12   52  d9   92  1a   d2  aa	12  12   52  aa   92  6b   d2  4b
13  13   53  e2   93  33   d3  ab	13  13   53  ab   93  6c   d3  4c
14  3c   54  e3   94  34   d4  ac	14  9d   54  ac   94  6d   d4  4d
15  3d   55  e4   95  35   d5  4a	15  85   55  ad   95  6e   d5  4e
16  32   56  e5   96  36   d6  ae	16  08   56  ae   96  6f   d6  4f
17  26   57  e6   97  08   d7  af	17  87   57  af   97  70   d7  50
18  18   58  e7   98  38   d8  b0	18  18   58  b0   98  71   d8  51
19  19   59  e8   99  39   d9  b1	19  19   59  b1   99  72   d9  52
1a  3f   5a  e9   9a  3a   da  b2	1a  92   5a  21   9a  5e   da  ee
1b  27   5b  ad   9b  3b   db  b3	1b  8f   5b  24   9b  cc   db  ef
1c  1c   5c  e0   9c  04   dc  b4	1c  1c   5c  2a   9c  cd   dc  f0
1d  1d   5d  bd   9d  14   dd  b5	1d  1d   5d  29   9d  ce   dd  f1
1e  1e   5e  9a   9e  3e   de  b6	1e  1e   5e  3b   9e  cf   de  f2
1f  1f   5f  6d   9f  e1   df  b7	1f  1f   5f  7e   9f  d0   df  f3

    8-bit ASCII to EBCDIC		    EBCDIC to 8-bit ASCII

20  40   60  79   a0  41   e0  b8	20  80   60  2d   a0  d1   e0  5c
21  5a   61  81   a1  42   e1  b9	21  81   61  2f   a1  e5   e1  9f
22  7f   62  82   a2  43   e2  ba	22  82   62  b2   a2  73   e2  53
23  7b   63  83   a3  44   e3  bb	23  83   63  b3   a3  74   e3  54
24  5b   64  84   a4  45   e4  bc	24  84   64  b4   a4  75   e4  55
25  6c   65  85   a5  46   e5  a1	25  0a   65  b5   a5  76   e5  56
26  50   66  86   a6  47   e6  be	26  17   66  b6   a6  77   e6  57
27  7d   67  87   a7  48   e7  bf	27  1b   67  b7   a7  78   e7  58
28  4d   68  88   a8  49   e8  ca	28  88   68  b8   a8  79   e8  59
29  5d   69  89   a9  51   e9  cb	29  89   69  b9   a9  7a   e9  5a
2a  5c   6a  91   aa  52   ea  cc	2a  8a   6a  cb   aa  d2   ea  f4
2b  4e   6b  92   ab  53   eb  cd	2b  8b   6b  2c   ab  d3   eb  f5
2c  6b   6c  93   ac  54   ec  ce	2c  8c   6c  25   ac  d4   ec  f6
2d  60   6d  94   ad  55   ed  cf	2d  05   6d  5f   ad  5b   ed  f7
2e  4b   6e  95   ae  56   ee  da	2e  06   6e  3e   ae  d6   ee  f8
2f  61   6f  96   af  57   ef  db	2f  07   6f  3f   af  d7   ef  f9

    8-bit ASCII to EBCDIC		    EBCDIC to 8-bit ASCII

30  f0   70  97   b0  58   f0  dc	30  90   70  ba   b0  d8   f0  30
31  f1   71  98   b1  59   f1  dd	31  91   71  bb   b1  d9   f1  31
32  f2   72  99   b2  62   f2  de	32  16   72  bc   b2  da   f2  32
33  f3   73  a2   b3  63   f3  df	33  93   73  bd   b3  db   f3  33
34  f4   74  a3   b4  64   f4  ea	34  94   74  be   b4  dc   f4  34
35  f5   75  a4   b5  65   f5  eb	35  95   75  bf   b5  dd   f5  35
36  f6   76  a5   b6  66   f6  ec	36  96   76  c0   b6  de   f6  36
37  f7   77  a6   b7  67   f7  ed	37  04   77  c1   b7  df   f7  37
38  f8   78  a7   b8  68   f8  ee	38  98   78  c2   b8  e0   f8  38
39  f9   79  a8   b9  69   f9  ef	39  99   79  60   b9  e1   f9  39
3a  7a   7a  a9   ba  70   fa  fa	3a  9a   7a  3a   ba  e2   fa  fa
3b  5e   7b  c0   bb  71   fb  fb	3b  9b   7b  23   bb  e3   fb  fb
3c  4c   7c  4f   bc  72   fc  fc	3c  14   7c  40   bc  e4   fc  fc
3d  7e   7d  d0   bd  73   fd  fd	3d  15   7d  27   bd  5d   fd  fd
3e  6e   7e  5f   be  74   fe  fe	3e  9e   7e  3d   be  e6   fe  fe
3f  6f   7f  07   bf  75   ff  ff	3f  1a   7f  22   bf  e7   ff  ff

Numbers

Other types of Terms

	lisp(array(X))

Type Testing with Delays

term_type(Term, Type) :-
	var(Term),
	wait_for_binding_of(Term),
	% or report an instantiation fault
	term_type1(Term, Type).
term_type(Term, Type) :-
	nonvar(Term),
	term_type1(Term, Type).

term_type1(Term, compound) :- compound(Term).
term_type1(Term, atom)     :- atom(Term).
term_type1(Term, string)   :- string(Term).
term_type1(Term, integer)  :- integer(Term).
term_type1(Term, rational) :- rational(Term).
term_type1(Term, float)    :- float(Term).
term_type1(Term, complex)  :- complex(Term).
term_type1(Term, number)   :- number(Term).
term_type1(Term, atomic)   :- atomic(Term).

Getting at the Print Names of Constants

string_chars(String, ListOfChars)
    if string(String) {
	unify ListOfChars with [c1,...,cn] where String has n
	characters and their codes are c1,....,cn.
    }
    if var(String) {
	check that ListOfChars is a valid list of character codes
	if it is too long, report a string overflow fault
	unify String with a new string containing those codes
    }
    if nonvar(String) and \+string(String) {
	type_fail(1, string)
    }

To check that X is a valid list of character codes:
    if var(X), report an instantiation fault.
    if X = [], succeed.
    if X = [H|T] {
	if var(H), report an instantiation fault.
	if \+ integer(H) or H < 0 or H > max_char, type_fail(2,chars).
	check that T is a valid list of character codes.
    }
    otherwise type_fail(2,chars).

atom_string(Atom, String)
    if var(Atom) and var(String) report an instantiation fault.
    if nonvar(Atom) and \+ atom(Atom) type_fail(1,atom).
    if nonvar(String) and \+ string(String) type_fail(2,string).
    if nonvar(Atom) {
	unify String with a new string whose contents are
	the character codes of the name of Atom
    } else {
	unify Atom with the atom whose name is String, creating
	the atom if necessary.
    }

atom_chars(Atom, ListOfChars) :-
	nonvar(Atom),
	atom_string(Atom, String),
	string_chars(String, ListOfChars).
atom_chars(Atom, ListOfChars) :-
	var(Atom),
	string_chars(String, ListOfChars),
	atom_string(Atom, String).

	atom_chars(append, [97,X,X,101|R])

number_string(Number, String)
    if var(Number) and var(String) report an instantiation fault.
    if nonvar(Number) and \+ number(Number) type_fail(1,number).
    if nonvar(String) and \+ string(String) type_fail(2,string).
    if nonvar(String) {
	if String cannot be parsed as a number, simply fail.
	unify Number with the number represented by String
    } else {
	"print" Number and unify String with a new string of the result
    }

number_chars(Number, ListOfChars) :-
	var(Number),
	string_chars(String, ListOfChars),
	number_string(Number, String).
number_chars(Number, ListOfChars) :-
	nonvar(Number),
	number_string(Number, String),
	string_chars(String, ListOfChars).

<number>    ::= <integer>
	     |  <ratio>
	     |  <float>
	     |  <complex>

<integer>   ::= <sign> <digits>

<sign>	    ::= <empty> | -
						       +
<digits>    ::= (0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9)

<ratio>	    ::= <integer> / <digits>

<float>     ::= {as in Common Lisp}

<complex>   ::= <float> I <float>

	?- name(X, "+2"), atom(X).

	?- X is +2.

	p(X) :-
		number_chars(X, L),
		number_chars(L, Y),
		Y = X.

name(Constant, ListOfChars) :-
	string(Constant),
	!,
	string_chars(Constant, ListOfChars).
name(Constant, ListOfChars) :-
	number(Constant),
	!,
	number_chars(Constant, ListOfChars).
name(Constant, ListOfChars) :-
	atom(Constant),
	!,
	atom_chars(Constant, ListOfChars).
name(Constant, ListOfChars) :-
	var(Constant),
	number_chars(Constant, ListOfChars),
	!.
name(Constant, ListOfChars) :-
	var(Constant),
	!,
	atom_chars(Constant, ListOfChars). 
name(Constant, ListOfChars) :-
	type_fail(1, atom-or-number).

	name(X, "(QUOTE (F))")

	nonvar(X), name(X, L), name(Y, L)

*rational(Q, N, D)		% NOT the real definition!
*   if nonvar(Q) and \+rational(Q), type_fail(1, rational).
*   if nonvar(N) and \+integer(N), type_fail(2, integer).
*   if nonvar(D) and \+integer(D), type_fail(3, integer).
*   if nonvar(N) and nonvar(D) {
*	if the implementation cannot handle 1/0,0/0,-1/0 {
*	    if D = 0, zero_divide.
*	}
*	unify Q with the value of N/D
*   } else
*   if nonvar(Q) {
*	let N1,D1 be such that N1/D1 = Q and gcd(N1,D1) = 1.
*	if nonvar(D) {
*	    if D = 0 then {
*		if D1 =/= 0 then fail.
*		unify N with N1.
*	    } else {
*		if gcd(|D|,D1) =/= D1 then fail.
*		unify N with N1*D/D1.
*	    }
*	} else
*	if nonvar(N) then {
*	    if gcd(|N|,|N1|) =/= |N1| then fail.
*	    unify D with D1*N/N1.
*	} else {
*	    unify N with N1, D with D1.
*	}
*   } else {
*	report an instantiation fault.
*   }

complex(C, R, I)
    if nonvar(C) and \+complex(C), type fail(1, complex).
    if nonvar(R) and \+float(R), type fail(2, float).
    if nonvar(I) and \+float(I), type fail(3, float).
    if nonvar(C) {
	unify R with re(C), I with im(C).
    } else
    if nonvar(R) and nonvar(I) {
	unify C with R+i*I.
    } else {
	report an instantiation fault.
    }

	complex(c(R,I), R, I) :-
		float(R), float(I),
		I \== 0.0.
	complex(R, R, 0.0) :-
		float(R).

	rational(1/2, N, D), D = 4

	D = 4, rational(1/2, N, D)

	rational(Q, 2, 4),
	rational(Q, 2, 4)

divide(Q, N, D)
    if nonvar(Q) and \+rational(Q), type_fail(1, rational).
    if nonvar(N) and \+ integer(N), type_fail(2, integer).
    if nonvar(D) and \+ integer(D), type_fail(3, integer).
    if var(N) or var(D), instantiation fault.
    unify Q with N/D.

rational(Q, N, D)
    if nonvar(Q) and \+rational(Q), type_fail(1, rational).
    if nonvar(N) and \+ integer(N), type_fail(2, integer).
    if nonvar(D) and \+ integer(D), type_fail(3, integer).
    if nonvar(Q) {
	let N1,D1 be such that Q=N1/D1, D1 >= 0, gcd(N1,D1) = 1.
	unify N=N1, D=D1.
    } else
    if nonvar(N) and nonvar(D) {
	if D1 < 0 or gcd(N1,D1) =/= 1, simply fail.
	unify Q with N1/D1.
    } else {
	instantiation fault.
    }

	rational(X, X, 1)
	complex(X, X, 0.0)

Constructing Compound Terms

functor(Term, Fsymbol, Arity)
    if nonvar(Fsymbol) and \+atomic(Fsymbol), type_fail(2,atomic).
    if nonvar(Arity) and (\+integer(Arity) or Arity < 0),
	type_fail(3,natural).
    if var(Term) {
	if var(Fsymbol) or var(Arity), instantiation fault.
	if Arity = 0 {
	    unify Term = Fsymbol.
	} else {
	    if Arity > some limit, implementation fault.
	    construct a new term with principal functor
		Fsymbol and arity Arity, all of whose
		arguments are distinct unbound new variables
	    unify Term = this new term
	}
    } else {
	if atomic(Term) {
	    unify Fsymbol = Term, Arity = 0.
	} else {
	    compound(Term) is true.
	    unify Fsymbol = the principal function symbol of Term
	      and Artiy = the arity of Term
	}
    }

The Arity argument of functor/3 and the ArgNo argument of arg/3 MUST NOT be integer expressions. The call MUST type fail if given such erroneous values.

	functor(T, a, 1+1)

	functor(a(1,2), a, X)

	N is Expr,
	functor(Term, F, N)

arg(ArgNo, Term, Argument)
    if var(ArgNo) or var(Term), instantiation fault.
    if \+integer(ArgNo) or ArgNo < 1, type fail 1.
    if constant(Term) and \+ atom(Term), type fail 2.
    if ArgNo > the arity of Term, simply fail.
    unify Argument with the ArgNoth argument of Term.

foo(Old, New, Context) :-
	var(Old),
	!,
	var_foo(Old, New, Context).
foo(Old, New, Context) :-
	nonvar_foo(Old, New, Context).
foo(Old, New, Context) :-
	functor(Old, F, N),
	functor(New, F, N),
	foo(N, Old, New, Context).

foo(0, _, _, _) :- !.
foo(N, Old, New, Context) :-
	succ(M, N),
	arg(N, Old, OldArg),
	foo(OldArg, NewArg, Context),
	arg(N, New, NewArg),
	foo(M, Old, New, Context).

	X =.. [F,A1,...,An],

	X = f(A1,...,An),

same_functor(T1, T2) :-
	same_functor(T1, T2, _, _).

same_functor(T1, T2, N) :-
	same_functor(T1, T2, _, N).

same_functor(T1, T2, F, N) :-
	nonvar(T1),
	functor(T1, F, N),
	functor(T2, F, N).
same_functor(T1, T2, F, N) :-
	var(T1),
	functor(T2, F, N),
	functor(T1, F, N).

foo(Old, New, Context) :-
	var(Old),
	!,
	var_foo(Old, New, Context).
foo(Old, New, Context) :-
	nonvar_foo(Old, New, Context).
foo(Old, New, Context) :-
	same_functor(Old, New, N),
	foo(N, Old, New, Context).

foo(0, _, _, _) :- !.
foo(N, Old, New, Context) :-
	succ(M, N),
	arg(N, Old, OldArg),
	arg(N, New, NewArg),
	foo(OldArg, NewArg, Context),
	foo(M, Old, New, Context).

Term Comparison

variables, in a standard order (roughly, oldest first - the order is NOT related to the names of variables);

integers, from -"infinity" to +"infinity";

atoms, in alphabetical (i.e. ASCII) order;

compound terms, ordered first by arity, then by the principal function system, then by the arguments in left to right order).

	X @< 1

"Major" types should correspond to intervals in the standard order.

	functor(T, F, N), atom(F)

var(X) :-
	X @< _.

variables, in some time-invariant order;

all "other" atomic objects, in some time-invariant implementation-defined order;

integers and floating point numbers, ordered according to numeric value (but see section 7.4 for 2 -vs- 2.0), and complex numbers in lexicographic order;

strings, in lexicographic order;

atoms, in lexicographic order;

compound terms, ordered first by arity, then by function symbol (always an atom), then by arguments from left to right.

compare(R, X, Y)
    If X comes before Y in the standard order, unify R with '<'.
    If X is identical to Y, unify R with '='.
    If X comes after Y in the standard order, unify R with '>'.

X @< Y :-
	compare(<, X, Y).

X @>= Y :-
	\+ compare(<, X, Y).

X == Y :-
	compare(=, X, Y).

X \== Y :-
	\+ compare(=, X, Y).

X @> Y :-
	compare(>, X, Y).

X @=< Y :-
	\+ compare(>, X, Y).

term_compare(R, X, Y) :-
    if X and Y are identical, unify R with '='.
    otherwise, find the first place in a left to right scan
    where they differ.  If either one has a variable in that
    place, wait for that variable to be bound and try again
    if the implementation supports coroutining or report an
    instantiation fault it it doesn't.
    call compare(R, X, Y).

X $< Y :-
	term_compare(<, X, Y).

X $>= Y :-
	term_compare(R, X, Y),
	(R = '=' ; R = '>').

X $> Y :-
	term_compare(>, X, Y).

X $=< Y :-
	term_compare(R, X, Y),
	(R = '=' ; R = '<').

X $= Y
    unify X=Y.  If this fails, fail.
    If no variables were bound, succeed.
    Otherwise, undo the bindings and wait
    until some variable in X or Y is bound.

X $\= Y
    unify X=Y.  If this fails, succeed.
    If no variables were bound, fail.
    Otherwise, undo the bindings and wait
    until some variable in X or Y is bound.

Sorting

keysort(PairList, SortedPairList) sorts a list of Key-Value pairs so that the Keys are in standard order, retains duplicates, and unifies the result with SortedPairList. This is needed for bagof/3 so that solutions with the same bindings for free variables can be grouped together. It is vital that this sort be stable.

sort(Random, Sorted) sorts the elements of the Random list into standard order, eliminates duplicates, and unifies the result with Sorted. This is used by setof/3 to convert a chronologically ordered list to a set representation, and is used by the ordered-set library package to convert lists to sets.

msort(Random, Sorted) sorts a list of terms as sort/2 does, but does not eliminate duplicates. This is useful for putting bags into a standard form.

merge(L1, L2, Merged) combines two ordered lists, retaining duplicates.

List Processing

append([], L, L).
append([H|T], L, [H|R]) :-
	append(T, L, R).

member(X, [X|_]).
member(X, [_|T]) :-
	member(X, T).

memberchk(X, [X|_]) :- !.
memberchk(X, [_|T]) :-
	memberchk(X, T).

append(L, X, Y) has at most one solution, whatever X and Y are, and cannot backtrack at all.

append(X, Y, L) as at most length(L)+1 solutions, whatever X and Y are, and though it can backtrack over these it cannot run away without finding a solution. A Prolog implementation is required to find all the relevant solutions. In this sense append/3 is not primitive, because a primitive would be allowed to delay or instantiation fault.

append(X, L, Y), however, can backtrack indefinitely if X and Y are variables. This may be reported as an instantiation fault.

The empty list may be represented by one of the atoms '[]', '()', 'nil', or 'NIL', the choice made once and for all by the implementor. It may not be represented by any other atom. The parser must turn the empty list [ ] into this atom.

Operations on Strings

string_size(StringOrAtom, Size)
    if nonvar(Size) and (\+integer(Size) or Size < 0),
	type_fail(2, natural).
    if atom(StringOrAtom) {
	atom_chars(StringOrAtom, L), length(L, Size)
    } else
    if string(StringOrAtom) {
	string_chars(StringOrAtom, L), length(L, Size)
    } else
    if var(StringOrAtom) instantiation_fault 
    else type_fail(1, string-or-atom).

string_char(CharNo, StringOrAtom, CharCode)
    if nonvar(CharNo) and (\+ integer(CharNo) or CharNo < 1),
	type_fail(1, natural).
    if nonvar(CharCode) and (\+ integer(CharCode) or CharCode < 0),
	type_fail(3, natural).
    if nonvar(StringOrAtom) and \+string(StringOrAtom)
	and \+atom(StringOrAtom), type_fail(2, string-or-atom).
    if var(CharNo) or var(StringOrAtom), instantiation_fault.
    succ(K, CharNo), length(P, K),
    if atom(StringOrAtom) {
	atom_chars(StringOrAtom, L),
	append(P, [CharCode|_], L)
    } else {
	string_chars(StringOrAtom, L),
	append(P, [CharCode|_], L)
    }

substring(StringOrAtom, Offset, Length, SubString)
    StringOrAtom must be a string or Atom
    Offset must be an integer >= 0
    Length must be an integer >= 0
    if bound, SubString must be a string or atom.
    atom(StringOrAtom) -> atom_chars(StringOrAtom, L)
    ;   string_chars(StringOrAtom, L).
    length(Drop, Offset), length(Keep, Length),
    append(Drop, X, L), append(Keep, _, X),
    atom(StringOrAtom) -> atom_chars(SubString, Keep)
    ;   string_chars(SubString, Keep).

concat(A, B, C) <->
	A is a string or atom, B is a string, atom or number,
	C is the same sort of constant as A, and the
	corresponding lists of characters satisfy append(La,Lb,Lc).

concat(A, B, C)
    if nonvar(A) and \+(string(A) or atom(A)),
	type_fail(1, string-or-atom).
    if nonvar(C) and \+(string(C) or atom(C)),
	type_fail(3, string-or-atom).
    if var(B), instantiation_fault.
    if \+(string(B) or atom(B) or number(B)),
	type_fail(2, constant).
    string(B) -> string_chars(B, Lb) ; name(B, Lb).
    if nonvar(A) {
	string(A) -> string_chars(A, La) ; atom_chars(A, La).
	append(La, Lb, Lc).
	string(A) -> string_chars(C, Lc) ; atom_chars(C, Lc).
    } else
    if nonvar(C) {
	string(C) -> string_chars(C, Lc) ; atom_chars(C, Lc).
	append(La, Lb, Lc).
	string(C) -> string_chars(A, La) ; atom_chars(A, La).
    } else {
	instantiation_fault.
    }

part_string(StringOrAtom, Neck, Before, After) :-
	string_size(StringOrAtom, Size),
	Keep is Size-Neck,
	substring(StringOrAtom, 0, Neck, Before),
	substring(StringOrAtom, Neck, Keep, After).

Simple Integer Arithmetic

They work on integers, not on expressions.

They are invertible (that is succ(M,N) will solve for N given M or for M given N) and so follow the "design principle" in a way that "N is M+1" does not.

They can be compiled into efficient code with little effort. For example, a compiler noticing that Sum is unbound in the goal plus(X,Y,Sum) can generate the equivalent of "Sum is X+Y" but without the necessity of invoking a tree walker to evaluate X and Y. Further, as the arguments can only be constants or variables (the compiler, detecting anything else, can replace such a goal by code to report a type failure) there is no need to build compound terms at run time or put these variables in the global stack.

They do not seduce beginners into writing "Sum = X+Y", which is a particularly nasty bug, as if Sum later on appears in an arithmetic relation or an 'is' it will appear to have the right value.

A clause containing at most one of the comparison predicates and at most one of the computation predicates is generally clearer than a clause containing "is". This is of course a matter of personal taste.

Comparison

lt(X, Y) <->
	integer(X) & integer(Y) & "X is less than Y".

if nonvar(X) and not integer(X) then type fail.
if nonvar(Y) and not integer(Y) then type fail.
if var(X) then instantiation fault.
if var(Y) then instantiation fault.
if X @< Y then succeed else fail.

le(X, Y) <->
	integer(X) & integer(Y) & "X is less than or equal to Y".

if nonvar(X) and not integer(X) then type fail.
if nonvar(Y) and not integer(Y) then type fail.
if var(X) then instantiation fault.
if var(Y) then instantiation fault.
if Y @< X then fail else succeed.

lt(X, Y) works only for integers, fails for non integers, and reports an instantiation fault if either argument is a variable and the other is a variable or integer.

X @< Y compares arbitrary terms, and defines an order on variables even. It generalises micro-PROLOG's "LESS" predicate, and is indispensable for the implementation of setof/3, bagof/3, and efficient implementation of sets and finite maps. The fact that "1 @< b" is useful, but when you intend to compare integers only it is even more useful to say so.

X < Y compares arbitrary ground arithmetic expressions, by evaluating both and then calling @< on the results. A Prolog definition for it is given in the second appendix.

	le(X, Y) <-> \+ lt(X, Y)

	gt(X, Y) :-
		lt(Y, X).

	ge(X, Y) :-
		le(X, Y).

if X and Y are both integers, the goal should be replaced by "true" or "fail" as appropriate. This case is most likely to arise in automatically generated code such as that produced by the unfolder.

if X or Y is a non-variable non-integer, the call should be replaced by a type_fail call.

if X or Y is a variable which must be uninstantiated at this point, the call should be replaced by an instantiation_fault call.

otherwise the compiler can generate the obvious machine code. There should be an implementation subroutine with a fast calling method that dereferences a variable and checks that the result is an integer; all the arithmetic code can use it.

Enumeration

between(Lower, Upper, X) <->
	integer(Lower) & integer(Upper) & integer(X) &
	Lower =< X =< Upper.

    if nonvar(Lower) and \+integer(Lower), type_fail(1,integer).
    if nonvar(Upper) and \+integer(Upper), type_fail(2,integer).
    if nonvar(X)     and \+integer(X),     type_fail(3,integer).
    if nonvar(Lower) and nonvar(Upper) then
	if Lower > Upper then fail else
	if var(X) then {
	    try binding X to each of the integers Lower..Upper
	    in turn, but the search order is not specified
	} else {
	    if Lower =< X =< Upper then succeed else fail
    } else
    if nonvar(X) then {
	if nonvar(Lower) and Lower > X then fail else
	if nonvar(Upper) and Upper < X then fail else
	instantiation fault
    } else {
	instantiation fault.
    }

range(Lower, X, Upper) :-
	between(Lower, Upper, X).

	foo(X, Lower, Upper)
	foo(Lower, X, Upper)
	foo(Lower, Upper, X)

if there is enough information at compile time to determine the result, generate a "true", "fail", "type fail", or "instantiation fault" call as appropriate.

if X is known to be uninstantiated (perhaps this is the first mention of it in the clause), call directly to the enumeration case (which has to check that Lower and Upper are integers in the right order).

it can happen that X is known to be instantiated. If it is mentioned in integer(X) or any other arithmetic relation upstream of this point, it must be instantiated to an integer, and comparison code can be generated as for the two le-s.

	case_shift(Ucase, Lcase) :-
		plus(Ucase, 32, Lcase),
		between(0'A, 0'Z, Ucase).

	case_shift(Ucase, Lcase) :-
		between(0'A, 0'Z, Ucase),
		plus(Ucase, 32, Lcase).

Addition and Subtraction

succ(P, S) <-> integer(P) & integer(S) & S = P+1 & P >= 0.

    if nonvar(P) and not integer(P) then type fail.
    if nonvar(S) and not integer(S) then type fail.
    if integer(P) then {
	if P >= 0 and S unifies with P+1 then succeed else fail
    } else
    if integer(S) then {
       if S > 0 then unify P with S-1 and succeed else fail
    } else
	instantiation fault.


plus(A, B, Sum) <->
	integer(A) & integer(B) & integer(Sum) & A+B = Sum.

    if nonvar(A) and not integer(A) then type fail.
    if nonvar(B) and not integer(B) then type fail.
    if nonvar(Sum) and not integer(Sum) then type fail.
    if var(A) then {
	if var(B) or var(Sum) then instantiation fault.
	unify A with Sum-B and succeed.
    } else
    if var(B) then {
	if var(Sum) then instantiation fault.
	unify B with Sum-A and succeed.
    } else {
	if Sum unifies with A+B then succeed else fail.
    }

	p(0, , ) :- !,
		<base case>.
	p(N, , ) :-
		<step case>(, ),
		M is N-1,
		p(M, , ).

	p(0, , ) :-
		<base case>.
	p(N, , ) :-
		succ(M, N),	% N is a successor natural
		<step case>(, ),
		p(M, , ).

	p(0, ...) :- ...
	p(s(M), ...) :- ...

Multiplication

times(A, B, P) <-> integer(A) & integer(B) & integer(P) & A*B=P.

    if nonvar(A) & not integer(A) then type fail.
    if nonvar(B) & not integer(B) then type fail.
    if nonvar(P) & not integer(P) then type fail.
    if nonvar(A) & nonvar(B) then
	if P unifies with A*B then succeed else fail
    if nonvar(A) & nonvar(P) then % B is var
	if A = 0 then if P = 0 then instantiation fault else fail
	else if A divides P then unify B with P/A and succeed else fail
    if nonvar(B) & nonvar(P) then % A is var
	if B = 0 then if P = 0 then instantiation fault else fail
	else if B divides P then unify A with P/B and succeed else fail
    else instantiation fault

	maplist(times(7), SingleFold, SevenFold)

	if var(X) then instantiation fault else
	if not integer(X) then type fail else
	if X is divisible by 7 then succeed else fail

	maplist(times(_), BaseList, Multiples)

	D is (sqrt(B^2 - 4*A*C) - B)/(2*A)

Division

	X div Y = sign(X/Y)*floor(abs(X/Y))
	X mod Y = X - (X div Y)*Y

divide(A, B, Q, R) <->
	integer(A) & integer(B) & integer(Q) & integer(R) &
	Q = A div B & R = A mod B

	Q is X/Y, R is X mod Y,

	divide(X, Y, _, Rem)

Optimisation

	p(A, B, C, Z) :-	% Z is (A-C)*(A-B)
		plus(A, X, B),
		plus(A, Y, C),
		times(X, Y, Z).

Delaying and Presburger Arithmetic

?- ge(X, 0),		 	% X:int >= 0
   ge(Y, 0),			% Y:int >= 0
   plus(X, Y, T1), lt(T1, 4),	% X+Y < 4
   times(2,X, T2), gt(T2, Y),	% 2X > Y
   times(2,Y, T3), le(T3, X)..	% 2Y =< X

The 'is' family.

V is E	evaluates E

X =:= Y	evaluates X and Y
X =\= Y	evaluates X and Y
X =< Y	evaluates X and Y
X >= Y	evaluates X and Y
X < Y	evaluates X and Y
X > Y	evaluates X and Y

put(C)	evaluates C
ttyput(C)	evaluates C

skip(C)	evaluates C
ttyskip(C)	evaluates C

tab(N)	evaluates N
ttytab(N)	evaluates N

I/O

put(C):
	if C is a variable, instantiation fault.
	if C is an integer in the range 0..127
	    append the character C to the current output stream
	otherwise
	    the implementation MAY type fail
	    the implementation MAY evaluate C/\127 as an arithmetic
		expression and append the result to the current
		output stream
	    the implementation may NOT do anything else

ttyput(C):
		as put(C), but reading "standard output stream"
		for "current output stream" throughout.

skip(C):
	if C is a variable, instantiation fault.
	if C is an integer in the range 0..127
	    repeat D := next character from current input stream
	    until D = 26 or D = C
	    if D =/= C then fail
	otherwise
	    the implementation MAY type fail
	    the implementation MAY evaluate C/\127 as an
	    arithmetic expression and call skip() on the result
	    the implementation may NOT do anything else

ttyskip(C):
	as skip(C) reading "standard input stream" for
	"current input stream" throughout.

tab(N):
	if N is a variable, instantiation fault
	if N is an integer then
	    if N < 0 the implementation MAY type fail
	    write max(N,0) spaces to the current output stream
	otherwise
	    the implementation MAY type fail
	    the implementation MAY evaluate N\/0 as an arithmetic
	    expression and call tab() on the result.

ttytab(N):
	as tab(N) but reading "standard output stream" for
	"current output stream".

Arithmetic Expressions

+ /1	complex conjugate (as in APL)

+ /2	addition (same as PLUS in Common Lisp)

- /1	negation (same as MINUS in Common Lisp)

- /2	subtraction (same as DIFFERENCE in Common Lisp)

* /2	multiplication (same as TIMES in Common Lisp)

/ /2	This one is a problem.  See the discussion in the text.

^ /2	exponentiation (same as in Common Lisp)

div /2	divide(X,Y,Q,R) -> Q is X div Y

mod /2	divide(X,Y,Q,R) -> R is X mod Y

num /1	rational(Q,N,D) -> N is num(Q)

den /1	rational(Q,N,D) -> D is den(Q)

re /1	complex(C,R,I) -> R is re(C)

im /1	complex(C,R,I) -> I is im(C)

i /2	complex(C,R,I) -> C is R i I

/\ /2	bitwise conjunction

\/ /2	bitwise disjunction

\ /1	bitwise complement

<< /2	left shift

> /2	right shift

The Evaluation of Lists

it is strongly recommended that new Prolog implementations should evaluate [X] as they evaluate X.

Division and Floating Point

	X == Y	->  X = Y

be consistent by forcing floating point results into an integer representation whenever possible. This requires a check in name/2 and is/2 and nowhere else (if there is a routine for constructing "boxed" floats, that is the place to put the check).

be consistent by converting floating point results whenever an integer is wanted. This requires checks all over the place, and is likely to have a substantial performance cost.

be consistent by ruling that 2.0 < 2 but there is no number lying between them

be inconsistent; have 2 == 2.0 but 2 \= 2.0 and not(integer(2.0))

	X < N iff X-epsilon < N
	X > N iff X-epsilon > N (since X \= N)
	X > N iff X-epsilon > N
	X < N iff X-epsilon < N (since X \= N)

no floating point value ever unifies with, compares equal to as a term, or is regarded as having the same numerical value as an integer

	float(N) < N and float(N+1) > N+1

	statistics(Key, ValueOrList)

X /\ Y does a bitwise and on X and Y.
X \/ Y does a bitwise or on X and Y.
\Y does a bitwise complement.
X << N shifts X left N bits (right if N < 0).
X >> N shifts X right N bits (left if N < 0).

X =:= Y :- foo(X, Y, =).
X =\= Y :- baz(X, Y, =).

X < Y   :- foo(X, Y, <).
X >= Y  :- baz(X, Y, <).

X > Y   :- foo(X, Y, >).
X =< Y  :- baz(X, Y, >).

foo(X, Y, R) :-
	A is X,
	B is Y,
	compare(R, X, Y).

baz(X, Y, R) :-
	A is X,
	B is Y,
	\+ compare(R, X, Y).

  lt(X, Y)	X and Y must both be integers
  X @< Y        X and Y may be any terms, but the number order is right
  X < Y		X and Y are arithmetic expressions

if X R Y then	(X R Y) evaluates to X.
otherwise the predicate evaluating X R Y fails.

	X := 1;
	X := 2

	X is 1,
	X is 2

	1 := 1

	1 is 1

haulong(N, B) :-
	N1 is local, B1 is local,
	N1 := N, B1 := 0,
	while N1 > 0 do (N1 := N1/2, B1 +:= 1),
	B is B1.

	atom := Expr

	T is Expr, lisp(set(atom,Expr))	

	p(Y, Z) :-
		Y > 1,
		Z is (Y+1)/(Y-1).

	assert((p(X) :- true,(p(X+1),(Y=1,Y=2))))

	p(X) :- p(X+1), fail.

	p(X) :- true, fail.
	p(X) :- fail.
	p(X) :- Y=1, p(X+Y), Y=2.
	p(X) :- p(X+Y), (Y=1,Y=2).
	p(X) :- call(p(X+1)), fail.

	end_of_line(C) :- C is 0'J-64.
to
	end_of_line(C) :- C = 10.

	end_of_line(10).

	expand_assert(Formula) :-
		expand_term(Formula, Clause),
		assert(Clause).

	true.

	fail :- integer(fred).

	repeat.
	repeat :-
		repeat.

	repeat(N) :-
		ge(N, 1).
	repeat(N) :-
		gt(N, 1),
		succ(M, N),
		repeat(M).

	repeat(Goal) :-
		( call(Goal), fail
		; true
		).

call(X) :-
	X.

call(X) :-		% non-example
	X.		% non-example

call(p(1,X,Y)) :-	% example
	p(1, X, Y).	% example

call((p, !, q; r)) :-	% example
	p, !, q; r.	% example

	?- assert(( z(X) :- repeat, X )),
	   clause(z(X), Body),
	   X = !.

	?- X = !,
	   assert(( z(X) :- repeat, X )),
	   clause(z(X), Body).

apply(Pred, ArgList) :-
	Pred =.. [F|GivenArgs],
	append(GivenArgs, ArgList, AllArgs),
	Goal =.. [F|AllArgs],
	call(Goal).

call(p(X1,...,Xm), Y1,...,Yn) :-
	p(X1,...,Xm,Y1,...,Yn).

	once(Body) :-
		call(Body),
		!.

	( Body -> fail ; true )

	p :- \+ !.
	p.

	p :- ( ! -> fail ; true ).
	p.

	p :- X = !, \+ X.
	p.

	p :- X = !, ( call(X) -> fail ; true ).
	p.

disjoint(S1, S2) :-
	not (member(X, S1), memberchk(X, S2)).

non_member(X, S) :-
	not(member(X, S)).

	\+ (Gen, \+ Test)

	( Gen, ( Test -> fail ; true) -> fail ; true )

	subset(Small, Big) :-
		forall(member(X, Small), memberchk(X, Big)).

prolog_clause(Clause, Head, Body)

prolog_bounded_quantification(Formula, Generator, Test)

prolog_negation(Formula, PositivePart)

prolog_if_branch(Formula, Hypothesis, Conclusion)

prolog_conjunction(Formula, ListOfConjuncts)

prolog_disjunction(Formula, ListOfDisjuncts)

for given L0
if	prolog_conjunction(F1, L0) succeeds
then	prolog_conjunction(F1, L1) succeeds
and	prolog_conjunction(F2, L1) succeeds
and	F2 == F1.

for given F0
if	prolog_conjunction(F0, L1) succeeds
and	prolog_conjunction(F1, L1) succeeds
then	prolog_conjunction(F1, L2) succeeds
and	L2 == L1.

	prolog_conjunction((1,2), [1,2])	succeeds
but	prolog_conjunction(X, [1,2])		fails.

	cases
	    Hypothesis1 -> Conclusion1
	;   Hypothesis2 -> Conclusion2
	...
	;   Hypothesisn -> Conclusionn

	DoneIt is local,
	Doneit := 0,
	(   Hypothesis1, DoneIt := 1, Conclusion1
	;   DoneIt =:= 0, Hypothesis2, DoneIt := 1, Conclusion2
	...
	;   DoneIt =:= 0, Hypothesisn, Conclusionn
	)

	(   H1 and C1
	or  not H1 and H2 and C2
	...
	or  not H1 and not H2 and... and not Hn-1 and Hn and Cn
	)

	p(...) :-
		...
		( ... -> ! ; true ),
		... .

	(   H1 -> C1
	    H2 -> C2
	...
	;   Else
	)

	(cases
	    once(H1) -> C1
	;   once(H2) -> C2
	...
	;   true -> Else
	)

current_atom(Atom)
    if var(Atom) {
	try binding Atom to each "currently known" atom in turn;
	the order is not specified
    } else {
	if atom(Atom) then succeed else type_fail(1, atom).
    }

	?- current_atom(X), X = fred.

current_functor(Atom, Term)
    if nonvar(Atom) and \+atom(Atom), type_fail(1, atom).
    if constant(Term) and \+atom(Term), type_fail(2, compound).
    if nonvar(Term) {
	unify Atom with the principal function symbol of Term
    } else {
	current_atom(Atom)
	try functor(Term, Atom, N) for each N such that Atom/N
	is a "currently known" functor; the order is not defined
    }

current_predicate(Atom, Goal) :-
	current_functor(Atom, Goal),
	"there have been clauses for Goal".

current_predicate(Goal) :-
	current_predicate(_, Goal).

current_predicate(Atom, Goal) :-
	current_functor(Atom, Goal),
	\+ \+ clause(Goal, _).

system(Atom, Goal) :-
	current_functor(Atom, Goal),
	"Goal has compiled code and compiled code only".

system(Goal) :-
	system(_, Goal).

safe_clause(Head, Body) :-
	current_predicate(Head),
	clause(Head, Body).

	with_input_from_file(FileName, Body)
	with_input_from_chars(ListOfChars, Body)
	with_input_from_string(String, Body)
	with_input_from_call(Pred, Body)

	with_output_to_file(FileName, Body)
	with_output_to_chars(ListOfChars, Body)
	with_output_to_string(String, Body)
	with_output_to_call(Pred, Body)

	with_io_to_terminal(Body)

@Include(Util:Arith.Pl)

Term =.. [FunctionSymbol|Args] :-
	nonvar(Term),
	!,
	functor(Term, FunctionSymbol, Arity),
	$argument_list(0, Arity, Term, Args).
Term =.. [Term] :-
	atomic(Term),
	!.
Term =.. [FunctionSymbol|Args] :-
	atom(FunctionSymbol),
	length(Args, Arity),
	functor(Term, FunctionSymbol, Arity),
	$argument_list(0, Arity, Term, Args).


$argument_list(N, N, _, []) :- !.
$argument_list(I, N, Term, [Arg|Args]) :-
	J is I+1,
	arg(J, Term, Arg),
	$argument_list(J, N, Term, Args).

repeat(N) :-
	telling(Old), tell(user),
	write('It is pointlessly stupid to use repeat/1.'), nl,
	write('Why don''t you use between/3 instead, fathead?'), nl,
	tell(Old),
	between(1, N, _).

@Include(Util:Sorts.Pl)

@Include(Util:DeCons.Pl)