a

2 files changed, 150 insertions, 0 deletions

diff --git a/nn.in b/nn.in
new file mode 100644
index 0000000..fb9a863
--- /dev/null
+++ b/nn.in
@@ -0,0 +1,79 @@
+// Rules
+Symbolic(id) >< Add(out, b) => b ~ AddCheck(out, (*L)Symbolic(id));
+Concrete(int k) >< Add(out, b)
+	| k == 0 => out ~ b
+	| _ => b ~ AddCheckConcrete(out, k);
+other >< Add(out, b) => out ~ Add((*L)other, b);
+
+Symbolic(id) >< AddCheck(out, a) => out ~ Add(a, (*L)Symbolic(id));
+Concrete(int j) >< AddCheck(out, a)
+	| j == 0 => out ~ a
+	| _ => out ~ Add(a, (*L)Concrete(j));
+other >< AddCheck(out, a) => out ~ Add(a, (*L)other);
+
+Symbolic(id) >< AddCheckConcrete(out, int k) => out ~ Add(Concrete(k), (*L) Symbolic(id));
+Concrete(int j) >< AddCheckConcrete(out, int k)
+	| j == 0 => out ~ Concrete(k)
+	| _ => out ~ Concrete(k + j);
+other >< AddCheckConcrete(out, int k) => out ~ Add(Concrete(k), (*L)other);
+
+Symbolic(id) >< Mul(out, b) => b ~ MulCheck(out, (*L)Symbolic(id));
+Concrete(int k) >< Mul(out, b)
+	| k == 0 => b ~ Eraser, out ~ (*L)Concrete(0)
+	| k == 1 => out ~ b
+	| _ => b ~ MulCheckConcrete(out, k);
+other >< Mul(out, b) => out ~ Mul((*L)other, b);
+
+Symbolic(id) >< MulCheck(out, a) => out ~ Mul(a, (*L)Symbolic(id));
+Concrete(int j) >< MulCheck(out, a)
+  | j == 0 => a ~ Eraser, out ~ (*L)Concrete(0)
+	| j == 1 => out ~ a
+	| _ => out ~ Mul(a, (*L)Concrete(j));
+other >< MulCheck(out, a) => out ~ Mul(a, (*L)other);
+
+Symbolic(id) >< MulCheckConcrete(out, int k) => out ~ Mul(Concrete(k), (*L)Symbolic(id));
+Concrete(int j) >< MulCheckConcrete(out, int k)
+  | j == 0 => out ~ Concrete(0)
+	| j == 1 => out ~ Concrete(k)
+	| _ => out ~ Concrete(k * j);
+other >< MulCheckConcrete(out, int k) => out ~ Mul(Concrete(k), (*L)other);
+
+Symbolic(id) >< ReLU(out) => out ~ ReLU((*L)Symbolic(id));
+Concrete(int k) >< ReLU(out)
+	| k > 0 => out ~ (*L)Concrete(k)
+	| _ => out ~ Concrete(0);
+other >< ReLU(out) => out ~ ReLU((*L)other);
+
+// Net
+Symbolic(X) ~ Add(out, b);
+Concrete(0) ~ Mul(b, Symbolic(Y));
+out;
+
+free out;
+Symbolic(X) ~ Mul(out, Concrete(0));
+out;
+
+free out;
+Symbolic(X) ~ Mul(out, b);
+Symbolic(Y) ~ Add(b, Concrete(1));
+out;
+
+free out;
+Concrete(1) ~ Add(out, b);
+Concrete(2) ~ Add(b, c);
+Concrete(3) ~ Mul(c, Concrete(2));
+out;
+
+free out;
+Symbolic(X) ~ Mul(a, Symbolic(W1));
+Symbolic(Y) ~ Mul(b, Symbolic(W2));
+b ~ Add(c, Symbolic(B));
+a ~ Add(d, c);
+d ~ ReLU(out);
+out;
+
+free out;
+Symbolic(X) ~ Dup(a, b);
+a ~ Add(c, Concrete(1));
+b ~ Mul(out, c);
+out;
diff --git a/nn.in~ b/nn.in~
new file mode 100644
index 0000000..dd89d03
--- /dev/null
+++ b/nn.in~
@@ -0,0 +1,71 @@
+// Agents
+
+Any >< Optimize(out) =>
+	out ~ Any;
+
+// Rules
+
+// Optimizer interacts with Const
+Const(k) >< Optimize(out) =>
+	out ~ Const(k);
+
+
+// Optimizer interacts with Add
+Add(a, b) >< Optimize(out) =>
+	a ~ Optimize(a_opt),
+	a_opt ~ Add_CheckLeft(out, b);
+
+// CHECK LEFT
+Const(int k) >< Add_CheckLeft(out, b)
+	| k == 0 => b ~ Optimize(b_opt), out ~ b_opt
+	| _ => b ~ Optimize(b_opt), b_opt ~ Add_CheckRight_WithConst(out, k);
+a_opt >< Add_CheckLeft(out, b) =>
+	b ~ Optimize(b_opt),
+	b_opt ~ Add_CheckRight_WithAny(out, (*L)a_opt);
+
+// CHECK RIGHT
+Const(int j) >< Add_CheckRight_WithConst(out, int k) =>
+	out ~ Const(k + j);
+b_opt >< Add_CheckRight_WithConst(out, int k) =>
+	out ~ Add(Const(k), (*L)b_opt);
+Const(int j) >< Add_CheckRight_WithAny(out, a_opt)
+	| j == 0 => out ~ a_opt
+	| _ => out ~ Add(a_opt, Const(j));
+b_opt >< Add_CheckRight_WithAny(out, a_opt) =>
+	out ~ Add(a_opt, (*L)b_opt);
+
+
+// Optimizer interacts with Mul
+Mul(a, b) >< Optimize(out) =>
+	a ~ Optimize(a_opt),
+	a_opt ~ Mul_CheckLeft(out, b);
+
+// Check LEFT
+Const(int k) >< Mul_CheckLeft(out, b)
+	| k == 0 => b ~ Eraser, out ~ Const(0)
+	| k == 1 => b ~ Optimize(b_opt), out ~ b_opt
+	| _ => b ~ Optimize(b_opt), b_opt ~ Mul_CheckRight_WithConst(out, k);
+a_opt >< Mul_CheckLeft(out, b) =>
+	b ~ Optimize(b_opt),
+	b_opt ~ Mul_CheckRight_WithAny(out, (*L)a_opt);
+
+// Check RIGHT
+Const(int j) >< Mul_CheckRight_WithConst(out, int k) =>
+	out ~ Const(k * j);
+b_opt >< Mul_CheckRight_WithConst(out, int k) =>
+	out ~ Mul(Const(k), (*L)b_opt);
+Const(int j) >< Mul_CheckRight_WithAny(out, a_opt)
+	| j == 0 => Eraser ~ a_opt, out ~ Const(0)
+	| j == 1 => out ~ a_opt
+	| _ => out ~ Mul(a_opt, Const(j));
+b_opt >< Mul_CheckRight_WithAny(out, a_opt) =>
+	out ~ Mul(a_opt, (*L)b_opt);
+
+
+// Net
+Mul(Const(1), Add(Any, Mul(Const(0), Add(Any, Any)))) ~ Optimize(out);
+out;
+
+free out;
+Mul(Const(0), Add(Any, Any)) ~ Optimize(out);
+out;