/* 

  Problem related to an IPL submission about deforestation

  dmap is a function that can obviously be evaluated without
  generating intermediate forms.
  
  Any expression in map, append, and rev can be translated into a right-recursive dmap-expression.
  However, this expression might contain 0, another source of inefficiency by ignoring
  partial intermediate results.


*/

% 0 introduce dmap1 which is dmap with different argument order (avoid ordering problem with equation 1)

dmap(F,G,X,Y)=dmap1(X,Y,F,G).

% 1
dmap(F,G,dmap(H,K,X,Y),Z)=
	dmap(comp(F,H),comp(F,K),X,dmap(F,G,Y,dmap(comp(G,K),comp(G,H),X,Z))).

% 2 - 4 
dmap(0,0,X,Y)=Y.
dmap(F,G,e,Y)=Y.
dmap(id,0,X,e)=X.

% 5 - 9
comp(F,0)=0.
comp(0,F)=0.
comp(F,id)=F.
comp(id,F)=F.
comp(comp(F,G),H)=comp(F,comp(G,H)).


% 10 - 12
X*Y = dmap(id,0,X,Y).
i(X)= dmap(0,id,X,e).
map(F,X) = dmap(F,0,X,e).


% precedence([i,map,*,dmap,dmap1,comp,id,0,e]).

/* 

With precedence
 
i > map > * > dmap > dmap1 > comp > id > 0 > e

we attempt at eliminating i, map, and * in favour of
dmap, avoiding the computation of intermediate forms.

This is successful, we get the canonical system


    1(1) : dmap(B,C,D,E)=dmap1(D,E,B,C)
    6(1) : comp(B,0)=0
    7(1) : comp(0,B)=0
    8(1) : comp(B,id)=B
    9(1) : comp(id,B)=B
   10(1) : comp(comp(B,C),D)=comp(B,comp(C,D))
   14(2) : dmap1(dmap1(B,C,D,E),F,G,H)=dmap1(B,dmap1(C,dmap1(B,F,comp(H,E),comp(H,D)),G,H),comp(G,D),comp(G,E))
   15(2) : dmap1(B,C,0,0)=C
   16(2) : dmap1(e,B,C,D)=B
   17(2) : dmap1(B,e,id,0)=B
   18(2) : B*C=dmap1(B,C,id,0)
   19(2) : i(B)=dmap1(B,e,0,id)
   20(2) : map(B,C)=dmap1(C,e,B,0)
   34(4) : dmap1(B,dmap1(B,C,0,D),E,0)=dmap1(B,C,E,D)


*/




precedence([dmap1,dmap,i,map,*,comp,id,0,e]).


/*


With precedence

dmap1 > dmap > i > map > * > comp > id > 0 > e

we try to eliminate dmap from the axioms and to synthesize a definition
for dmap in terms of i, *, and map. This is also successful, 
additionally giving us the usual laws about i, *, and map:


Saturation terminated.

Persisting Clauses:

    1(1) : dmap1(B,C,D,E)=map(D,B)*(map(E,i(B))*C)
    6(1) : comp(B,0)=0
    7(1) : comp(0,B)=0
    8(1) : comp(B,id)=B
    9(1) : comp(id,B)=B
   10(1) : comp(comp(B,C),D)=comp(B,comp(C,D))
   14(2) : map(id,B)=B
   15(2) : i(e)=e
   16(2) : e*B=B
   17(2) : map(0,B)=e
   18(2) : map(B,e)=e
   20(3) : B*e=B
   73(7) : B*C*D=B*(C*D)
 154(11) : map(B,C*D)=map(B,C)*map(B,D)
 191(10) : map(comp(B,C),D)=map(B,map(C,D))
1712(15) : i(map(B,C))=map(B,i(C))
1766(18) : i(i(B))=B
1880(15) : i(B*C)=i(C)*i(B)
11424(12) : dmap(B,C,D,E)=map(B,D)*(map(C,i(D))*E)



Total time: 784260 milliseconds

Number of forward inferences: 9873
Number of tableau inferences: 0
Number of kept clauses: 1937



This equivalent set of equations now contains
the standard laws about *, map, and i that Phil used
to derive your law 1 about dmap, and also contains
the explicit definition of dmap in terms of *, i, and map.


*/