1/*
    2  quantifiers.pl
    3  
    4  @author Francois Fages
    5  @email Francois.Fages@inria.fr
    6  @license LGPL-2
    7
    8@author Francois Fages
    9@version 1.1.0  
   10
   11  Bounded quantifiers, let expressions and shorthand notations.
   12  
   13*/
   14
   15
   16:- module(
   17	  quantifiers,
   18	  [
   19	   for_all/2,
   20	   exists/2,
   21	   let/2,
   22
   23	   list_of/2,
   24
   25	   apply_list/2,
   26	   call_list/2,
   27	   call_list/3,
   28	   call_list/4,
   29	   call_list/5,
   30	   call_list/6,
   31
   32	   expand/2,
   33	   expand/1,
   34	   evaluate/2,
   35	   
   36	   indent_term/1,
   37	   
   38	   op(501, xfx, ..),
   39	   op(502, yfx, \/),
   40	   
   41	   op(700, xfx, in),
   42	   op(990, xfx, where)
   43	  ]).

Bounded quantifiers, let expressions, and expandable shorthand notations.

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].

*/

  102				% CONJUNCTIVE APPLICATION OF A GOAL TO ARGUMENTS IN LISTS
  103
  104:- meta_predicate apply_list(1, ?).
 apply_list(+Goal, +ArgsList)
Conjunctive application of Goal to list ArgsList of arguments. Fails if the conjunction is not satisfiable.
  110apply_list(Goal, ArgsList):-
  111    list_apply(ArgsList, Goal).
  112
  113
  114list_apply([], _).
  115list_apply([Args | ArgsList], Goal):-
  116    apply(Goal, Args),
  117    list_apply(ArgsList, Goal).
  118
  119
  120:- meta_predicate call_list(1, ?).  121:- meta_predicate call_list(2, ?, ?).  122:- meta_predicate call_list(3, ?, ?, ?).  123
  124:- meta_predicate list_call(?, 1).  125:- meta_predicate list_call(?, ?, 2).  126:- meta_predicate list_call(?, ?, ?, 3).
 call_list(+Goal, ?Args)
More efficient conjunctive application of a unary Goal to each argument in list Args.
  132call_list(Goal, Args1):-
  133    list_call(Args1, Goal).
  134
  135list_call([], _).
  136list_call([Arg1 | Args1], Goal):-
  137    call(Goal, Arg1),
  138    list_call(Args1, Goal).
 call_list(+Goal, ?Args1, ?Args2)
Conjunctive application of a binary Goal to the arguments in lists Args1, Args2.
  145call_list(Goal, Args1, Args2):-
  146    list_call(Args1, Args2, Goal).
  147
  148list_call([], [], _).
  149list_call([Arg1 | Args1], [Arg2 | Args2], Goal):-
  150    call(Goal, Arg1, Arg2),
  151    list_call(Args1, Args2, Goal).
 call_list(+Goal, ?Args1, ?Args2, ?Args3)
Conjunctive application of a ternary Goal to the arguments in lists Args1, Args2, Args3.
  159call_list(Goal, Args1, Args2, Args3):-
  160    list_call(Args1, Args2, Args3, Goal).
  161
  162list_call([], [], [], _).
  163list_call([Arg1 | Args1], [Arg2 | Args2], [Arg3 | Args3], Goal):-
  164    call(Goal, Arg1, Arg2, Arg3),
  165    list_call(Args1, Args2, Args3, Goal).
 call_list(+Goal, ?Args1, ?Args2, ?Args3, ?Args4)
Conjunctive application of a 4-ary Goal.
  172call_list(Goal, Args1, Args2, Args3, Args4):-
  173    list_call(Args1, Args2, Args3, Args4, Goal).
  174
  175list_call([], [], [], [], _).
  176list_call([Arg1 | Args1], [Arg2 | Args2], [Arg3 | Args3], [Arg4 | Args4], Goal):-
  177    call(Goal, Arg1, Arg2, Arg3, Arg4),
  178    list_call(Args1, Args2, Args3, Args4, Goal).
 call_list(+Goal, ?Args1, ?Args2, ?Args3, ?Args4, ?Args5)
Conjunctive application of a 5-ary Goal.
  185call_list(Goal, Args1, Args2, Args3, Args4, Args5):-
  186    list_call(Args1, Args2, Args3, Args4, Args5, Goal).
  187
  188list_call([], [], [], [], [], _).
  189list_call([Arg1 | Args1], [Arg2 | Args2], [Arg3 | Args3], [Arg4 | Args4], [Arg5 | Args5], Goal):-
  190    call(Goal, Arg1, Arg2, Arg3, Arg4, Arg5),
  191    list_call(Args1, Args2, Args3, Args4, Args5, Goal).
  192
  193
  194
  195				% BOUNDED UNIVERSAL QUANTIFIER
 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.
  204for_all(VarDomains, Goal) :-
  205    var_domains(VarDomains, VarDoms, Condition),
  206    for_list(VarDoms, [], [], Condition, Goal).
  207
  208
  209
  210				% LIST OF INSTANCES DEFINED BY IN AND WHERE CONDITIONS
 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.
  218list_of(VarDomains, Values):-
  219    var_domains(VarDomains, VarDoms, Condition),
  220    list_list(VarDoms, [], [], Condition, Values).
  221
  222
  223
  224var_domains(VarDomains, _VarDoms, _Condition) :-
  225    var(VarDomains),
  226    !,
  227    must_be(nonvar,VarDomains). % bounded quantification only
  228
  229var_domains(VarDomains where _Condition, _VarDoms, _Cond) :-
  230    var(VarDomains),
  231    !,
  232    must_be(nonvar, VarDomains).
  233
  234var_domains(Vars in Domain where Condition, VarDoms, Condition) :-
  235    !,
  236    (var(Vars)
  237    ->
  238     VarDoms=[Vars in Domain]
  239    ;
  240     distribute(Vars, Domain, VarDoms)).
  241
  242var_domains(VarDomains where Condition, VarDomains, Condition) :-
  243    !.
  244
  245var_domains(Vars in Domain, VarDoms, Condition) :-
  246    !,
  247    var_domains(Vars in Domain where true, VarDoms, Condition).
  248
  249var_domains(VarDomains, VarDoms, Condition) :-
  250    var_domains(VarDomains where true, VarDoms, Condition).
  251
  252
  253
  254distribute([], _, []).
  255distribute([Var | Vars], Domain, [Var in Domain | Domains]):-
  256    distribute(Vars, Domain, Domains).
  257
  258
  259for_list([], Vars, Values, Condition, Goal):-
  260    copy_term(Vars, Condition, Values, Cond),
  261    expand(Cond, C),
  262    (\+ C			% condition satisfiability test only 
  263    ->
  264     true
  265    ;
  266     copy_term(Vars, Goal, Values, G), % no shorthand expansion for the goal
  267     G				       % backtrackable goal
  268    ).
  269    
  270
  271for_list([D | Domains], Vars, Values, Condition, Goal):-
  272    must_be(nonvar, D),
  273    D = (V in Domain),
  274    expand(Domain, Dom),
  275    (next_value(Dom, Min, Greater)
  276    ->
  277     Vs = [V | Vars],
  278     Vals = [Min | Values],
  279     %copy_term(Vs, Domains, Vals, Doms),
  280     copy_term([V], Domains, [Min], Doms),
  281     for_list(Doms, Vs, Vals, Condition, Goal),
  282     (Greater=[]
  283     ->
  284      true
  285     ;
  286      for_list([V in Greater | Domains], Vars, Values, Condition, Goal))
  287    ;
  288     true).			% V has an empty domain
  289
  290
  291list_list([], Vars, Values, Condition, List):-
  292    copy_term(Vars, Condition, Values, Cond),
  293    expand(Cond, C),
  294    (\+ C			% scondition atisfiability test only
  295    ->
  296     List=[]
  297    ;
  298     List=Values
  299    ).
  300
  301list_list([D | Domains], Vars, Values, Condition, List):-
  302    must_be(nonvar, D),
  303    D = (V in Domain),
  304    expand(Domain, Dom),
  305    (next_value(Dom, Min, Greater)
  306    ->
  307     Vs = [V | Vars],
  308     Vals = [Min | Values],
  309     copy_term([V], Domains, [Min], Doms),
  310     list_list(Doms, Vs, Vals, Condition, List1), % to append 
  311     (Greater=[]
  312     ->
  313      List = List1
  314     ;
  315      list_list([V in Greater | Domains], Vars, Values, Condition, List2),
  316      append(List1, List2, List))
  317    ;
  318     List = []). 
  319
  320
  321next_value(Min .. Max, Mi, Greater):-
  322    Mi is Min, % shorthand expansions of domains are already done
  323    Ma is Max,
  324    (Mi < Ma
  325    ->
  326     Mi1 is Mi+1,
  327     Greater = Mi1..Ma
  328    ;
  329     Mi = Ma, % otherwise fail, empty domain
  330     Greater = []).
  331
  332next_value(Domain1 \/ Domain2, Min, Greater):-
  333    nextvalue(Domain1, Min, Great),
  334    (Great = []
  335    ->
  336     Greater = Domain2
  337    ;
  338     Greater = Great \/ Domain2).
  339
  340next_value([Min | List], Mi, List):-
  341    catch(evaluate(Min, Mi), _, Mi=Min).
  342
  343
  344				% EXISTENTIAL QUANTIFIER AND LET EXPRESSIONS
 exists(+Vars, +Goal)
calls Goal with existentially quantified variables Vars.
  350exists(Vars, Goal):- 
  351    copy_term(Vars, Goal, _, RenamedGoal),
  352    RenamedGoal.
 let(+Bindings, +Goal)
calls Goal with Bindings for existentially quantified variables bound to expressions allowing shorthand/3 notations.
  360let(Bindings, Goal):-
  361    var_bindings(Bindings, Vars),
  362    copy_term(Vars, f(Bindings, Goal), _, f(BindingsRenamed, GoalRenamed)),
  363    bindings(BindingsRenamed),
  364    GoalRenamed.
  365
  366
  367var_bindings([], []).
  368var_bindings([Binding | Bindings], [X |Vars]) :-
  369    (var(Binding)
  370    ->
  371     X=Binding
  372    ;
  373     Binding =.. [_, X, _]
  374    ),
  375    var_bindings(Bindings, Vars).
  376
  377
  378% instantiates the let variables
  379
  380bindings([]).
  381    
  382bindings([Binding | Bindings]):-
  383    (var(Binding)
  384    ->
  385     % allows using let/2 for unbound existentially quantified variables as in exists/2
  386     bindings(Bindings)
  387    ;
  388     Binding =.. [Binder, X, Term],
  389     must_be(var, X),
  390     member(Binder, [=, is, =.., in, ins, #=, #<, #>, #=<, #>=, #\=]), % whatever makes sense for a let
  391     !,
  392     expand(Term, Expr),
  393     Goal =.. [Binder, X, Expr],
  394     Goal,
  395     bindings(Bindings)).
  396
  397
  398				% GENERAL PURPOSE SHORTHAND NOTATION FACILITY
  399
  400
  401:- multifile shorthand/3.
 shorthand(+Term, +Expanded, +Goal)
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.
  409shorthand(if(Condition, Expr1, Expr2), Var, (Condition -> Var=Expr1 ; Var=Expr2)) :-
  410    !.
  411
  412% Possible additional definition for expanding global variables with numeric values
  413%
  414% shorthand(Atom, Value):-
  415%     atom(Atom),
  416%     catch(nb_getval(Atom, Value), _, fail),
  417%     number(Value),
  418%     !.
 expand(+Term, ?Expanded)
expands a Term according to multifile shorthand/3 definitions.
  425expand(Term, Expr):-
  426    (var(Term)
  427    ->
  428     Expr=Term
  429    ;
  430     (shorthand(Term, T, Goal)
  431     ->
  432      Goal
  433     ;
  434      T=Term),
  435     expand_subterms(T, Expr)
  436    ).
  437
  438
  439expand_subterms(Term, Expanded):-
  440    (compound(Term)
  441    ->
  442     (Term=[T | Tail]
  443     ->
  444      Expanded=[ET | ETail],
  445      expand_subterms(T, ET),
  446      expand_subterms(Tail,ETail)
  447     ;
  448      Term =.. [F | Subterms],
  449      call_list(expand, Subterms, ExpandedSubterms),
  450      Expanded =.. [F | ExpandedSubterms]
  451     )
  452    ;
  453     Expanded=Term
  454    ).
 expand(+Goal)
expands and call a Goal according to multifile shorthand/3 definitions.
  461expand(Goal) :-
  462    expand(Goal, G),
  463    G.
 evaluate(+Expr, ?Number)
evaluates an arithmetic expression with shorthand/3 notations.
  470evaluate(Expr, Number):-
  471    expand(Expr, E),
  472    Number is E.
  473
  474
  475
  476				% EXAMPLE OF USE FOR DEFINING indent_term/1
 indent_term(+Term)
Just an example of use of quantifiers to pretty print the tree structure of a term.
  482indent_term(T):-
  483    indent_term(0, T).
  484
  485indent_term(N, Term):-
  486    for_all(_ in 1..N, write(' ')),
  487    (
  488     compound(Term)
  489    ->
  490     functor(Term, F, A),
  491     writeln(F),
  492     N1 is N+1,
  493     for_all(I in 1..A, exists([Ti], (arg(I, Term, Ti), indent_term(N1, Ti))))
  494    ;
  495     writeln(Term)
  496    )