From 4bc1909e72473b1f1965f3dc2d31ecdd7bcd86b4 Mon Sep 17 00:00:00 2001 From: Shinya Sato Date: Fri, 28 Jan 2022 21:28:11 +0900 Subject: Update AckSZ-3_5.in --- sample/AckSZ-3_5.in | 43 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 37 insertions(+), 6 deletions(-) (limited to 'sample/AckSZ-3_5.in') diff --git a/sample/AckSZ-3_5.in b/sample/AckSZ-3_5.in index 0d0ebe4..41674d8 100644 --- a/sample/AckSZ-3_5.in +++ b/sample/AckSZ-3_5.in @@ -1,18 +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)); -// -ack(r,y)>< Z => r~S(y); + +// 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)>< 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 3 5 -ack(r, S(S(S(S(S(Z))))))~S(S(S(Z))); -prnat r; +// 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; -- cgit v1.2.3