diff options
| author | Shinya Sato <shinnya.sato@gmail.com> | 2021-09-24 16:42:54 +0900 |
|---|---|---|
| committer | Shinya Sato <shinnya.sato@gmail.com> | 2021-09-24 16:42:54 +0900 |
| commit | 6b3075d90d945d5e7e8fd4d28284ffd99dbeb82e (patch) | |
| tree | 4d9e58166e36452bc3a19172d9cfb7a245f996b0 /sample/ack_3_5.in | |
| parent | dd62122ee43d2c388fb96518eaa527976fddfc38 (diff) | |
| download | inpla-6b3075d90d945d5e7e8fd4d28284ffd99dbeb82e.tar.gz inpla-6b3075d90d945d5e7e8fd4d28284ffd99dbeb82e.zip | |
v0.4.1
Diffstat (limited to 'sample/ack_3_5.in')
| -rw-r--r-- | sample/ack_3_5.in | 32 |
1 files changed, 32 insertions, 0 deletions
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; + |