Yves Bekkers Universit'e de Rennes I and IRISA/INRIA Rennes, bekkers@irisa.fr Paul Tarau D'epartement d'Informatique, Universit'e de Moncton, tarau@info.umoncton.ca
% primitive operations % maps a single element of A to an object of the monad type unitList A -> (list A) -> o. unitList X [X]. % applies to a list an operation from elements to lists % to obtain a new list type bindList (list A)-> (A ->(list B)->o)-> (list B)-> o. bindList [] _K []. bindList [X|Xs] K R :- K X Ys, bindList Xs K Zs, append Ys Zs R. |
---|
% derived operations concatenates the elements of a list of lists type joinList (list (list A)) -> (list A) -> o joinList Xss Xs :- bindList Xss id Xs. % applies an operation to each element of a list type mapList (A->B->o) -> (list A) -> (list B) -> o. mapList F Xs Ys :- bindList Xs ( compose F unitList) Ys. |
---|
%tools type id A -> A ->o. id X X. % composes two predicates which implement functions type compose (A->B->o) -> (B->C->o) -> (A->C->o). compose F G X Y :- F X Z, G Z Y. type dupList A -> (list A) -> o. dupList X [X,X]. |
---|
%tools #define flistT(A) ((list A) -> (list A)) #define NIL x\x #define CONS x\l\u\ [x | (l u)] #define CONC l1\l2\x\ (l1 (l2 x)) |
---|
% primitive monad operations % primitive monad operations unitFlist X (CONS X NIL). type bindFlist flistT(A)->(A->flistT(B)->o)->flistT(B) -> o. bindFlist NIL _K NIL. bindFlist (CONS X Xs) K (CONC Ys Zs) :- K X Ys, bindFlist Xs K Zs. |
---|
% derived monad operations type joinFlist flistT(flistT(A)) -> flistT(A) -> o. joinFlist Xss Xs :- bindFlist Xss id Xs. type mapFlist (A->B->o) -> flistT(A) -> flistT(B) -> o. |
---|
By replacing the list constructor '.'/2 and terminator []/0 by nothr par we can generalize the list monad to a more general `constructor sequence' monad. Two widely used instances are:
The implementation of this monad is similar to that of the monads of lists and lazy function-lists. However, its correctness in the absence of occur check and the need for extra logical tests to detect `the end' of such lists make it less interesting especially when a concept of lazy function-list is available as it is the case with \lambdaProlog-Mali.
type list2flist (list A) -> flistT(A) -> o. list2flist L FL :- pi nil\ (append L nil (FL nil)). type flist2list flistT(A) -> (list A) -> o. flist2list F (F []). |
---|
Definition 1 Let A_0:-A_1,A_2,...,A_n and B_0:-B_1,...,B_m be two clauses (suppose n > 0, m >= 0). We define
(A_0:-A_1,A_2,...,A_n) <+> (B_0:-B_1,...,B_m) = (A_0:-B_1,...,B_m,A_2,...,A_n)\thetawith \theta = mgu( A_1,B_0). If the atoms A_1 and B_0 do not unify, the result of the composition is denoted as _|_.
unitClause(Cs,G,[A]):-A=(G:-[G]). joinClause(Cs,Gs,NewGs):- findall(NewG,expandClause(Cs,Gs,NewG),NewGs). expandClause(Cs,Gs,NewG):- member(G,Gs), member(C,Cs), composeClause(G,C,NewG). composeClause((H:-[]),_,(H:-[])). composeClause((H:-[B|Bs]),(B:-NewBs),(H:-Gs)):- append(NewBs,Bs,Gs). |
---|
kind prologT type. type pINT int -> prologT. joinClause(Cs,Gs,NewGs):- type pSTRUCT (list int) -> (list prologT) -> prologT. |
---|
app([],Ys,Ys). app([A|Xs],Ys,[A|Zs]) :- app(Xs,Ys,Zs). |
---|
becomes:
type demo prologT -> o. demo (pSTRUCT "app" [(pSTRUCT "[]" []),A,A]). demo (pSTRUCT "app" [(pSTRUCT "." [A,B]),C, (pSTRUCT "." [A,D])]) :- demo (pSTRUCT "app" [B,C,D]). |
---|
B_1 = {x|x E L & x} B_2 = {[x,y]|x E L_1 & y E L_2}
B1 <== (all x\ (x : (x <-- L, 1 is x mod 2))) B2 <== (all y\ (all x\ ([x, y] : (x <-- L1, y <-- L2)))) |
---|
lcT_\tau ::= (all variable\ lcT_\tau) | (term_\tau : qualifiers) qualifiers ::= qualifier | qualifier , qualifiers | qualifiers) qualifier ::= generator | filter generator ::= variable <-- list
Set comp. | List comp. -----------|----------- E | <-- | | : & | , = | <== |
kind lcT type -> type. type all (_B -> (lcT A)) -> (lcT A). type : A -> o -> (lcT A). |
---|
% -X <-- +Xs : X is an element of the list Xs type <-- X -> (list X) -> o. |
---|
type <== (list A) -> (lcT A) -> o. |
---|
Translating list comprehensions to lists with the list-monad P. Wadler [wadler:comprehending:lfp:90] gives a translation of list comprehensions into list-monad functions as follows:
[t|x<--L] = (map \lambda x -> t L) [t|(p,q)] = (join [[t|q]|p]) [t|true] = (unit t) [t|b] = (if b then [t] else [])
\exists _X \forall x
% X <== Lc : X is the simple list corresponding to % the comprehension list Lc Ys <== (all F) :- !, pi x\ (variable x _X => (Ys <== (F x))). Ys <== ((F U) : (U <-- Xs)) :- \+ (\+ (variable U F)), !, mapList x\ y\ (x <== y) Ys Xs, Zs <== (T : (P , Q)) :- !, Xs <== ((T : Q) : P), mapList x\ y\ (x <== y) Ys Xs, joinList Ys Zs. Ys <== (T : true) :- !, unitList T Ys. Ys <== (T : P) :- (P ? unitList T Ys ; Ys = []). |
---|
Figure 1: From list comprehensions to listsThe intuitionistic interpretation of such a declaration means that the signature of the logical variable _X does not contain the universal constant x. Hence, \lambdaProlog system, subsequently enforces that the substitution values for_X do not contain the universal constant x. This is fundamental for the rest of the interpretation, see further the interpretation of the generators <--.
type variable A -> (A -> B) -> o. dynamic variable. |
---|
Here are four examples of the use of list comprehensions:
Odds <== (all x\ (x : (x <-- L, 1 is x mod 2))) Pairs <== (all y\ (v x\ ([x, y] : (x <-- L1, y <-- L2)))) Pairs <== (all y\ (v x\ ([x, y] : (x <-- L1, y <-- L2, y =\= x)))) R <== (all c\ (all b\ (all a\ ([a,b,c] : (a <-- L, b <-- L, a < b, c <-- L; a*a + b*b =:= c*c))))) |
---|
Here is a quick sort program using list comprehensions.
% sort X Y : list Y is a sorted version of list X type sort (list A) -> (list A) -> o. sort [] []. sort [X | L] S :- Low <== (all y\ (y : (y <-- L , y < X))), sort Low SLow, Up <== (all y\ (y : (y <-- L , y > X))), sort Up SUp, append SLow [X | SUp] S. |
---|
type bagof (A->o) -> (list A) -> o. mode (setof +AbstractGoal ?SetOfSols) |
---|
type join (list (list T)) -> (list T) -> o. join Xss Ys :- bagof X\(sigma Xs\(member Xs Xss, member X Xs)) Ys. type map (A -> B -> o) -> (list A) -> (list B) -> o. map F Xs Ys :- bagof Y\(sigma X\(member X Xs, F X Y)) Ys. |
---|
map _ [] []. map F [X|Xs] [Y|Ys] :- F X Y, map F Xs Y |
---|
Xs=[A,B,B,A], map unit Xs Zs.will return Zs=[[A],[B],[B],[A]].
% get_list +Lc -Goal type get_list (lcT A) -> (A -> o) -> o. get_list (all F) y\ (sigma x\ (R x y)) :- !, pi x\ (get_list (F x) y\ (R x y)). get_list (T : P) x\ (x = T, P). X <-- Xs :- member X Xs. Ys <== P :- get_list P G, bagof G Ys. |
---|