ISO/IEC JTC1 SC22 WG17 post-N235
A Prologue for Prolog (working draft)

Ulrich Neumerkel, 2012-09-06

Motivation

Many commonly used predicates are not part of the Prolog standard core. Current Prolog processors differ in the way how they provide these predicates. They may reside in a library, or are imported from a module, or may be built-in predicates and therefore implementation specific extensions due to 5.5.9. In the past, discussions on this level have prevented defining these predicates.

The aim of the Prolog prologue is to avoid discussing such details and concentrate on the identification and precise definition of these commonly used predicates instead. The Prolog prologue is a possibly empty file to be included (7.4.2.7). After inclusion, the following predicates are defined. A processor may provide also some other means to include the prologue. For example, via a command line switch.

History

2011-07-10: WG17 resolution.
2012-07-06: First announcement on PROLOG-STANDARD

Status quo

The following is defined by IS 13211-1:1995 and IS 13211-2:2000. Changes by Cor.2:2012 link to the draft (but not to the actual ISO/IEC document, you have to download it), additions are bold green links
Part 1: General core
7.4.2 Directives
1 dynamic/1. 2 multifile/1. 3 discontiguous/1. 4 op/3. 5 char_conversion/2. 6 initialization/1. 7 include/1. 8 ensure_loaded/1. 9 set_prolog_flag/2.
7.8 Control constructs
1 true/0. 2 fail/0. 3 call/1. 4 !/0. 5 (',')/2. 6 (;)/2 – disjunction. 7 (->)/2. 8 (;)/2 – if-then-else. 9 catch/3. 10 throw/1.
7.10.2.13 Stream properties
file_name/1. mode/1. input/0. output/0. alias/1. position/1. end_of_stream/1. eof_action/1. reposition/1. type/1.
7.10.3 Read-options list
variables/1. variable_names/1. singletons/1.
7.10.4 Write-options list
quoted/1. ignore_ops/1. numbervars/1.
7.11.1 Flags defining integer type I
1 bounded. 2 max_integer. 3 min_integer. 4 integer_rounding_function.
7.11.2 Other flags
1 char_conversion. 2 debug. 3 maxarity. 4 unknown. 5 double_quotes.
7.12.2 Error classification
a) instantiation_error. b) type_error. c) domain_error. d) existence_error. e) permission_error. f) representation_error. g) evaluation_error. h) resource_error. i) syntax_error. j) system_error. k) uninstantiation_error.
8.2 Term unification
1 (=)/2. 2 unify_with_occurs_check/2. 3 (\=)/2. 4 subsumes_term/2.
8.3 Type testing
1 var/1. 2 atom/1. 3 integer/1. 4 float/1. 5 atomic/1. 6 compound/1. 7 nonvar/1. 8 number/1. 9 callable/1. 10 ground/1. 11 acyclic_term/1.
8.4 Term comparison
1 (@=<)/2, (==)/2, (\==)/2, (@<)/2, (@>)/2, (@>=)/2. 2 compare/3. 3 sort/2. 4 keysort/2.
8.5 Term creation and decomposition
1 functor/3. 2 arg/3. 3 (=..)/2. 4 copy_term/2 5 term_variables/2.
8.6 Arithmetic evaluation
1 (is)/2.
8.7 Arithmetic comparison
1 (=:=)/2, (=\=)/2, (<)/2, (=<)/2, (>)/2, (>=)/2.
8.8 Clause retrieval and information
1 clause/2. 2 current_predicate/1.
8.9 Clause creation and destruction
1 asserta/1. 2 assertz/1. 3 retract/1. 4 abolish/1. 5 retractall/1.
8.10 All solutions
1 findall/3. 2 bagof/3. 3 setof/3.
8.11 Stream selection and control
1 current_input/1. 2 current_output/1. 3 set_input/1. 4 set_output/1. 5 open/4, open/3. 6 close/2, close/1. 7 flush_output/1, flush_output/0. 8 stream_property/2, at_end_of_stream/0, at_end_of_stream/1. 9 set_stream_position/2.
8.12 Character input/output
1 get_char/2, get_char/1, get_code/1, get_code/2. 2 peek_char/2, peek_char/1, peek_code/1, peek_code/2. 3 put_char/2, put_char/1, put_code/1, put_code/2, nl/0, nl/1.
8.13 Byte input/output
1 get_byte/2, get_byte/1. 2 peek_byte/2, peek_byte/1. 3 put_byte/2, put_byte/1.
8.14 Term input/output
1 read_term/3, read_term/2, read/1, read/2. 2 write_term/3, write_term/2, write/1, write/2, writeq/1, writeq/2, write_canonical/1, write_canonical/2. 3 op/3. 4 current_op/3. 5 char_conversion/2. 6 current_char_conversion/2.
8.15 Logic and control
1 (\+)/1. 2 once/1. 3 repeat/0. 4 call/2..8. 5 false/0.
8.16 Atomic term processing
1 atom_length/2. 2 atom_concat/3. 3 sub_atom/5. 4 atom_chars/2. 5 atom_codes/2. 6 char_code/2. 7 number_chars/2. 8 number_codes/2.
8.17 Implementation defined hooks
1 set_prolog_flag/2. 2 current_prolog_flag/2. 3 halt/0. 4 halt/1.
9.1 The simple arithmetic functors
(+)/2, (-)/2, (*)/2, (//)/2, (/)/2, (rem)/2, (mod)/2, (-)/1, abs/1, sign/1, float_integer_part/1, float_fractional_part/1, float/1, floor/1, truncate/1, round/1, ceiling/1, (+)/1, (div)/2.
9.3 Other arithmetic functors
1 (**)/2. 2 sin/1. 3 cos/1. 4 atan/1. 5 exp/1. 6 log/1. 7 sqrt/1. 8 max/2. 9 min/2. 10 (^)/2. 11 asin/1. 12 acos/1. 13 atan2/2. 14 tan/1. 15 pi/0.
9.4 Bitwise functors
1 (>>)/2. 2 (<<)/2. 3 (/\)/2. 4 (\/)/2. 5 (\)/1. 6 xor/2.
Part 2: Modules
7.2 Module predicates
1 current_module/1. 2 predicate_property/2.
7.3 Clause retrieval and information
2 current_predicate/1.

Proposed for Prolog prologue

The format and notation of the definition of each predicate is consistent with that used for built-in predicates (8.1). The logical condition for a predicate to be true is sometimes divided into two parts. In the first formulation a sufficient condition is given, using "if". This condition often corresponds to the intended use of a predicate. The second formulation starts with "More precisely," and gives a necessary and sufficient condition using "iff".
p.p Prolog prologue
1 member/2. 2 append/3. 3 length/2. 4 between/3. 5 select/3. 6 succ/2. 7 maplist/2..8.
further propositions:
nth/3

p.p.1 member/2

p.p.1.1 Description

member(X, L) is true if X is an element of the list L.

More precisely, member(X, L) is true iff X is an element of a list prefix of L.

Procedurally, member/2 is defined with the following clauses.

member(X, [X|_L]).
member(X, [_|L]) :-
   member(X, L).
Alternatively:
member(X, [E|L]) :-
   ( X = E
   ; member(X, L)
   ).

p.p.1.2 Template and modes

member(?term, ?term).

p.p.1.3 Errors

None.

p.p.1.4 Examples

member(X, [1,2]).
   Succeeds, unifying X with 1.
   On re-execution, succeeds, unifying Y with 2.

member(1, L).
   Succeeds, unifying L with [1|_].
   On re-execution, succeeds, unifying L with [_,1|_].
   On re-execution, succeeds, unifying L with [_,_,1|_].
   Ad infinitum.

member(X, [Y,Z|nonlist]).
   Succeeds, unifying X with Y.
   On re-execution, succeeds, unifying X with Z.

member(X, nonlist).
   Fails.

member(X, X).
   Undefined.
   [STO 7.3.3, in many implementations succeeds, or loops,
   or produces an error]

p.p.2 append/3

p.p.2.1 Description

append(Xs, Ys, Zs) is true if Zs is the concatenation of the lists Xs and Ys.

More precisely, append(Xs, Ys, Zs) is true iff the list Xs is a list prefix of Zs and Ys is Zs with prefix Xs removed.

Procedurally, append/3 is defined with the following clauses.

append([], Zs, Zs).
append([X|Xs], Ys, [X|Zs]) :-
   append(Xs, Ys, Zs).

p.p.2.2 Template and modes

append(?term, ?term, ?term).

p.p.2.3 Errors

None.

p.p.2.4 Examples

append([a,b],[c,d], Xs).
   Succeeds, unifying Xs with [a,b,c,d].

append([a], nonlist, Xs).
   Succeeds, unifying Xs with [a|nonlist].

append([a], Ys, Zs).
   Succeeds, unifying Zs with [a|Ys].

append(Xs, Ys, [a,b,c]).
   Succeeds, unifying Xs with [], and Ys with [a,b,c].
   On re-execution, succeeds, unifying Xs with [a], and Ys with [b,c].
   On re-execution, succeeds, unifying Xs with [a,b], and Ys with [c].
   On re-execution, succeeds, unifying Xs with [a,b,c], and Ys with [].

p.p.3 length/2

p.p.3.1 Description

length(List, Length) is true iff List is a list of length Length.

Procedurally, length(List, Length) is executed as follows:
a) If List is neither a partial list nor a list, then the goal fails.
b) If List is a list, then unifies Length with the length of List.
c) Else the goal fails.
d) If Length is an integer, then unifies List with a list of length Length with Length distinct fresh variables as elements.
e) Else the goal fails.
f) Chooses the first element Len of N0 being the integer 0.
g) The goal succeeds, unifying Length with Len and List with a list of length Len with Len distinct fresh variables as elements.
h) If List is a partial list and Length is a variable, chooses the next element Len of N0 and proceeds to step p.p.3.1 g.
i) Else the goal fails.

length(List, Length) is re-executable. On backtracking, continue at p.p.3.1 h above.

p.p.3.2 Template and modes

length(?term, ?integer)

p.p.3.3 Errors

a) Length is neither a variable nor an integer
type_error(integer, Length).
b) Length is an integer that is less than zero
domain_error(not_less_than_zero, Length).
c) List is a partial list and Length is the variable of the partial list. (Implementation defined)
type_error(integer, []).

p.p.3.4 Examples

length([a,b,c], Length).
   Succeeds, unifying Length with 3.

length(List, 5).
   Succeeds, unifying List with [_,_,_,_,_].

length(List, Length).
   Succeeds, unifying List with [] and Length with 0.
   On re-execution, succeeds, unifying List with [_] and Length with 1.
   On re-execution, succeeds, unifying List with [_,_] and Length with 2.
   Ad infinitum.

p.p.4 between/3

p.p.4.1 Description

between(Lower, Upper, X) is true iff X is greater than or equal to Lower, and less than or equal to Upper.

Procedurally, between(Lower, Upper, X) is defined with the following clauses when no error conditions apply.
between(Lower, Upper, Lower) :-
   Lower =< Upper.
between(Lower1, Upper, X) :-
   Lower1 < Upper,
   Lower2 is Lower1 + 1,
   between(Lower2, Upper, X).

p.p.4.2 Template and modes

between(+integer,+integer,?integer)

p.p.4.3 Errors

a) Lower is a variable
instantiation_error.
b) Upper is a variable
instantiation_error.
c) Lower is neither a variable nor an integer
type_error(integer,Lower).
d) Upper is neither a variable nor an integer
type_error(integer,Upper).
e) X is neither a variable nor an integer
type_error(integer,X).
NOTE — There are goals with a unique solution that still require an instantiation error. E.g.: between(X, X, 1).

p.p.4.4 Examples

between(1, 2, 0).
   Fails.

between(1, 2, I).
   Succeeds,
      unifying I with 1.
   On re-execution, succeeds,
      unifying I with 2.

between(I, I, 0).
   instantiation_error.

between(1, I, 0).
   instantiation_error.

between(I, 1, 0).
   instantiation_error.

between(1, c, 0).
   type_error(integer,c).

between(1+1,2,I).
   type_error(integer,1+1).

p.p.5 select/3

select(X, Xs, Ys) is true if X is an element of the list Xs and Ys is the list Xs with one occurrence of X removed.

Procedurally, select/3 is defined with the following clauses.

select(E, [E|Xs], Xs).
select(E, [X|Xs], [X|Ys]) :-
	select(E, Xs, Ys).

p.p.5.2 Template and modes

select(?term, ?term, ?term)

p.p.5.3 Errors

None.

p.p.5.4 Examples

select(X, [1,2], Xs).
   Succeeds, unifying X with 1 and Xs with [2].
   On re-execution, succeeds, unifying X with 2 and Xs with [1].

select(X, [Y|inf], Xs).
   Succeeds, unifying X with Y and Xs with inf.

select(E, Xs, Xs).
   STO.

p.p.6 succ/2

p.p.6.1 Description

succ(X, S) is true iff S is the successor of the non-negative integer X.

p.p.6.2 Template and modes

succ(+integer,?integer)
succ(-integer,+integer)

p.p.6.3 Errors

a) X is a variable and S is a variable.
instantiation_error.
b) X is neither a variable nor an integer
type_error(integer,X).
c) S is neither a variable nor an integer
type_error(integer,S).
d) X is an integer that is less than zero
domain_error(not_less_than_zero, X).
e) S is an integer that is less than zero
domain_error(not_less_than_zero, S).
NOTE — succ(X, X) requires an instantiation error although there is no solution.

p.p.6.4 Examples

succ(X, S).
   instantiation_error.

succ(X, X).
   instantiation_error.

succ(0, S).
   Succeeds, unifying S with 1.

succ(1, 1+1).
   type_error(integer, 1+1).

succ(X, 0).
   Fails.

succ(-1, S).
   domain_error(not_less_than_zero, -1).

p.p.7 maplist/2..8

p.p.7.1 Description

maplist(Cont_1, E1s) is true iff E1s is a list and for each element E1 of E1s, call(Cont_1, E1) is true.

maplist(Cont_2, E1s, E2s) is true iff E1s and E2s are lists of same length and for each element E1 of E1s and each corresponding element of E2, call(Cont_2, E1, E2) is true.

maplist(Cont_n, E1s, E2s, ... Ens) is true iff E1s, E2s up to Ens are lists of same length and call(Cont_n, E1_i, E2_i, ... En_i) is true for each i where Ek_i is the i-th element of Listk.

Procedurally, maplist/2..8 is defined with the following clauses.

maplist(_Cont_1, []).
maplist(Cont_1, [E1|E1s]) :-
   call(Cont_1, E1),
   maplist(Cont_1, E1s).

maplist(_Cont_2, [], []).
maplist(Cont_2, [E1|E1s], [E2|E2s]) :-
   call(Cont_2, E1, E2),
   maplist(Cont_2, E1s, E2s).

maplist(_Cont_3, [], [], []).
maplist(Cont_3, [E1|E1s], [E2|E2s], [E3|E3s]) :-
   call(Cont_3, E1, E2, E3),
   maplist(Cont_3, E1s, E2s, E3s).

...

maplist(_Cont_n, [], [], ... []).
maplist(Cont_n, [E1|E1s], [E2|E2s], ... [En|Ens]) :-
   call(Cont_n, E1, E2, ... En),
   maplist(Cont_n, E1s, E2s, ... Ens).

p.p.7.2 Template and modes

maplist(?term, ?term)
maplist(?term, ?term, ?term)
maplist(?term, ?term, ?term, ?term)
...
maplist(?term, ?term, ?term, ... ?term)

p.p.7.3 Errors

None.

p.p.7.4 Examples

maplist(>(3), [1, 2]).
   Succeeds.

maplist(>(3), [1, 2, 3]).
   Fails.

maplist(=(X), Xs).
   Succeeds,
      unifying Xs with [].
   On re-execution, succeeds,
      unifying Xs with [X].
   On re-execution, succeeds,
      unifying Xs with [X, X].
   On re-execution, succeeds,
      unifying Xs with [X, X, X].
   Ad infinitum.

Administrativa

Version control, ISO Prolog works, Validated HTML