home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / prolog / brklyprl.lha / Emulator / Tests / dboyer.pl < prev    next >
Encoding:
Text File  |  1989-04-14  |  9.0 KB  |  409 lines
  1.  
  2. /* Copyright (C) 1988, 1989 Herve' Touati, Aquarius Project, UC Berkeley */
  3.  
  4. /* Copyright Herve' Touati, Aquarius Project, UC Berkeley */
  5.  
  6. %------------------------------------------------------------------------------
  7. %    Benchmark Program - Boyer
  8. %    Lisp vs. Prolog Study
  9. %
  10. %    Copyright by Evan Tick
  11. %    Date: November 12 1985
  12. %
  13. %------------------------------------------------------------------------------
  14.  
  15. main :-    wff(X),tautology(X).
  16.  
  17. wff(implies(and(implies(X,Y),
  18.         and(implies(Y,Z),
  19.             and(implies(Z,U),
  20.             implies(U,W)))),
  21.         implies(X,W))) :-
  22.     X = f(plus(plus(a,b),plus(c,zero))),
  23.     Y = f(times(times(a,b),plus(c,d))),
  24.     Z = f(reverse(append(append(a,b),[]))),
  25.     U = equal(plus(a,b),difference(x,y)),
  26.     W = lessp(remainder(a,b),member(a,length(b))).
  27.  
  28. tautology(Wff) :-
  29.     write('rewriting...'),nl,
  30.     rewrite(Wff,NewWff),
  31.     write('proving...'),nl,
  32.     tautology(NewWff,[],[]).
  33.  
  34. tautology(Wff,Tlist,Flist) :-
  35.     (truep(Wff,Tlist) -> true
  36.     ;falsep(Wff,Flist) -> fail
  37.     ;Wff = if(If,Then,Else) ->
  38.         (truep(If,Tlist) -> tautology(Then,Tlist,Flist)
  39.         ;falsep(If,Flist) -> tautology(Else,Tlist,Flist)
  40.         ;tautology(Then,[If|Tlist],Flist),    % both must hold
  41.          tautology(Else,Tlist,[If|Flist])
  42.         )
  43.     ),!.
  44.  
  45. rewrite(Atom,Atom) :-
  46.     atomic(Atom),!.
  47. rewrite(Old,New) :-
  48.     functor(Old,F,N),
  49.     functor(Mid,F,N),
  50. %    rewrite_args(N,Old,Mid),
  51.     Old =.. [_|OldArgs],
  52.     rewrite_args(OldArgs,1,Mid),
  53.     ( equal(Mid,Next),    % should be ->, but is compiler smart enough?
  54.       rewrite(Next,New)    % to generate cut for ->?
  55.     ; New=Mid
  56.     ),!.
  57.  
  58. %rewrite_args(0,_,_) :- !.
  59. %rewrite_args(N,Old,Mid) :- 
  60. %    arg(N,Old,OldArg),
  61. %    arg(N,Mid,MidArg),
  62. %    rewrite(OldArg,MidArg),
  63. %    N1 is N-1,
  64. %    rewrite_args(N1,Old,Mid).
  65. rewrite_args([],_,_) :- !.
  66. rewrite_args([Arg|Args],N,Mid) :-
  67.     rewrite(Arg,NewArg),
  68.     arg(N,Mid,NewArg),
  69.     N1 is N+1,
  70.     rewrite_args(Args,N1,Mid).
  71.  
  72. truep(t,_) :- !.
  73. truep(Wff,Tlist) :- member(Wff,Tlist).
  74.  
  75. falsep(f,_) :- !.
  76. falsep(Wff,Flist) :- member(Wff,Flist).
  77.  
  78. member(X,[X|_]) :- !.
  79. member(X,[_|T]) :- member(X,T).
  80.  
  81.  
  82. equal(    and(P,Q),            % 106 rules
  83.     if(P,if(Q,t,f),f)
  84.     ).
  85. equal(    append(append(X,Y),Z),
  86.     append(X,append(Y,Z))
  87.     ).
  88. equal(    assignment(X,append(A,B)),
  89.     if(assignedp(X,A),
  90.        assignment(X,A),
  91.        assignment(X,B))
  92.     ).
  93. equal(    assume_false(Var,Alist),
  94.     cons(cons(Var,f),Alist)
  95.     ).
  96. equal(    assume_true(Var,Alist),
  97.     cons(cons(Var,t),Alist)
  98.     ).
  99. equal(    boolean(X),
  100.     or(equal(X,t),equal(X,f))
  101.     ).
  102. equal(    car(gopher(X)),
  103.     if(listp(X),
  104.        car(flatten(X)),
  105.        zero)
  106.     ).
  107. equal(    compile(Form),
  108.     reverse(codegen(optimize(Form),[]))
  109.     ).
  110. equal(    count_list(Z,sort_lp(X,Y)),
  111.     plus(count_list(Z,X),
  112.          count_list(Z,Y))
  113.     ).
  114. equal(    countps_(L,Pred),
  115.           countps_loop(L,Pred,zero)
  116.     ).
  117. equal(    difference(A,B),
  118.     C
  119.     ) :- difference(A,B,C).
  120. equal(    divides(X,Y),
  121.     zerop(remainder(Y,X))
  122.     ).
  123. equal(    dsort(X),
  124.     sort2(X)
  125.     ).
  126. equal(    eqp(X,Y),
  127.     equal(fix(X),fix(Y))
  128.     ).
  129. equal(    equal(A,B),
  130.     C
  131.     ) :- eq(A,B,C).
  132. equal(    even1(X),
  133.     if(zerop(X),t,odd(decr(X)))
  134.     ).
  135. equal(    exec(append(X,Y),Pds,Envrn),
  136.     exec(Y,exec(X,Pds,Envrn),Envrn)
  137.     ).
  138. equal(    exp(A,B),
  139.     C
  140.     ) :- exp(A,B,C).
  141. equal(    fact_(I),
  142.     fact_loop(I,1)
  143.     ).
  144. equal(    falsify(X),
  145.     falsify1(normalize(X),[])
  146.     ).
  147. equal(    fix(X),
  148.     if(numberp(X),X,zero)
  149.     ).
  150. equal(    flatten(cdr(gopher(X))),
  151.     if(listp(X),
  152.        cdr(flatten(X)),
  153.        cons(zero,[]))
  154.     ).
  155. equal(  gcd(A,B),
  156.     C
  157.     ) :- gcd(A,B,C).
  158. equal(    get(J,set(I,Val,Mem)),
  159.     if(eqp(J,I),Val,get(J,Mem))
  160.     ).
  161. equal(    greatereqp(X,Y),
  162.     not(lessp(X,Y))
  163.     ).
  164. equal(    greatereqpr(X,Y),
  165.     not(lessp(X,Y))
  166.     ).
  167. equal(    greaterp(X,Y),
  168.     lessp(Y,X)
  169.     ).
  170. equal(    if(if(A,B,C),D,E),
  171.     if(A,if(B,D,E),if(C,D,E))
  172.     ).
  173. equal(    iff(X,Y),
  174.     and(implies(X,Y),implies(Y,X))
  175.     ).
  176. equal(    implies(P,Q),
  177.     if(P,if(Q,t,f),t)
  178.     ).
  179. equal(    last(append(A,B)),
  180.     if(listp(B),
  181.        last(B),
  182.        if(listp(A),
  183.           cons(car(last(A))),
  184.           B))
  185.     ).
  186. equal(    length(A),
  187.     B
  188.     ) :- mylength(A,B).
  189. equal(    lesseqp(X,Y),
  190.     not(lessp(Y,X))
  191.     ).
  192. equal(    lessp(A,B),
  193.     C
  194.     ) :- lessp(A,B,C).
  195. equal(    listp(gopher(X)),
  196.     listp(X)
  197.     ).
  198. equal(    mc_flatten(X,Y),
  199.     append(flatten(X),Y)
  200.     ).
  201. equal(    meaning(A,B),
  202.     C
  203.     ) :- meaning(A,B,C).
  204. equal(  member(A,B),
  205.     C
  206.     ) :- mymember(A,B,C).
  207. equal(    not(P),
  208.     if(P,f,t)
  209.     ).
  210. equal(  nth(A,B),
  211.     C
  212.     ) :- nth(A,B,C).
  213. equal(    numberp(greatest_factor(X,Y)),
  214.     not(and(or(zerop(Y),equal(Y,1)),
  215.         not(numberp(X))))        
  216.     ).
  217. equal(    or(P,Q),
  218.     if(P,t,if(Q,t,f),f)
  219.     ).
  220. equal(  plus(A,B),
  221.     C
  222.     ) :- plus(A,B,C).
  223. equal(  power_eval(A,B),
  224.     C
  225.     ) :- power_eval(A,B,C).
  226. equal(    prime(X),
  227.     and(not(zerop(X)),
  228.         and(not(equal(X,add1(zero))),
  229.             prime1(X,decr(X))))
  230.     ).
  231. equal(    prime_list(append(X,Y)),
  232.     and(prime_list(X),prime_list(Y))
  233.     ).
  234. equal(  quotient(A,B),
  235.     C
  236.     ) :- quotient(A,B,C).
  237. equal(  remainder(A,B),
  238.     C
  239.     ) :- remainder(A,B,C).
  240. equal(    reverse_(X),
  241.     reverse_loop(X,[])
  242.     ).
  243. equal(    reverse(append(A,B)),
  244.     append(reverse(B),reverse(A))
  245.     ).
  246. equal(    reverse_loop(A,B),
  247.     C
  248.     ) :- reverse_loop(A,B,C).
  249. equal(    samefringe(X,Y),
  250.     equal(flatten(X),flatten(Y))
  251.     ).
  252. equal(    sigma(zero,I),
  253.     quotient(times(I,add1(I)),2)
  254.     ).
  255. equal(    sort2(delete(X,L)),
  256.     delete(X,sort2(L))
  257.     ).
  258. equal(    tautology_checker(X),
  259.     tautologyp(normalize(X),[])
  260.     ).
  261. equal(  times(A,B),
  262.     C
  263.     ) :- times(A,B,C).
  264. equal(    times_list(append(X,Y)),
  265.     times(times_list(X),times_list(Y))
  266.     ).
  267. equal(    value(normalize(X),A),
  268.     value(X,A)
  269.     ).
  270. equal(    zerop(X),
  271.     or(equal(X,zero),not(numberp(X)))
  272.     ).
  273.  
  274. difference(X,            X,        zero        ) :- !.
  275. difference(plus(X,Y),        X,        fix(Y)        ) :- !.
  276. difference(plus(Y,X),        X,        fix(Y)        ) :- !.
  277. difference(plus(X,Y),        plus(X,Z),    difference(Y,Z)    ) :- !.
  278. difference(plus(B,plus(A,C)),    A,        plus(B,C)    ) :- !.
  279. difference(add1(plus(Y,Z)),    Z,        add1(Y)        ) :- !.
  280. difference(add1(add1(X)),    2,        fix(X)        ).
  281.  
  282. eq(plus(A,B),        zero,        and(zerop(A),zerop(B))        ) :- !.
  283. eq(plus(A,B),        plus(A,C),    equal(fix(B),fix(C))        ) :- !.
  284. eq(zero,        difference(X,Y),not(lessp(Y,X))            ) :- !.
  285. eq(X,            difference(X,Y),and(numberp(X),
  286.                         and(or(equal(X,zero),
  287.                             zerop(Y))))        ) :- !.
  288. eq(times(X,Y),        zero,        or(zerop(X),zerop(Y))        ) :- !.
  289. eq(append(A,B),        append(A,C),    equal(B,C)            ) :- !.
  290. eq(flatten(X),        cons(Y,[]),    and(nlistp(X),equal(X,Y))    ) :- !.
  291. eq(greatest_factor(X,Y),zero,        and(or(zerop(Y),equal(Y,1)),
  292.                         equal(X,zero))        ) :- !.
  293. eq(greatest_factor(X,_),1,        equal(X,1)            ) :- !.
  294. eq(Z,            times(W,Z),    and(numberp(Z),
  295.                         or(equal(Z,zero),
  296.                            equal(W,1)))        ) :- !.
  297. eq(X,            times(X,Y),    or(equal(X,zero),
  298.                        and(numberp(X),equal(Y,1)))    ) :- !.
  299. eq(times(A,B),        1,        and(not(equal(A,zero)),
  300.                       and(not(equal(B,zero)),
  301.                         and(numberp(A),
  302.                           and(numberp(B),
  303.                             and(equal(decr(A),zero),
  304.                           equal(decr(B),zero))))))
  305.                                     ) :- !.
  306. eq(difference(X,Y),    difference(Z,Y),if(lessp(X,Y),
  307.                         not(lessp(Y,Z)),
  308.                         if(lessp(Z,Y),
  309.                             not(lessp(Y,X)),
  310.                             equal(fix(X),fix(Z))))    ) :- !.
  311. eq(lessp(X,Y),        Z,        if(lessp(X,Y),
  312.                        equal(t,Z),
  313.                        equal(f,Z))            ).
  314.  
  315. exp(I,        plus(J,K),    times(exp(I,J),exp(I,K))) :- !.
  316. exp(I,        times(J,K),    exp(exp(I,J),K)        ).
  317.  
  318. gcd(X,        Y,        gcd(Y,X)        ) :- !.
  319. gcd(times(X,Z),    times(Y,Z),    times(Z,gcd(X,Y))    ).
  320.  
  321. mylength(reverse(X),length(X)).
  322. mylength(cons(_,cons(_,cons(_,cons(_,cons(_,cons(_,X7)))))),
  323.      plus(6,length(X7))).
  324.  
  325. lessp(remainder(_,Y),    Y,    not(zerop(Y))            ) :- !.
  326. lessp(quotient(I,J),    I,    and(not(zerop(I)),
  327.                     or(zerop(J),
  328.                        not(equal(J,1))))    ) :- !.
  329. lessp(remainder(X,Y),    X,    and(not(zerop(Y)),
  330.                     and(not(zerop(X)),
  331.                           not(lessp(X,Y))))    ) :- !.
  332. lessp(plus(X,Y),    plus(X,Z),    lessp(Y,Z)        ) :- !.
  333. lessp(times(X,Z),    times(Y,Z),    and(not(zerop(Z)),
  334.                         lessp(X,Y))        ) :- !.
  335. lessp(Y,        plus(X,Y),    not(zerop(X))        ) :- !.
  336. lessp(length(delete(X,L)),      length(L),    member(X,L)    ).
  337.  
  338. meaning(plus_tree(append(X,Y)),A,
  339.     plus(meaning(plus_tree(X),A),
  340.          meaning(plus_tree(Y),A))
  341.     ) :- !.
  342. meaning(plus_tree(plus_fringe(X)),A,
  343.     fix(meaning(X,A))
  344.     ) :- !.
  345. meaning(plus_tree(delete(X,Y)),A,
  346.     if(member(X,Y),
  347.        difference(meaning(plus_tree(Y),A),
  348.               meaning(X,A)),
  349.        meaning(plus_tree(Y),A))).
  350.  
  351. mymember(X,append(A,B),or(member(X,A),member(X,B))) :- !.
  352. mymember(X,reverse(Y),member(X,Y)) :- !.
  353. mymember(A,intersect(B,C),and(member(A,B),member(A,C))).
  354.  
  355. nth(zero,_,zero).
  356. nth([],I,if(zerop(I),[],zero)).
  357. nth(append(A,B),I,append(nth(A,I),nth(B,difference(I,length(A))))).
  358.  
  359. plus(plus(X,Y),Z,
  360.     plus(X,plus(Y,Z))
  361.     ) :- !.
  362. plus(remainder(X,Y),
  363.          times(Y,quotient(X,Y)),
  364.     fix(X)
  365.     ) :- !.
  366. plus(X,add1(Y),
  367.     if(numberp(Y),
  368.        add1(plus(X,Y)),
  369.        add1(X))
  370.     ).
  371.  
  372. power_eval(big_plus1(L,I,Base),Base,
  373.     plus(power_eval(L,Base),I)
  374.     ) :- !.
  375. power_eval(power_rep(I,Base),Base,
  376.     fix(I)
  377.     ) :- !.
  378. power_eval(big_plus(X,Y,I,Base),Base,
  379.     plus(I,plus(power_eval(X,Base),
  380.             power_eval(Y,Base)))
  381.     ) :- !.
  382. power_eval(big_plus(power_rep(I,Base),
  383.                 power_rep(J,Base),
  384.                 zero,
  385.                 Base),
  386.            Base,
  387.     plus(I,J)
  388.     ).
  389.  
  390. quotient(plus(X,plus(X,Y)),2,plus(X,quotient(Y,2))).
  391. quotient(times(Y,X),Y,if(zerop(Y),zero,fix(X))).
  392.  
  393. remainder(_,        1,zero) :- !.
  394. remainder(X,        X,zero) :- !.
  395. remainder(times(_,Z),    Z,zero) :- !.
  396. remainder(times(Y,_),    Y,zero).
  397.  
  398. reverse_loop(X,Y,    append(reverse(X),Y)    ) :- !.
  399. reverse_loop(X,[],    reverse(X)        ).
  400.  
  401. times(X,     plus(Y,Z),     plus(times(X,Y),times(X,Z))    ) :- !.
  402. times(times(X,Y),Z,         times(X,times(Y,Z))        ) :- !.
  403. times(X,     difference(C,W),difference(times(C,X),times(W,X))) :- !.
  404. times(X,     add1(Y),        if(numberp(Y),
  405.                     plus(X,times(X,Y)),
  406.                     fix(X))            ).
  407.  
  408.  
  409.