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/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 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 338 insertions(+) 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/unary_numbers') 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