1/* 2 comprehension.pl 3 4@author Francois Fages 5@email Francois.Fages@inria.fr 6@license LGPL-2 7@version 1.1.5 8 9 List comprehension for constraint quantifiers, aggregates, and let bindings. 10 11*/ 12 13 14:- module( 15 comprehension, 16 [ 17 for_all/2, 18 list_of/3, 19 aggregate_for/6, 20 21 exists/2, let/2, op(501, xfx, ..), op(502, yfx, \/), op(700, xfx, in), op(990, xfx, where) ]).

List comprehension for constraint quantifiers, aggregates, and let bindings.

author

- Francois Fages

version

- 1.1.5

Prolog metapredicates for set comprehension like setof/3 were introduced by David Warren in 1982 to collect goal instantiations by backtracking. This necessitated indeed a special mechanism to add to Prolog, which is used for bagof/3, findall/3, forall/2, foreach/2, or aggregate/3 for instance.

This approach to set comprehension is correct for the goal success semantics of Prolog, but incorrect for the answer constraint semantics, e.g. universal quantifier constraint for_all/2 defined here compared to standard forall/2 foreach/2 metapredicates:

?- L=[A, B, C], for_all(X in L, X=1). % constraint posted for all elements
L = [1, 1, 1],
A = B, B = C, C = 1.

?- L=[A, B, C], forall(member(X, L), X=1). % satisfiability test for all elements
L = [A, B, C].

?- L=[A, B, C], foreach(member(X, L), X=1). % idem
L = [A, B, C].

?- L=[A, B, C], for_all([X, Y] in L, X=Y).
L = [C, C, C],
A = B, B = C.

?- L=[A, B, C], forall((member(X, L), member(Y, L)), X=Y).
L = [A, B, C].

?- use_module(library(clpfd)).
true.

?- L=[A, B, C], forall(member(X, L), X#>1).
L = [A, B, C].

?- L=[A, B, C], for_all(X in L, X#>1).
L = [A, B, C],
clpfd:(A in 2..sup),
clpfd:(B in 2..sup),
clpfd:(C in 2..sup).

?- forall(member(X, [1, 2, 3]), Y#>X).
true.

?- for_all(X in [1, 2, 3], Y#>X).
clpfd:(Y in 4..sup).

We provide here metapredicates for comprehension by iteration, instead of backtracking, which

rename comprehension variables and raise an error if they are instantiated (they can be attributed and will be renamed without attributes),
constrain the calling context variables,
possibly non-deterministically, if the conditions or goal are non-deterministic.

The comprehension variables must be given with a mandatory "in" domain, and optionally a "where" condition.

The "in" domain must be either a domain of integers (i.e. union \/ of intervals ..) or a list of terms. Shorthand notations are evaluated in the domain.

?- for_all([I, J] in 1..3 where I<J, writeln(I-J)).
1-2
1-3
2-3
true.

?- for_all([I in 1..3, J in I+1..3], writeln(I-J)).
1-2
1-3
2-3
true.

list_of/3 collects the elements defined by comprehension in a list:

?- list_of([I, J] in 1..3 where I<J, I-J, List).
List = [1-2, 1-3, 2-3].

aggregate_for/6 expresses a relation on the application of a binary operator between elements defined by comprehension:

?- aggregate_for(X in 1..5, X+1, +, 0, =, Term).
Term = 1+1+(2+1+(3+1+(4+1+(5+1+0)))).

?- use_module(library(clpfd)).
true.
  
?- aggregate_for(X in 1..5, X+1, +, 0, #=, Result).
Result = 20.

The "where" condition in intensional definitions can bind or constrain context variables. In particular, if the "where" condition is a constraint, the constraint is posted and thus tested for satisfiability, not entailment. The example below illustrates the difference: X=Y is satisfiable and posted for all X, Y, whereas in the second query, the condition X==Y is just a test and succeeds on the elements where it is satisfied without changing L:

?- L=[A, B, C], for_all([X, Y] in L where X=Y, true).
L = [C, C, C],
A = B, B = C.

?- L=[A, B, C], for_all([X, Y] in L where X==Y, true).
L = [A, B, C].

The "where" condition goal can also be non-deterministic, making the comprehension metapredicate non-deterministic in this case.

166for_all(Var, _Goal) :- 167 var(Var), 168 !, 169 must_be(nonvar, Var). % bounded quantification only 170 171for_all([VarDomain | VarDomains], Goal) :- 172 (VarDomains = [] 173 -> 174 (VarDomain = (_ where _) 175 -> 176 for_all_complete(VarDomain, Goal) 177 ; 178 for_all_complete(VarDomain where true, Goal)) 179 ; 180 for_all(VarDomain, for_all(VarDomains, Goal))). 181 182for_all(Vars in Domain, Goal) :- 183 for_all(Vars in Domain where true, Goal). 184 185for_all(VarDomains where Condition, Goal) :- 186 must_be(nonvar, VarDomains), 187 (VarDomains = (Vs in Domain) 188 -> 189 (var(Vs) -> Vars=[Vs] ; must_be(list(var), Vs), Vars=Vs), 190 for_all_complete(Vars in Domain where Condition, Goal) 191 ; 192 VarDomains = [VarDomain1 | VarDomains2], 193 (VarDomains2 = [] 194 -> 195 (VarDomain1 = (VarDom1 where Cond) 196 -> 197 for_all_complete(VarDom1 where (Cond, Condition), Goal) 198 ; 199 for_all_complete(VarDomain1 where Condition, Goal)) 200 ; 201 for_all(VarDomain1, for_all(VarDomains2 where Condition, Goal)))). 202 203 204% VarDomains is a flat list of variables given with their domain 205for_all_complete(VarDomains where Condition, Goal) :- 206 var_domains(VarDomains where Condition, VarDoms, Condition), 207 variables(VarDoms, Vars), 208 copy_term_nat(Vars, f(VarDoms, Condition, Goal), _, f(VDoms, Cond, G)), % needed in VarDoms since e.g. X in [Y] unifies X=Y 209 call_comprehension(VDoms, [], [], Cond, G). 210 211 212 213var_domains(VarDomains, _VarDoms, _Condition) :- 214 var(VarDomains), 215 !, 216 must_be(nonvar,VarDomains). 217 218var_domains(Var where Condition, [Var], Condition) :- 219 var(Var), 220 !. 221 222var_domains(Vars in Domain where Condition, VarDoms, Condition) :- 223 !, 224 (var(Vars) 225 -> 226 VarDoms=[Vars in Domain] 227 ; 228 distribute(Vars, Domain, VarDoms)). 229 230var_domains(Vars in Domain, VarDoms, Condition) :- 231 !, 232 var_domains(Vars in Domain where true, VarDoms, Condition). 233 234var_domains(VarDomains where Condition, VarDomains, Condition) :- 235 !. 236 237var_domains(VarDomains, VarDoms, Condition) :- 238 must_be(list, VarDomains), 239 var_domains(VarDomains where true, VarDoms, Condition). 240 241 242variables([], []). 243variables([VarDom | VarDoms], [V | Vars]):- 244 (var(VarDom) 245 -> 246 V=VarDom 247 ; 248 VarDom = (V in _) 249 -> 250 must_be(var, V) 251 ; 252 must_be(var, VarDom) % instantiated variable 253 ), 254 variables(VarDoms, Vars). 255 256 257% allow only variables to distribute domain to. 258distribute([], _, []). 259distribute([Var | Vars], Domain, [Var in Domain | Domains]):- 260 must_be(var, Var), 261 distribute(Vars, Domain, Domains). 262 263 264 % GENERATOR COMPREHENSION 265 266 267% iteratively calls Goal on valuations of Vars in Domains satisfying a possibly non-deterministic where Condition 268% VarDomains is a list of (Var in Domain) terms 269% Vars and Values are built in reversed order 270call_comprehension([VarD | VarDomains], Vars, Values, Condition, Goal) :- 271 must_be(nonvar, VarD), 272 VarD = (V in VarDomain), 273 expand(VarDomain, VarDom), 274 (next_value(VarDom, Min, Greater) 275 -> 276 Vs = [V | Vars], 277 Vals = [Min | Values], 278 copy_term_nat([V], VarDomains, [Min], VarDoms), % partial evaluation 279 call_comprehension(VarDoms, Vs, Vals, Condition, Goal), % to append to next valuations 280 (Greater=[] 281 -> 282 true 283 ; 284 call_comprehension([V in Greater | VarDomains], Vars, Values, Condition, Goal) 285 ) 286 ; 287 true). 288 289call_comprehension([], Vars, Values, Condition, Goal) :- 290 copy_term_nat(Vars, Condition, Values, Cond), 291 (expand(Cond) % one great use of soft cut at last ! 292 *-> 293 copy_term_nat(Vars, Goal, Values, G), 294 G 295 ; 296 true). 297 298 299next_value(Min .. Max, Mi, Greater):- 300 Mi is Min, % shorthand expansions of domains are already done 301 Ma is Max, 302 (Mi < Ma 303 -> 304 Mi1 is Mi+1, 305 Greater = Mi1..Ma 306 ; 307 Mi = Ma, % otherwise fail, empty domain 308 Greater = []). 309 310next_value(Domain1 \/ Domain2, Min, Greater):- 311 next_value(Domain1, Min, Great), 312 (Great = [] 313 -> 314 Greater = Domain2 315 ; 316 Greater = Great \/ Domain2). 317 318next_value([Min | List], Mi, List):- 319 catch(evaluate(Min, Mi), _, Mi=Min). % just to allow non numerical values in a domain list 320 321 322 323 % LIST OF VALUATIONS DEFINED BY IN AND WHERE CONDITIONS

337list_of(VarDomains, Expr, List):- 338 aggregate_for(VarDomains, Expr, '[|]', [], =, List). 339 340 341 342 % GENERAL AGGREGATE_FOR PREDICATE 343 344%! aggregate_for(+VarDomains, +Expression, +Op, +E, +Relation, ?Term) 345% 346% true iff Relation(Term, Aggregate) holds where Aggregate is the application of binary operation Op with starting element E, 347% to all instances of Expression defined in comprehension by VarDomains with mandatory "in" domain and optional "where" condition. 348% An error is raised if a comprehension variable is instantiated (if it is attributed it is renamed without attributes). 349% 350% For example, list_of(VarDomains, Expression, List) is defined here by ``aggregate_for(VarDomains, Expression, [|], [], =, List)``. 351% 352% The instances of Expression are not evaluated unless Expression is of the form "Variable where Goal" in which case the Goal is executed. 353% It is an error if the first argument of where is not a variable. The variable is existentially quantified and renamed in the Goal. 354% 355% The list of arguments of a term could be defined by 356% == 357% ?- Term=f(a,g(X),Y), functor(Term, _, N), aggregate_for([I in 1..N], Arg where arg(I, Term, Arg), '[|]', [], =, Args). 358% Term = f(a, g(X), Y), 359% N = 3, 360% Args = [a, g(X), Y]. 361% == 362% 363% aggregate_for/6 is similar to foldl/4 but more general and using Goal pattern with arguments defined in comprehension. 364% 365% Used in library(clp) to define some hybrid global constraints. 366 367aggregate_for(VarDomains, Expression, Op, E, Relation, Term):- 368 (compound(Expression), Expression=(X where _Goal) 369 -> 370 must_be(var, X), 371 copy_term_nat([X], Expression, _, Expr) 372 ; 373 Expr=Expression), 374 var_domains(VarDomains, VarDoms, Condition), 375 variables(VarDoms, Vars), 376 copy_term_nat(Vars, f(VarDoms, Condition, Expr), Vs, f(VDoms, Cond, Exp)), % needed in VarDoms since X in [Y] unifies X=Y 377 values(VDoms, [], [], Cond, ValuesList), 378 aggregate_rec(ValuesList, Vs, Exp, Op, E, Aggregate), 379 Rel =.. [Relation, Term, Aggregate], 380 expand(Rel). 381 382aggregate_rec([], _, _, _, E, E). 383aggregate_rec([Values | ValuesList], Vars, Expression, Op, E, Term) :- 384 copy_term_nat(Vars, Expression, Values, Expr), 385 (compound(Expr), Expr=(X where _Goal) 386 -> 387 must_be(var, X), 388 copy_term_nat([X], Expr, _, Exp where Goal), 389 expand(Goal) % binding or constraining X in Expr renamed 390 ; 391 expand(Expr, Exp)), %Exp=Expr), 392 Term =.. [Op, Exp, Aggregate], % TODO do not construct the full aggregate_for expression 393 aggregate_rec(ValuesList, Vars, Expression, Op, E, Aggregate). 394 395 396% computes the List of valuations of Vars in Domains satisfying a, possibly non-deterministic, where Condition 397values([], Vars, Values, Condition, List):- 398 copy_term_nat(Vars, Condition, Values, Cond), 399 (expand(Cond) % one great use of soft cut at last ! 400 *-> 401 reverse(Values, Vals), 402 List=[Vals] 403 ; 404 List = []). 405 406values([VarD | VarDomains], Vars, Values, Condition, List):- 407 must_be(nonvar, VarD), 408 VarD = (V in VarDomain), 409 expand(VarDomain, VarDom), 410 (next_value(VarDom, Min, Greater) 411 -> 412 Vs = [V | Vars], 413 Vals = [Min | Values], 414 copy_term_nat([V], VarDomains, [Min], VarDoms), % partial evaluation 415 values(VarDoms, Vs, Vals, Condition, List1), % to append to next valuations 416 (Greater=[] 417 -> 418 List = List1 419 ; 420 values([V in Greater | VarDomains], Vars, Values, Condition, List2), 421 append(List1, List2, List)) 422 ; 423 List = []). 424 425 % EXISTENTIAL QUANTIFIER AND LET EXPRESSIONS

446let(Bindings, Goal):- 447 must_be(list, Bindings), 448 var_bindings(Bindings, Vars), 449 must_be(list(var), Vars), 450 copy_term_nat(Vars, f(Bindings, Goal), _, f(BindingsRenamed, GoalRenamed)), 451 bindings(BindingsRenamed), 452 GoalRenamed. 453 454 455:- multifile user:shorthand/3.

470user:shorthand(let(Bindings, Expr), Ex, (expand(Expr, Exp), let(Bindings, Ex=Exp))) :- !. 471 472 473 474% constrains the let variables 475 476bindings([]). 477bindings([Binding | Bindings]):- 478 (var(Binding) 479 -> 480 % allows using let/2 for unbound existentially quantified variables as in exists/2 481 bindings(Bindings) 482 ; 483 Binding =.. [Binder, X, Term], 484 must_be(var, X), 485 Goal =.. [Binder, X, Term], 486 (member(Binder, [=, is, =..]) 487 -> 488 expand(Goal) 489 ; 490 member(Binder, [in, ins, #=, #<==>, #<, #>, #=<, #>=, #\=]) % whatever makes sense for a let 491 -> 492 Goal 493 ; 494 throw(error(unauthorized_let_binder(Binding)))), 495 bindings(Bindings)). 496 497var_bindings([], []). 498var_bindings([Binding | Bindings], [X |Vars]) :- 499 (var(Binding) 500 -> 501 X=Binding 502 ; 503 compound(Binding), Binding =.. [_, X, _] 504 -> 505 must_be(var, X) 506 ; 507 throw(error(unauthorized_let_expression(Binding)))), 508 var_bindings(Bindings, Vars)