1:- module(intervals). % SEPIA header 2 3:- export 4 intervals_are_disjoint/2, 5 intervals_meet/2, 6 interval_union/3, 7 interval_intersection/3, 8 interval_difference/3, 9 interval_is_less_and_not_coalescable/2, 10 interval_is_less/2, 11 intervals_are_not_coalescable/2, 12 intervals_are_coalescable/2, 13 interval_ends_first/2, 14 interval_includes/2, 15 interval_contains/2, 16 iset_union/3, 17 iset_intersection/3, 18 iset_difference/3, 19 iset_complement/3, 20 canonical_iset/2, 21 iset_includes/2, 22 iset_contains/2. 23 24 25/* INTERVALS.PL 26 Shelved on the 21st of December 1987 27 Updated on the 20th of February 1988 to fix 'canonical_iset', which 28 previously did not coalesce all adjacent intervals. 29*/ 30 31 32/* 33This file defines predicates for set algebra on sets of integers. 34 35Each set is to be thought of as the union of disjoint intervals, and is 36represented as a list, each element of which is one such interval. 37 38The intervals are represented as 39 L -- U 40where L and U are integers, and L must be less than or equal to U. Note 41that 10--9 (corresponding to the null set) is not a valid interval, and 42the predicates will not cope with it. 43 44I call the sets of intervals I-sets. Their representation has these 45properties: 46 47(1) [] is an I-set. 48 49(2) [ I ] is an I-set, for any interval I. 50 51(3) [ I1, I2, ... In ] is an I-set if: 52 53 (3.1) All Ii, Ij are disjoint. 54 55 (3.2) For any pair of adjacent intervals, Ii and Ii+1, the upper 56 bound of I1 is less than the lower bound of I2. This ordering 57 makes the I-sets more efficient to process. 58 59 (3.3) For any pair of adjacent intervals, Ii and Ii+1, the upper 60 bound of I1 is at least 2 less than the lower bound of I2. 61 This enforces a unique representation, prohibiting I-sets 62 like 63 [ 1--9, 10--12 ] and [ 1--3, 4--12 ] 64 being equivalent to 65 [ 1--12 ] 66 67 68Proofs of correctness: 69 70I'll summarise these for iset_union, iset_intersection, iset_difference, 71and iset_complement, since those predicates are rather tricky. 72 73We can divide each proof into five parts: 74(1) Proof that the predicates terminate on correct arguments. 75(2) Proof that the result is algebraically correct (even though it may 76 not be a valid I-set). 77(3) Proof that the result's intervals are disjoint. 78(4) Proof that the result's intervals are ordered in ascending order. 79(5) Proof that the result contains no adjacent pairs like 1--2,3--4 80 which should be coalesced. 81 82The last three correspond to proving that the result is a canonical 83I-set. 84 85(1) Proof of termination. 86 87 This is easy. Sets are represented as lists. We can show that on each 88 recursive call, the sets grow smaller - either because a whole interval 89 is removed from a list, or because it is reduced in size. 90 91(2) Proof of algebraic correctness. 92 93 For 'iset_union', this is trivial, because the only operations used in 94 the tail of 'iset_union' are set unions. The operation [H|T] on an 95 I-set corresponds to H u T. The predicates 'interval_join', and 96 'union_overlap' also correspond to union. All we need do is show that 97 the union denoted by the head of each clause is equal to that denoted 98 by its tail. 99 100 For 'iset_intersection', we use the distributive law: 101 102 (A1 u A2 u A3...) /\ (B1 u B2 u B3... ) = 103 (A1 /\ B1 ) u (A2 /\ B1 ) u (A1 /\ B2) u (A2 /\ B2) ... 104 105 We can optimise by noting that Ai/\Bi = {} if Ai<Bi. Hence the use of 106 'is_less'. 107 108 We also use the ordering and disjointness of intervals within I-sets to 109 show that if A1 /\ B1 is not empty, then either A1 /\ B2 is empty or A2 110 /\ B1 is empty. Thus, after intersecting A1 and B1, we can drop either 111 A1 or B1 in the recursive call. This is what 'drop_lowest' does. 112 113 For 'iset_difference', we use the equivalence 114 115 A1 - B1 = A1 /\ -B1 116 117 So 118 (A1 u A2 ... ) - (B1 u B2 ...) 119 = 120 (A1 u A2 ... ) /\ -(B1 u B2 u B3...) 121 = (by De Morgan) 122 (A1 u A2 ... ) /\ -B1 /\ -B2 /\ B3 ... 123 = (distributive) 124 (A1 /\ -B1 /\ -B2...) u (A2 /\ -B1 /\ -B2...) u ... 125 126 Since An-Bn = An if An and Bn are disjoint, we can ignore all the Bi 127 which don't overlap with An in each term, reducing to 128 129 (A1 /\ overlapping Bi) u (A2 /\ overlapping Bi) u ... 130 131 Most of the code in 'iset_difference' and 'iset_complement' is for 132 detecting which Bi overlaps which Ai, and passing along bits of 133 intervals which overlap more than one other. 134 135(3) Disjointness of intervals within I-sets. 136 137 For 'iset_intersection', 'iset_complement', and 'iset_difference' this 138 is trivial. If the intervals in A are disjoint, then intersecting or 139 differencing can only take parts away, so preserving disjointness. 140 141 For 'iset_union', if Ai overlaps Bi, we must take care not to add the 142 overlap twice to the result. This is what 'union_overlap' does; its 143 first argument is Ai u Bi; an interval which may need to have its upper 144 bound raised if A(i+1) or B(i+1) overlaps it. 145 146(4) Ordering of intervals within I-sets. 147 148 This is trivial, as long as the inputs are properly ordered. The 149 operation [ H | T ] corresponds to uniting the interval H with I-set T. 150 When new I-sets are built, lesser intervals are always put onto the 151 head of a list which is either empty or contains greater intervals. 152 153(5) Non-coalescability of intervals within I-sets. 154 155 This follows in the same way as (3). For 'iset_union', we must take 156 care to coalesce intervals which come from different sets, and which 157 are disjoint but coalescable. This is why 'iset_union' calls 158 'interval_is_less_and_not_coalescable'. 159*/ 160 161 162% /* UTILITIES */ 163% 164% 165% /* append( L1+, L2+, L3- ): 166% 167% L3 is the result of appending list L2 to list L1. 168% */ 169% append( [], L, L ) :- !. 170% append( [H|T], L, [H|T1] ) :- 171% append( T, L, T1 ), !. 172% 173% 174% /* max( A+, B+, M- ): 175% 176% M is the maximum of A and B. 177% */ 178% max( A, B, A ) :- A > B, !. 179% max( A, B, B ). 180% 181% 182% /* min( A+, B+, M- ): 183% 184% M is the minimum of A and B. 185% */ 186% min( A, B, A ) :- A < B, !. 187% min( A, B, B ). 188 189 190/* INTERVALS and I-SETS */ 191 192 193/* L--U is the interval [L,U] : i.e. that containing 194 L and U as endpoints. 195 L and U must be integers, not reals. 196*/ 197:- op( 31, xfx, -- ). 198 199 200/* PUBLIC intervals_are_disjoint( I1+, I2+ ): 201 202 Intervals I1 and I2 are disjoint - i.e. have no points in common. 203*/ 204intervals_are_disjoint( _L1--U1, L2--_U2 ) :- 205 U1 < L2, !. 206 207intervals_are_disjoint( L1--_U1, _L2--U2 ) :- 208 U2 < L1, !. 209 210 211/* PUBLIC intervals_meet( I1+, I2+ ): 212 213 Intervals I1 and I2 are not disjoint - i.e. have at least one 214 point in common. 215*/ 216intervals_meet( I1, I2 ) :- 217 not( intervals_are_disjoint(I1,I2) ). 218 219 220/* PUBLIC interval_union( I1+, I2+, I3- ): 221 222 I3 is that interval which is the union of intervals I1 and I2. 223 Only defined if I1 and I2 are coalescable. 224*/ 225interval_union( L1--U1, L2--U2, L3--U3 ) :- 226 min( L1, L2, L3 ), 227 max( U1, U2, U3 ). 228 229 230/* PUBLIC interval_intersection( I1+, I2+, I3- ): 231 232 I3 is that interval which is the intersection of intervals I1 and I2. 233 Only defined if I1 and I2 are not disjoint. 234*/ 235interval_intersection( L1--U1, L2--U2, L3--U3 ) :- 236 max( L1, L2, L3 ), 237 min( U1, U2, U3 ). 238 239 240/* PUBLIC interval_difference( I1+, I2+, I3- ): 241 242 I3 is that I-set which is the difference of intervals I1 and I2. 243*/ 244interval_difference( I1, I2, [I1] ) :- 245 intervals_are_disjoint( I1, I2 ), !. 246 247interval_difference( L1--U1, L2--U2, [ L1--L2_less_1, U2_add_1--U1 ] ) :- 248 L1 < L2, U1 > U2, 249 U2_add_1 is U2 + 1, 250 L2_less_1 is L2 - 1, !. 251 252interval_difference( L1--U1, L2--U2, [ L1--L2_less_1 ] ) :- 253 L1 < L2, U1 =< U2, 254 L2_less_1 is L2 - 1, !. 255 256interval_difference( L1--U1, L2--U2, [ U2_add_1--U1 ] ) :- 257 L1 >= L2, U1 > U2, 258 U2_add_1 is U2 + 1, !. 259 260interval_difference( L1--U1, L2--U2, [] ) :- 261 L1 >= L2, U1 =< U2, !. 262 263 264/* PUBLIC interval_is_less_and_not_coalescable( I1+, I2+ ): 265 266 Interval I1 is strictly less than I2; and I1 union I2 can not 267 be expressed as one interval. 268 I.e. the upper bound of I1 is at least 2 less than the lower bound of I2. 269*/ 270interval_is_less_and_not_coalescable( _L1--U1, L2--_U2 ) :- 271 L2_less_1 is L2-1, 272 U1 < L2_less_1, !. 273 274 275/* PUBLIC interval_is_less( I1+, I2+ ): 276 277 Interval I1 is strictly less than I2. 278 I.e. there is no point P2 in I2 such that I1 contains a point 279 greater than or equal to P2. 280 281 |-----| |----| 282 I1 I2 283 284 interval_is_less( I1, I2 ) implies disjoint( I1, I2 ). 285*/ 286interval_is_less( _L1--U1, L2--_U2 ) :- 287 U1 < L2, !. 288 289 290/* PUBLIC intervals_are_not_coalescable( I1+, I2+ ): 291 292 True if I1 union I2 can not be expressed as one interval. 293*/ 294intervals_are_not_coalescable( I1, I2 ) :- 295 interval_is_less_and_not_coalescable( I1, I2 ), !. 296 297intervals_are_not_coalescable( I1, I2 ) :- 298 interval_is_less_and_not_coalescable( I2, I1 ), !. 299 300 301/* PUBLIC intervals_are_coalescable( I1+, I2+ ): 302 303 True if I1 union I2 can be expressed as one interval. 304*/ 305intervals_are_coalescable( I1, I2 ) :- 306 not( intervals_are_not_coalescable( I1, I2 ) ). 307 308 309/* PUBLIC interval_ends_first( I1+, I2+ ): 310 311 The upper bound of I1 is less than that of I2. 312*/ 313interval_ends_first( _--U1, _--U2 ) :- 314 U1 < U2, !. 315 316 317/* PUBLIC interval_includes( I1+, I2+ ): 318 I1 is a superset of (or equal to) I2. 319*/ 320interval_includes( L1--U1, L2--U2 ) :- 321 L1 =< L2, U1 >= U2. 322 323 324/* PUBLIC interval_contains( I1+, P+ ): 325 P is a member of I1. 326*/ 327interval_contains( L1--U1, P ) :- 328 L1 =< P, U1 >= P. 329 330 331/* PUBLIC iset_union( A+, B+, U- ): 332 333 U is the union of A and B, where A, B, and U are I-sets. 334*/ 335iset_union( A, [], A ) :- !. 336 337iset_union( [], B, B ) :- !. 338 339iset_union( [A1|A2_n], [B1|B2_n], [B1|URest] ) :- 340 interval_is_less_and_not_coalescable( B1, A1 ), 341 iset_union( [A1|A2_n], B2_n, URest ), !. 342 343iset_union( [A1|A2_n], [B1|B2_n], [A1|URest] ) :- 344 interval_is_less_and_not_coalescable( A1, B1 ), 345 iset_union( A2_n, [B1|B2_n], URest ), !. 346 347iset_union( [A1|A2_n], [B1|B2_n], U ) :- 348 /* A1 overlaps B1 */ 349 interval_union( A1, B1, U1 ), 350 union_overlap( U1, A2_n, B2_n, U ). 351 352 353union_overlap( U1, [A1|A2_n], B, URest ) :- 354 intervals_are_coalescable( U1, A1 ), 355 interval_union( U1, A1, J ), 356 union_overlap( J, A2_n, B, URest ), !. 357 358union_overlap( U1, A, [B1|B2_n], URest ) :- 359 intervals_are_coalescable( U1, B1 ), 360 interval_union( U1, B1, J ), 361 union_overlap( J, A, B2_n, URest ), !. 362 363union_overlap( U1, A, B, [U1|URest] ) :- 364 iset_union( A, B, URest ), !. 365 366 367/* PUBLIC iset_intersection( A+, B+, I- ): 368 369 U is the intersection of A and B, where A, B, and I are I-sets. 370*/ 371iset_intersection( _A, [], [] ) :- !. 372 373iset_intersection( [], _B, [] ) :- !. 374 375iset_intersection( [A1|A2_n], [B1|B2_n], IRest ) :- 376 interval_is_less( A1, B1 ), 377 iset_intersection( A2_n, [B1|B2_n], IRest ), !. 378 379iset_intersection( [A1|A2_n], [B1|B2_n], IRest ) :- 380 interval_is_less( B1, A1 ), 381 iset_intersection( [A1|A2_n], B2_n, IRest ), !. 382 383iset_intersection( [A1|A2_n], [B1|B2_n], [I1|IRest] ) :- 384 interval_intersection( A1, B1, I1 ), 385 drop_lowest( [A1|A2_n], [B1|B2_n], A_Rest, B_Rest ), 386 iset_intersection( A_Rest, B_Rest, IRest ). 387 388 389drop_lowest( [I|A2_n], [I|B2_n], A2_n, B2_n ) :- !. 390 391drop_lowest( [A1|A2_n], [B1|B2_n], A2_n, [B1|B2_n] ) :- 392 interval_ends_first( A1, B1 ), !. 393 394drop_lowest( A, [_B1|B2_n], A, B2_n ). 395 396 397/* PUBLIC iset_difference( A+, B+, D- ): 398 399 U is the difference of A and B, where A, B, and D are I-sets. 400*/ 401iset_difference( A, [], A ) :- !. 402 403iset_difference( [], _B, [] ) :- !. 404 405iset_difference( [A1|A2_n], [B1|B2_n], [A1|DRest] ) :- 406 interval_is_less( A1, B1 ), 407 iset_difference( A2_n, [B1|B2_n], DRest ), !. 408 409iset_difference( [A1|A2_n], [B1|B2_n], DRest ) :- 410 interval_is_less( B1, A1 ), 411 iset_difference( [A1|A2_n], B2_n, DRest ), !. 412 413iset_difference( [A1_low--A1_high|A2_n], [B1_low--B1_high|B2_n], 414 [ A1_low--B1_low_less_1 | D_Rest ] ) :- 415 A1_low < B1_low, 416 !, 417 B1_low_less_1 is B1_low - 1, 418 iset_difference( [ B1_low--A1_high | A2_n ], 419 [ B1_low--B1_high | B2_n ], 420 D_Rest ), !. 421 422iset_difference( [_A1_low--High|A2_n], [_B1_low--High|B2_n], D ) :- 423 iset_difference( A2_n, B2_n, D ), !. 424 425iset_difference( [_A1_low--A1_high|A2_n], [_B1_low--B1_high|B2_n], D ) :- 426 A1_high > B1_high, 427 !, 428 B1_high_add_1 is B1_high + 1, 429 iset_difference( [ B1_high_add_1--A1_high | A2_n ], B2_n, D ), !. 430 431iset_difference( [_A1_low--A1_high|A2_n], [_B1_low--B1_high|B2_n], D ) :- 432 A1_high < B1_high, 433 !, 434 A1_high_add_1 is A1_high + 1, 435 iset_difference( A2_n, [ A1_high_add_1--B1_high | B2_n ], D ), !. 436 437 438/* PUBLIC iset_complement( I+, A+, C- ): 439 C is the complement of I-set A in interval I. 440*/ 441iset_complement( L--U, A, C ) :- 442 iset_complement( L, U, A, C ). 443 444 445iset_complement( L, U, _, [] ) :- 446 L > U, !. 447 448iset_complement( L, U, [], [L--U] ) :- !. 449 450iset_complement( L, U, [ _A1_low--A1_high | A2_n ], C ) :- 451 A1_high < L, 452 !, 453 /* A1 disjoint from and less than I. */ 454 iset_complement( L, U, A2_n, C ). 455 456iset_complement( L, U, [ A1_low--_ | _ ], [L--U] ) :- 457 A1_low > U, 458 /* A1 disjoint from and greater than I. */ 459 !. 460 461iset_complement( L, U, [ A1_low--A1_high | A2_n ], [ L -- A1_low_less_1 | C_Rest ] ) :- 462 A1_low > L, 463 !, 464 /* A1 greater than lower end of I. */ 465 A1_low_less_1 is A1_low - 1, 466 A1_high_add_1 is A1_high + 1, 467 iset_complement( A1_high_add_1, U, A2_n, C_Rest ). 468 469iset_complement( L, U, [ A1_low--A1_high | A2_n ], C_Rest ) :- 470 A1_low =< L, 471 !, 472 /* A1 overlaps lower end of I. */ 473 A1_high_add_1 is A1_high + 1, 474 iset_complement( A1_high_add_1, U, A2_n, C_Rest ). 475 476 477/* PUBLIC canonical_iset( S+, C- ): 478 479 S is a list of intervals. They can be in any order, and 480 need not be disjoint. 481 482 C is the corresponding I-set. 483*/ 484canonical_iset( [], [] ) :- !. 485 486canonical_iset( [X|L], U ) :- 487 canonical_iset( L, LC ), 488 iset_union( [X], LC, U ). 489 490 491/* PUBLIC iset_includes( I1+, I2+ ): 492 I1 is a superset of (or equal to) I2. 493*/ 494iset_includes( _, [] ) :- !. 495 496iset_includes( [A1|A2_n], [B1|B2_n] ) :- 497 interval_is_less( A1, B1 ), 498 !, 499 iset_includes( A2_n, [B1|B2_n] ). 500 501iset_includes( [A1|A2_n], [B1|B2_n] ) :- 502 interval_includes( A1, B1 ), 503 iset_includes( [A1|A2_n], B2_n ), !. 504 505 506/* PUBLIC iset_contains( I1+, P+ ): 507 P is a member of I-set I1. 508*/ 509iset_contains( [A1|_], P ) :- 510 interval_contains( A1, P ), !. 511 512iset_contains( [_|A2_n], P ) :- 513 iset_contains( A2_n, P ), !. 514