From 6b3075d90d945d5e7e8fd4d28284ffd99dbeb82e Mon Sep 17 00:00:00 2001
From: Shinya Sato <shinnya.sato@gmail.com>
Date: Fri, 24 Sep 2021 16:42:54 +0900
Subject: v0.4.1

---
 sample/ack_3_5.in | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 sample/ack_3_5.in

(limited to 'sample/ack_3_5.in')

diff --git a/sample/ack_3_5.in b/sample/ack_3_5.in
new file mode 100644
index 0000000..87057a2
--- /dev/null
+++ b/sample/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 below rule is wrong because there is no gurantee that
+// the 'cnt' is 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);
+
+
+ack(ret, n) >< (int m)
+| m==0 => inc(ret)~n
+| _ => ackn(ret, m)~n;
+
+ackn(ret, int m) >< (int n)
+| n==0 => ack(ret,1) ~ (m-1)
+| _ => ack(cnt,n-1)~m, ack(ret,cnt)~(m-1);
+
+inc(ret)><(int n) => ret~(n+1);
+
+
+ackMain(ret)><(int m, int n) => ack(ret,n)~m;
+
+ackMain(ret)~(3,5);
+ret;
+free ret;
+
-- 
cgit v1.2.3