From 49960d8950d001a372a0abde670a66ee60026957 Mon Sep 17 00:00:00 2001
From: Shinya Sato <shinnya.sato@gmail.com>
Date: Tue, 5 Mar 2024 18:19:27 +0900
Subject: v0.12.0

---
 sample/linear-systemT.in | 142 -----------------------------------------------
 1 file changed, 142 deletions(-)
 delete mode 100644 sample/linear-systemT.in

(limited to 'sample/linear-systemT.in')

diff --git a/sample/linear-systemT.in b/sample/linear-systemT.in
deleted file mode 100644
index f0e3ccb..0000000
--- a/sample/linear-systemT.in
+++ /dev/null
@@ -1,142 +0,0 @@
-// 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;
-- 
cgit v1.2.3