/* INTERVALS.PL
Shelved on the 21st of December 1987
Updated on the 20th of February 1988 to fix 'canonical_iset', which
previously did not coalesce all adjacent intervals.
Updated on the 6th of May 1991 to move all the specification comments
together.
*/
/*
SPECIFICATION.
--------------
This file defines predicates for set algebra on sets of integers.
Each set is to be thought of as the union of disjoint intervals, and is
represented as a list, each element of which is one such interval.
PUBLIC intervals_are_disjoint( I1+, I2+ ):
Intervals I1 and I2 are disjoint - i.e. have no points in common.
PUBLIC intervals_meet( I1+, I2+ ):
Intervals I1 and I2 are not disjoint - i.e. have at least one
point in common.
PUBLIC interval_union( I1+, I2+, I3- ):
I3 is that interval which is the union of intervals I1 and I2.
Only defined if I1 and I2 are coalescable.
PUBLIC interval_intersection( I1+, I2+, I3- ):
I3 is that interval which is the intersection of intervals I1 and I2.
Only defined if I1 and I2 are not disjoint.
PUBLIC interval_difference( I1+, I2+, I3- ):
I3 is that I-set which is the difference of intervals I1 and I2.
PUBLIC interval_is_less_and_not_coalescable( I1+, I2+ ):
Interval I1 is strictly less than I2; and I1 union I2 can not
be expressed as one interval.
I.e. the upper bound of I1 is at least 2 less than the lower bound of I2.
PUBLIC interval_is_less( I1+, I2+ ):
Interval I1 is strictly less than I2.
I.e. there is no point P2 in I2 such that I1 contains a point
greater than or equal to P2.
|-----| |----|
I1 I2
interval_is_less( I1, I2 ) implies disjoint( I1, I2 ).
PUBLIC intervals_are_not_coalescable( I1+, I2+ ):
True if I1 union I2 can not be expressed as one interval.
PUBLIC intervals_are_coalescable( I1+, I2+ ):
True if I1 union I2 can be expressed as one interval.
PUBLIC interval_ends_first( I1+, I2+ ):
The upper bound of I1 is less than that of I2.
PUBLIC interval_includes( I1+, I2+ ):
I1 is a superset of (or equal to) I2.
PUBLIC interval_contains( I1+, P+ ):
P is a member of I1.
PUBLIC iset_union( A+, B+, U- ):
U is the union of A and B, where A, B, and U are I-sets.
PUBLIC iset_intersection( A+, B+, I- ):
U is the intersection of A and B, where A, B, and I are I-sets.
PUBLIC iset_difference( A+, B+, D- ):
U is the difference of A and B, where A, B, and D are I-sets.
PUBLIC iset_complement( I+, A+, C- ):
C is the complement of I-set A in interval I.
PUBLIC canonical_iset( S+, C- ):
S is a list of intervals. They can be in any order, and
need not be disjoint.
C is the corresponding I-set.
PUBLIC iset_includes( I1+, I2+ ):
I1 is a superset of (or equal to) I2.
PUBLIC iset_contains( I1+, P+ ):
P is a member of I-set I1.
IMPLEMENTATION.
---------------
The intervals are represented as
L -- U
where L and U are integers, and L must be less than or equal to U. Note
that 10--9 (corresponding to the null set) is not a valid interval, and
the predicates will not cope with it.
I call the sets of intervals I-sets. Their representation has these
properties:
(1) [] is an I-set.
(2) [ I ] is an I-set, for any interval I.
(3) [ I1, I2, ... In ] is an I-set if:
(3.1) All Ii, Ij are disjoint.
(3.2) For any pair of adjacent intervals, Ii and Ii+1, the upper
bound of I1 is less than the lower bound of I2. This ordering
makes the I-sets more efficient to process.
(3.3) For any pair of adjacent intervals, Ii and Ii+1, the upper
bound of I1 is at least 2 less than the lower bound of I2.
This enforces a unique representation, prohibiting I-sets
like
[ 1--9, 10--12 ] and [ 1--3, 4--12 ]
being equivalent to
[ 1--12 ]
Proofs of correctness:
I'll summarise these for iset_union, iset_intersection, iset_difference,
and iset_complement, since those predicates are rather tricky.
We can divide each proof into five parts:
(1) Proof that the predicates terminate on correct arguments.
(2) Proof that the result is algebraically correct (even though it may
not be a valid I-set).
(3) Proof that the result's intervals are disjoint.
(4) Proof that the result's intervals are ordered in ascending order.
(5) Proof that the result contains no adjacent pairs like 1--2,3--4
which should be coalesced.
The last three correspond to proving that the result is a canonical
I-set.
(1) Proof of termination.
This is easy. Sets are represented as lists. We can show that on each
recursive call, the sets grow smaller - either because a whole interval
is removed from a list, or because it is reduced in size.
(2) Proof of algebraic correctness.
For 'iset_union', this is trivial, because the only operations used in
the tail of 'iset_union' are set unions. The operation [H|T] on an
I-set corresponds to H u T. The predicates 'interval_join', and
'union_overlap' also correspond to union. All we need do is show that
the union denoted by the head of each clause is equal to that denoted
by its tail.
For 'iset_intersection', we use the distributive law:
(A1 u A2 u A3...) /\ (B1 u B2 u B3... ) =
(A1 /\ B1 ) u (A2 /\ B1 ) u (A1 /\ B2) u (A2 /\ B2) ...
We can optimise by noting that Ai/\Bi = {} if Ai B, !.
max( A, B, B ).
/* min( A+, B+, M- ):
M is the minimum of A and B.
*/
min( A, B, A ) :- A < B, !.
min( A, B, B ).
/* INTERVALS and I-SETS */
/* L--U is the interval [L,U] : i.e. that containing
L and U as endpoints.
L and U must be integers, not reals.
*/
?- op( 31, xfx, -- ).
intervals_are_disjoint( L1--U1, L2--U2 ) :-
U1 < L2, !.
intervals_are_disjoint( L1--U1, L2--U2 ) :-
U2 < L1, !.
intervals_meet( I1, I2 ) :-
not( intervals_are_disjoint(I1,I2) ).
interval_union( L1--U1, L2--U2, L3--U3 ) :-
min( L1, L2, L3 ),
max( U1, U2, U3 ).
interval_intersection( L1--U1, L2--U2, L3--U3 ) :-
max( L1, L2, L3 ),
min( U1, U2, U3 ).
interval_difference( I1, I2, [I1] ) :-
intervals_are_disjoint( I1, I2 ), !.
interval_difference( L1--U1, L2--U2, [ L1--L2_less_1, U2_add_1--U1 ] ) :-
L1 < L2, U1 > U2,
U2_add_1 is U2 + 1,
L2_less_1 is L2 - 1, !.
interval_difference( L1--U1, L2--U2, [ L1--L2_less_1 ] ) :-
L1 < L2, U1 =< U2,
L2_less_1 is L2 - 1, !.
interval_difference( L1--U1, L2--U2, [ U2_add_1--U1 ] ) :-
L1 >= L2, U1 > U2,
U2_add_1 is U2 + 1, !.
interval_difference( L1--U1, L2--U2, [] ) :-
L1 >= L2, U1 =< U2, !.
interval_is_less_and_not_coalescable( L1--U1, L2--U2 ) :-
L2_less_1 is L2-1,
U1 < L2_less_1, !.
interval_is_less( L1--U1, L2--U2 ) :-
U1 < L2, !.
intervals_are_not_coalescable( I1, I2 ) :-
interval_is_less_and_not_coalescable( I1, I2 ), !.
intervals_are_not_coalescable( I1, I2 ) :-
interval_is_less_and_not_coalescable( I2, I1 ), !.
intervals_are_coalescable( I1, I2 ) :-
not( intervals_are_not_coalescable( I1, I2 ) ).
interval_ends_first( _--U1, _--U2 ) :-
U1 < U2, !.
interval_includes( L1--U1, L2--U2 ) :-
L1 =< L2, U1 >= U2.
interval_contains( L1--U1, P ) :-
L1 =< P, U1 >= P.
iset_union( A, [], A ) :- !.
iset_union( [], B, B ) :- !.
iset_union( [A1|A2_n], [B1|B2_n], [B1|URest] ) :-
interval_is_less_and_not_coalescable( B1, A1 ),
iset_union( [A1|A2_n], B2_n, URest ), !.
iset_union( [A1|A2_n], [B1|B2_n], [A1|URest] ) :-
interval_is_less_and_not_coalescable( A1, B1 ),
iset_union( A2_n, [B1|B2_n], URest ), !.
iset_union( [A1|A2_n], [B1|B2_n], U ) :-
/* A1 overlaps B1 */
interval_union( A1, B1, U1 ),
union_overlap( U1, A2_n, B2_n, U ).
union_overlap( U1, [A1|A2_n], B, URest ) :-
intervals_are_coalescable( U1, A1 ),
interval_union( U1, A1, J ),
union_overlap( J, A2_n, B, URest ), !.
union_overlap( U1, A, [B1|B2_n], URest ) :-
intervals_are_coalescable( U1, B1 ),
interval_union( U1, B1, J ),
union_overlap( J, A, B2_n, URest ), !.
union_overlap( U1, A, B, [U1|URest] ) :-
iset_union( A, B, URest ), !.
iset_intersection( A, [], [] ) :- !.
iset_intersection( [], B, [] ) :- !.
iset_intersection( [A1|A2_n], [B1|B2_n], IRest ) :-
interval_is_less( A1, B1 ),
iset_intersection( A2_n, [B1|B2_n], IRest ), !.
iset_intersection( [A1|A2_n], [B1|B2_n], IRest ) :-
interval_is_less( B1, A1 ),
iset_intersection( [A1|A2_n], B2_n, IRest ), !.
iset_intersection( [A1|A2_n], [B1|B2_n], [I1|IRest] ) :-
interval_intersection( A1, B1, I1 ),
drop_lowest( [A1|A2_n], [B1|B2_n], A_Rest, B_Rest ),
iset_intersection( A_Rest, B_Rest, IRest ).
drop_lowest( [I|A2_n], [I|B2_n], A2_n, B2_n ) :- !.
drop_lowest( [A1|A2_n], [B1|B2_n], A2_n, [B1|B2_n] ) :-
interval_ends_first( A1, B1 ), !.
drop_lowest( A, [B1|B2_n], A, B2_n ).
iset_difference( A, [], A ) :- !.
iset_difference( [], B, [] ) :- !.
iset_difference( [A1|A2_n], [B1|B2_n], [A1|DRest] ) :-
interval_is_less( A1, B1 ),
iset_difference( A2_n, [B1|B2_n], DRest ), !.
iset_difference( [A1|A2_n], [B1|B2_n], DRest ) :-
interval_is_less( B1, A1 ),
iset_difference( [A1|A2_n], B2_n, DRest ), !.
iset_difference( [A1_low--A1_high|A2_n], [B1_low--B1_high|B2_n],
[ A1_low--B1_low_less_1 | D_Rest ] ) :-
A1_low < B1_low,
!,
B1_low_less_1 is B1_low - 1,
iset_difference( [ B1_low--A1_high | A2_n ],
[ B1_low--B1_high | B2_n ],
D_Rest ), !.
iset_difference( [A1_low--High|A2_n], [B1_low--High|B2_n], D ) :-
iset_difference( A2_n, B2_n, D ), !.
iset_difference( [A1_low--A1_high|A2_n], [B1_low--B1_high|B2_n], D ) :-
A1_high > B1_high,
!,
B1_high_add_1 is B1_high + 1,
iset_difference( [ B1_high_add_1--A1_high | A2_n ], B2_n, D ), !.
iset_difference( [A1_low--A1_high|A2_n], [B1_low--B1_high|B2_n], D ) :-
A1_high < B1_high,
!,
A1_high_add_1 is A1_high + 1,
iset_difference( A2_n, [ A1_high_add_1--B1_high | B2_n ], D ), !.
iset_complement( L--U, A, C ) :-
iset_complement( L, U, A, C ).
iset_complement( L, U, _, [] ) :-
L > U, !.
iset_complement( L, U, [], [L--U] ) :- !.
iset_complement( L, U, [ A1_low--A1_high | A2_n ], C ) :-
A1_high < L,
!,
/* A1 disjoint from and less than I. */
iset_complement( L, U, A2_n, C ).
iset_complement( L, U, [ A1_low--_ | _ ], [L--U] ) :-
A1_low > U,
/* A1 disjoint from and greater than I. */
!.
iset_complement( L, U, [ A1_low--A1_high | A2_n ], [ L -- A1_low_less_1 | C_Rest ] ) :-
A1_low > L,
!,
/* A1 greater than lower end of I. */
A1_low_less_1 is A1_low - 1,
A1_high_add_1 is A1_high + 1,
iset_complement( A1_high_add_1, U, A2_n, C_Rest ).
iset_complement( L, U, [ A1_low--A1_high | A2_n ], C_Rest ) :-
A1_low =< L,
!,
/* A1 overlaps lower end of I. */
A1_high_add_1 is A1_high + 1,
iset_complement( A1_high_add_1, U, A2_n, C_Rest ).
canonical_iset( [], [] ) :- !.
canonical_iset( [X|L], U ) :-
canonical_iset( L, LC ),
iset_union( [X], LC, U ).
iset_includes( _, [] ) :- !.
iset_includes( [A1|A2_n], [B1|B2_n] ) :-
interval_is_less( A1, B1 ),
!,
iset_includes( A2_n, [B1|B2_n] ).
iset_includes( [A1|A2_n], [B1|B2_n] ) :-
interval_includes( A1, B1 ),
iset_includes( [A1|A2_n], B2_n ), !.
iset_contains( [A1|_], P ) :-
interval_contains( A1, P ), !.
iset_contains( [_|A2_n], P ) :-
iset_contains( A2_n, P ), !.