elp0 1

Higher-Order Programming: in ML

fun filter prop [] = []
| filter prop (a::tl) =
         if (prop a)
 then a::(filter prop tl)
 else filter prop tl;

elp0 2

Higher-Order Programming: in Prolog

even(0).
even(X) :- 0<X,Y is X-2,even(Y).

filter(Prop,[],[]).
filter(Prop, [X|Xs],[X|Ys]) :- W =.. [Prop,X],
        call(W),
        filter(Prop,Xs,Ys).
filter(Prop,[X|Xs],Ys) :- filter(Prop,Xs,Ys).

Higher-Order Programming

module filter.
import lists.
kind nums      type.
type z         nums.
type s         nums -> nums.
type s_even    nums -> o.
type even      int -> o.
type trip      int -> int -> o.
type filter    (A -> o) -> list A -> list A -> o.
type mappred   (A -> B  -> o) -> list A -> list B -> o.
type compose   (A -> A  -> o) -> (A -> A -> o) -> nums -> nums -> o.
type triple    nums -> nums -> o.
type double    nums -> nums -> o.

elp0 4

   higher-order predicates (cont.)
double z z.
double (s X) (s (s Y)) :- double X Y.
triple z z.
triple (s X) (s (s (s Y))) :- triple X Y.
trip X Y :- Y is (3 * X).
even 0.
even X :- 0 < X, Y is X - 2, even Y.
s_even z.
s_even (s (s X)) :- s_even X.

     filter, map, compose (cont.)
filter Prop nil nil.
filter Prop (H :: T)  (H :: T1) :-
        Prop H, filter Prop T T1.
filter Prop (H :: T)  T1 :-
        filter Prop T T1.
mappred Prop nil nil.
mappred Prop (H :: T) (K :: S) :- Prop H K,
         mappred Prop T S.

compose P1 P2 X Y :- P2 X Z, P1 Z Y.

elp0 6

Some sample Queries

?- load "filter".
?- use "filter".
?- filter even
         (1::(2::(3::(4::(5::(6::(7::(8::nil)))))))) L.
L = 2 :: 4 :: 6 :: 8 :: nil.
?- mappred trip
          (1::(2::(3::(4::(5::(6::(7::(8::nil)))))))) L.
L = 3 :: 6 :: 9 :: 12 :: 15 :: 18 :: 21 :: 24 :: nil.
yes

elp0 7

λ-prolog examples (cont.)

?- mappred triple
     ( s(z)::( s(s(z))::( s(s(s(s(z))))::( s(z)::nil)))) L.
L =
   s (s (s z)) :: s (s (s (s (s (s z)))))
      :: s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))
      :: s (s (s z)) :: nil.
?- compose double triple (s z) N.
N = s (s (s (s (s (s z))))).

elp0 8

Hypothetical Implication

Assume we have a database describing a graph:

  edge(a,b).
  edge(b,c).
  edge(f,e).
  edge(e,d).

and the usual code for conn:

conn(X,X).
conn(X,Y) :- edge(X,Z),con(Z,Y).

elp0 9

Hypothetical queries in prolog

How do we test some hypotheses, such as if c and e were connected would a and d be as well?

  ?- assert(edge(c,e)),conn(a,d),retract(edge(c,e)).

Solution in λProlog

kind node type.
type a,b,c,d,e,f node.
type edge node -> node -> o.
type conn node -> node -> o.
  edge a b.
  edge b c.
  edge f e.
  edge e d.
  conn X X.
  conn X Y :- edge X Z,
              conn Z Y.

The required query is:

 ?- edge c e => conn a d.
solved
 ?- edge c e => conn a X.
X = a.
;
X = b.

elp0 11

;
X = c.
;
X = e.
;
X = d.
:
no more solutions
?-