From 49960d8950d001a372a0abde670a66ee60026957 Mon Sep 17 00:00:00 2001 From: Shinya Sato Date: Tue, 5 Mar 2024 18:19:27 +0900 Subject: v0.12.0 --- sample/245II.in | 62 -------- sample/245II_abbr.in | 101 -------------- sample/245II_new.in | 70 ---------- sample/AckSZ-3_5.in | 49 ------- sample/FibSZ_9.in | 33 ----- sample/TuringMachine.in | 131 ----------------- sample/ack_3_5.in | 32 ----- sample/bsort.in | 18 --- sample/fib-tail_9.in | 10 -- sample/fib_9.in | 16 --- sample/fib_9_abbr.in | 16 --- sample/gcd.in | 16 --- sample/gcd_another.in | 16 --- sample/hanoi.in | 30 ---- sample/isort.in | 15 -- sample/lambda/245II.in | 62 ++++++++ sample/lambda/245II_abbr.in | 101 ++++++++++++++ sample/lambda/245II_new.in | 70 ++++++++++ sample/lambda/linear-systemT.in | 142 +++++++++++++++++++ sample/linear-systemT.in | 142 ------------------- sample/map.in | 49 ------- sample/msort.in | 28 ---- sample/nqueen.in | 141 ------------------- sample/nqueenSZ.in | 225 ------------------------------ sample/pow.in | 16 --- sample/process_networks/processnet1.in | 22 +++ sample/process_networks/processnet_fib.in | 30 ++++ sample/processnet1.in | 22 --- sample/processnet_fib.in | 30 ---- sample/pseudo_higher_order/map.in | 49 +++++++ sample/pseudo_higher_order/reduce.in | 57 ++++++++ sample/puzzle/hanoi.in | 30 ++++ sample/puzzle/nqueen.in | 141 +++++++++++++++++++ sample/qsort.in | 19 --- sample/recursive_functions/ack_3_5.in | 32 +++++ sample/recursive_functions/fib-tail_9.in | 10 ++ sample/recursive_functions/fib_9.in | 16 +++ sample/recursive_functions/fib_9_abbr.in | 16 +++ sample/recursive_functions/gcd.in | 16 +++ sample/recursive_functions/gcd_another.in | 16 +++ sample/recursive_functions/pow.in | 16 +++ sample/reduce.in | 57 -------- sample/sort/bsort.in | 18 +++ sample/sort/isort.in | 15 ++ sample/sort/msort.in | 28 ++++ sample/sort/qsort.in | 19 +++ sample/turing_machine/TuringMachine.in | 131 +++++++++++++++++ sample/unary_numbers/AckSZ-3_5.in | 49 +++++++ sample/unary_numbers/FibSZ_9.in | 33 +++++ sample/unary_numbers/hanoiSZ.in | 31 ++++ sample/unary_numbers/nqueenSZ.in | 225 ++++++++++++++++++++++++++++++ 51 files changed, 1375 insertions(+), 1344 deletions(-) delete mode 100644 sample/245II.in delete mode 100644 sample/245II_abbr.in delete mode 100644 sample/245II_new.in delete mode 100644 sample/AckSZ-3_5.in delete mode 100644 sample/FibSZ_9.in delete mode 100644 sample/TuringMachine.in delete mode 100644 sample/ack_3_5.in delete mode 100644 sample/bsort.in delete mode 100644 sample/fib-tail_9.in delete mode 100644 sample/fib_9.in delete mode 100644 sample/fib_9_abbr.in delete mode 100644 sample/gcd.in delete mode 100644 sample/gcd_another.in delete mode 100644 sample/hanoi.in delete mode 100644 sample/isort.in create mode 100644 sample/lambda/245II.in create mode 100644 sample/lambda/245II_abbr.in create mode 100644 sample/lambda/245II_new.in create mode 100644 sample/lambda/linear-systemT.in delete mode 100644 sample/linear-systemT.in delete mode 100644 sample/map.in delete mode 100644 sample/msort.in delete mode 100644 sample/nqueen.in delete mode 100644 sample/nqueenSZ.in delete mode 100644 sample/pow.in create mode 100644 sample/process_networks/processnet1.in create mode 100644 sample/process_networks/processnet_fib.in delete mode 100644 sample/processnet1.in delete mode 100644 sample/processnet_fib.in create mode 100644 sample/pseudo_higher_order/map.in create mode 100644 sample/pseudo_higher_order/reduce.in create mode 100644 sample/puzzle/hanoi.in create mode 100644 sample/puzzle/nqueen.in delete mode 100644 sample/qsort.in create mode 100644 sample/recursive_functions/ack_3_5.in create mode 100644 sample/recursive_functions/fib-tail_9.in create mode 100644 sample/recursive_functions/fib_9.in create mode 100644 sample/recursive_functions/fib_9_abbr.in create mode 100644 sample/recursive_functions/gcd.in create mode 100644 sample/recursive_functions/gcd_another.in create mode 100644 sample/recursive_functions/pow.in delete mode 100644 sample/reduce.in create mode 100644 sample/sort/bsort.in create mode 100644 sample/sort/isort.in create mode 100644 sample/sort/msort.in create mode 100644 sample/sort/qsort.in create mode 100644 sample/turing_machine/TuringMachine.in create mode 100644 sample/unary_numbers/AckSZ-3_5.in create mode 100644 sample/unary_numbers/FibSZ_9.in create mode 100644 sample/unary_numbers/hanoiSZ.in create mode 100644 sample/unary_numbers/nqueenSZ.in (limited to 'sample') diff --git a/sample/245II.in b/sample/245II.in deleted file mode 100644 index 27910eb..0000000 --- a/sample/245II.in +++ /dev/null @@ -1,62 +0,0 @@ -// 245II in YALE encoding - -// Rules -Lam(a,b,c) >< App(x,y) => a~x, b~y, c~D; -D >< V => ; -B(a,x,e) >< Lam(b,c,y) => x~Lam(b,c,d), y~DB(a,d,e); -DB(a,b,c) >< V => a~c, b~V; -C(x,y) >< Lam(s,t,u) => - x~Lam(a,b,c), y~Lam(d,e,f), - s~Delta(a,d), t~Delta(b,e), u~C(c,f); -C(x,y) >< V => x~V, y~V; -Delta(x,y) >< Delta(a,b) => x~a, y~b; -B(x,a,b) >< Delta(c,d) => x~CB(a,b,Delta(c,d)); -Delta(a,b) >< CB(x,y,z) => - x~Delta(c,d), y~Delta(e,f), z~Delta(B(a,c,e),B(b,d,f)); -Delta(x,y) >< V => x~V, y~V; -Delta(x,y) >< C(t,s) => - x~C(a,b), y~C(c,d), t~Delta(b,d), s~Delta(a,c); -Delta(x,y) >< App(t,s) => - x~App(a,b), y~App(c,d), t~Delta(a,c), s~Delta(b,d); -Delta(x,y) >< Lam(t,s,u)=> - x~Lam(a,b,c), y~Lam(d,e,f), - t~Delta(a,d), s~Delta(b,e), u~Delta(c,f); -DB(x,y,z) >< CB(t,s,u) => - x~CB(d,e,u), y~CB(t,f,d), s~DB(e,f,z); -C(x,y) >< CB(t,s,u) => - x~CB(a,b,c), y~CB(d,e,f), - t~Delta(a,d), s~C(b,e), u~C(c,f); -D >< CB(a,b,c) => a~c, b~D; - -Eps >< Eps => ; -Eps >< S(x) => x~Eps; -Eps >< V => ; -Eps >< D =>; -Eps >< Delta(t,s) => t~Eps,s~Eps; -Eps >< Lam(t,s,u) => t~Eps,s~Eps,u~Eps; -Eps >< App(t,s) => t~Eps,s~Eps; -Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps; -Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps; - - -// Nets -// lam x.x -id1 ~ Lam(i,i,V); -id2 ~ Lam(i2,i2,V); - -// lam f. lam x. f(fx) -two ~ Lam(Lam(a,b,c),B(c,C(App(a,d),App(d,b)),V),V); - -// lam f. lam x. f(fx) -four ~ Lam(Lam(dz4, dx2, da1), B(da1, C(App(dz4, dz3), C(App(dz3, dz2), C(App(dz2, dz1), App(dz1, dx2)))), V), V); - -// lam f. lam x. f(fx) -five ~ Lam(Lam(z53, x23, a13), B(a13, C(App(z53, z43), C(App(z43, z33), C(App(z33,z23), C(App(z23, z13), App(z13, x23))))), V), V); - -// 245II -two ~ App(aux1, four); -aux1 ~ App(aux2, five); -aux2 ~ App(aux3, id1); -aux3 ~ App(aux4, id2); -aux4; -exit; diff --git a/sample/245II_abbr.in b/sample/245II_abbr.in deleted file mode 100644 index c2084ec..0000000 --- a/sample/245II_abbr.in +++ /dev/null @@ -1,101 +0,0 @@ -// 245II in YALE encoding - -// Rules - -D >< V => ; -B(a,b,c) >< Z => a~c, b~Z; -B(a,b,c) >< Lam(x,t,v) => b~Lam(x,t,w), v~DB(a,w,c); -DB(a,b,c) >< V => a~c, b~V; -C(x,y) >< Z => x~Z, y~Z; -C(x,y) >< Lam(s,t,u) => - x~Lam(a,b,c), y~Lam(d,e,f), - s~Delta(a,d), t~Delta(b,e), u~C(c,f); -C(x,y) >< V => x~V, y~V; -Delta(x,y) >< Delta(a,b) => x~a, y~b; -B(x,a,b) >< Delta(c,d) => x~CB(a,b,Delta(c,d)); -Delta(a,b) >< CB(x,y,z) => - x~Delta(c,d), y~Delta(e,f), z~Delta(B(a,c,e),B(b,d,f)); -Delta(x,y) >< S(z) => - x~S(a), y~S(b), z~Delta(a,b); -Delta(x,y) >< Z => x~Z, y~Z; -Delta(x,y) >< V => x~V, y~V; -Delta(x,y) >< C(t,s) => - x~C(a,b), y~C(c,d), t~Delta(b,d), s~Delta(a,c); -Delta(x,y) >< AppTo(t,s) => - x~AppTo(a,b), y~AppTo(c,d), t~Delta(a,c), s~Delta(b,d); -Delta(x,y) >< Lam(t,s,u)=> - x~Lam(a,b,c), y~Lam(d,e,f), - t~Delta(a,d), s~Delta(b,e), u~Delta(c,f); -DB(x,y,z) >< CB(t,s,u) => - x~CB(d,e,u), y~CB(t,f,d), s~DB(e,f,z); -C(x,y) >< CB(t,s,u) => - x~CB(a,b,c), y~CB(d,e,f), - t~Delta(a,d), s~C(b,e), u~C(c,f); -D >< CB(a,b,c) => a~c, b~D; - -Eps >< Eps => ; -Eps >< S(x) => x~Eps; -Eps >< V => ; -Eps >< D =>; -Eps >< Delta(t,s) => t~Eps,s~Eps; -Eps >< Lam(t,s,u) => t~Eps,s~Eps,u~Eps; -Eps >< AppTo(t,s) => t~Eps,s~Eps; -Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps; -Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps; - - - -Lam(x,t,c) >< AppTo(result,s) => result~t, x~s, c~D; -// We can write this avtive pair in nets as -// result << AppTo(s, lam_term) for AppTo(result, s)~ lam_term. - -// If the `<<' could be defined as user macro in future, -// then it becomes more readable: -// result << App(lam_term, s) =def= lam_term ~ App(result, s) - - -// Nets - -// lam x.x -id1 ~ Lam(x,x,V); -id2 ~ Lam(x,x,V); - - -// lam f. lam x. f(fx) -two ~ Lam(fb, Lam(x,r2,c),V), - fb ~ B(c,f,V), - f2,f1 << C(f), // C(f2,f1) ~ f - r2 << AppTo(r1, f2), - r1 << AppTo(x, f1); - - -// lam f. lam x. f(f(f(fx))) -four ~ Lam(fb, Lam(x, r4, c), V), - fb~B(c, f, V), - f4, C(f3, C(f2, f1)) << C(f), - r4 << AppTo(r3, f4), - r3 << AppTo(r2, f3), - r2 << AppTo(r1, f2), - r1 << AppTo(x, f1); - - -// lam f. lam x. f(f(f(f(fx)))) -five ~ Lam(fb, Lam(x, r5, c), V), - fb~B(c, f, V), - f5, C(f4, C(f3, C(f2, f1))) << C(f), - r5 << AppTo(r4, f5), - r4 << AppTo(r3, f4), - r3 << AppTo(r2, f3), - r2 << AppTo(r1, f2), - r1 << AppTo(x, f1); - - - -// (((24)5)I)I -aux24 << AppTo(four, two); -aux245 << AppTo(five, aux24); -aux245I << AppTo(id1, aux245); -aux245II << AppTo(id2, aux245I); - -aux245II; -exit; diff --git a/sample/245II_new.in b/sample/245II_new.in deleted file mode 100644 index 2050179..0000000 --- a/sample/245II_new.in +++ /dev/null @@ -1,70 +0,0 @@ -// 245II in YALE encoding - -// Rules -Lam(a,b,c) >< App(x,y) => a~x, b~y, c~D; -D >< V => ; -B(a,x,e) >< Lam(b,c,y) => x~Lam(b,c,d), y~DB(a,d,e); -DB(a,b,c) >< V => a~c, b~V; -C(x,y) >< Lam(s,t,u) => - x~Lam(a,b,c), y~Lam(d,e,f), - s~Delta(a,d), t~Delta(b,e), u~C(c,f); -C(x,y) >< V => x~V, y~V; -Delta(x,y) >< Delta(a,b) => x~a, y~b; -B(x,a,b) >< Delta(c,d) => x~CB(a,b,Delta(c,d)); -Delta(a,b) >< CB(x,y,z) => - x~Delta(c,d), y~Delta(e,f), z~Delta(B(a,c,e),B(b,d,f)); -Delta(x,y) >< V => x~V, y~V; -Delta(x,y) >< C(t,s) => - x~C(a,b), y~C(c,d), t~Delta(b,d), s~Delta(a,c); -Delta(x,y) >< App(t,s) => - x~App(a,b), y~App(c,d), t~Delta(a,c), s~Delta(b,d); -Delta(x,y) >< Lam(t,s,u)=> - x~Lam(a,b,c), y~Lam(d,e,f), - t~Delta(a,d), s~Delta(b,e), u~Delta(c,f); -DB(x,y,z) >< CB(t,s,u) => - x~CB(d,e,u), y~CB(t,f,d), s~DB(e,f,z); -C(x,y) >< CB(t,s,u) => - x~CB(a,b,c), y~CB(d,e,f), - t~Delta(a,d), s~C(b,e), u~C(c,f); -D >< CB(a,b,c) => a~c, b~D; - -Eps >< Eps => ; -Eps >< S(x) => x~Eps; -Eps >< V => ; -Eps >< D =>; -Eps >< Delta(t,s) => t~Eps,s~Eps; -Eps >< Lam(t,s,u) => t~Eps,s~Eps,u~Eps; -Eps >< App(t,s) => t~Eps,s~Eps; -Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps; -Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps; - - -// Nets -// lam x.x -new(r) >< Id => r~Lam(i,i,V); - -// lam f. lam x. f(fx) -new(r) >< Two => r~Lam(Lam(a,b,c),B(c,C(App(a,d),App(d,b)),V),V); - -// lam f. lam x. f(fx) -new(r) >< Four => r~Lam(Lam(a,b,c), B(c,C(App(a,d), C(App(d, e), C(App(e, f), App(f, b)))), V), V); - -// lam f. lam x. f(fx) -new(r) >< Five => r~Lam(Lam(a, b, c), B(c, C(App(a, d), C(App(d, e), C(App(e,f), C(App(f, g), App(g, b))))), V), V); - - -// instances -id1 << new(Id); -id2 << new(Id); -two << new(Two); -four << new(Four); -five << new(Five); - - -// 245II -two ~ App(aux1, four); -aux1 ~ App(aux2, five); -aux2 ~ App(aux3, id1); -aux3 ~ App(aux4, id2); -aux4; -exit; diff --git a/sample/AckSZ-3_5.in b/sample/AckSZ-3_5.in deleted file mode 100644 index 4f41966..0000000 --- a/sample/AckSZ-3_5.in +++ /dev/null @@ -1,49 +0,0 @@ -// Ackermann function on unary natural numbers - -// Originally the function is written as follows: -// fun ack(0,y) = y+1 -// | ack(x,0) = ack(x-1,1) -// | ack(x,y) = ack(x-1,ack(x,y-1)); - -// This is written one on unary natural nunbers: -// fun ack(Z , y) = S(y) -// | ack(S(x), Z) = ack(x,S(Z)) -// | ack(S(x), S(y)) = ack(x,ack(S(x),y)); - -// For easily translation to interaction nets, -// the first argument will be moved to the last: -// fun ack(y, Z) = S(y) -// | ack(Z, S(x)) = ack(S(Z),x) -// | ack(S(y), S(x)) = ack(ack(y,S(x)),x); - -// It is traslated directly as follows: -// ack(r,y)>< Z => r~S(y); -// ack(r,y)>< S(x) => ack_Sx(r, x)~y; -// ack_Sx(r,x)>< Z => ack(r, S(Z))~x; -// ack_Sx(r,x)>< S(y) => Dup(x1,x2)~x, ack(r,cnt)~x1, ack(cnt,y)~S(x2); - -// The last connection can be optimised by applying the rule ack>< Z => r~S(y); -ack(r,y)>< S(x) => ack_Sx(r, x)~y; -ack_Sx(r,x)>< Z => ack(r, S(Z))~x; -ack_Sx(r,x)>< S(y) => Dup(x1,x2)~x, ack(r,cnt)~x1, ack_Sx(cnt,x2)~y; - - -// By the way, it is possible to write it by using abbreviation notation: -// ack(r,y)>< Z => r~S(y); -// ack(r,y)>< S(x) => r<< Z => r<< S(y) => x1,x2<< Z => a1~Z, a2~Z; -// Dup(a1,a2)>< S(x) => a1~S(w1), a2~S(w2), Dup(w1,w2)~x; - -// ack(result, y)~x -// For computation `ack 3 5', it is written as follows: -ack(result, S(S(S(S(S(Z))))))~S(S(S(Z))); - -prnat result; -exit; diff --git a/sample/FibSZ_9.in b/sample/FibSZ_9.in deleted file mode 100644 index b5a65a8..0000000 --- a/sample/FibSZ_9.in +++ /dev/null @@ -1,33 +0,0 @@ -// Fibonacci number on unary natural numbers -fib(r)> r~Z; -fib(r)> fibS(r)~x; -fibS(r)> r~S(Z); -fibS(r)> Dup(x1,x2)~x, add(r,r2)~r1, fib(r2)~x2, fibS(r1)~x1; - - - -//------ ADD ------ -//Add para -add(r,x)> r~x; -add(r,x)> r~S(w), add(w,x)~y; - -//Add_Seq -//add(r,y)> y~r; -//add(r,y)> add(r, S(y))~x; - - -// ------ DUP ------ -// Dup is defined as built-in: -// -// Dup(x1,x2)> x1~Z, x2~Z; -// Dup(x1,x2)> x1~S(w1), x2~S(w2), Dup(w1,w2)~x; - - - - -// Execution -// Fib 9 -fib(r)~S(S(S(S(S(S(S(S(S(Z))))))))); -prnat r; -free r; - diff --git a/sample/TuringMachine.in b/sample/TuringMachine.in deleted file mode 100644 index 2819d19..0000000 --- a/sample/TuringMachine.in +++ /dev/null @@ -1,131 +0,0 @@ -// ------------------------------------------------------------- -// Turing Machine -// ------------------------------------------------------------- -// Every 1 on tapes becomes 0. -// It finishes when the head reads a tape cell whose value is 0. -// -// Rule -// (state, sym) => command -// (0 , 1) => Write(0, 1) // write 0 and change state into 1 -// (1 , 0) => GoRight(2) // headPos+1 and change state into 2 -// (2 , 1) => Write(0, 1) // write 0 and change state into 1 -// otherwise => Halt -// -// Example: -// (tape, state, headPos) -// ([0,1,1,1,1,0], 1, 0) -->* ([0,0,0,0,0,0,0],2,5) -// - - - -// ----------------------------------------- -// getRule -// rule << getRule( (int state, int sym) ) -// NOTE: getRule needs a pair (state, sym). -// So it should be called such as -// ret << getRule( (state, sym) ); -// ----------------------------------------- - -getRule(r) >< (int state, int sym) -| (state==0) && (sym==1) => r~Write(0, 1) -| (state==1) && (sym==0) => r~GoRight(2) -| (state==2) && (sym==1) => r~Write(0, 1) -| _ => r~Halt; - - - - -// ----------------------------------------- -// changeSym -// resultTape << changeSym(headPos, sym, tape) -// ----------------------------------------- - -changeSym(resultTape, headPos, sym) >< t:ts => // <-- t:ts is tape - resultTape << changeSym_sub([], headPos, sym, t:ts); - -changeSym_sub(r, done, int headPos, int sym) >< (int t):ts - | headPos == 0 => r << Append(done, sym:ts) - | _ => done_new << Append(done, [t]), - r << changeSym_sub(done_new, headPos-1, sym, ts); - -changeSym_sub(r, done, headPos, sym) >< [] => - r~Error(done, headPos, sym); - - - - -// ----------------------------------------- -// do -// configure << do(tape, int state, int headPos, Command) -// ----------------------------------------- - -do(r, tape, int state, int headPos) >< Write(sym, new_state) => - changeSym(doneTape, headPos, sym) ~ tape, - r ~ Configure(doneTape, new_state, headPos); - -do(r, tape, int state, int head) >< GoRight(int new_state) => - r ~ Configure(tape, new_state, head+1); - -do(r, tape, int state, int head) >< Halt => - r ~ STOP_Configure(tape, state, head); - - - -// ----------------------------------------- -// getSym -// tapeDone << getSym(sym, int headPos, tape) -// ----------------------------------------- - -getSym(tapeDone, sym, int headPos) >< t:ts => // <- t:ts is tape - tapeDone << getSym_sub([], sym, headPos, t:ts); - - -getSym_sub(r, done, sym, int headPos) >< (int t):ts - | headPos == 0 => r << Append(done, t:ts), sym~t - | _ => cnt << Append(done,[t]), - r << getSym_sub(cnt, sym, headPos-1, ts); - -getSym_sub(r, done, sym, int headPos) >< [] - | headPos == 0 => r << Append(done, [0]), sym~0 - | _ => new_done << Append(done, [0]), - r << getSym_sub(new_done, sym, headPos-1, []); - - - -// ----------------------------------------- -// oneCycle -// configure << Configure(tape, int state, int headPos) -// ----------------------------------------- - -oneCycle(r) >< Configure(tape, int state, int headPos) => - tapeDone, sym << getSym(headPos, tape), - r << oneCycle_sub(tapeDone, state, headPos, sym); - -oneCycle_sub(r, tapeDone, int state, int headPos)><(int sym) => - rule << getRule( (state, sym) ), - r << do(tapeDone, state, headPos, rule); - - - -// ----------------------------------------- -// allCycle -// result << allCycle(Configure(tape, state, headPos)) -// ----------------------------------------- - -allCycle(r) >< Configure(tape, state, headPos) => - r1 << oneCycle(Configure(tape, state, headPos)), - r << allCycle(r1); - -allCycle(r) >< STOP_Configure(tape, state, headPos) => - r ~ Configure(tape, state, headPos); - - - - -// ----------------------------------------- -// main -// ----------------------------------------- - -configure ~ Configure([1,1,1,1,1,0], 0, 0), //(tape, state, headPos) -r << allCycle(configure); -r; // -->* Configure([0,0,0,0,0,0,0],2,5) diff --git a/sample/ack_3_5.in b/sample/ack_3_5.in deleted file mode 100644 index 19f92fa..0000000 --- a/sample/ack_3_5.in +++ /dev/null @@ -1,32 +0,0 @@ -// Ackermann Function -// -// fun ack(0,n) = n+1 -// | ack(m,0) = ack(m-1,1) -// | ack(m,n) = ack(m-1,ack(m,n-1)); - -// The following rule is wrong because there is no gurantee that -// the 'cnt' is connected to an integer agent -// when ack(r)~(m-1,cnt) is evaluated. -// -// ack(r) >< (int m, int n) -// | m==0 => r~(n+1) -// | n==0 => ack(r) ~ (m-1,1) -// | _ => ack(cnt)~(m,n-1), ack(r)~(m-1,cnt); -// -// So, the `cnt' should be connected as an element of connections. - -ack(ret, int m) >< (int n) -| m==0 => ret~(n+1) -| n==0 => ack(ret, m-1)~1 -| _ => ack(cnt, m)~(n-1), ack(ret, m-1)~cnt; - -ackMain(ret)><(int m, int n) => ack(ret,m)~n; - - -// main -const M=3; -const N=5; -ackMain(ret)~(M,N); -ret; -free ret; - diff --git a/sample/bsort.in b/sample/bsort.in deleted file mode 100644 index 7b2e2d6..0000000 --- a/sample/bsort.in +++ /dev/null @@ -1,18 +0,0 @@ -// Bubble sort - -// Rules -bsort(ret) >< [] => ret~[]; -bsort(ret) >< x:xs => bsort(ret)~cnt, bubble(cnt, x)~xs; -bsort(ret) >< M(x) => ret~x; - -bubble(ret, int x) >< [] => ret~M([x]); -bubble(ret, int x) >< M(w) => ret~M(x:w); -bubble(ret, int x) >< (int y):ys -| x ret~(x:cnt), bubble(cnt, y)~ys -| _ => ret~(y:cnt), bubble(cnt, x)~ys; - - -// Nets -bsort(r)~[3,6,1,9,2]; -r; - diff --git a/sample/fib-tail_9.in b/sample/fib-tail_9.in deleted file mode 100644 index 58f4cc5..0000000 --- a/sample/fib-tail_9.in +++ /dev/null @@ -1,10 +0,0 @@ -// Fibonacci number -fibt(r, int a, int b) >< (int n) -| n == 0 => r~0 -| n == 1 => r~a -| _ => fibt(r, a+b, a) ~ (n-1); - -fibMain(r) >< (int n) => fibt(r, 1, 0) ~ n; - -fibMain(r)~9; -r; diff --git a/sample/fib_9.in b/sample/fib_9.in deleted file mode 100644 index 7c4af1f..0000000 --- a/sample/fib_9.in +++ /dev/null @@ -1,16 +0,0 @@ -// Fibonacci number - -// Rules -fib(ret) >< (int n) -| n == 0 => ret~0 -| n == 1 => ret~1 -| _ => fib(cnt1)~(n-1), fib(cnt2)~(n-2), Add(ret, cnt2)~cnt1; - - -// Note: Add is implemented as a built-in agent such that: -// Add(ret, int m) ~ (int n) --> ret~(m+n); - -// Nets -fib(ret)~9; -ret; - diff --git a/sample/fib_9_abbr.in b/sample/fib_9_abbr.in deleted file mode 100644 index 57a8c62..0000000 --- a/sample/fib_9_abbr.in +++ /dev/null @@ -1,16 +0,0 @@ -// Fibonacci number - -// Rules -fib(ret) >< (int n) -| n == 0 => ret~0 -| n == 1 => ret~1 -| _ => cnt1 << fib(n-1), cnt2 << fib(n-2), ret << Add(cnt1,cnt2); - - -// Note: Add is implemented as a built-in agent such that: -// Add(ret, int m) ~ (int n) --> ret~(m+n); - -// Nets -ret << fib(9); -ret; - diff --git a/sample/gcd.in b/sample/gcd.in deleted file mode 100644 index 5a57d8d..0000000 --- a/sample/gcd.in +++ /dev/null @@ -1,16 +0,0 @@ -// Greatest common divisor -// -//def gcd(a: Int, b: Int): Int = -// if (b==0) a else gcd(b, a%b) - - -// Rule -gcd(ret, int a) >< (int b) -| b==0 => ret ~ a -| _ => gcd(ret, b) ~ a%b; - -// Net -gcd(r, 14) ~ 21; -r; // it should be 7 - - diff --git a/sample/gcd_another.in b/sample/gcd_another.in deleted file mode 100644 index e616e28..0000000 --- a/sample/gcd_another.in +++ /dev/null @@ -1,16 +0,0 @@ -// Greatest common divisor -// -//def gcd(a: Int, b: Int): Int = -// if (b==0) a else gcd(b, a%b) - - -// Rule -gcd(ret) >< (int a, int b) -| b==0 => ret ~ a -| _ => gcd(ret) ~ (b, a%b); - -// Net -gcd(r) ~ (14,21); -r; // it should be 7 - - diff --git a/sample/hanoi.in b/sample/hanoi.in deleted file mode 100644 index 5be47c6..0000000 --- a/sample/hanoi.in +++ /dev/null @@ -1,30 +0,0 @@ -// Tower of Hanoi Puzzle - -// Rules -hanoi(return, source, target, aux) >< (int n) -| n==0 => - // Erase the source, target and aux - source ~ Eraser, - target ~ Eraser, - aux ~ Eraser, - - // result - return~[] - -| _ => - // Duplicate the source, target and aux - source ~ Dup(src1, Dup(src2, src3)), - target ~ Dup(tgt1, Dup(tgt2, tgt3)), - aux ~ Dup(aux1, aux2), - - // recursive applications - hanoi(ret1, src1, aux1, tgt1)~(n-1), - hanoi(ret2, aux2, tgt2, src2)~(n-1), - - // result - return << Append(ret1, (n,src3,tgt3):ret2); - - -// Net -hanoi(result, A, C, B) ~ 3; -result; // should be [(1,A,C),(2,A,B),(1,C,B),(3,A,C),(1,B,A),(2,B,C),(1,A,C)] diff --git a/sample/isort.in b/sample/isort.in deleted file mode 100644 index e637055..0000000 --- a/sample/isort.in +++ /dev/null @@ -1,15 +0,0 @@ -// Insertion sort - -// Rules -isort(ret) >< [] => ret~[]; -isort(ret) >< x:xs => insert(ret, x)~cnt, isort(cnt)~xs; - -insert(ret, int x) >< [] => ret~[x]; -insert(ret, int x) >< (int y):ys -| x<=y => ret~(x:y:ys) -| _ => ret~(y:cnt), insert(cnt, x)~ys; - - -// Nets -isort(r)~[3,6,1,9,2]; -r; diff --git a/sample/lambda/245II.in b/sample/lambda/245II.in new file mode 100644 index 0000000..27910eb --- /dev/null +++ b/sample/lambda/245II.in @@ -0,0 +1,62 @@ +// 245II in YALE encoding + +// Rules +Lam(a,b,c) >< App(x,y) => a~x, b~y, c~D; +D >< V => ; +B(a,x,e) >< Lam(b,c,y) => x~Lam(b,c,d), y~DB(a,d,e); +DB(a,b,c) >< V => a~c, b~V; +C(x,y) >< Lam(s,t,u) => + x~Lam(a,b,c), y~Lam(d,e,f), + s~Delta(a,d), t~Delta(b,e), u~C(c,f); +C(x,y) >< V => x~V, y~V; +Delta(x,y) >< Delta(a,b) => x~a, y~b; +B(x,a,b) >< Delta(c,d) => x~CB(a,b,Delta(c,d)); +Delta(a,b) >< CB(x,y,z) => + x~Delta(c,d), y~Delta(e,f), z~Delta(B(a,c,e),B(b,d,f)); +Delta(x,y) >< V => x~V, y~V; +Delta(x,y) >< C(t,s) => + x~C(a,b), y~C(c,d), t~Delta(b,d), s~Delta(a,c); +Delta(x,y) >< App(t,s) => + x~App(a,b), y~App(c,d), t~Delta(a,c), s~Delta(b,d); +Delta(x,y) >< Lam(t,s,u)=> + x~Lam(a,b,c), y~Lam(d,e,f), + t~Delta(a,d), s~Delta(b,e), u~Delta(c,f); +DB(x,y,z) >< CB(t,s,u) => + x~CB(d,e,u), y~CB(t,f,d), s~DB(e,f,z); +C(x,y) >< CB(t,s,u) => + x~CB(a,b,c), y~CB(d,e,f), + t~Delta(a,d), s~C(b,e), u~C(c,f); +D >< CB(a,b,c) => a~c, b~D; + +Eps >< Eps => ; +Eps >< S(x) => x~Eps; +Eps >< V => ; +Eps >< D =>; +Eps >< Delta(t,s) => t~Eps,s~Eps; +Eps >< Lam(t,s,u) => t~Eps,s~Eps,u~Eps; +Eps >< App(t,s) => t~Eps,s~Eps; +Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps; +Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps; + + +// Nets +// lam x.x +id1 ~ Lam(i,i,V); +id2 ~ Lam(i2,i2,V); + +// lam f. lam x. f(fx) +two ~ Lam(Lam(a,b,c),B(c,C(App(a,d),App(d,b)),V),V); + +// lam f. lam x. f(fx) +four ~ Lam(Lam(dz4, dx2, da1), B(da1, C(App(dz4, dz3), C(App(dz3, dz2), C(App(dz2, dz1), App(dz1, dx2)))), V), V); + +// lam f. lam x. f(fx) +five ~ Lam(Lam(z53, x23, a13), B(a13, C(App(z53, z43), C(App(z43, z33), C(App(z33,z23), C(App(z23, z13), App(z13, x23))))), V), V); + +// 245II +two ~ App(aux1, four); +aux1 ~ App(aux2, five); +aux2 ~ App(aux3, id1); +aux3 ~ App(aux4, id2); +aux4; +exit; diff --git a/sample/lambda/245II_abbr.in b/sample/lambda/245II_abbr.in new file mode 100644 index 0000000..c2084ec --- /dev/null +++ b/sample/lambda/245II_abbr.in @@ -0,0 +1,101 @@ +// 245II in YALE encoding + +// Rules + +D >< V => ; +B(a,b,c) >< Z => a~c, b~Z; +B(a,b,c) >< Lam(x,t,v) => b~Lam(x,t,w), v~DB(a,w,c); +DB(a,b,c) >< V => a~c, b~V; +C(x,y) >< Z => x~Z, y~Z; +C(x,y) >< Lam(s,t,u) => + x~Lam(a,b,c), y~Lam(d,e,f), + s~Delta(a,d), t~Delta(b,e), u~C(c,f); +C(x,y) >< V => x~V, y~V; +Delta(x,y) >< Delta(a,b) => x~a, y~b; +B(x,a,b) >< Delta(c,d) => x~CB(a,b,Delta(c,d)); +Delta(a,b) >< CB(x,y,z) => + x~Delta(c,d), y~Delta(e,f), z~Delta(B(a,c,e),B(b,d,f)); +Delta(x,y) >< S(z) => + x~S(a), y~S(b), z~Delta(a,b); +Delta(x,y) >< Z => x~Z, y~Z; +Delta(x,y) >< V => x~V, y~V; +Delta(x,y) >< C(t,s) => + x~C(a,b), y~C(c,d), t~Delta(b,d), s~Delta(a,c); +Delta(x,y) >< AppTo(t,s) => + x~AppTo(a,b), y~AppTo(c,d), t~Delta(a,c), s~Delta(b,d); +Delta(x,y) >< Lam(t,s,u)=> + x~Lam(a,b,c), y~Lam(d,e,f), + t~Delta(a,d), s~Delta(b,e), u~Delta(c,f); +DB(x,y,z) >< CB(t,s,u) => + x~CB(d,e,u), y~CB(t,f,d), s~DB(e,f,z); +C(x,y) >< CB(t,s,u) => + x~CB(a,b,c), y~CB(d,e,f), + t~Delta(a,d), s~C(b,e), u~C(c,f); +D >< CB(a,b,c) => a~c, b~D; + +Eps >< Eps => ; +Eps >< S(x) => x~Eps; +Eps >< V => ; +Eps >< D =>; +Eps >< Delta(t,s) => t~Eps,s~Eps; +Eps >< Lam(t,s,u) => t~Eps,s~Eps,u~Eps; +Eps >< AppTo(t,s) => t~Eps,s~Eps; +Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps; +Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps; + + + +Lam(x,t,c) >< AppTo(result,s) => result~t, x~s, c~D; +// We can write this avtive pair in nets as +// result << AppTo(s, lam_term) for AppTo(result, s)~ lam_term. + +// If the `<<' could be defined as user macro in future, +// then it becomes more readable: +// result << App(lam_term, s) =def= lam_term ~ App(result, s) + + +// Nets + +// lam x.x +id1 ~ Lam(x,x,V); +id2 ~ Lam(x,x,V); + + +// lam f. lam x. f(fx) +two ~ Lam(fb, Lam(x,r2,c),V), + fb ~ B(c,f,V), + f2,f1 << C(f), // C(f2,f1) ~ f + r2 << AppTo(r1, f2), + r1 << AppTo(x, f1); + + +// lam f. lam x. f(f(f(fx))) +four ~ Lam(fb, Lam(x, r4, c), V), + fb~B(c, f, V), + f4, C(f3, C(f2, f1)) << C(f), + r4 << AppTo(r3, f4), + r3 << AppTo(r2, f3), + r2 << AppTo(r1, f2), + r1 << AppTo(x, f1); + + +// lam f. lam x. f(f(f(f(fx)))) +five ~ Lam(fb, Lam(x, r5, c), V), + fb~B(c, f, V), + f5, C(f4, C(f3, C(f2, f1))) << C(f), + r5 << AppTo(r4, f5), + r4 << AppTo(r3, f4), + r3 << AppTo(r2, f3), + r2 << AppTo(r1, f2), + r1 << AppTo(x, f1); + + + +// (((24)5)I)I +aux24 << AppTo(four, two); +aux245 << AppTo(five, aux24); +aux245I << AppTo(id1, aux245); +aux245II << AppTo(id2, aux245I); + +aux245II; +exit; diff --git a/sample/lambda/245II_new.in b/sample/lambda/245II_new.in new file mode 100644 index 0000000..2050179 --- /dev/null +++ b/sample/lambda/245II_new.in @@ -0,0 +1,70 @@ +// 245II in YALE encoding + +// Rules +Lam(a,b,c) >< App(x,y) => a~x, b~y, c~D; +D >< V => ; +B(a,x,e) >< Lam(b,c,y) => x~Lam(b,c,d), y~DB(a,d,e); +DB(a,b,c) >< V => a~c, b~V; +C(x,y) >< Lam(s,t,u) => + x~Lam(a,b,c), y~Lam(d,e,f), + s~Delta(a,d), t~Delta(b,e), u~C(c,f); +C(x,y) >< V => x~V, y~V; +Delta(x,y) >< Delta(a,b) => x~a, y~b; +B(x,a,b) >< Delta(c,d) => x~CB(a,b,Delta(c,d)); +Delta(a,b) >< CB(x,y,z) => + x~Delta(c,d), y~Delta(e,f), z~Delta(B(a,c,e),B(b,d,f)); +Delta(x,y) >< V => x~V, y~V; +Delta(x,y) >< C(t,s) => + x~C(a,b), y~C(c,d), t~Delta(b,d), s~Delta(a,c); +Delta(x,y) >< App(t,s) => + x~App(a,b), y~App(c,d), t~Delta(a,c), s~Delta(b,d); +Delta(x,y) >< Lam(t,s,u)=> + x~Lam(a,b,c), y~Lam(d,e,f), + t~Delta(a,d), s~Delta(b,e), u~Delta(c,f); +DB(x,y,z) >< CB(t,s,u) => + x~CB(d,e,u), y~CB(t,f,d), s~DB(e,f,z); +C(x,y) >< CB(t,s,u) => + x~CB(a,b,c), y~CB(d,e,f), + t~Delta(a,d), s~C(b,e), u~C(c,f); +D >< CB(a,b,c) => a~c, b~D; + +Eps >< Eps => ; +Eps >< S(x) => x~Eps; +Eps >< V => ; +Eps >< D =>; +Eps >< Delta(t,s) => t~Eps,s~Eps; +Eps >< Lam(t,s,u) => t~Eps,s~Eps,u~Eps; +Eps >< App(t,s) => t~Eps,s~Eps; +Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps; +Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps; + + +// Nets +// lam x.x +new(r) >< Id => r~Lam(i,i,V); + +// lam f. lam x. f(fx) +new(r) >< Two => r~Lam(Lam(a,b,c),B(c,C(App(a,d),App(d,b)),V),V); + +// lam f. lam x. f(fx) +new(r) >< Four => r~Lam(Lam(a,b,c), B(c,C(App(a,d), C(App(d, e), C(App(e, f), App(f, b)))), V), V); + +// lam f. lam x. f(fx) +new(r) >< Five => r~Lam(Lam(a, b, c), B(c, C(App(a, d), C(App(d, e), C(App(e,f), C(App(f, g), App(g, b))))), V), V); + + +// instances +id1 << new(Id); +id2 << new(Id); +two << new(Two); +four << new(Four); +five << new(Five); + + +// 245II +two ~ App(aux1, four); +aux1 ~ App(aux2, five); +aux2 ~ App(aux3, id1); +aux3 ~ App(aux4, id2); +aux4; +exit; diff --git a/sample/lambda/linear-systemT.in b/sample/lambda/linear-systemT.in new file mode 100644 index 0000000..f0e3ccb --- /dev/null +++ b/sample/lambda/linear-systemT.in @@ -0,0 +1,142 @@ +// sample programs of linear-systemT (see POPL2016 paper) + +// Basic Rules ---------------------------------------- +Lamc(x,y) >< App(a,b) => a~x, b~y; +Times(a,b) >< Par(x,y) => a~x, b~y; +B(a,b,c) >< Lamc(x,y) => a~c, b~Lamc(x,y); +V >< Lam(x,y,z) => z~Lamc(x,y); +B(a,b,c)> b~S(w), x~B(a,w,c); // original +//B(a,b,c) >< S(x) => a~c, b~S(x); // alternative +B(a,b,c) >< Z => a~c, b~Z; + + +// Iterator ---------------------------------------- +Iter(r,n,u) >< Lamc(x,t) => n~Itc(u,x,t,r); +Itc(u,x,t,r) >< Z => u~r,x~Eps,t~Eps; +Itc(u,x,t,r) >< S(y) => y~Itc(t2,w,t1,r), x~Dup(w,u),t~Dup(t1,t2); + +// Dup ---------------------------------------- +Dup(x,y) >< Dup(a,b) => x~a, y~b; +Dup(x,y) >< Lamc(a,b) => x~Lamc(w1,w2), y~Lamc(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2); +Dup(x,y) >< App(a,b) => x~App(w1,w2), y~App(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2); +Dup(x,y) >< Times(a,b) => x~Times(w1,w2), y~Times(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2); +Dup(x,y) >< Par(a,b) => x~Par(w1,w2), y~Par(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2); +Dup(x,y) >< V => x~V, y~V; + +Dup(a1,a2)>< Z => a1~Z, a2~Z; +Dup(a1,a2)>< S(x) => a1~S(w1), a2~S(w2), x~Dup(w1,w2); + + +Dup(x,y) >< Iter(a,b,c) => + x~Iter(u1,w1,z1), y~Iter(u2,w2,z2), + a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2); + +Dup(x,y) >< Itc(a,b,c,d) => + x~Itc(u1,w1,z1,k1), y~Itc(u2,w2,z2,k2), + a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2), d~Dup(k1,k2); + + +/* required */ +Dup(x,y) >< B(a,b,c) => x~B(u1,z1,w1), y~B(u2,z2,w2), + a~Dup(u1,u2), b~Dup(z1,z2), c~Dup(w1,w2); +Dup(x,y) >< Lam(a,b,c) => x~Lam(w1,u1,z1), y~Lam(w2,u2,z2), + a~Dup(w1,w2), b~Dup(u1,u2), c~Dup(z1,z2); + + +// Eps ---------------------------------------- +Eps >< Eps => ; +Eps >< Dup(x,y) => Eps~x,Eps~y; +Eps >< Lamc(x,y) => Eps~x,Eps~y; +Eps >< App(x,y) => Eps~x, Eps~y; +Eps >< Par(x,y) => Eps~x, Eps~y; +Eps >< Times(x,y) => Eps~x, Eps~y; + +Eps >< S(x) => x~Eps; +Eps >< Z => ; + +Eps >< Iter(a,b,c) => a~Eps, b~Eps, c~Eps; +Eps >< Itc(a,b,c,d) => a~Eps, b~Eps, c~Eps,d~Eps; + +/* required */ +Eps >< B(a,b,c) => a~Eps, b~Eps, c~Eps; +Eps >< Lam(a,b,c) => a~Eps, b~Eps, c~Eps; +Eps >< V => ; + + +// sample ---------------------------------------- +// Cp: nat -o nat Times nat +n~S(S(Z)), +cp~Lamc(x,r), Iter(r,x,Times(Z,Z))~Lamc(Par(a,b),Times(S(a),S(b))); +cp~App(n,res); +res; +free res; + +// fst: nat Times nat -o nat +pair~Times(S(S(S(Z))),S(Z)), +fst~Lamc(Par(n,m), r), Iter(r,m,n)~Lamc(x,x); +fst~App(pair,res); +res; +free res; + +// snd: nat Times nat -o nat +pair~Times(S(S(S(Z))),S(Z)), +snd~Lamc(Par(n,m), r), Iter(r,n,m)~Lamc(x,x); +snd~App(pair,res); +res; +free res; + + +// ((Add a) b) +a~S(S(Z)), b~S(S(S(Z))), +add~Lamc(B(V,u,Lam(n,r,r1)),r1), Iter(r,n,u)~Lamc(x,S(x)); +add~App(a,App(b,res)); +prnat res; +free res; + + +// ((Mult a) b) +a~S(S(Z)), b~S(S(S(Z))); +add~Lamc(B(V,au,Lam(an,ar,ar1)),ar1),Iter(ar,an,au)~Lamc(ax,S(ax)), +App(n,Iter(r,m,Z))~add, +mult~Lamc(B(V,n,Lam(m,r,r1)),r1); +mult~App(a,App(b,res)); +prnat res; +free res; + +// ((Exp a) b) +a~S(S(Z)), b~S(S(S(Z))); +add~Lamc(B(V,au,Lam(an,ar,ar1)),ar1),Iter(ar,an,au)~Lamc(ax,S(ax)), +App(mn,Iter(mr,mm,Z))~add, +mult~Lamc(B(V,mn,Lam(mm,mr,mr1)),mr1), +App(n,Iter(r,m,S(Z)))~mult, +exp~Lamc(B(V,n,Lam(m,r,r1)),r1); +exp~App(a,App(b,res)); +prnat res; +free res; + + +// Ack 3 10 +// ver.1: the same as the example on the paper +a~S(S(S(Z))), +b~S(S(S(S(S(S(S(S(S(S(Z)))))))))); +Iter(t,x,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1), +Lamc(x,t)~App(a,App(b, r)); +prnat r; +free r; + +// ver.2: \m.(\n.(iter m (\x.(S x)) (\x.(\y.(iter (S y) (S 0) x))) n)) +a~S(S(S(Z))), +b~S(S(S(S(S(S(S(S(S(S(Z)))))))))); +Iter(App(n,apr),x,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1), +Lamc(B(V,x,Lam(n,apr,nr)),nr)~App(a,App(b, r)); +prnat r; +free r; + +// ver.3: another encoding of ver.2. +a~S(S(S(Z))), +b~S(S(S(S(S(S(S(S(S(S(Z)))))))))); +Iter(t,m,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1), +Lamc(m,t)~App(n,apr), +Lamc(n,apr)~App(a,App(b, r)); +prnat r; +free r; diff --git a/sample/linear-systemT.in b/sample/linear-systemT.in deleted file mode 100644 index f0e3ccb..0000000 --- a/sample/linear-systemT.in +++ /dev/null @@ -1,142 +0,0 @@ -// sample programs of linear-systemT (see POPL2016 paper) - -// Basic Rules ---------------------------------------- -Lamc(x,y) >< App(a,b) => a~x, b~y; -Times(a,b) >< Par(x,y) => a~x, b~y; -B(a,b,c) >< Lamc(x,y) => a~c, b~Lamc(x,y); -V >< Lam(x,y,z) => z~Lamc(x,y); -B(a,b,c)> b~S(w), x~B(a,w,c); // original -//B(a,b,c) >< S(x) => a~c, b~S(x); // alternative -B(a,b,c) >< Z => a~c, b~Z; - - -// Iterator ---------------------------------------- -Iter(r,n,u) >< Lamc(x,t) => n~Itc(u,x,t,r); -Itc(u,x,t,r) >< Z => u~r,x~Eps,t~Eps; -Itc(u,x,t,r) >< S(y) => y~Itc(t2,w,t1,r), x~Dup(w,u),t~Dup(t1,t2); - -// Dup ---------------------------------------- -Dup(x,y) >< Dup(a,b) => x~a, y~b; -Dup(x,y) >< Lamc(a,b) => x~Lamc(w1,w2), y~Lamc(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2); -Dup(x,y) >< App(a,b) => x~App(w1,w2), y~App(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2); -Dup(x,y) >< Times(a,b) => x~Times(w1,w2), y~Times(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2); -Dup(x,y) >< Par(a,b) => x~Par(w1,w2), y~Par(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2); -Dup(x,y) >< V => x~V, y~V; - -Dup(a1,a2)>< Z => a1~Z, a2~Z; -Dup(a1,a2)>< S(x) => a1~S(w1), a2~S(w2), x~Dup(w1,w2); - - -Dup(x,y) >< Iter(a,b,c) => - x~Iter(u1,w1,z1), y~Iter(u2,w2,z2), - a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2); - -Dup(x,y) >< Itc(a,b,c,d) => - x~Itc(u1,w1,z1,k1), y~Itc(u2,w2,z2,k2), - a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2), d~Dup(k1,k2); - - -/* required */ -Dup(x,y) >< B(a,b,c) => x~B(u1,z1,w1), y~B(u2,z2,w2), - a~Dup(u1,u2), b~Dup(z1,z2), c~Dup(w1,w2); -Dup(x,y) >< Lam(a,b,c) => x~Lam(w1,u1,z1), y~Lam(w2,u2,z2), - a~Dup(w1,w2), b~Dup(u1,u2), c~Dup(z1,z2); - - -// Eps ---------------------------------------- -Eps >< Eps => ; -Eps >< Dup(x,y) => Eps~x,Eps~y; -Eps >< Lamc(x,y) => Eps~x,Eps~y; -Eps >< App(x,y) => Eps~x, Eps~y; -Eps >< Par(x,y) => Eps~x, Eps~y; -Eps >< Times(x,y) => Eps~x, Eps~y; - -Eps >< S(x) => x~Eps; -Eps >< Z => ; - -Eps >< Iter(a,b,c) => a~Eps, b~Eps, c~Eps; -Eps >< Itc(a,b,c,d) => a~Eps, b~Eps, c~Eps,d~Eps; - -/* required */ -Eps >< B(a,b,c) => a~Eps, b~Eps, c~Eps; -Eps >< Lam(a,b,c) => a~Eps, b~Eps, c~Eps; -Eps >< V => ; - - -// sample ---------------------------------------- -// Cp: nat -o nat Times nat -n~S(S(Z)), -cp~Lamc(x,r), Iter(r,x,Times(Z,Z))~Lamc(Par(a,b),Times(S(a),S(b))); -cp~App(n,res); -res; -free res; - -// fst: nat Times nat -o nat -pair~Times(S(S(S(Z))),S(Z)), -fst~Lamc(Par(n,m), r), Iter(r,m,n)~Lamc(x,x); -fst~App(pair,res); -res; -free res; - -// snd: nat Times nat -o nat -pair~Times(S(S(S(Z))),S(Z)), -snd~Lamc(Par(n,m), r), Iter(r,n,m)~Lamc(x,x); -snd~App(pair,res); -res; -free res; - - -// ((Add a) b) -a~S(S(Z)), b~S(S(S(Z))), -add~Lamc(B(V,u,Lam(n,r,r1)),r1), Iter(r,n,u)~Lamc(x,S(x)); -add~App(a,App(b,res)); -prnat res; -free res; - - -// ((Mult a) b) -a~S(S(Z)), b~S(S(S(Z))); -add~Lamc(B(V,au,Lam(an,ar,ar1)),ar1),Iter(ar,an,au)~Lamc(ax,S(ax)), -App(n,Iter(r,m,Z))~add, -mult~Lamc(B(V,n,Lam(m,r,r1)),r1); -mult~App(a,App(b,res)); -prnat res; -free res; - -// ((Exp a) b) -a~S(S(Z)), b~S(S(S(Z))); -add~Lamc(B(V,au,Lam(an,ar,ar1)),ar1),Iter(ar,an,au)~Lamc(ax,S(ax)), -App(mn,Iter(mr,mm,Z))~add, -mult~Lamc(B(V,mn,Lam(mm,mr,mr1)),mr1), -App(n,Iter(r,m,S(Z)))~mult, -exp~Lamc(B(V,n,Lam(m,r,r1)),r1); -exp~App(a,App(b,res)); -prnat res; -free res; - - -// Ack 3 10 -// ver.1: the same as the example on the paper -a~S(S(S(Z))), -b~S(S(S(S(S(S(S(S(S(S(Z)))))))))); -Iter(t,x,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1), -Lamc(x,t)~App(a,App(b, r)); -prnat r; -free r; - -// ver.2: \m.(\n.(iter m (\x.(S x)) (\x.(\y.(iter (S y) (S 0) x))) n)) -a~S(S(S(Z))), -b~S(S(S(S(S(S(S(S(S(S(Z)))))))))); -Iter(App(n,apr),x,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1), -Lamc(B(V,x,Lam(n,apr,nr)),nr)~App(a,App(b, r)); -prnat r; -free r; - -// ver.3: another encoding of ver.2. -a~S(S(S(Z))), -b~S(S(S(S(S(S(S(S(S(S(Z)))))))))); -Iter(t,m,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1), -Lamc(m,t)~App(n,apr), -Lamc(n,apr)~App(a,App(b, r)); -prnat r; -free r; diff --git a/sample/map.in b/sample/map.in deleted file mode 100644 index c96daae..0000000 --- a/sample/map.in +++ /dev/null @@ -1,49 +0,0 @@ -// Map operation - -// target function -inc(r)><(int i) => r~(i+1); -subPair(r)><(int m, int n) => r~(m-n); - - -// ----------- main (with the built-in Map and `%' notation) ----------- -Map(r, %inc) ~ [1,2,3]; -r; // r ->[2,3,4] - -Map(rr, %subPair) ~ [(10,2), (30,13)]; -rr; // r4 ->[8,17] - - - - -// ----------- main (without the built-in Map) ----------- -// map -map(result, f) >< [] => result~[], Eraser~f; -map(result, f) >< x:xs => Dup(f1,f2)~f, - result~w:ws, - f1 ~ (w, x), map(ws, f2)~xs; - - -// --- map application without the `%' notation --- -map(r1, (a, inc(a))) ~ [10,11,12]; -r1; // r1 ->[11,12,13] - -map(r2, (a, subPair(a))) ~ [(10,2), (30,13)]; -r2; // r2 ->[8,17] - - -// --- map application with the `%' notation --- -map(r3, %inc) ~ [1,2,3]; -r3; // r3 ->[2,3,4] - -map(r4, %subPair) ~ [(10,2), (30,13)]; -r4; // r4 ->[8,17] - - -// --- map application with `<<' abbriviation also -// --- It seems the simplest to read. -r5 << map(%inc, [100,200,300]); -r5; // r5 ->[101,201,301] - -r6 << map(%subPair, [(10,2), (30,13)]); -r6; // r6 ->[8,17] - diff --git a/sample/msort.in b/sample/msort.in deleted file mode 100644 index 599990b..0000000 --- a/sample/msort.in +++ /dev/null @@ -1,28 +0,0 @@ -// Merge sort - -// Rules -msort(ret) >< [] => ret~[]; -msort(ret) >< x:xs => ms_tail(ret, x)~xs; - -ms_tail(ret, n) >< [] => ret~[n]; -ms_tail(ret, n) >< x:xs => - split(left,right) ~ (n:x:xs), - msort(a)~left, msort(b)~right, merge(ret,b)~a; - -merge(ret, snd) >< [] => ret~snd; -merge(ret, snd) >< x:xs => mergeCC(ret, x, xs)~snd; - -mergeCC(ret, int y, ys) >< [] => ret~(y:ys); -mergeCC(ret, int y, ys) >< (int x):xs -| x <= y => ret~(x:cnt), mergeCC(cnt, y, ys) ~ xs -| _ => ret~(y:cnt), mergeCC(cnt, x, xs) ~ ys; - - -split(right,left) >< [] => right~[], left~[]; -split(right,left) >< x:xs => - right~(x:cntl), left~cntr, split(cntr,cntl)~xs; - - -// Nets -msort(ret)~[3,6,1,9,2]; -ret; \ No newline at end of file diff --git a/sample/nqueen.in b/sample/nqueen.in deleted file mode 100644 index dd50ad1..0000000 --- a/sample/nqueen.in +++ /dev/null @@ -1,141 +0,0 @@ -// N-Queen -// -// The original is written as a Lisp program in the following file: -// https://www.istc.kobe-u.ac.jp/activity/mage/m27/27_Lisp.pdf - - -/** - * member - * r, done << member(m, list) - * return - * r: 1 if m occurs in list - * done: the same to `list' - */ -// fun member x [] = false -// | member x (y::ys) = if x=y then true else (member x ys); - -member(r, list, int x) >< [] => - r~0, list~[]; -member(r, list, int x) >< (int y):ys -| x==y => - r~1, list~y:ys -| _ => - list~y:cnt, member(r, cnt, x)~ys; - - -/** - * len_list (stream version) - * len, done << len_list(list) - * return - * len: length of `list' - * done: the same to `list' - */ - -len_list(len, done) >< [] => - len~0, done~[]; -len_list(len, done) >< x:xs => - done~x:cnt, - len_list_(len, cnt, 1)~xs; - -len_list_(len, done, int ct) >< [] => - len~ct, done~[]; -len_list_(len, done, int ct) >< x:xs => - done~x:cnt, - len_list_(len, cnt, ct+1) ~ xs; - -/** - * len (non-stream version) - * ret << len(list) - * return - * ret: length of `list' - */ - -len(ret) >< [] => - ret~0; -len(ret) >< x:xs => - len_list(ret, Eraser)~x:xs; - - - -/** - * threat (stream version) - * check for (0,q) and (k, qpos[col=k]) where k=1... - * http://www.nct9.ne.jp/m_hiroi/func/haskell06.html - 0 1 2 --> - +------------- - 1| . . . . . . - 2| . . . -3. . 5 - 3 = 2 - 3| . . -2. . . 5 - 2 = 3 - 4| . -1. . . . 5 - 1 = 4 - 5| Q . . . . . Q position is 5 - 6| . +1. . . . 5 + 1 = 6 - 7| . . +2. . . 5 + 2 = 7 - 8| . . . +3. . 5 + 2 = 8 - +------------- - * r, done << threat(k,m, board) - * return - * r: 1 if threat conditions are satisfied - * done: the same to `board' - */ -// fun threat k m [] = false -// | threat k m (x::xs) = -// if (k = x-m) orelse (k = x+m) then true -// else (threat (k+1) m xs); - -threat(r, done, int k, int q)><[] => - r~0, done~[]; -threat(r, done, int k, int q)><(int x):xs -| (k == x-q) or (k == q-x) => - r~1, done~(x:xs) -| _ => - done~x:cnt, threat(r, cnt, k+1, q)~xs; - - - -// fun queen1 b n 0 = [] -// | queen1 b n m = -// if (member m b) orelse (threat 1 m b) then (queen1 b n (m-1)) -// else if (length b) = (n-1) then (m::b)::(queen1 b n (m-1)) -// else (queen1 (m::b) n n) @ (queen1 b n (m-1)); -// fun queen n = queen1 n [] n; - -queen(ret) >< (int n) => queen_(ret, [], n)~n; - -queen_(r, b, int n) >< (int m) -| m==0 => - r~[], Eraser~b -| _ => - mem_ret, done_b << member(m,b), - queen__chk_m_in_b(r, done_b, n, m)~mem_ret; - -queen__chk_m_in_b(r, b, int n, int m) >< (int mem_ret) -| mem_ret == 1 => - queen_(r, b, n)~(m-1) -| _ => - th_ret, done_b << threat(1, m, b), - queen__chk_threat(r, done_b, n, m)~th_ret; - -queen__chk_threat(r, b, int n, int m) >< (int threat_ret) -| threat_ret == 1 => - queen_(r, b, n)~(m-1) -| _ => - len_ret, done_b << len_list(b), - queen__chk_lastelem(r, done_b, n, m)~len_ret; - -queen__chk_lastelem(r, b, int n, int m) >< (int len_ret) -| len_ret == n-1 => - b1, b2 << Dup(b), - r~(m:b1):cnt, queen_(cnt, b2, n)~(m-1) -| _ => - b1, b2 << Dup(b), - r << Append(cnt1, cnt2), - queen_(cnt1, m:b1, n)~n, queen_(cnt2, b2, n)~(m-1); - - - -// ---------------------------------------------------------- -// main -// ---------------------------------------------------------- -const N=8; -queen(ret)~N, len(count)~ret; -count; // count ->92 diff --git a/sample/nqueenSZ.in b/sample/nqueenSZ.in deleted file mode 100644 index c61515c..0000000 --- a/sample/nqueenSZ.in +++ /dev/null @@ -1,225 +0,0 @@ -// N-Queen on unary natural numbers -// -// The original is written as a Lisp program in the following file: -// https://www.istc.kobe-u.ac.jp/activity/mage/m27/27_Lisp.pdf - - -// --------------------------------------- -// eq -// equality between unary natural numbers numbers -// r << eq(m, n) -// --------------------------------------- -eq(r,m) >< Z => eqZ(r)~m; -eq(r,m) >< S(x) => eqS(r,x)~m; - -eqZ(r) >< Z => r~True; -eqZ(r) >< S(x) => r~False, Eraser~x; - -eqS(r,x) >< Z => r~False, Eraser~x; -eqS(r,x) >< S(y) => eq(r,y)~x; - - - -// --------------------------------------- -// r, m1, n1 << eq_stream(m,n) -// --------------------------------------- -eq_stream(r,m1,n1, m) >< Z => eqZ_stream(r,m1,n1)~m; -eq_stream(r,m1,n1, m) >< S(n) => n1~S(w), eqS_stream(r,m1,w, n)~m; - -eqZ_stream(r,m1,n1) >< Z => r~True, m1~Z, n1~Z; -eqZ_stream(r,m1,n1) >< S(m) => r~False, m1~S(m), n1~Z; - - -eqS_stream(r,m1,n1, n) >< Z => r~False, m1~Z, n1~n; -eqS_stream(r,m1,n1, n) >< S(m) => m1~S(w), eq_stream(r,w , n1, m)~n; - - - - - -// --------------------------------------- -// member -// r, m1, list1 << member(m, list) -// --------------------------------------- -// fun member x [] = false -// | member x (y::ys) = if x=y then true else (member x ys); - -member(r, m1, list1, m) >< [] => - r~False, m1~m, list1~[]; - -member(r, m1, list1, m) >< n:ys => - eq_result, m2, n2 << eq_stream(m,n), - list1~n2:cnt, - member1(r, m1, cnt, m2, ys) ~ eq_result; - - -member1(r, m1, list1, m2, ys) >< True => - r~True, m1~m2, list1~ys; - -member1(r, m1, list1, m2, ys) >< False => - member(r, m1, list1, m2) ~ys; - - - - - -// --------------------------------------- -// len_list (stream version) -// len, done << len_list(list) -// --------------------------------------- - -len_list(len, done) >< [] => - len~Z, done~[]; -len_list(len, done) >< x:xs => - done~x:cnt, - len_list_(len, cnt, S(Z))~xs; - -len_list_(len, done, ct) >< [] => - len~ct, done~[]; -len_list_(len, done, ct) >< x:xs => - done~x:cnt, - len_list_(len, cnt, S(ct)) ~ xs; - - -// --------------------------------------- -// len (non-stream version) -// ret << len(list) -// --------------------------------------- - -len(ret) >< [] => - ret~Z; -len(ret) >< x:xs => - len_list(ret, Eraser)~x:xs; - - - -/** - * threat (stream version) - * check for (0,q) and (k, qpos[col=k]) where k=1... - * http://www.nct9.ne.jp/m_hiroi/func/haskell06.html - 0 1 2 --> - +------------- - 1| . . . . . . - 2| . . . -3. . 5 - 3 = 2 - 3| . . -2. . . 5 - 2 = 3 - 4| . -1. . . . 5 - 1 = 4 - 5| Q . . . . . Q position is 5 - 6| . +1. . . . 5 + 1 = 6 - 7| . . +2. . . 5 + 2 = 7 - 8| . . . +3. . 5 + 2 = 8 - +------------- - * r, board_done << threat(k,m, board) - * return - * r: True if threat conditions are satisfied - * done: the same to `board' - */ -// fun threat k m [] = false -// | threat k m (x::xs) = -// if (k = x-m) orelse (k = x+m) then true -// else (threat (k+1) m xs); - - - -// r << diff(m,n) -diff(r,m) >< Z => r~m; -diff(r,m) >< S(n) => diff_S(r,n)~m; -diff_S(r, n) >< Z => r~S(n); -diff_S(r, n) >< S(m) => diff(r,m)~n; - - - -threat(r, done, k, q) >< [] => - r~False, done~[], Eraser~k, Eraser~q; - -threat(r, done, k, q) >< x:xs => - x1,x2 << Dup(x), - q1,q2 << Dup(q), - diff_xq << diff(x1,q1), - k1,k2 << Dup(k), - eq_ret << eq(k1, diff_xq), - threat1(r, done, k2, q2 , x2:xs)~eq_ret; - -threat1(r, done, k, q, xxs) >< True => - r~True, done~xxs, Eraser~k, Eraser~q; - -threat1(r, done, k, q, xxs) >< False => - x1:xs1 ~ xxs, - done~x1:cnt, threat(r, cnt, S(k), q)~xs1; - - -// fun queen1 b n 0 = [] -// | queen1 b n m = -// if (member m b) orelse (threat 1 m b) then (queen1 b n (m-1)) -// else if (length b) = (n-1) then (m::b)::(queen1 b n (m-1)) -// else (queen1 (m::b) n n) @ (queen1 b n (m-1)); -// fun queen n = queen1 n [] n; - -queen(ret, n) >< () => - n1, n2 << Dup(n), - queen_(ret, [], n1)~n2; - - -queen_(r, b, n) >< Z => - r~[], Eraser~b, Eraser~n; - -queen_(r, b, n) >< S(m) => - mem_ret, done_m, done_b << member(S(m), b), - queen__chk_m_in_b(r, done_b, n, done_m)~mem_ret; - - -dec(r)> r~Z; -dec(r)> r~n; - -queen__chk_m_in_b(r, b, n, m) >< True => - m1 << dec(m), - queen_(r, b, n)~m1; - -queen__chk_m_in_b(r, b, n, m) >< False => - m1,m2 << Dup(m), - th_ret, done_b << threat(S(Z), m1, b), - queen__chk_threat(r, done_b, n, m2)~th_ret; - - - -queen__chk_threat(r, b, n, m) >< True => - m_dec << dec(m), - queen_(r, b, n)~m_dec; - -queen__chk_threat(r, b, n, m) >< False => - len_ret, done_b << len_list(b), - n1,nn << Dup(n), - n_dec << dec(nn), - eq_ret << eq(len_ret, n_dec), - queen__chk_lastelem(r, done_b, n1, m) ~ eq_ret; - - - -queen__chk_lastelem(r,b,n, m) >< True => - b1, b2 << Dup(b), - m1, mm << Dup(m), - m_dec << dec(mm), - r~(m1:b1):cnt, queen_(cnt, b2, n)~m_dec; - -queen__chk_lastelem(r,b,n, m) >< False => - b1, b2 << Dup(b), - r << Append(cnt1, cnt2), - n1, Dup(n2,n3) << Dup(n), - m1, mm << Dup(m), - m_dec << dec(mm), - queen_(cnt1, m1:b1, n1)~n2, queen_(cnt2, b2, n3)~m_dec; - - - -// ---------------------------------------------------------- -// main -// ---------------------------------------------------------- -n~S(S(S(S(S(S(S(S(Z)))))))), // 8 -//n~S(S(S(S(S(S(S(S(S(Z))))))))), // 9 -//n~S(S(S(S(S(S(S(S(S(S(Z)))))))))), // 10 -//n~S(S(S(S(S(S(S(S(S(S(S(Z))))))))))), // 11 -//n~S(S(S(S(Z)))), // 4 -//n~S(Z), // 1 - - -queen(ret,n)~(), len(count)~ret; -prnat count; // count ->92 when n=8 \ No newline at end of file diff --git a/sample/pow.in b/sample/pow.in deleted file mode 100644 index a123b9f..0000000 --- a/sample/pow.in +++ /dev/null @@ -1,16 +0,0 @@ -pow2(r, int m) >< (int n) -| n == 0 => r~m -| _ => pow2(r, m*2)~(n-1); - -pow(r) >< (int n) -| n == 0 => r~1 -| _ => pow2(r, 1)~(n); - - -// Caclulate 2^10 -const NUM=10; -pow(r)~NUM; // it can also be written with abbreviation: r << pow(NUM) -r; - - - diff --git a/sample/process_networks/processnet1.in b/sample/process_networks/processnet1.in new file mode 100644 index 0000000..c648650 --- /dev/null +++ b/sample/process_networks/processnet1.in @@ -0,0 +1,22 @@ +// Rules +dup(a1,a2) >< (int i):xs => a1~(i:xs1), a2~(i:xs2), dup(xs1,xs2)~xs; +dup(a1,a2) >< [] => a1~[], a2~[]; + +inc(r) >< (int i):xs => r~(i+1):w, inc(w)~xs; +inc(r) >< [] => r~[]; + + +// Nets +dup(r,w)~r1, inc(r1) ~ (0:w); + +// r,w << dup(r1), r1 << inc(0:w) + +// +-----+ +-----+ +---+ +// r ----| | r1 | | | | +// | dup |--->---| inc |---><---| 0 |----+ +// +---| | | | | | | +// | +-----+ +-----+ +---+ | +// | | +// +-----------------------------------------+ +// w + \ No newline at end of file diff --git a/sample/process_networks/processnet_fib.in b/sample/process_networks/processnet_fib.in new file mode 100644 index 0000000..ab19eec --- /dev/null +++ b/sample/process_networks/processnet_fib.in @@ -0,0 +1,30 @@ +// Rules +dup(a1,a2) >< (int i):xs => a1~(i:xs1), a2~(i:xs2), dup(xs1,xs2)~xs; +dup(a1,a2) >< [] => a1~[], a2~[]; + +add(r, ys) >< (int i):xs => addn(r, xs, i)~ys; +addn(r, xs, int i) >< (int j):ys => r~(i+j):w, add(w,ys)~xs; + + +// Nets +dup(r, r1)~(1:xs), r1~add(sum, w), dup(xs, w)~(1:sum); + +// r,r1 << dup(1:xs), +// xs,w << dup(1:sum), +// sum << add(r1,w); + +// +-----+ +---+ +// r ----| | | | xs +-----+ +---+ +// | dup |---><---| 1 |-----| | | | +// +---| | | | | dup |---><---| 1 |----+ +// | +-----+ +---+ +--| | | | | +// | | +-----+ +---+ | sum +// | | | +// | | +-----+ +// | | | add | +// | | +-----+ +// | | w | | +// | +------------------------+ v +// | r1 | +// +------------------------------------------------------+ +// diff --git a/sample/processnet1.in b/sample/processnet1.in deleted file mode 100644 index c648650..0000000 --- a/sample/processnet1.in +++ /dev/null @@ -1,22 +0,0 @@ -// Rules -dup(a1,a2) >< (int i):xs => a1~(i:xs1), a2~(i:xs2), dup(xs1,xs2)~xs; -dup(a1,a2) >< [] => a1~[], a2~[]; - -inc(r) >< (int i):xs => r~(i+1):w, inc(w)~xs; -inc(r) >< [] => r~[]; - - -// Nets -dup(r,w)~r1, inc(r1) ~ (0:w); - -// r,w << dup(r1), r1 << inc(0:w) - -// +-----+ +-----+ +---+ -// r ----| | r1 | | | | -// | dup |--->---| inc |---><---| 0 |----+ -// +---| | | | | | | -// | +-----+ +-----+ +---+ | -// | | -// +-----------------------------------------+ -// w - \ No newline at end of file diff --git a/sample/processnet_fib.in b/sample/processnet_fib.in deleted file mode 100644 index ab19eec..0000000 --- a/sample/processnet_fib.in +++ /dev/null @@ -1,30 +0,0 @@ -// Rules -dup(a1,a2) >< (int i):xs => a1~(i:xs1), a2~(i:xs2), dup(xs1,xs2)~xs; -dup(a1,a2) >< [] => a1~[], a2~[]; - -add(r, ys) >< (int i):xs => addn(r, xs, i)~ys; -addn(r, xs, int i) >< (int j):ys => r~(i+j):w, add(w,ys)~xs; - - -// Nets -dup(r, r1)~(1:xs), r1~add(sum, w), dup(xs, w)~(1:sum); - -// r,r1 << dup(1:xs), -// xs,w << dup(1:sum), -// sum << add(r1,w); - -// +-----+ +---+ -// r ----| | | | xs +-----+ +---+ -// | dup |---><---| 1 |-----| | | | -// +---| | | | | dup |---><---| 1 |----+ -// | +-----+ +---+ +--| | | | | -// | | +-----+ +---+ | sum -// | | | -// | | +-----+ -// | | | add | -// | | +-----+ -// | | w | | -// | +------------------------+ v -// | r1 | -// +------------------------------------------------------+ -// diff --git a/sample/pseudo_higher_order/map.in b/sample/pseudo_higher_order/map.in new file mode 100644 index 0000000..c96daae --- /dev/null +++ b/sample/pseudo_higher_order/map.in @@ -0,0 +1,49 @@ +// Map operation + +// target function +inc(r)><(int i) => r~(i+1); +subPair(r)><(int m, int n) => r~(m-n); + + +// ----------- main (with the built-in Map and `%' notation) ----------- +Map(r, %inc) ~ [1,2,3]; +r; // r ->[2,3,4] + +Map(rr, %subPair) ~ [(10,2), (30,13)]; +rr; // r4 ->[8,17] + + + + +// ----------- main (without the built-in Map) ----------- +// map +map(result, f) >< [] => result~[], Eraser~f; +map(result, f) >< x:xs => Dup(f1,f2)~f, + result~w:ws, + f1 ~ (w, x), map(ws, f2)~xs; + + +// --- map application without the `%' notation --- +map(r1, (a, inc(a))) ~ [10,11,12]; +r1; // r1 ->[11,12,13] + +map(r2, (a, subPair(a))) ~ [(10,2), (30,13)]; +r2; // r2 ->[8,17] + + +// --- map application with the `%' notation --- +map(r3, %inc) ~ [1,2,3]; +r3; // r3 ->[2,3,4] + +map(r4, %subPair) ~ [(10,2), (30,13)]; +r4; // r4 ->[8,17] + + +// --- map application with `<<' abbriviation also +// --- It seems the simplest to read. +r5 << map(%inc, [100,200,300]); +r5; // r5 ->[101,201,301] + +r6 << map(%subPair, [(10,2), (30,13)]); +r6; // r6 ->[8,17] + diff --git a/sample/pseudo_higher_order/reduce.in b/sample/pseudo_higher_order/reduce.in new file mode 100644 index 0000000..90ba145 --- /dev/null +++ b/sample/pseudo_higher_order/reduce.in @@ -0,0 +1,57 @@ +// foldr, foldl functions + + +// target functions +// Here, we use built-in agents Add and Sub + + +// -------------------------------------------------------------------- +// foldr f v [x0, x1, ..., xn] = f(x0, f(x1, ... f(xn-1, f(xn, v))...)) +// -------------------------------------------------------------------- +foldr(r, f, v) >< x:xs => foldr_Cons(r,f,v,x)~xs; +foldr_Cons(r,f,v,x) >< [] => f~((r,x),v); +foldr_Cons(r,f,v,x) >< y:ys => + Dup(f1,f2)~f, + foldr(w, f2, v)~y:ys, + f1~((r,x),w); + +// -------------------------------------------------------------------- +// foldl f v [x0, x1, ..., xn] = f( ... f(f(v,x0),x1) ..., xn) +// -------------------------------------------------------------------- +foldl(r, f, v) >< x:xs => foldl_Cons(r,f,v,x)~xs; +foldl_Cons(r,f,v,x) >< [] => f~((r,v),x); +foldl_Cons(r,f,v,x) >< y:ys => + Dup(f1,f2)~f, + f1~((w,v),x), + foldl(r, f2, w)~y:ys; + + + + +// ---------- main ---------- + +// foldr f v [x0, x1, ..., xn] = f(x0, f(x1, ... f(xn-1, f(xn, v))...)) +// foldr plus 10 [1,2,3] = plus(1, plus(2, plus(3, 10))) = 16 + +foldr(r, %Add, 10) ~ [1,2,3]; +r; free r; // r ->16 + + +// foldr subt 1 [30,20,10] = subt(30, subt(20, subt(10, 1))) +// = 30-(20-(10-1)) = 30-(20-9) = 30-11 = 19 + +foldr(r, %Sub, 1) ~ [30,20,10]; +r; free r; // r ->19 + + + +// foldl f v [x0, x1, ..., xn] = f( ... f(f(v,x0),x1) ..., xn) +// foldl plus 10 [1,2,3] = plus(3, plus(2, plus(1, 10))) = 16 + +foldl(r, %Add, 10) ~ [1,2,3]; +r; free r; // r ->16 + + +// foldl subt 10 [1,2,3] = subt(subt(subt(10,1),2),3) = ((10-1)-2)-3 = 4 +foldl(r, %Sub, 10) ~ [1,2,3]; +r; free r; // r ->4 diff --git a/sample/puzzle/hanoi.in b/sample/puzzle/hanoi.in new file mode 100644 index 0000000..5be47c6 --- /dev/null +++ b/sample/puzzle/hanoi.in @@ -0,0 +1,30 @@ +// Tower of Hanoi Puzzle + +// Rules +hanoi(return, source, target, aux) >< (int n) +| n==0 => + // Erase the source, target and aux + source ~ Eraser, + target ~ Eraser, + aux ~ Eraser, + + // result + return~[] + +| _ => + // Duplicate the source, target and aux + source ~ Dup(src1, Dup(src2, src3)), + target ~ Dup(tgt1, Dup(tgt2, tgt3)), + aux ~ Dup(aux1, aux2), + + // recursive applications + hanoi(ret1, src1, aux1, tgt1)~(n-1), + hanoi(ret2, aux2, tgt2, src2)~(n-1), + + // result + return << Append(ret1, (n,src3,tgt3):ret2); + + +// Net +hanoi(result, A, C, B) ~ 3; +result; // should be [(1,A,C),(2,A,B),(1,C,B),(3,A,C),(1,B,A),(2,B,C),(1,A,C)] diff --git a/sample/puzzle/nqueen.in b/sample/puzzle/nqueen.in new file mode 100644 index 0000000..dd50ad1 --- /dev/null +++ b/sample/puzzle/nqueen.in @@ -0,0 +1,141 @@ +// N-Queen +// +// The original is written as a Lisp program in the following file: +// https://www.istc.kobe-u.ac.jp/activity/mage/m27/27_Lisp.pdf + + +/** + * member + * r, done << member(m, list) + * return + * r: 1 if m occurs in list + * done: the same to `list' + */ +// fun member x [] = false +// | member x (y::ys) = if x=y then true else (member x ys); + +member(r, list, int x) >< [] => + r~0, list~[]; +member(r, list, int x) >< (int y):ys +| x==y => + r~1, list~y:ys +| _ => + list~y:cnt, member(r, cnt, x)~ys; + + +/** + * len_list (stream version) + * len, done << len_list(list) + * return + * len: length of `list' + * done: the same to `list' + */ + +len_list(len, done) >< [] => + len~0, done~[]; +len_list(len, done) >< x:xs => + done~x:cnt, + len_list_(len, cnt, 1)~xs; + +len_list_(len, done, int ct) >< [] => + len~ct, done~[]; +len_list_(len, done, int ct) >< x:xs => + done~x:cnt, + len_list_(len, cnt, ct+1) ~ xs; + +/** + * len (non-stream version) + * ret << len(list) + * return + * ret: length of `list' + */ + +len(ret) >< [] => + ret~0; +len(ret) >< x:xs => + len_list(ret, Eraser)~x:xs; + + + +/** + * threat (stream version) + * check for (0,q) and (k, qpos[col=k]) where k=1... + * http://www.nct9.ne.jp/m_hiroi/func/haskell06.html + 0 1 2 --> + +------------- + 1| . . . . . . + 2| . . . -3. . 5 - 3 = 2 + 3| . . -2. . . 5 - 2 = 3 + 4| . -1. . . . 5 - 1 = 4 + 5| Q . . . . . Q position is 5 + 6| . +1. . . . 5 + 1 = 6 + 7| . . +2. . . 5 + 2 = 7 + 8| . . . +3. . 5 + 2 = 8 + +------------- + * r, done << threat(k,m, board) + * return + * r: 1 if threat conditions are satisfied + * done: the same to `board' + */ +// fun threat k m [] = false +// | threat k m (x::xs) = +// if (k = x-m) orelse (k = x+m) then true +// else (threat (k+1) m xs); + +threat(r, done, int k, int q)><[] => + r~0, done~[]; +threat(r, done, int k, int q)><(int x):xs +| (k == x-q) or (k == q-x) => + r~1, done~(x:xs) +| _ => + done~x:cnt, threat(r, cnt, k+1, q)~xs; + + + +// fun queen1 b n 0 = [] +// | queen1 b n m = +// if (member m b) orelse (threat 1 m b) then (queen1 b n (m-1)) +// else if (length b) = (n-1) then (m::b)::(queen1 b n (m-1)) +// else (queen1 (m::b) n n) @ (queen1 b n (m-1)); +// fun queen n = queen1 n [] n; + +queen(ret) >< (int n) => queen_(ret, [], n)~n; + +queen_(r, b, int n) >< (int m) +| m==0 => + r~[], Eraser~b +| _ => + mem_ret, done_b << member(m,b), + queen__chk_m_in_b(r, done_b, n, m)~mem_ret; + +queen__chk_m_in_b(r, b, int n, int m) >< (int mem_ret) +| mem_ret == 1 => + queen_(r, b, n)~(m-1) +| _ => + th_ret, done_b << threat(1, m, b), + queen__chk_threat(r, done_b, n, m)~th_ret; + +queen__chk_threat(r, b, int n, int m) >< (int threat_ret) +| threat_ret == 1 => + queen_(r, b, n)~(m-1) +| _ => + len_ret, done_b << len_list(b), + queen__chk_lastelem(r, done_b, n, m)~len_ret; + +queen__chk_lastelem(r, b, int n, int m) >< (int len_ret) +| len_ret == n-1 => + b1, b2 << Dup(b), + r~(m:b1):cnt, queen_(cnt, b2, n)~(m-1) +| _ => + b1, b2 << Dup(b), + r << Append(cnt1, cnt2), + queen_(cnt1, m:b1, n)~n, queen_(cnt2, b2, n)~(m-1); + + + +// ---------------------------------------------------------- +// main +// ---------------------------------------------------------- +const N=8; +queen(ret)~N, len(count)~ret; +count; // count ->92 diff --git a/sample/qsort.in b/sample/qsort.in deleted file mode 100644 index 523d7d8..0000000 --- a/sample/qsort.in +++ /dev/null @@ -1,19 +0,0 @@ -// Quick sort - -// Rules -qsort(ret) >< [] => ret~[]; -qsort(ret) >< (int x):xs => - Append(ret, x:right)~left, part(smaller, larger, x)~xs, - qsort(left)~smaller, qsort(right)~larger; - -// Note: `Append' is implemented as the following built-in agent: -// Append(ret, b)~a --> ret ~ (a++b) - -part(smaller, larger, int x) >< [] => smaller~[], larger~[]; -part(smaller, larger, int x) >< (int y):ys -| y smaller~(y:cnt), part(cnt, larger, x)~ys -| _ => larger~(y:cnt), part(smaller, cnt, x)~ys; - -// Nets -qsort(ret)~[3,6,1,9,2]; -ret; \ No newline at end of file diff --git a/sample/recursive_functions/ack_3_5.in b/sample/recursive_functions/ack_3_5.in new file mode 100644 index 0000000..19f92fa --- /dev/null +++ b/sample/recursive_functions/ack_3_5.in @@ -0,0 +1,32 @@ +// Ackermann Function +// +// fun ack(0,n) = n+1 +// | ack(m,0) = ack(m-1,1) +// | ack(m,n) = ack(m-1,ack(m,n-1)); + +// The following rule is wrong because there is no gurantee that +// the 'cnt' is connected to an integer agent +// when ack(r)~(m-1,cnt) is evaluated. +// +// ack(r) >< (int m, int n) +// | m==0 => r~(n+1) +// | n==0 => ack(r) ~ (m-1,1) +// | _ => ack(cnt)~(m,n-1), ack(r)~(m-1,cnt); +// +// So, the `cnt' should be connected as an element of connections. + +ack(ret, int m) >< (int n) +| m==0 => ret~(n+1) +| n==0 => ack(ret, m-1)~1 +| _ => ack(cnt, m)~(n-1), ack(ret, m-1)~cnt; + +ackMain(ret)><(int m, int n) => ack(ret,m)~n; + + +// main +const M=3; +const N=5; +ackMain(ret)~(M,N); +ret; +free ret; + diff --git a/sample/recursive_functions/fib-tail_9.in b/sample/recursive_functions/fib-tail_9.in new file mode 100644 index 0000000..58f4cc5 --- /dev/null +++ b/sample/recursive_functions/fib-tail_9.in @@ -0,0 +1,10 @@ +// Fibonacci number +fibt(r, int a, int b) >< (int n) +| n == 0 => r~0 +| n == 1 => r~a +| _ => fibt(r, a+b, a) ~ (n-1); + +fibMain(r) >< (int n) => fibt(r, 1, 0) ~ n; + +fibMain(r)~9; +r; diff --git a/sample/recursive_functions/fib_9.in b/sample/recursive_functions/fib_9.in new file mode 100644 index 0000000..7c4af1f --- /dev/null +++ b/sample/recursive_functions/fib_9.in @@ -0,0 +1,16 @@ +// Fibonacci number + +// Rules +fib(ret) >< (int n) +| n == 0 => ret~0 +| n == 1 => ret~1 +| _ => fib(cnt1)~(n-1), fib(cnt2)~(n-2), Add(ret, cnt2)~cnt1; + + +// Note: Add is implemented as a built-in agent such that: +// Add(ret, int m) ~ (int n) --> ret~(m+n); + +// Nets +fib(ret)~9; +ret; + diff --git a/sample/recursive_functions/fib_9_abbr.in b/sample/recursive_functions/fib_9_abbr.in new file mode 100644 index 0000000..57a8c62 --- /dev/null +++ b/sample/recursive_functions/fib_9_abbr.in @@ -0,0 +1,16 @@ +// Fibonacci number + +// Rules +fib(ret) >< (int n) +| n == 0 => ret~0 +| n == 1 => ret~1 +| _ => cnt1 << fib(n-1), cnt2 << fib(n-2), ret << Add(cnt1,cnt2); + + +// Note: Add is implemented as a built-in agent such that: +// Add(ret, int m) ~ (int n) --> ret~(m+n); + +// Nets +ret << fib(9); +ret; + diff --git a/sample/recursive_functions/gcd.in b/sample/recursive_functions/gcd.in new file mode 100644 index 0000000..5a57d8d --- /dev/null +++ b/sample/recursive_functions/gcd.in @@ -0,0 +1,16 @@ +// Greatest common divisor +// +//def gcd(a: Int, b: Int): Int = +// if (b==0) a else gcd(b, a%b) + + +// Rule +gcd(ret, int a) >< (int b) +| b==0 => ret ~ a +| _ => gcd(ret, b) ~ a%b; + +// Net +gcd(r, 14) ~ 21; +r; // it should be 7 + + diff --git a/sample/recursive_functions/gcd_another.in b/sample/recursive_functions/gcd_another.in new file mode 100644 index 0000000..e616e28 --- /dev/null +++ b/sample/recursive_functions/gcd_another.in @@ -0,0 +1,16 @@ +// Greatest common divisor +// +//def gcd(a: Int, b: Int): Int = +// if (b==0) a else gcd(b, a%b) + + +// Rule +gcd(ret) >< (int a, int b) +| b==0 => ret ~ a +| _ => gcd(ret) ~ (b, a%b); + +// Net +gcd(r) ~ (14,21); +r; // it should be 7 + + diff --git a/sample/recursive_functions/pow.in b/sample/recursive_functions/pow.in new file mode 100644 index 0000000..a123b9f --- /dev/null +++ b/sample/recursive_functions/pow.in @@ -0,0 +1,16 @@ +pow2(r, int m) >< (int n) +| n == 0 => r~m +| _ => pow2(r, m*2)~(n-1); + +pow(r) >< (int n) +| n == 0 => r~1 +| _ => pow2(r, 1)~(n); + + +// Caclulate 2^10 +const NUM=10; +pow(r)~NUM; // it can also be written with abbreviation: r << pow(NUM) +r; + + + diff --git a/sample/reduce.in b/sample/reduce.in deleted file mode 100644 index 90ba145..0000000 --- a/sample/reduce.in +++ /dev/null @@ -1,57 +0,0 @@ -// foldr, foldl functions - - -// target functions -// Here, we use built-in agents Add and Sub - - -// -------------------------------------------------------------------- -// foldr f v [x0, x1, ..., xn] = f(x0, f(x1, ... f(xn-1, f(xn, v))...)) -// -------------------------------------------------------------------- -foldr(r, f, v) >< x:xs => foldr_Cons(r,f,v,x)~xs; -foldr_Cons(r,f,v,x) >< [] => f~((r,x),v); -foldr_Cons(r,f,v,x) >< y:ys => - Dup(f1,f2)~f, - foldr(w, f2, v)~y:ys, - f1~((r,x),w); - -// -------------------------------------------------------------------- -// foldl f v [x0, x1, ..., xn] = f( ... f(f(v,x0),x1) ..., xn) -// -------------------------------------------------------------------- -foldl(r, f, v) >< x:xs => foldl_Cons(r,f,v,x)~xs; -foldl_Cons(r,f,v,x) >< [] => f~((r,v),x); -foldl_Cons(r,f,v,x) >< y:ys => - Dup(f1,f2)~f, - f1~((w,v),x), - foldl(r, f2, w)~y:ys; - - - - -// ---------- main ---------- - -// foldr f v [x0, x1, ..., xn] = f(x0, f(x1, ... f(xn-1, f(xn, v))...)) -// foldr plus 10 [1,2,3] = plus(1, plus(2, plus(3, 10))) = 16 - -foldr(r, %Add, 10) ~ [1,2,3]; -r; free r; // r ->16 - - -// foldr subt 1 [30,20,10] = subt(30, subt(20, subt(10, 1))) -// = 30-(20-(10-1)) = 30-(20-9) = 30-11 = 19 - -foldr(r, %Sub, 1) ~ [30,20,10]; -r; free r; // r ->19 - - - -// foldl f v [x0, x1, ..., xn] = f( ... f(f(v,x0),x1) ..., xn) -// foldl plus 10 [1,2,3] = plus(3, plus(2, plus(1, 10))) = 16 - -foldl(r, %Add, 10) ~ [1,2,3]; -r; free r; // r ->16 - - -// foldl subt 10 [1,2,3] = subt(subt(subt(10,1),2),3) = ((10-1)-2)-3 = 4 -foldl(r, %Sub, 10) ~ [1,2,3]; -r; free r; // r ->4 diff --git a/sample/sort/bsort.in b/sample/sort/bsort.in new file mode 100644 index 0000000..7b2e2d6 --- /dev/null +++ b/sample/sort/bsort.in @@ -0,0 +1,18 @@ +// Bubble sort + +// Rules +bsort(ret) >< [] => ret~[]; +bsort(ret) >< x:xs => bsort(ret)~cnt, bubble(cnt, x)~xs; +bsort(ret) >< M(x) => ret~x; + +bubble(ret, int x) >< [] => ret~M([x]); +bubble(ret, int x) >< M(w) => ret~M(x:w); +bubble(ret, int x) >< (int y):ys +| x ret~(x:cnt), bubble(cnt, y)~ys +| _ => ret~(y:cnt), bubble(cnt, x)~ys; + + +// Nets +bsort(r)~[3,6,1,9,2]; +r; + diff --git a/sample/sort/isort.in b/sample/sort/isort.in new file mode 100644 index 0000000..e637055 --- /dev/null +++ b/sample/sort/isort.in @@ -0,0 +1,15 @@ +// Insertion sort + +// Rules +isort(ret) >< [] => ret~[]; +isort(ret) >< x:xs => insert(ret, x)~cnt, isort(cnt)~xs; + +insert(ret, int x) >< [] => ret~[x]; +insert(ret, int x) >< (int y):ys +| x<=y => ret~(x:y:ys) +| _ => ret~(y:cnt), insert(cnt, x)~ys; + + +// Nets +isort(r)~[3,6,1,9,2]; +r; diff --git a/sample/sort/msort.in b/sample/sort/msort.in new file mode 100644 index 0000000..599990b --- /dev/null +++ b/sample/sort/msort.in @@ -0,0 +1,28 @@ +// Merge sort + +// Rules +msort(ret) >< [] => ret~[]; +msort(ret) >< x:xs => ms_tail(ret, x)~xs; + +ms_tail(ret, n) >< [] => ret~[n]; +ms_tail(ret, n) >< x:xs => + split(left,right) ~ (n:x:xs), + msort(a)~left, msort(b)~right, merge(ret,b)~a; + +merge(ret, snd) >< [] => ret~snd; +merge(ret, snd) >< x:xs => mergeCC(ret, x, xs)~snd; + +mergeCC(ret, int y, ys) >< [] => ret~(y:ys); +mergeCC(ret, int y, ys) >< (int x):xs +| x <= y => ret~(x:cnt), mergeCC(cnt, y, ys) ~ xs +| _ => ret~(y:cnt), mergeCC(cnt, x, xs) ~ ys; + + +split(right,left) >< [] => right~[], left~[]; +split(right,left) >< x:xs => + right~(x:cntl), left~cntr, split(cntr,cntl)~xs; + + +// Nets +msort(ret)~[3,6,1,9,2]; +ret; \ No newline at end of file diff --git a/sample/sort/qsort.in b/sample/sort/qsort.in new file mode 100644 index 0000000..523d7d8 --- /dev/null +++ b/sample/sort/qsort.in @@ -0,0 +1,19 @@ +// Quick sort + +// Rules +qsort(ret) >< [] => ret~[]; +qsort(ret) >< (int x):xs => + Append(ret, x:right)~left, part(smaller, larger, x)~xs, + qsort(left)~smaller, qsort(right)~larger; + +// Note: `Append' is implemented as the following built-in agent: +// Append(ret, b)~a --> ret ~ (a++b) + +part(smaller, larger, int x) >< [] => smaller~[], larger~[]; +part(smaller, larger, int x) >< (int y):ys +| y smaller~(y:cnt), part(cnt, larger, x)~ys +| _ => larger~(y:cnt), part(smaller, cnt, x)~ys; + +// Nets +qsort(ret)~[3,6,1,9,2]; +ret; \ No newline at end of file diff --git a/sample/turing_machine/TuringMachine.in b/sample/turing_machine/TuringMachine.in new file mode 100644 index 0000000..260f609 --- /dev/null +++ b/sample/turing_machine/TuringMachine.in @@ -0,0 +1,131 @@ +// ------------------------------------------------------------- +// Turing Machine +// ------------------------------------------------------------- +// Every 1 on tapes becomes 0. +// It finishes when the head reads a tape cell whose value is 0. +// +// Rule +// (state, sym) => command +// (0 , 1) => Write(0, 1) // write 0 and change state into 1 +// (1 , 0) => GoRight(2) // headPos+1 and change state into 2 +// (2 , 1) => Write(0, 1) // write 0 and change state into 1 +// otherwise => Halt +// +// Example: +// (tape, state, headPos) +// ([0,1,1,1,1,0], 1, 0) -->* ([0,0,0,0,0,0,0],2,5) +// + + + +// ----------------------------------------- +// getRule +// rule << getRule( (int state, int sym) ) +// NOTE: getRule needs a pair (state, sym). +// So it should be called such as +// ret << getRule( (state, sym) ); +// ----------------------------------------- + +getRule(r) >< (int state, int sym) +| (state==0) && (sym==1) => r~Write(0, 1) +| (state==1) && (sym==0) => r~GoRight(2) +| (state==2) && (sym==1) => r~Write(0, 1) +| _ => r~Halt; + + + + +// ----------------------------------------- +// changeSym +// resultTape << changeSym(headPos, sym, tape) +// ----------------------------------------- + +changeSym(resultTape, headPos, sym) >< tape => // <-- tape is a list + resultTape << changeSym_sub([], headPos, sym, tape); + +changeSym_sub(r, done, int headPos, int sym) >< (int t):ts + | headPos == 0 => r << Append(done, sym:ts) + | _ => done_new << Append(done, [t]), + r << changeSym_sub(done_new, headPos-1, sym, ts); + +changeSym_sub(r, done, headPos, sym) >< [] => + r~Error(done, headPos, sym); + + + + +// ----------------------------------------- +// do +// configure << do(tape, int state, int headPos, Command) +// ----------------------------------------- + +do(r, tape, int state, int headPos) >< Write(sym, new_state) => + changeSym(doneTape, headPos, sym) ~ tape, + r ~ Configure(doneTape, new_state, headPos); + +do(r, tape, int state, int head) >< GoRight(int new_state) => + r ~ Configure(tape, new_state, head+1); + +do(r, tape, int state, int head) >< Halt => + r ~ STOP_Configure(tape, state, head); + + + +// ----------------------------------------- +// getSym +// tapeDone << getSym(sym, int headPos, tape) +// ----------------------------------------- + +getSym(tapeDone, sym, int headPos) >< tape => // <- tape is a list + tapeDone << getSym_sub([], sym, headPos, tape); + + +getSym_sub(r, done, sym, int headPos) >< (int t):ts + | headPos == 0 => r << Append(done, t:ts), sym~t + | _ => cnt << Append(done,[t]), + r << getSym_sub(cnt, sym, headPos-1, ts); + +getSym_sub(r, done, sym, int headPos) >< [] + | headPos == 0 => r << Append(done, [0]), sym~0 + | _ => new_done << Append(done, [0]), + r << getSym_sub(new_done, sym, headPos-1, []); + + + +// ----------------------------------------- +// oneCycle +// configure << Configure(tape, int state, int headPos) +// ----------------------------------------- + +oneCycle(r) >< Configure(tape, int state, int headPos) => + tapeDone, sym << getSym(headPos, tape), + r << oneCycle_sub(tapeDone, state, headPos, sym); + +oneCycle_sub(r, tapeDone, int state, int headPos)><(int sym) => + rule << getRule( (state, sym) ), + r << do(tapeDone, state, headPos, rule); + + + +// ----------------------------------------- +// allCycle +// result << allCycle(Configure(tape, state, headPos)) +// ----------------------------------------- + +allCycle(r) >< Configure(tape, state, headPos) => + r1 << oneCycle(Configure(tape, state, headPos)), + r << allCycle(r1); + +allCycle(r) >< STOP_Configure(tape, state, headPos) => + r ~ Configure(tape, state, headPos); + + + + +// ----------------------------------------- +// main +// ----------------------------------------- + +configure ~ Configure([1,1,1,1,1,0], 0, 0), //(tape, state, headPos) +r << allCycle(configure); +r; // -->* Configure([0,0,0,0,0,0,0],2,5) diff --git a/sample/unary_numbers/AckSZ-3_5.in b/sample/unary_numbers/AckSZ-3_5.in new file mode 100644 index 0000000..4f41966 --- /dev/null +++ b/sample/unary_numbers/AckSZ-3_5.in @@ -0,0 +1,49 @@ +// Ackermann function on unary natural numbers + +// Originally the function is written as follows: +// fun ack(0,y) = y+1 +// | ack(x,0) = ack(x-1,1) +// | ack(x,y) = ack(x-1,ack(x,y-1)); + +// This is written one on unary natural nunbers: +// fun ack(Z , y) = S(y) +// | ack(S(x), Z) = ack(x,S(Z)) +// | ack(S(x), S(y)) = ack(x,ack(S(x),y)); + +// For easily translation to interaction nets, +// the first argument will be moved to the last: +// fun ack(y, Z) = S(y) +// | ack(Z, S(x)) = ack(S(Z),x) +// | ack(S(y), S(x)) = ack(ack(y,S(x)),x); + +// It is traslated directly as follows: +// ack(r,y)>< Z => r~S(y); +// ack(r,y)>< S(x) => ack_Sx(r, x)~y; +// ack_Sx(r,x)>< Z => ack(r, S(Z))~x; +// ack_Sx(r,x)>< S(y) => Dup(x1,x2)~x, ack(r,cnt)~x1, ack(cnt,y)~S(x2); + +// The last connection can be optimised by applying the rule ack>< Z => r~S(y); +ack(r,y)>< S(x) => ack_Sx(r, x)~y; +ack_Sx(r,x)>< Z => ack(r, S(Z))~x; +ack_Sx(r,x)>< S(y) => Dup(x1,x2)~x, ack(r,cnt)~x1, ack_Sx(cnt,x2)~y; + + +// By the way, it is possible to write it by using abbreviation notation: +// ack(r,y)>< Z => r~S(y); +// ack(r,y)>< S(x) => r<< Z => r<< S(y) => x1,x2<< Z => a1~Z, a2~Z; +// Dup(a1,a2)>< S(x) => a1~S(w1), a2~S(w2), Dup(w1,w2)~x; + +// ack(result, y)~x +// For computation `ack 3 5', it is written as follows: +ack(result, S(S(S(S(S(Z))))))~S(S(S(Z))); + +prnat result; +exit; diff --git a/sample/unary_numbers/FibSZ_9.in b/sample/unary_numbers/FibSZ_9.in new file mode 100644 index 0000000..b5a65a8 --- /dev/null +++ b/sample/unary_numbers/FibSZ_9.in @@ -0,0 +1,33 @@ +// Fibonacci number on unary natural numbers +fib(r)> r~Z; +fib(r)> fibS(r)~x; +fibS(r)> r~S(Z); +fibS(r)> Dup(x1,x2)~x, add(r,r2)~r1, fib(r2)~x2, fibS(r1)~x1; + + + +//------ ADD ------ +//Add para +add(r,x)> r~x; +add(r,x)> r~S(w), add(w,x)~y; + +//Add_Seq +//add(r,y)> y~r; +//add(r,y)> add(r, S(y))~x; + + +// ------ DUP ------ +// Dup is defined as built-in: +// +// Dup(x1,x2)> x1~Z, x2~Z; +// Dup(x1,x2)> x1~S(w1), x2~S(w2), Dup(w1,w2)~x; + + + + +// Execution +// Fib 9 +fib(r)~S(S(S(S(S(S(S(S(S(Z))))))))); +prnat r; +free r; + diff --git a/sample/unary_numbers/hanoiSZ.in b/sample/unary_numbers/hanoiSZ.in new file mode 100644 index 0000000..a533d2d --- /dev/null +++ b/sample/unary_numbers/hanoiSZ.in @@ -0,0 +1,31 @@ +// Tower of Hanoi Puzzle + +// Rules +hanoi(return, source, target, aux) >< Z => + // Erase the source, target and aux + source ~ Eraser, + target ~ Eraser, + aux ~ Eraser, + + // result + return~[]; + +hanoi(return, source, target, aux) >< S(n) => + // Duplicate the source, target and aux + source ~ Dup(src1, Dup(src2, src3)), + target ~ Dup(tgt1, Dup(tgt2, tgt3)), + aux ~ Dup(aux1, aux2), + + + // recursive applications + n ~ Dup(nn1, Dup(nn2, nn3)), + hanoi(ret1, src1, aux1, tgt1)~nn1, + hanoi(ret2, aux2, tgt2, src2)~nn2, + + // result + return << Append(ret1, (nn3,src3,tgt3):ret2); + + +// Net +hanoi(result, A, C, B) ~ S(S(S(Z))); +result; \ No newline at end of file diff --git a/sample/unary_numbers/nqueenSZ.in b/sample/unary_numbers/nqueenSZ.in new file mode 100644 index 0000000..b83b89c --- /dev/null +++ b/sample/unary_numbers/nqueenSZ.in @@ -0,0 +1,225 @@ +// N-Queen on unary natural numbers +// +// The original is written as a Lisp program in the following file: +// https://www.istc.kobe-u.ac.jp/activity/mage/m27/27_Lisp.pdf + + +// --------------------------------------- +// eq +// equality between unary natural numbers numbers +// r << eq(m, n) +// --------------------------------------- +eq(r,m) >< Z => eqZ(r)~m; +eq(r,m) >< S(x) => eqS(r,x)~m; + +eqZ(r) >< Z => r~True; +eqZ(r) >< S(x) => r~False, Eraser~x; + +eqS(r,x) >< Z => r~False, Eraser~x; +eqS(r,x) >< S(y) => eq(r,y)~x; + + + +// --------------------------------------- +// r, m1, n1 << eq_stream(m,n) +// --------------------------------------- +eq_stream(r,m1,n1, m) >< Z => eqZ_stream(r,m1,n1)~m; +eq_stream(r,m1,n1, m) >< S(n) => n1~S(w), eqS_stream(r,m1,w, n)~m; + +eqZ_stream(r,m1,n1) >< Z => r~True, m1~Z, n1~Z; +eqZ_stream(r,m1,n1) >< S(m) => r~False, m1~S(m), n1~Z; + + +eqS_stream(r,m1,n1, n) >< Z => r~False, m1~Z, n1~n; +eqS_stream(r,m1,n1, n) >< S(m) => m1~S(w), eq_stream(r,w , n1, m)~n; + + + + + +// --------------------------------------- +// member +// r, m1, list1 << member(m, list) +// --------------------------------------- +// fun member x [] = false +// | member x (y::ys) = if x=y then true else (member x ys); + +member(r, m1, list1, m) >< [] => + r~False, m1~m, list1~[]; + +member(r, m1, list1, m) >< n:ys => + eq_result, m2, n2 << eq_stream(m,n), + list1~n2:cnt, + member1(r, m1, cnt, m2, ys) ~ eq_result; + + +member1(r, m1, list1, m2, ys) >< True => + r~True, m1~m2, list1~ys; + +member1(r, m1, list1, m2, ys) >< False => + member(r, m1, list1, m2) ~ys; + + + + + +// --------------------------------------- +// len_list (stream version) +// len, done << len_list(list) +// --------------------------------------- + +len_list(len, done) >< [] => + len~Z, done~[]; +len_list(len, done) >< x:xs => + done~x:cnt, + len_list_(len, cnt, S(Z))~xs; + +len_list_(len, done, ct) >< [] => + len~ct, done~[]; +len_list_(len, done, ct) >< x:xs => + done~x:cnt, + len_list_(len, cnt, S(ct)) ~ xs; + + +// --------------------------------------- +// len (non-stream version) +// ret << len(list) +// --------------------------------------- + +len(ret) >< [] => + ret~Z; +len(ret) >< list => + len_list(ret, Eraser)~list; + + + +/** + * threat (stream version) + * check for (0,q) and (k, qpos[col=k]) where k=1... + * http://www.nct9.ne.jp/m_hiroi/func/haskell06.html + 0 1 2 --> + +------------- + 1| . . . . . . + 2| . . . -3. . 5 - 3 = 2 + 3| . . -2. . . 5 - 2 = 3 + 4| . -1. . . . 5 - 1 = 4 + 5| Q . . . . . Q position is 5 + 6| . +1. . . . 5 + 1 = 6 + 7| . . +2. . . 5 + 2 = 7 + 8| . . . +3. . 5 + 2 = 8 + +------------- + * r, board_done << threat(k,m, board) + * return + * r: True if threat conditions are satisfied + * done: the same to `board' + */ +// fun threat k m [] = false +// | threat k m (x::xs) = +// if (k = x-m) orelse (k = x+m) then true +// else (threat (k+1) m xs); + + + +// r << diff(m,n) +diff(r,m) >< Z => r~m; +diff(r,m) >< S(n) => diff_S(r,n)~m; +diff_S(r, n) >< Z => r~S(n); +diff_S(r, n) >< S(m) => diff(r,m)~n; + + + +threat(r, done, k, q) >< [] => + r~False, done~[], Eraser~k, Eraser~q; + +threat(r, done, k, q) >< x:xs => + x1,x2 << Dup(x), + q1,q2 << Dup(q), + diff_xq << diff(x1,q1), + k1,k2 << Dup(k), + eq_ret << eq(k1, diff_xq), + threat1(r, done, k2, q2 , x2:xs)~eq_ret; + +threat1(r, done, k, q, xxs) >< True => + r~True, done~xxs, Eraser~k, Eraser~q; + +threat1(r, done, k, q, xxs) >< False => + x1:xs1 ~ xxs, + done~x1:cnt, threat(r, cnt, S(k), q)~xs1; + + +// fun queen1 b n 0 = [] +// | queen1 b n m = +// if (member m b) orelse (threat 1 m b) then (queen1 b n (m-1)) +// else if (length b) = (n-1) then (m::b)::(queen1 b n (m-1)) +// else (queen1 (m::b) n n) @ (queen1 b n (m-1)); +// fun queen n = queen1 n [] n; + +queen(ret, n) >< () => + n1, n2 << Dup(n), + queen_(ret, [], n1)~n2; + + +queen_(r, b, n) >< Z => + r~[], Eraser~b, Eraser~n; + +queen_(r, b, n) >< m => + mem_ret, done_m, done_b << member(m, b), + queen__chk_m_in_b(r, done_b, n, done_m)~mem_ret; + + +dec(r)> r~Z; +dec(r)> r~n; + +queen__chk_m_in_b(r, b, n, m) >< True => + m1 << dec(m), + queen_(r, b, n)~m1; + +queen__chk_m_in_b(r, b, n, m) >< False => + m1,m2 << Dup(m), + th_ret, done_b << threat(S(Z), m1, b), + queen__chk_threat(r, done_b, n, m2)~th_ret; + + + +queen__chk_threat(r, b, n, m) >< True => + m_dec << dec(m), + queen_(r, b, n)~m_dec; + +queen__chk_threat(r, b, n, m) >< False => + len_ret, done_b << len_list(b), + n1,nn << Dup(n), + n_dec << dec(nn), + eq_ret << eq(len_ret, n_dec), + queen__chk_lastelem(r, done_b, n1, m) ~ eq_ret; + + + +queen__chk_lastelem(r,b,n, m) >< True => + b1, b2 << Dup(b), + m1, mm << Dup(m), + m_dec << dec(mm), + r~(m1:b1):cnt, queen_(cnt, b2, n)~m_dec; + +queen__chk_lastelem(r,b,n, m) >< False => + b1, b2 << Dup(b), + r << Append(cnt1, cnt2), + n1, Dup(n2,n3) << Dup(n), + m1, mm << Dup(m), + m_dec << dec(mm), + queen_(cnt1, m1:b1, n1)~n2, queen_(cnt2, b2, n3)~m_dec; + + + +// ---------------------------------------------------------- +// main +// ---------------------------------------------------------- +n~S(S(S(S(S(S(S(S(Z)))))))), // 8 +//n~S(S(S(S(S(S(S(S(S(Z))))))))), // 9 +//n~S(S(S(S(S(S(S(S(S(S(Z)))))))))), // 10 +//n~S(S(S(S(S(S(S(S(S(S(S(Z))))))))))), // 11 +//n~S(S(S(S(Z)))), // 4 +//n~S(Z), // 1 + + +queen(ret,n)~(), len(count)~ret; +prnat count; // count ->92 when n=8 \ No newline at end of file -- cgit v1.2.3