diff options
Diffstat (limited to '')
| -rw-r--r-- | sample/245II_abbr.in | 98 | ||||
| -rw-r--r-- | sample/fib_9.in | 2 | ||||
| -rw-r--r-- | sample/fib_9_abbr.in | 16 | ||||
| -rw-r--r-- | sample/linear-systemT.in | 8 | ||||
| -rw-r--r-- | sample/processnet1.in | 2 | ||||
| -rw-r--r-- | sample/processnet_fib.in | 30 |
6 files changed, 151 insertions, 5 deletions
diff --git a/sample/245II_abbr.in b/sample/245II_abbr.in new file mode 100644 index 0000000..a6797d8 --- /dev/null +++ b/sample/245II_abbr.in @@ -0,0 +1,98 @@ +// 245II in YALE encoding + +// Rules + +D >< V => ; +B(a,b,c) >< Z => a~c, b~Z; +B(a,b,c) >< Lam(x,t,v) => b~Lam(x,t,w), v~DB(a,w,c); +DB(a,b,c) >< V => a~c, b~V; +C(x,y) >< Z => x~Z, y~Z; +C(x,y) >< Lam(s,t,u) => + x~Lam(a,b,c), y~Lam(d,e,f), + s~Delta(a,d), t~Delta(b,e), u~C(c,f); +C(x,y) >< V => x~V, y~V; +Delta(x,y) >< Delta(a,b) => x~a, y~b; +B(x,a,b) >< Delta(c,d) => x~CB(a,b,Delta(c,d)); +Delta(a,b) >< CB(x,y,z) => + x~Delta(c,d), y~Delta(e,f), z~Delta(B(a,c,e),B(b,d,f)); +Delta(x,y) >< S(z) => + x~S(a), y~S(b), z~Delta(a,b); +Delta(x,y) >< Z => x~Z, y~Z; +Delta(x,y) >< V => x~V, y~V; +Delta(x,y) >< C(t,s) => + x~C(a,b), y~C(c,d), t~Delta(b,d), s~Delta(a,c); +Delta(x,y) >< AppTo(t,s) => + x~AppTo(a,b), y~AppTo(c,d), t~Delta(a,c), s~Delta(b,d); +Delta(x,y) >< Lam(t,s,u)=> + x~Lam(a,b,c), y~Lam(d,e,f), + t~Delta(a,d), s~Delta(b,e), u~Delta(c,f); +DB(x,y,z) >< CB(t,s,u) => + x~CB(d,e,u), y~CB(t,f,d), s~DB(e,f,z); +C(x,y) >< CB(t,s,u) => + x~CB(a,b,c), y~CB(d,e,f), + t~Delta(a,d), s~C(b,e), u~C(c,f); +D >< CB(a,b,c) => a~c, b~D; + +Eps >< Eps => ; +Eps >< S(x) => x~Eps; +Eps >< V => ; +Eps >< D =>; +Eps >< Delta(t,s) => t~Eps,s~Eps; +Eps >< Lam(t,s,u) => t~Eps,s~Eps,u~Eps; +Eps >< AppTo(t,s) => t~Eps,s~Eps; +Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps; +Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps; + + + +Lam(x,t,c) >< AppTo(result,s) => result~t, x~s, c~D; +// We can write this avtive pair in nets as +// result << AppTo(s, lam_term) for AppTo(result, s)~ lam_term. + +// If the `<<' is defined as user macro, then it becomes more readable: +// result << App(lam_term, s) =def= lam_term ~ App(result, s) + + +// Nets +id1 ~ Lam(x,x,V); +id2 ~ Lam(x,x,V); + + +// lam f. lam x. f(fx) +two ~ Lam(fb, Lam(x,r2,c),V), + fb ~ B(c,f,V), + f2,f1 << C(f), // C(f2,f1) ~ f + r2 << AppTo(r1, f2), + r1 << AppTo(x, f1); + + +// lam f. lam x. f(f(f(fx))) +four ~ Lam(fb, Lam(x, r4, c), V), + fb~B(c, f, V), + f4, C(f3, C(f2, f1)) << C(f), + r4 << AppTo(r3, f4), + r3 << AppTo(r2, f3), + r2 << AppTo(r1, f2), + r1 << AppTo(x, f1); + + +// lam f. lam x. f(f(f(f(fx)))) +five ~ Lam(fb, Lam(x, r5, c), V), + fb~B(c, f, V), + f5, C(f4, C(f3, C(f2, f1))) << C(f), + r5 << AppTo(r4, f5), + r4 << AppTo(r3, f4), + r3 << AppTo(r2, f3), + r2 << AppTo(r1, f2), + r1 << AppTo(x, f1); + + + +// (((24)5)I)I +aux24 << AppTo(four, two); +aux245 << AppTo(five, aux24); +aux245I << AppTo(id1, aux245); +aux245II << AppTo(id2, aux245I); + +aux245II; +exit; diff --git a/sample/fib_9.in b/sample/fib_9.in index f4f17e8..7c4af1f 100644 --- a/sample/fib_9.in +++ b/sample/fib_9.in @@ -8,7 +8,7 @@ fib(ret) >< (int n) // Note: Add is implemented as a built-in agent such that: -// Add(ret, int m) ~ (int n) --> ret~(n+m); +// Add(ret, int m) ~ (int n) --> ret~(m+n); // Nets fib(ret)~9; diff --git a/sample/fib_9_abbr.in b/sample/fib_9_abbr.in new file mode 100644 index 0000000..57a8c62 --- /dev/null +++ b/sample/fib_9_abbr.in @@ -0,0 +1,16 @@ +// Fibonacci number + +// Rules +fib(ret) >< (int n) +| n == 0 => ret~0 +| n == 1 => ret~1 +| _ => cnt1 << fib(n-1), cnt2 << fib(n-2), ret << Add(cnt1,cnt2); + + +// Note: Add is implemented as a built-in agent such that: +// Add(ret, int m) ~ (int n) --> ret~(m+n); + +// Nets +ret << fib(9); +ret; + diff --git a/sample/linear-systemT.in b/sample/linear-systemT.in index 648d9e1..f0e3ccb 100644 --- a/sample/linear-systemT.in +++ b/sample/linear-systemT.in @@ -36,7 +36,7 @@ Dup(x,y) >< Itc(a,b,c,d) => a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2), d~Dup(k1,k2); -/* needed */ +/* required */ Dup(x,y) >< B(a,b,c) => x~B(u1,z1,w1), y~B(u2,z2,w2), a~Dup(u1,u2), b~Dup(z1,z2), c~Dup(w1,w2); Dup(x,y) >< Lam(a,b,c) => x~Lam(w1,u1,z1), y~Lam(w2,u2,z2), @@ -116,7 +116,7 @@ free res; // Ack 3 10 -// ver 1: the same as the example on the paper +// ver.1: the same as the example on the paper a~S(S(S(Z))), b~S(S(S(S(S(S(S(S(S(S(Z)))))))))); Iter(t,x,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1), @@ -124,7 +124,7 @@ Lamc(x,t)~App(a,App(b, r)); prnat r; free r; -// ver 2: \m.(\n.(iter m (\x.(S x)) (\x.(\y.(iter (S y) (S 0) x))) n)) +// ver.2: \m.(\n.(iter m (\x.(S x)) (\x.(\y.(iter (S y) (S 0) x))) n)) a~S(S(S(Z))), b~S(S(S(S(S(S(S(S(S(S(Z)))))))))); Iter(App(n,apr),x,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1), @@ -132,7 +132,7 @@ Lamc(B(V,x,Lam(n,apr,nr)),nr)~App(a,App(b, r)); prnat r; free r; -// ver 3: another encoding of ver 2. +// ver.3: another encoding of ver.2. a~S(S(S(Z))), b~S(S(S(S(S(S(S(S(S(S(Z)))))))))); Iter(t,m,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1), diff --git a/sample/processnet1.in b/sample/processnet1.in index d02404e..c648650 100644 --- a/sample/processnet1.in +++ b/sample/processnet1.in @@ -9,6 +9,8 @@ inc(r) >< [] => r~[]; // Nets dup(r,w)~r1, inc(r1) ~ (0:w); +// r,w << dup(r1), r1 << inc(0:w) + // +-----+ +-----+ +---+ // r ----| | r1 | | | | // | dup |--->---| inc |---><---| 0 |----+ diff --git a/sample/processnet_fib.in b/sample/processnet_fib.in new file mode 100644 index 0000000..ab19eec --- /dev/null +++ b/sample/processnet_fib.in @@ -0,0 +1,30 @@ +// Rules +dup(a1,a2) >< (int i):xs => a1~(i:xs1), a2~(i:xs2), dup(xs1,xs2)~xs; +dup(a1,a2) >< [] => a1~[], a2~[]; + +add(r, ys) >< (int i):xs => addn(r, xs, i)~ys; +addn(r, xs, int i) >< (int j):ys => r~(i+j):w, add(w,ys)~xs; + + +// Nets +dup(r, r1)~(1:xs), r1~add(sum, w), dup(xs, w)~(1:sum); + +// r,r1 << dup(1:xs), +// xs,w << dup(1:sum), +// sum << add(r1,w); + +// +-----+ +---+ +// r ----| | | | xs +-----+ +---+ +// | dup |---><---| 1 |-----| | | | +// +---| | | | | dup |---><---| 1 |----+ +// | +-----+ +---+ +--| | | | | +// | | +-----+ +---+ | sum +// | | | +// | | +-----+ +// | | | add | +// | | +-----+ +// | | w | | +// | +------------------------+ v +// | r1 | +// +------------------------------------------------------+ +// |