home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / SWI / induction.pl < prev    next >
Text File  |  2007-02-13  |  13KB  |  385 lines
  1. /*  INDUCTION
  2.  
  3.   copyright 1993-2001,  P. H. Roosen-Runge
  4.  
  5. Uses simplification and Wang's algorithm to attempt to verify
  6. simple recursive programs expressed as
  7.          F(Arg) = if(Arg, Initial, Result)
  8. with respect to a Goal.
  9.  
  10. Here
  11.          F = function name,
  12.         Arg = name of the integer argument,
  13.         Initial = F(0),
  14.         Expression = F(Arg) if Arg <> 0.
  15.  
  16. The input to induction is a term  in one of the following forms:
  17.  
  18.   (1)  F(Integer) = if(Integer=0, Initial, Result) : Goal.
  19. where Goal = desired mathematical value of F(Integer) for Integer >=
  20. 0.
  21.  
  22. Example: f(n) = if(n=0, 0, f(n-1) + m) : n*m.
  23.  
  24.   (2a)   F(Stack) = if(Stack = nil, Initial, Result) : Goal
  25.   (2b)   F(List) = if(List = [], Initial, Result) : Goal
  26.  
  27.   (3)    tail(if(V=0, Result, F(Reduce(V), C(V, Result))):Goal,
  28.               Identity).
  29.  
  30. Example: tail(if(n=0,s,sum(n-1,s+n)):n* (n+1)/2,0)
  31.  
  32. A special form which 'counts up' is also acceptable:
  33.  
  34.          tail(if(Index = V, Result, F(Index+1, C(Index, Result))):
  35.               Goal, Identity).
  36.  
  37.   (4)  F(Tree) = if(Tree = nilTree, Initial, Result) : Goal.
  38.  
  39. Only meaningful example I can find:
  40.  
  41.        leaves(t) = if(t = nilTree, 1, leaves(left(t))+leaves(right(t))) :
  42.            1 + nodes(t).
  43. */
  44. % Version 1.1, Dec. 29, 1993: induction over stacks
  45. %         2.1  Dec. 20, 1998: transform tail-recursion into simple recursion
  46. %         2.2  Jan. 10, 1999: added error-checking for tail-recursion
  47. %         2.4  Feb. 22: supports gen. induction; allows any "assert(Rule)"
  48. %         2.4.3 January 2, 2000: recompiled with getTheories, v. 2.0
  49. %         2.4.4 February 7: asserts that the induction variable is a nat.
  50. %         2.5  Feb. 13: special form for counting-up for-loops
  51. %         2.5.1 March 21: recompiled with simp, v. 2.1
  52. %         2.6 April 15: identity test repaired
  53. %         2.6.1 September 1: recompiled with condtrans.prolog
  54. %         2.6.2 September 14: test for identity rather than left-identity
  55. %                 (Is Kubiak wrong?)
  56. %         2.7   October 31: goal substitution (finally, really) fixed
  57. %         2.7.1 November 10: recompiled with simp v 3.1.1 to catch
  58. %               circular recursive simplification rules.
  59. %         2.8  Jan. 25, 2002: added induction over binary trees
  60. %         2.9SWI Feb. 12, 2007: SWI version
  61. %====================================================================
  62.  
  63. :- multifile '->>'/2. :- dynamic '->>'/2.
  64.  
  65. % uses paths from .plrc
  66. :-ensure_loaded([qlib(arg), qlib(change_arg), qlib(occurs)]).
  67. :-ensure_loaded([lib('simp.pl'), lib('equtaut.pl'), lib('getTheories.pl')]).
  68.  
  69. error(Message) :- nl, write('!! '), write(Message), nl, halt.
  70.  
  71. activate :-
  72.         write('Version 2.9SWI, February 12, 2007'), nl,
  73.         op(400, yfx, mod),  %  960 in SWI ??
  74.     fileerrors(OldFlag, off),
  75.         getTheories,
  76.     proveTerms,
  77.         fileerrors(_, OldFlag)
  78.      ;
  79.         nl, error('Something wrong.'), nl, halt.
  80.  
  81. proveTerms :- read(T),
  82.        ( T==end_of_file -> halt
  83.         ;
  84.          T=theory(File), theory(File)
  85.         ;
  86.          T=assert(Rule), addRule(Rule)
  87.         ;
  88.          nl, write(T), nl, verify(T), nl
  89.         ),
  90.         proveTerms.
  91.  
  92. verify(LHS = if(Arg=0, Initial, Expression) : Goal) :-
  93.     functor(LHS, F, Arity),
  94.     (
  95.      arg(1, LHS, Arg), nonvar(Arg)
  96.         ;
  97.      error('Error in recursion argument.')
  98.     ),
  99.     assert(nat(Arg)),
  100.     substitutex(0, Arg, Goal, Goal0),
  101.     nl, write('Base case: '),
  102.     try(Goal0 = Initial), !, % base case for the induction.
  103.     instep(LHS, Expression, Arg, Goal, Step),
  104.         nl, write('Inductive step: '),
  105.         try(Goal = Step).
  106.       
  107. verify(LHS = if(Arg=nil, Initial, Expression) : Goal) :-
  108.     LHS =.. [F, Arg | Rest],
  109.         substitutex(nil, Arg, Goal, Goal0),
  110.     nl, write('Base case: '),
  111.         try(Goal0 = Initial), !, % base case for the induction.
  112.         substitutex(pop(Arg), Arg, Goal, Goal1),
  113.         FA1 =.. [F, pop(Arg) | Rest],
  114.         substitutex(Goal1, FA1, Expression, Exp1), % inductive hypothesis.
  115.         nl, write('Inductive step: '),  
  116.         try(Goal = Exp1). 
  117.  
  118. verify(LHS = if(leaf(Arg), Initial, Expression) : Goal) :-
  119.         LHS =.. [F, Arg | Rest],
  120.         nl, write('Base case: '),
  121.         try(leaf(Arg) implies Goal = Initial), !, 
  122.               % base case for the induction.
  123.         substitutex(left(Arg), Arg, Goal, Goal1),
  124.         FA1 =.. [F,left(Arg) | Rest],
  125.         substitutex(Goal1, FA1, Expression, Exp1), % inductive hypothesis.
  126.         nl, write('Inductive step: '),
  127.     substitutex(right(Arg), Arg, Goal, Goal2),
  128.         FA2 =.. [F, right(Arg) | Rest],
  129.         substitutex(Goal2, FA2, Exp1, Exp2), % inductive hypothesis.
  130.     try(Goal = Exp2).
  131.  
  132. verify(LHS = if(Arg=[], Initial, Expression) : Goal) :-
  133.         LHS =.. [F, Arg | Rest],
  134.         substitutex([], Arg, Goal, Goal0),
  135.         nl, write('Base case: '),
  136.         try(Goal0 = Initial), !, % base case for the induction.
  137.         substitutex(rest(Arg), Arg, Goal, Goal1),
  138.         FA1 =.. [F, rest(Arg) | Rest],
  139.         substitutex(Goal1, FA1, Expression, Exp1), % inductive hypothesis.
  140.         nl, write('Inductive step: '),
  141.         try(Goal = Exp1). 
  142.  
  143. verify(tail(Definition: Goal, Identity)) :-
  144.         tail(Definition, Identity, Left = Naive) ->
  145.     Def = (Left = Naive : Goal),
  146.     nl, write('Verifying: '), write(Def),
  147.         verify(Def).
  148.  
  149. verify(_) :-    nl, write('!! Cannot recognize input format.').
  150.  
  151. % call this (Args, LHS, Arity, 1, Goal, Result).    
  152. subArgsInGoal(Args, LHS, Arity, N, Goal, Result) :-
  153.     N =< Arity,
  154.     arg(N, LHS, A), 
  155.     item(N, Args, Arg), 
  156.     substitutex(Arg, A, Goal, Modified),
  157.     N1 is N+1,
  158.     subArgsInGoal(Args, LHS, Arity, N1, Modified, Result).
  159. subArgsInGoal(_, _, _, _, Result, Result).
  160.  
  161. subGoalForF(LHS, Path,Goal,  Expression, Result) :-
  162.     functor(LHS, F, Arity),
  163.     path_arg(Path, Expression, Call),
  164.     Call =.. [F|Args],
  165.     subArgsInGoal(Args, LHS, Arity, 1, Goal, ModGoal),
  166.     change_path_arg(Path, Expression, _, Result, ModGoal).
  167.     
  168. subGoalForCalls(LHS, Goal, Expression, Result) :-
  169.     functor(LHS, F, Arity),
  170.     setof(Path, Match^(path_arg(Path, Expression, Match), 
  171.              functor(Match, F, Arity)), Calls),
  172. % any better way to find these paths than to try them all?
  173.         subGoalForFs(LHS, Goal, Expression, Calls, Result).
  174.  
  175. subGoalForFs(_, _, Expression, [], Expression).
  176. subGoalForFs(LHS, Goal, Expression, [Call | Rest], Result) :-
  177.     subGoalForF(LHS, Call, Goal, Expression, Modified),
  178.     subGoalForFs(LHS, Goal, Modified, Rest, Result).
  179.  
  180. item(1, [X|_], X) :- !.
  181. item(N, [_| Rest], X) :- N>1, N1 is N-1, item(N1, Rest, X).
  182.  
  183. /*
  184. subInGoal(N, LHS,  Lists, Goal, Expression, Result) :-
  185.     functor(LHS, _, Arity), N =< Arity,
  186.     subInGoalforArg(N, LHS, Lists, Goal, Expression, Modified),
  187.     N1 is N+1, 
  188.     subInGoal(N1, LHS, Lists, Goal, Modified, Result).
  189. subInGoal(_, _, _, _, Expression, Expression).
  190.  
  191. subInGoalforArg(N, LHS, [List | Rest], Goal, Expression, Result) :-
  192.     arg(N, LHS, A),
  193.     functor(LHS, F, _),
  194.     path_arg(Path, Expression, Term),
  195.     functor(Term, F, _), arg(N, Term, X),
  196.     changeAll(List, X, Goal, ModifiedGoal),
  197.     change_path_arg(Path, Expression, NewExpression, ModifiedGoal),
  198.     !,
  199.     subInGoalforArg(N, LHS, Rest, Goal, NewExpression, Result).
  200. subInGoalforArg(_, _, _, _, Expression, Expression).
  201. */
  202.  
  203.  
  204. instep(LHS, Expression, Arg, Goal, Result) :-
  205.     functor(LHS, F, Arity),
  206.     varList(Arity, VarList),
  207.     Template =..  [F | VarList],
  208.     arg(1, Template, V),
  209.     findall(V, sub_term(Template, Expression), Vs),
  210.     sort(Vs, Exps),
  211.         (
  212.      checkBounds(Exps, F, Expression, Arg) 
  213.         ; 
  214.      error('Error in function argument.')
  215.     ),
  216.     (
  217.      Arity = 1 -> substituteArgs(Exps, Goal, Arg, Goals),
  218.      substituteGoals1(Goals, Exps, F, Expression, Result)
  219.        % substitute function args for induction variable in Goal
  220.        % substitute Goal for F(Exp)
  221.     ;
  222.      subGoalForCalls(LHS, Goal, Expression, Result)
  223.         ).
  224.  
  225. varList(0, []).
  226. varList(Arity, [_ | Rest]) :- A1 is Arity - 1, varList(A1, Rest).
  227.  
  228. firstArg(V, Template, Expression) :-
  229.     arg(1, Template, V), sub_term(Template, Expression).
  230.  
  231. checkBounds([], _, _, _).
  232. checkBounds([Arg - 1 | Rest], F, Expression, Arg) :-
  233.     checkBounds(Rest, F, Expression, Arg).
  234. checkBounds([Term | Rest], F, Expression, Arg) :- 
  235.     (
  236.      sub_term(if(B, If, Else), Expression),
  237.      (
  238.       sub_term(Term, If),
  239.       try(0 < Arg and B implies 0 <= Term and Term < Arg)
  240.      ;
  241.       sub_term(Term, Else),
  242.       try(0 < Arg and not B implies 0 <= Term and Term < Arg)  
  243.      )
  244.     ;
  245.          try(0 <= Term and Term < Arg)
  246.     ),
  247.     checkBounds(Rest, F, Expression, Arg).  
  248.  
  249.  
  250.     
  251. substituteArgs([], _, _, []).
  252. substituteArgs([Exp | Rest], Goal, Arg, [G | Goals]) :-
  253.        substitutex(Exp, Arg, Goal, G),
  254.        substituteArgs(Rest, Goal, Arg, Goals).
  255. /*
  256. % for F(Args) in the recursive expression, subArgs creates an
  257. % equivalent goal (assuming the premises of the induction step.)
  258.  
  259. subArgs(_, [], Goal, Goal).
  260. subArgs([P |RestP], [A | RestA], Goal, NewGoal) :-
  261.        substitutex(A, P, Goal, Modified),
  262.        subArgs(RestP, RestA, Modified, NewGoal).
  263. */
  264.  
  265. subGoals([], _, _, _, _, Expression, Expression).
  266. subGoals([Exp | Rest], F, V, Arity, Goal, Expression, Result) :-
  267.     substitutex(Exp, V, Goal, EGoal),
  268.     substituteGoal(EGoal, F, Arity, Exp, Expression, New),
  269.     subGoals(Rest, F, V, Arity, Goal, New, Result).
  270.  
  271. substituteGoal(EGoal, F, Arity, Exp, Expression, Result) :-
  272.     path_arg(Path, Expression, Term),
  273.     functor(Term, F, Arity),
  274.     arg(1, Term, Exp),
  275.     change_path_arg(Path, Expression, Modified, EGoal),
  276.     !,
  277.     substituteGoal(EGoal, F, Arity, Exp, Modified, Result).
  278. substituteGoal(_, _, _, _, Expression, Expression).
  279.  
  280. substituteGoals1([], _,  _, Exp, Exp).
  281. substituteGoals1([G | Goals], [Ex | Rest], F, Expression, Exp)  :-
  282.     Fex =.. [F, Ex],
  283.     substitutex(G, Fex, Expression, Exp1),
  284.     substituteGoals1(Goals, Rest, F, Exp1, Exp).
  285.  
  286. % once again, based on the waterfall predicate, QP Library manual.
  287. % but far from optimal?
  288. substituteFunctor(F, G, Arity, Expression, Result) :-
  289.     path_arg(Path, Expression, Term),
  290.     change_functor(Term, F, New, G, Arity), 
  291.     change_path_arg(Path,  Expression, _, Modified, New),
  292.     !,
  293.     substituteFunctor(F, G, Arity, Modified, Result).
  294. substituteFunctor(_, _, _, Expression, Expression).
  295.  
  296. tail(if(A1 = A2, Terminal, G), Identity, Naive) :-
  297.     G =.. [F, Index + 1, C, V],!,
  298.     (A1 = V, A2 = Index ; A2 = V, A1 = Index),
  299.     substitutex(V, Index, C, C1),
  300.     G1 =..[F, V - 1, C1],
  301.     tail(if(V = 0, Terminal, G1), Identity, Naive).
  302.  
  303. tail(if(A, Terminal, G), Identity, Naive) :-
  304.        (
  305.         \+atom(Terminal), error('The result argument must be a variable.'),
  306.         !, fail
  307.        ;
  308.        Final = Identity,
  309.        findvar(A, X),
  310.        G =.. [F, E, C],functor(C, CFun, Arity),
  311.        (Arity = 2 ->
  312.         nl, write('Assume '), write(CFun), write(' is associative. '), nl,
  313.         Arg =.. [F, E],
  314.            % E =.. should involve X, but we don't check
  315.         Left =.. [F, X],
  316.        (
  317.     findTerm(X, Terminal, C, D), contains_term(X, D), Path=[]
  318.        ;
  319.         findTerm(X, Terminal, C, D), path_arg(Path, C, D)
  320.        ), !,
  321.         substitutex(Identity, Terminal, C, IT),
  322.     subForD(X, Path, 'X', D, IT, Ident),
  323.     substitutex('X', Terminal, C, IT2),
  324.     subForD(X, Path, Identity, D, IT2, Ident2),
  325.         try(Ident = 'X'), try(Ident2 = 'X'),
  326.         swapArgs(D, Terminal, C, CR),
  327.     substitutex(Arg, Terminal, CR, Recurse),
  328.         Naive = (Left = if(A, Final, Recurse))
  329.        ;
  330.         nl, write('Error! '), 
  331.     write(C), 
  332.     write(' doesn''t have the right structure for transformation.'),
  333.     halt
  334.        )).
  335.  
  336. tail(_, _, _) :-
  337.         error('Something wrong in tail-recursion definition.').
  338.  
  339. subForD(N, Path, New, D, Old, Result) :-
  340.     contains_term(N, D),
  341.     substitutex(New, D, Old, Result)
  342.        ; 
  343.     path_arg(Path, Old, D),
  344.     change_path_arg(Path, Old, Result, New).
  345.  
  346. findvar(X=_, X) :- functor(X, _, 0), \+number(X).
  347. findvar(_=X, X) :- functor(X, _, 0), \+number(X).
  348. findvar(A, X) :-
  349.         A =.. [_, Y],
  350.            (functor(X, _, 0) -> X=Y
  351.             ;
  352.             findvar(Y, X)
  353.            ).          
  354.  
  355. findTerm(X, Result, Term, Sub) :-
  356.     sub_term(Sub, Term ), 
  357.     free_of_term(Result, Sub).
  358.  
  359.         
  360. try(T) :- simplify(T, SimpT),
  361.         ( tautology(SimpT), write(T), write(' is valid.'), nl
  362.          ;
  363.           nl, write('Cannot prove '), write(SimpT), write('.'), nl
  364.         ).
  365.  
  366. swapArgs(A, B, C, Result) :-
  367.     substitutex('DUMMY'(A), A, C, CA),
  368.         substitutex('DUMMY'(B), B, CA,CAB),
  369.         substitutex(B, 'DUMMY'(A), CAB, CB),
  370.         substitutex(A, 'DUMMY'(B), CB, Result).
  371.  
  372. substitutex(V, R, G, W) :-
  373.         setof(Path,path_arg(Path, G, R), Paths),
  374.         changeAllx(Paths, V, G, W), !.
  375. substitutex(_, _, G, G).
  376.  
  377. changeAllx([Path | Rest], V, G, W) :-
  378.         change_path_arg(Path, G, Modified, V),
  379.         changeAll( Rest, V, Modified, W).
  380. changeAllx(_, _, G, G).    
  381.  
  382.  
  383.                                      
  384.  
  385.