Optimal reduction expressed in CHR

graph_reduction.chr

/* There may be mistakes here.
   This program implements "optimal reduction" in CHR,
   it runs in CHR.js playground.
   
   The N in front of each structure is a label.
   Rest of the numbers are edges between combinators.
   fresh(N) tracks fresh numbers to produce new edges.
 */

eq(X,Y), eq(Y,Z) <=> eq(X,Z)
eq(X,Y), eq(Z,Y) <=> eq(X,Z)

eq(X,Y), fan(N,X,A,B) <=> fan(N,Y,A,B)
eq(X,Y), fan(N,Y,A,B) <=> fan(N,X,A,B)
eq(X,Y), cro(N,X,A) <=> cro(N,Y,A)
eq(X,Y), cro(N,Y,A) <=> cro(N,X,A)
eq(X,Y), bra(N,X,A) <=> bra(N,Y,A)
eq(X,Y), bra(N,Y,A) <=> bra(N,X,A)

cro(N,X,Y), cro(N,X,Z) <=> eq(X,Z)
bra(N,X,Y), bra(N,X,Z) <=> eq(X,Z)
fan(N,W,X,Y), fan(N,W,A,B) <=> eq(X,A), eq(Y,B)

cro(N,X,Y), bra(M,X,Z) <=> N<M |
  bra(M-1,Y,X), cro(N,Z,X)
bra(N,X,Y), cro(M,X,Z) <=> N<M |
  cro(M+1,Y,X), bra(N,Z,X)
fan(M,X,A,B), cro(M,X,Y), fresh(K) <=> N<M |
  fan(M,Y,K+0,K+1),
  cro(N,A,K+0),
  cro(N,B,K+1),
  fresh(K+2)
fan(M,X,A,B), bra(M,X,Y), fresh(K) <=> N<M |
  fan(M,Y,K+0,K+1),
  cro(N,A,K+0),
  cro(N,B,K+1),
  fresh(K+2)
cro(N,X,Y), fan(M,X,A,B), fresh(K) <=> N<M |
  fan(M-1,Y,K+0,K+1),
  cro(N,A,K+0),
  cro(N,B,K+1),
  fresh(K+2)
bra(N,X,Y), fan(M,X,A,B), fresh(K) <=> N<M |
  fan(M+1,Y,K+0,K+1),
  cro(N,A,K+0),
  cro(N,B,K+1),
  fresh(K+2)
fan(N,W,X,Y), fan(M,W,A,B), fresh(K) <=> N<M |
  fan(M,X,K+0,K+1), fan(M,Y,K+2,K+3),
  fan(N,A,K+0,K+2), fan(N,B,K+1,K+3),
  fresh(K+4)