v0.12.0

1 files changed, 32 insertions, 0 deletions

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;
+