Pack modeling -- prolog/quantifiers.pl

author

- Francois Fages

version

- 1.1.0

This module defines bounded quantifiers, let expressions, and a multifile predicate to create new shorthand notations.

for_all/2 bounded universal quantifier with "in" domain and "where" conditions allowing shorthand/3 notations, e.g. Array[Indices] notation for subscripted variables defined in library(arrays). The "in" domain must be a finite (union) interval of integers or a list of values. The "where" condition goal is supposed to be deterministic and just checked for satisfiability without constraining context's variables.

list_of/2 list of values satisfying "in" and "where" conditions.

exists/2 existential quantifier.

let/2 existential quantifier for variables bound to expressions allowing shorthand/3 notations.

apply_list/2, call_list/2, /3/4/5 conjunctive application of a goal on a list of arguments.

indent_term/1 just one example of use of quantifiers to pretty print the tree structure of a term.

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

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

The "where" condition is a test of satisfiability, not of entailment. The example below illustrates the difference: X=Y is satisfiable for all X, Y hence the goal is executed for all X, Y, while in the fourth query, the condition X==Y is always false hence no constraint is posted:

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

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

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

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

apply_list(+Goal, +ArgsList): Conjunctive application of Goal to list ArgsList of arguments. Fails if the conjunction is not satisfiable.
call_list(+Goal, ?Args): More efficient conjunctive application of a unary Goal to each argument in list Args.
call_list(+Goal, ?Args1, ?Args2): Conjunctive application of a binary Goal to the arguments in lists Args1, Args2.
call_list(+Goal, ?Args1, ?Args2, ?Args3): Conjunctive application of a ternary Goal to the arguments in lists Args1, Args2, Args3.
call_list(+Goal, ?Args1, ?Args2, ?Args3, ?Args4): Conjunctive application of a 4-ary Goal.
call_list(+Goal, ?Args1, ?Args2, ?Args3, ?Args4, ?Args5): Conjunctive application of a 5-ary Goal.
for_all(+VarDomains, +Goal): executes universally quantified Goal for all variables values with "in" and "where" conditions in VarDomains. The "where" condition is a deterministic test of satisfiability, not of entailment. for_all/2 is non-deterministic only if the Goal is non-deterministic.
list_of(+VarDomains, ?Values): Values is the list of tuple values for the variables in VarDomains specified with "in" domains and "where" conditions. The "where" condition is a deterministic test of satisfiability, not of entailment.
exists(+Vars, +Goal): calls Goal with existentially quantified variables Vars.
let(+Bindings, +Goal): calls Goal with Bindings for existentially quantified variables bound to expressions allowing shorthand/3 notations.
shorthand(+Term, +Expanded, +Goal)[multifile]: Multifile user-defined predicate to define a shorthand Expanded for Term by executing Goal at runtime (unlike compile time macros). Defined here for conditional expression if/3 in let/2 bindings and in for_all/2 list_of/2 "in" domains and "where" conditions, and in other modules like library(arrays) for defining shorthand Array[Indices] for subscripted variables.
expand(+Term, ?Expanded): expands a Term according to multifile shorthand/3 definitions.
expand(+Goal): expands and call a Goal according to multifile shorthand/3 definitions.
evaluate(+Expr, ?Number): evaluates an arithmetic expression with shorthand/3 notations.
indent_term(+Term): Just an example of use of quantifiers to pretty print the tree structure of a term.