elp1 1

Some sample programs in lambda-prolog

An example of hypothetical implication: the British Citizen program.

  module hyp.

kind person     type.
type citizen person -> o.
type alive person -> o.
type born_eng person -> o.
type father     person -> person -> o.

type joe person.
type fred person.
type mary person.
type juan person.
father juan mary.
father fred joe.
alive joe.
alive mary.
born_eng fred.
citizen X :- alive X, born_eng X.
citizen X :- father Y X, (alive Y => citizen Y).

elp1 3

A session with the hyp module

  nec%elp
Standard ML of New Jersey, Version 0.93, February 15, 1993
Elp, Version 0.1x, Built: Thu Jan 11 17:49:29 GMT-0500 1996
?- load "hyp".
[reading file ./hyp.mod]
person : type.
citizen : person -> o.
alive : person -> o.
born_eng : person -> o.
father : person -> person -> o.
joe : person.
fred : person.
mary : person.
juan : person.
[closed file ./hyp.mod]
solved
yes

elp1 4

?- use "hyp".
?- alive joe.
solved
yes
?- citizen joe.
solved
yes
?- citizen mary.
no
?- (born_eng juan => citizen mary).
solved

Some Queries

The list module:

  %% $Id: lists.mod,v 1.1 1992/01/14 20:59:12 felty Exp $
module lists.
type memb A -> list A -> o.
type member A -> list A -> o.
type append list A -> list A -> list A -> o.
type join list A -> list A -> list A -> o.
type    memb_and_rest   A -> list A -> list A -> o.
type    nth_item        int -> A -> list A -> o.
type    nth_and_rest    int -> A -> list A -> list A -> o.
doc memb
 "``memb X L'' succeeds if X is a member of L.  In contrast to ``member'',
this will succeed as often as X unifies with members of L.".
index memb 2.

memb X (X :: L).
memb X (Y :: L) :- memb X L.
doc member
"``member X L'' succeeds if X is a member of L.  In contrast to ``memb'',
this will succeed only once: for the first unifier of X with a member of L.".
index member 2.
member X (X :: L) :- !.
member X (Y :: L) :- member X L.
doc append
"``append L K M'' succeeds if M is the result of appending K to L.".
index append 1.

elp1 7

append nil K K.
append (X :: L) K (X :: M) :- append L K M.
doc join
 "``join L K M'' is similar to append except that members of L that already
appear in K are not appended to form M.  Note that this `check' will do
unification!".
index join 1.
join nil K K.
join (X :: L) K M :- memb X K, !, join L K M.
join (X :: L) K (X :: M) :- join L K M.
doc memb_and_rest
 "``memb_and_rest X L M'' succeeds for every occurrence of X in L,
where M is the result of removing that occurrence from L.".
memb_and_rest A (A :: Rest) Rest.

memb_and_rest A (B :: Tail) (B :: Rest) :- memb_and_rest A Tail Rest.
doc nth_item
 "``nth_item N X L'' succeeds if the Nth item of L is X, where
counting starts at 1.  For N = 0 it behaves like ``memb''.".
nth_item 0 A List :- !, memb A List.
nth_item 1 A (B::Rest) :- !, A = B.
nth_item N A (B::Tail) :- M is (N - 1), nth_item M A Tail.
doc nth_and_rest
 "``nth_and_rest N X L Rest'' succeeds if the Nth item of L is X, and
Rest is the rest of L.  Counting starts at 1.  For N = 0, it behaves
like memb_and_rest.".
nth_and_rest 0 A List Rest :- !, memb_and_rest A List Rest.
nth_and_rest 1 A (B::Rest) Rest :- !, A = B.
nth_and_rest N A (B::Tail) (B::Rest) :-
  M is (N - 1), nth_and_rest M A Tail Rest.

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.

elp1 10

   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.

elp1 12

Some sample Queries

?- filter even
         (1::(2::(3::(4::(5::(6::(7::(8::nil)))))))) L.
L = 2 :: 4 :: 6 :: 8 :: nil.
yes
?-
?- mappred trip
          (1::(2::(3::(4::(5::(6::(7::(8::nil)))))))) L.
L = 3 :: 6 :: 9 :: 12 :: 15 :: 18 :: 21 :: 24 :: nil.
yes
?- 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)))))

elp1 13

      :: 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))))).
yes
?-