% file:    recursion.pro
% author:  Robert Keller
% purpose: Implementation of the van Dalen language for partial recursive functions
% $Id: recursion.pl,v 1.6 2007/04/22 02:20:06 keller Exp keller $
%
% Top level call:
%
%     eval(Program, Arguments, Answer)
%
% where 
%     Program is a program, i.e. "index" 
%     Arguments is a list of arguments for the program
%     Answer is the answer returned by Prolog as the value of Program applied to Arguments
%
% Note that we use symbols and nesting rather than actual Godel numbers, although this
% is actually a minor point, to avoid building up huge numbers to represent indices,
% and also to make the programs somewhat more readable.
%
% Currently a trace of the program in execution is produced, like it or not.
%
% Examples may be found at the end of this file.

eval(Prog, Vector, Ans) :-
    nl,
    write('trace eval of '),
    writeProg(Prog),
    write(' : '),
    writeArgs(Vector),
    eval1(Prog, Vector, Ans) ->
      (
      nl,
      write('trace eval out '),
      writeProg(Prog),
      write(' : '),
      write(Vector), nl,
      write(' --> '),
      write(Ans),
      nl
      )
   ; (
      nl,
      write('error, unrecognized index: '),
      nl,
      writeProg(Prog),
      nl,
      length(Vector, NumArgs),
      write('applied to '),
      write(NumArgs),
      write(' argument vector: '),
      nl,
      writeArgs(Vector),
      nl,
      fail
      ).

% indentation handling

indentation('  ').

increaseIndent(Old, New) :-
    indentation(Indent),
    concat(Old, Indent, New).

% print program, with some amount of indentation

writeProg(Prog) :-
    writeProg0(Prog, '').

writeProg0([const, N, C], Indent) :- 
    write(Indent),
    write([const, N, C]).

writeProg0([proj,  N, I], Indent) :-
    write(Indent),
    write([proj,  N, I]).

writeProg0([succ,  N, I], Indent) :-
    write(Indent),
    write([succ,  N, I]).

writeProg0([cond, N4], Indent) :-
    write(Indent),
    write([cond, N4]).

writeProg0([compose, N, B | Cs], Indent) :-
    write(Indent),
    write('[compose, '),
    write(N),
    write(', '),
    nl,
    increaseIndent(Indent, NewIndent),
    writeProg0(B, NewIndent),
    write(','),
    nl,
    increaseIndent(NewIndent, NewerIndent),
    write(NewerIndent),
    write('['),
    nl,
    writeProgs(Cs, NewerIndent),
    write(NewerIndent),
    write(']'),
    nl.

writeProg0([s1n, N], Indent) :- write(Indent), write([s1n, N]).
writeProg0([s2n, N], Indent) :- write(Indent), write([s2n, N]).
writeProg0([app, N], Indent) :- write(Indent), write([app, N]).
writeProg0(Other, Indent) :- 
    write(Indent),
    write('unrecognized program: '),
    nl,
    write(Indent),
    write(Other),
    nl.

% print a list of programs

writeProgs([], _Indent).
writeProgs([Prog | Progs], Indent) :-
    writeProg0(Prog, Indent),
    nl,
    writeProgs(Progs, Indent).

% print the arguments.

writeArgs(Vector) :-
    nl,
    write('['),
    nl,
    writeArgs1(Vector),
    write(']').

writeArgs1([]).
writeArgs1([A | X]) :-
    write(' '),
    write(A),
    writeArgs2(X).

writeArgs2([]) :- nl.
writeArgs2([B | X]) :-
    write(','), nl,
    write(' '),
    write(B),
    writeArgs2(X).

% The top level evaluator, without tracing.
% This dispatches the program to rules r1-r7 as in van Dalen.
% I've included an r6a for s2n, in addition to r6 for s1n, for possible use 
% in the recursion theorem (to be illustrated).  However, I conjecture that
% neither s1n nor s2n are essential, as their effect can be achieved by
% just using composition, projection, constant, and application.

eval1([const, N, C], Vector, Ans)        :- !, r1([const, N, C], Vector, Ans).
eval1([proj,  N, I], Vector, Ans)        :- !, r2([proj,  N, I], Vector, Ans).
eval1([succ,  N, I], Vector, Ans)        :- !, r3([succ,  N, I], Vector, Ans).
eval1([cond, N4],    Vector, Ans)        :- !, r4([cond, N4],    Vector, Ans).
eval1([compose, N, B | Cs], Vector, Ans) :- !, r5([compose, N, B | Cs], Vector, Ans).
eval1([s1n, N], Vector, Ans)             :- !, r6([s1n, N], Vector, Ans).
eval1([s2n, N], Vector, Ans)             :- !, r6a([s2n, N], Vector, Ans).
eval1([app, N], Vector, Ans)             :- !, r7([app, N], Vector, Ans).

% The van Dalen rules:

% R1 is for constant functions:
% [const N, C] : [X1, X2, ..., Xn] --> C

r1([const, N, C], Vector, C) :- 
    length_check(Vector, N).


% R2 is for projections
% [proj N, I] : [X1, X2, ..., Xn] --> XI

r2([proj, N, I], Vector, Vi) :- 
    length_check(Vector, N), 
    select(I, Vector, Vi).

% auxiliary for projection and successor, to select Ith argument from list

select(0, [V0 | _], V0).
select(I, [_ | Vs], Vi) :- I > 0, I1 is I-1, select(I1, Vs, Vi).


% R3 is for successors
% [succ N, I] : [X1, X2, ..., Xn] --> 1+XI

r3([succ, N, I], Vector, SVi) :- 
    length_check(Vector, N), 
    select(I, Vector, Vi), 
    SVi is Vi + 1.


% R4 is for conditional
% [cond, N+4] : [P, Q, R, S | . . .] --> P if R == S
% [cond, N+4] : [P, Q, R, S | . . .] --> Q if not

r4([cond, N4], [P, Q, R, S | Vector], Ans) :- 
    N is N4-4,
    length_check(Vector, N),
    (R =:= S -> 
       (
       nl,
       write('equality true, returning '),
       write(P),
       nl,
       Ans = P
       )
    ; (
      nl,
      write('equality false, returning '),
      write(Q),
      nl,
      Ans = Q
      )
    ).

% R5 is composition
% [compose, N, B, C1, C2, ...., Ck] : [X1, X2, ..., XN] -->
% B : (C1: [X1, X2, ..., XN], ...., Ck: [X1, X2, ..., XN])
%
% Note that N is NOT the number of things being composed, but
% rather it is the arity of the resulting function, which is
% the same as the arity of the inner functions.

r5([compose, N, B | Cs], Vector, Ans) :-
    length_check(Vector, N),
    evalEach(Cs, Vector, Intermediate),
    eval(B, Intermediate, Ans).


% evalEach evaluates the sub-applications in a composition

evalEach([], _, []).
evalEach([C | Cs], Vector, [Ans | Anss]) :-
    eval(C, Vector, Ans),
    evalEach(Cs, Vector, Anss).


% R6 is the s1n function.
% See the text or examples for explanation

r6([s1n, N], [P, Q | Vector], Ans) :-
    N2 is N-2,
    length_check(Vector, N2),
    P = [_, Arity | _],
    Arity1 is Arity-1,
    makeProjections(Arity1, 0, N2, Projs),
    Ans = [compose, Arity1, P, [const, Arity1, Q] | Projs].

makeProjections(_Arity1, I, N2, []) :-
    I > N2.
makeProjections(Arity1, I, N2, [[proj, Arity1, I] | Projs]) :-
    I =< N2,
    I1 is I + 1,
    makeProjections(Arity1, I1, N2, Projs).


% R6a is the s2n function, included for convenience.
% See the text or examples for explanation

r6a([s2n, N], [P, Q, R | Vector], Ans) :-
    N3 is N-3,
    length_check(Vector, N3),
    P = [_, Arity | _],
    Arity2 is Arity-2,
    makeProjections(Arity2, 0, N3, Projs),
    Ans = [compose, Arity2, P, [const, Arity2, Q], [const, Arity2, R] | Projs].


% R7 is the universal application function
% form: [app, N+1] applies an N-ary function to the N elements following in the list
% i.e. [app, N+1] : [F, X1, X2, X3, ..., XN] = F : [X1, X2, X3 , ..., XN]

r7([app, N], [B | Vector], Ans) :-
    N1 is N-1,
    length_check(Vector, N1),
    eval(B, Vector, Ans).


% auxiliary for checking argument compatibility

length_check(Vector, N) :-
    length(Vector, N1),
    (N1 =:= N -> true ; 
     (nl,
      write('length checked failed, expected length '), 
      write(N),
      write(', but got length '),
      write(N1),
      write(', irritant: '), nl,
      write(Vector),
      nl,
      fail)).


% Testing stuff, to track number of tests, successes, failures

:- dynamic tests/1, successes/1, failures/1.

tests(0).
successes(0).
failures(0).

showResults :-
    tests(T),
    successes(S), 
    failures(F),
    nl,
    write('Conclusion: in '),
    write(T), write(' tests: '),
    write(S), write(' successes, '),
    write(F), write(' failures.'),
    nl, nl.

addToCount(Pred) :-
    OldTerm =.. [Pred, N],
    retract(OldTerm),
    N1 is N + 1,
    NewTerm =.. [Pred, N1],
    assert(NewTerm).

test(Prog, Args, Desired) :-
    nl,
    addToCount(tests),
    tests(T),
    write('test number '), write(T), write(':'), nl,
    eval(Prog, Args, Actual) ->
    (Desired == Actual -> 
        (
        nl,
        write('end test number '), write(T), write(', succeeded: '), nl,
        addToCount(successes),
        writeProg(Prog),
        write(' : '),
        write(Args), nl,
        write(' --> '),
        nl,
        write(Actual),
        nl, nl
        )
     ;  (
        nl,
        write('end test number '), write(T), write(', failed: '), nl,
        addToCount(failures),
        writeProg(Prog),
        write(' : '),
        write(Args),
        nl,
        write(' --> '), 
        write(Actual), nl,
        write(' but desired '), nl,
        write(Desired),
        nl
        )
     )
    ; (
      write('end test number '), write(T), write(', failed with no result.'), nl,
      addToCount(failures),
      writeProg(Prog),
      write(' : '),
      write(Args),
      write(', desired '),
      write(Desired),
      nl
      ).
        
% Test cases.  test(Program, Arguments, Desired result)

test :-
    test([const, 1, 99], [1],    99),
    test([const, 2, 99], [1, 2], 99),
    test([const, 2, 99], [1, 2], 99),

    test([proj, 1, 0], [98],     98),
    test([proj, 2, 0], [98, 99], 98),
    test([proj, 2, 1], [98, 99], 99),

    test([succ, 1, 0], [97],     98),
    test([succ, 2, 0], [97, 98], 98),
    test([succ, 2, 1], [97, 98], 99),

    test([cond, 4], [98, 99, 1, 1], 98),
    test([cond, 4], [98, 99, 1, 2], 99),

    test([compose, 1, [succ, 1, 0], [succ, 1, 0]], [97], 99),
    test([compose, 2, [succ, 1, 0], [succ, 2, 0]], [96, 97], 98),
    test([compose, 2, [succ, 1, 0], [succ, 2, 1]], [96, 97], 99),
    test([compose, 3, [succ, 1, 0], [succ, 3, 2]], [95, 96, 97], 99),
    test([compose, 2, [succ, 2, 0], [proj, 2, 0], [succ, 2, 1]], [95, 96], 96),
    test([compose, 2, [succ, 2, 1], [proj, 2, 0], [succ, 2, 1]], [95, 96], 98),

    test([s1n, 2], [[proj, 2, 0], 98], 
         [compose, 1, [proj, 2, 0], [const, 1, 98], [proj, 1, 0]]),

    test([s1n, 2], [[proj, 2, 2], 98], 
         [compose, 1, [proj, 2, 2], [const, 1, 98], [proj, 1, 0]]),

    test([app, 2], [[succ, 1, 0], 98], 99),

    test([app, 3], [[succ, 2, 0], 97, 98], 98),
    test([app, 3], [[succ, 2, 1], 97, 98], 99),

    test([app, 4], [[succ, 3, 0], 96, 97, 98], 97),
    test([app, 4], [[succ, 3, 1], 96, 97, 98], 98),
    test([app, 4], [[succ, 3, 2], 96, 97, 98], 99),

    test([app, 2], [[compose, 1, [succ, 1, 0], [succ, 1, 0]], 97], 99),

    test([app, 3], [[s1n, 2], [proj, 2, 2], 98], 
         [compose, 1, [proj, 2, 2], [const, 1, 98], [proj, 1, 0]]),

    test([s2n, 3], [[proj, 3, 0], [proj, 3, 0], 1], 
         [compose, 1, [proj, 3, 0], [const, 1, [proj, 3, 0]], [const, 1, 1], [proj, 1, 0]]),

    % fun(x, y, z) = x == 0 ? y : z

    % if first argument is 0, return 2nd argument, else third

    test([compose, 3, [cond, 4], [proj, 3, 1], [proj, 3, 2], [proj, 3, 0], [const, 3, 0]], [0, 97, 98], 97),
    test([compose, 3, [cond, 4], [proj, 3, 1], [proj, 3, 2], [proj, 3, 0], [const, 3, 0]], [1, 97, 98], 98),

    % an apply version of the preceding

    test([app, 4], [[compose, 3, [cond, 4], [proj, 3, 1], [proj, 3, 2], [proj, 3, 0], [const, 3, 0]], 1, 97, 98], 98),

    % if second argument is 0, apply the proj to the remaining argument, else apply succ

    test([app, 3], [[compose, 2, [cond, 4], [proj, 2, 1], [succ, 2, 1], [proj, 2, 0], [const, 2, 0]], 0, 97], 97),
    test([app, 3], [[compose, 2, [cond, 4], [proj, 2, 1], [succ, 2, 1], [proj, 2, 0], [const, 2, 0]], 1, 97], 98),

    test([compose, 3, [cond, 4], [proj, 3, 1], [compose, 3, [succ, 1, 0], [succ, 3, 0]], [proj, 3, 0], [const, 3, 0]], [1, 97, 98], 3),

% Below, we use some Prolog variables simply to avoid repeating large terms

% study leading up to predecessor:
% S(x) = x + 1
% psi(fun, x, y) = S(y) == x ? y : fun(fun, x, S(y));
% psi is the mu operator with a fixed function: Successor
% pred(x) = x == 0 ? psi(psi, x, 0)

% This program is psi above, and essentially computes the predecessor function.
% It shows the onerous task of using a conditional construct that evaluates all arguments.
% We have to create functions that become the result of conditional, then apply them outside.

    PredCore = 
        [compose, 3,
           [app, 4],
            [compose, 3,
              [cond, 4], 
                [const, 3, [proj, 3, 2]],        % y, the T branch
                [const, 3, [compose, 3,          % fun(fun, x, S(y)), the F branch
                             [app, 4],
                                 [proj, 3, 0], 
                                 [proj, 3, 0], 
                                 [proj, 3, 1], 
                                 [succ, 3, 2]]], 
                [succ, 3, 2],          % S(y) one argument of ==
                [proj, 3, 1]],         % x other argument of ==

             [proj, 3, 0],
             [proj, 3, 1],
             [proj, 3, 2]
         ],

    test(PredCore,
        [
         PredCore,
         1,  % number whose predecessor is to be determined
         0], 

         0),

    test(PredCore,
        [
         PredCore,
         2,  % number whose predecessor is to be determined
         0], 

         1),

    test(PredCore,
        [
         PredCore,
         3,  % number whose predecessor is to be determined
         0], 

         2),

    test(PredCore,
        [
         PredCore,
         5,  % number whose predecessor is to be determined
         0], 

         4),

% predecessor
% pred(x) = x == 0 ? psi(psi, x, 0)

  % We use PredCore defined above, although we could have done the literal substitution,
  % and we could have added another level of composition/projection to avoid duplication.

  Pred = 
    [compose, 1,
       [app, 2],
         [compose, 1,
           [cond, 4],
             [const, 1, [const, 1, 0]],
             [const, 1, [compose, 1, PredCore, [const, 1, PredCore], [proj, 1, 0], [const, 1, 0]]],
             [proj, 1, 0],
             [const, 1, 0]],
         [proj, 1, 0]
       ],

    test(Pred, [1], 0),
    test(Pred, [2], 1),
    test(Pred, [3], 2),
    test(Pred, [0], 0),

    showResults.

:- test.