4 files changed, 375 insertions, 0 deletions
diff --git a/sample/lambda/245II.in b/sample/lambda/245II.in
new file mode 100644
index 0000000..27910eb
--- /dev/null
+++ b/sample/lambda/245II.in
@@ -0,0 +1,62 @@
+// 245II in YALE encoding
+
+// Rules
+Lam(a,b,c) >< App(x,y) => a~x, b~y, c~D;
+D >< V => ;
+B(a,x,e) >< Lam(b,c,y) => x~Lam(b,c,d), y~DB(a,d,e);
+DB(a,b,c) >< V => a~c, b~V;
+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) >< 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) >< App(t,s) =>
+	x~App(a,b), y~App(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 >< App(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;
+
+
+// Nets
+// lam x.x
+id1 ~ Lam(i,i,V);
+id2 ~ Lam(i2,i2,V);
+
+// lam f. lam x. f(fx)
+two ~ Lam(Lam(a,b,c),B(c,C(App(a,d),App(d,b)),V),V);
+
+// lam f. lam x. f(fx)
+four ~ Lam(Lam(dz4, dx2, da1), B(da1, C(App(dz4, dz3), C(App(dz3, dz2), C(App(dz2, dz1), App(dz1, dx2)))), V), V);
+
+// lam f. lam x. f(fx)
+five ~ Lam(Lam(z53, x23, a13), B(a13, C(App(z53, z43), C(App(z43, z33), C(App(z33,z23), C(App(z23, z13), App(z13, x23))))), V), V);
+
+// 245II
+two  ~ App(aux1, four);
+aux1 ~ App(aux2, five);
+aux2 ~ App(aux3, id1);
+aux3 ~ App(aux4, id2);
+aux4;
+exit;
diff --git a/sample/lambda/245II_abbr.in b/sample/lambda/245II_abbr.in
new file mode 100644
index 0000000..c2084ec
--- /dev/null
+++ b/sample/lambda/245II_abbr.in
@@ -0,0 +1,101 @@
+// 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 `<<' could be defined as user macro in future, 
+// then it becomes more readable:
+//   result << App(lam_term, s)  =def=  lam_term ~ App(result, s)
+
+
+// Nets
+
+// lam x.x
+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/lambda/245II_new.in b/sample/lambda/245II_new.in
new file mode 100644
index 0000000..2050179
--- /dev/null
+++ b/sample/lambda/245II_new.in
@@ -0,0 +1,70 @@
+// 245II in YALE encoding
+
+// Rules
+Lam(a,b,c) >< App(x,y) => a~x, b~y, c~D;
+D >< V => ;
+B(a,x,e) >< Lam(b,c,y) => x~Lam(b,c,d), y~DB(a,d,e);
+DB(a,b,c) >< V => a~c, b~V;
+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) >< 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) >< App(t,s) =>
+	x~App(a,b), y~App(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 >< App(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;
+
+
+// Nets
+// lam x.x
+new(r) >< Id => r~Lam(i,i,V);
+
+// lam f. lam x. f(fx)
+new(r) >< Two => r~Lam(Lam(a,b,c),B(c,C(App(a,d),App(d,b)),V),V);
+
+// lam f. lam x. f(fx)
+new(r) >< Four => r~Lam(Lam(a,b,c), B(c,C(App(a,d), C(App(d, e), C(App(e, f), App(f, b)))), V), V);
+
+// lam f. lam x. f(fx)
+new(r) >< Five => r~Lam(Lam(a, b, c), B(c, C(App(a, d), C(App(d, e), C(App(e,f), C(App(f, g), App(g, b))))), V), V);
+
+
+// instances
+id1 << new(Id);
+id2 << new(Id);
+two << new(Two);
+four << new(Four);
+five << new(Five);
+
+
+// 245II
+two  ~ App(aux1, four);
+aux1 ~ App(aux2, five);
+aux2 ~ App(aux3, id1);
+aux3 ~ App(aux4, id2);
+aux4;
+exit;
diff --git a/sample/lambda/linear-systemT.in b/sample/lambda/linear-systemT.in
new file mode 100644
index 0000000..f0e3ccb
--- /dev/null
+++ b/sample/lambda/linear-systemT.in
@@ -0,0 +1,142 @@
+// sample programs of linear-systemT (see POPL2016 paper)
+
+// Basic Rules ----------------------------------------
+Lamc(x,y) >< App(a,b) => a~x, b~y;
+Times(a,b) >< Par(x,y) => a~x, b~y;
+B(a,b,c) >< Lamc(x,y) => a~c, b~Lamc(x,y);
+V >< Lam(x,y,z) => z~Lamc(x,y);
+B(a,b,c)><S(x) => b~S(w), x~B(a,w,c);	// original
+//B(a,b,c) >< S(x) => a~c, b~S(x);	// alternative
+B(a,b,c) >< Z => a~c, b~Z;
+
+
+// Iterator ----------------------------------------
+Iter(r,n,u) >< Lamc(x,t) => n~Itc(u,x,t,r);
+Itc(u,x,t,r) >< Z => u~r,x~Eps,t~Eps;
+Itc(u,x,t,r) >< S(y) => y~Itc(t2,w,t1,r), x~Dup(w,u),t~Dup(t1,t2);
+
+// Dup ----------------------------------------
+Dup(x,y) >< Dup(a,b) => x~a, y~b;
+Dup(x,y) >< Lamc(a,b) => x~Lamc(w1,w2), y~Lamc(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2);
+Dup(x,y) >< App(a,b) => x~App(w1,w2), y~App(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2);
+Dup(x,y) >< Times(a,b) => x~Times(w1,w2), y~Times(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2);
+Dup(x,y) >< Par(a,b) => x~Par(w1,w2), y~Par(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2);
+Dup(x,y) >< V => x~V, y~V;
+
+Dup(a1,a2)>< Z => a1~Z, a2~Z;
+Dup(a1,a2)>< S(x) => a1~S(w1), a2~S(w2), x~Dup(w1,w2);
+
+
+Dup(x,y) >< Iter(a,b,c) =>
+	x~Iter(u1,w1,z1), y~Iter(u2,w2,z2),
+	a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2);
+
+Dup(x,y) >< Itc(a,b,c,d) =>
+	x~Itc(u1,w1,z1,k1), y~Itc(u2,w2,z2,k2), 
+	a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2), d~Dup(k1,k2);
+
+
+/* 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),
+	a~Dup(w1,w2), b~Dup(u1,u2), c~Dup(z1,z2);
+
+
+// Eps ----------------------------------------
+Eps >< Eps => ;
+Eps >< Dup(x,y) => Eps~x,Eps~y;
+Eps >< Lamc(x,y) => Eps~x,Eps~y;
+Eps >< App(x,y) => Eps~x, Eps~y;
+Eps >< Par(x,y) => Eps~x, Eps~y;
+Eps >< Times(x,y) => Eps~x, Eps~y;
+
+Eps >< S(x) => x~Eps;
+Eps >< Z => ;
+
+Eps >< Iter(a,b,c) => a~Eps, b~Eps, c~Eps;
+Eps >< Itc(a,b,c,d) => a~Eps, b~Eps, c~Eps,d~Eps;
+
+/* required */
+Eps >< B(a,b,c) => a~Eps, b~Eps, c~Eps;
+Eps >< Lam(a,b,c) => a~Eps, b~Eps, c~Eps;
+Eps >< V => ;
+
+
+// sample ----------------------------------------
+// Cp: nat -o nat Times nat
+n~S(S(Z)),
+cp~Lamc(x,r), Iter(r,x,Times(Z,Z))~Lamc(Par(a,b),Times(S(a),S(b)));
+cp~App(n,res);
+res;
+free res;
+
+// fst: nat Times nat -o nat
+pair~Times(S(S(S(Z))),S(Z)),
+fst~Lamc(Par(n,m), r), Iter(r,m,n)~Lamc(x,x);
+fst~App(pair,res);
+res;
+free res;
+
+// snd: nat Times nat -o nat
+pair~Times(S(S(S(Z))),S(Z)),
+snd~Lamc(Par(n,m), r), Iter(r,n,m)~Lamc(x,x);
+snd~App(pair,res);
+res;
+free res;
+
+
+// ((Add a) b)
+a~S(S(Z)), b~S(S(S(Z))),
+add~Lamc(B(V,u,Lam(n,r,r1)),r1), Iter(r,n,u)~Lamc(x,S(x));
+add~App(a,App(b,res));
+prnat res;
+free res;
+
+
+// ((Mult a) b)
+a~S(S(Z)), b~S(S(S(Z)));
+add~Lamc(B(V,au,Lam(an,ar,ar1)),ar1),Iter(ar,an,au)~Lamc(ax,S(ax)),
+App(n,Iter(r,m,Z))~add,
+mult~Lamc(B(V,n,Lam(m,r,r1)),r1);
+mult~App(a,App(b,res));
+prnat res;
+free res;
+
+// ((Exp a) b)
+a~S(S(Z)), b~S(S(S(Z)));
+add~Lamc(B(V,au,Lam(an,ar,ar1)),ar1),Iter(ar,an,au)~Lamc(ax,S(ax)),
+App(mn,Iter(mr,mm,Z))~add,
+mult~Lamc(B(V,mn,Lam(mm,mr,mr1)),mr1),
+App(n,Iter(r,m,S(Z)))~mult,
+exp~Lamc(B(V,n,Lam(m,r,r1)),r1);
+exp~App(a,App(b,res));
+prnat res;
+free res;
+
+
+// Ack 3 10
+// 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),
+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))
+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),
+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.
+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),
+Lamc(m,t)~App(n,apr),
+Lamc(n,apr)~App(a,App(b, r));
+prnat r;
+free r;