From 1e5837c9076830876bbdafceeb84f342d712ce8d Mon Sep 17 00:00:00 2001
From: Anton Salikhmetov <anton.salikhmetov@gmail.com>
Date: Fri, 2 Mar 2018 15:17:05 +0200
Subject: [PATCH 1/6] Initial commit

---
 Makefile     |  8 ++++++++
 README       | 53 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 compute.js   | 32 +++++++++++++++++++++++++++++++
 diff.awk     | 42 +++++++++++++++++++++++++++++++++++++++++
 exhaust.js   | 27 ++++++++++++++++++++++++++
 generate.js  | 11 +++++++++++
 package.json |  6 ++++++
 stats.awk    | 28 +++++++++++++++++++++++++++
 8 files changed, 207 insertions(+)
 create mode 100644 Makefile
 create mode 100644 README
 create mode 100644 compute.js
 create mode 100644 diff.awk
 create mode 100644 exhaust.js
 create mode 100644 generate.js
 create mode 100644 package.json
 create mode 100644 stats.awk

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..9310852
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,8 @@
+all:
+	npm install
+	time -p node generate.js 1 8 >terms.txt
+	time -p node compute.js abstract 250 1 5 >abstract.tsv
+
+clean:
+	-rm -fr node_modules
+	-rm -f abstract.tsv terms.txt
diff --git a/README b/README
new file mode 100644
index 0000000..bc3673a
--- /dev/null
+++ b/README
@@ -0,0 +1,53 @@
+Exhaustive search through MLC inputs
+
+Usage:
+
+node generate.js min max >file.txt
+node compute.js algo limit min max >file.tsv
+tail -f -n +1 file.tsv | awk -f stats.awk
+paste left.tsv right.tsv | awk -f diff.awk
+
+where
+
+algo - MLC algorithm to use
+limit - maximum number of interactions per term
+min/max - minimum/maximum size for terms
+
+and
+
+size(x) = 0;
+size(x: M) = 1 + size(M);
+size(M N) = 1 + size(M) + size(N).
+
+The idea was suggested by Gabriel Scherer:
+http://lambda-the-ultimate.org/node/5487
+
+Number of closed lambda-terms of size n with size 0 for the variables:
+http://oeis.org/A220894
+
+All 69445532 closed terms of sizes 1-10:
+https://drive.google.com/open?id=1XjEa-N40wSqmSWnesahnxz6SXVUzzBig
+
+Results for "abstract", up to 250 interactions, sizes 1-9:
+https://drive.google.com/open?id=1O2aTULUXuLIl3LArehMtwmoQiIGB62-A
+
+Results for "optimal", up to 250 interactions, sizes 1-9:
+https://drive.google.com/open?id=16W_HSmwlRB6EAW5XxwVb4MqvkEZPf9HN
+
+Difference between results for "abstract" and "optimal":
+https://drive.google.com/open?id=1ldxxnbzdxZDk5-9VMDzLvS7BouxwbCfH
+
+Results for "standard", up to 250 interactions, sizes 1-9:
+https://drive.google.com/open?id=1k4HJTbafkhMJ6s2-vCs99YoKcJYdDhdl
+
+Difference between "abstract" and "standard", sizes 1-9:
+https://drive.google.com/open?id=1-acHtF-qmahPxzEzQGiPBcRj4EZ69V1l
+
+Results for "abstract", up to 250 interactions, size 10:
+https://drive.google.com/open?id=1irvjKZlKpXQykZvY2DPBWF7oYyES070I
+
+Results for "standard", up to 250 interactions, size 10:
+https://drive.google.com/open?id=1pyiiMKeCDdei9GJrRZmEV80axjE6karf
+
+Difference between "abstract" and "standard", size 10:
+https://drive.google.com/open?id=1zttDhqTHNrWZMBgXUndrFlWy0NC6eMBF
diff --git a/compute.js b/compute.js
new file mode 100644
index 0000000..f7290ec
--- /dev/null
+++ b/compute.js
@@ -0,0 +1,32 @@
+"use strict";
+
+const exhaust = require("./exhaust");
+const mlc = require("@alexo/lambda");
+const fs = require("fs");
+
+const argv = process.argv;
+const max = parseInt(argv.pop());
+const min = parseInt(argv.pop());
+const limit = parseInt(argv.pop());
+const algo = argv.pop();
+
+for (const term of exhaust(min, max)) {
+	let result;
+
+	try {
+		const output = mlc(term, algo, limit);
+		const total = output.total;
+		const beta = output.beta;
+		const stats = `${total}/${beta}`;
+		let nf = output.nf;
+
+		if (!nf)
+			nf = "?";
+
+		result = `${stats}\t${nf}`;
+	} catch (error) {
+		result = `N/A\t${error}`;
+	}
+
+	fs.writeSync(1, `${term}\t${result}\n`);
+}
diff --git a/diff.awk b/diff.awk
new file mode 100644
index 0000000..5eca268
--- /dev/null
+++ b/diff.awk
@@ -0,0 +1,42 @@
+function beta(s)
+{
+	return substr(s, index(s, "/"));
+}
+
+function detect(b1, b2, nf1, nf2)
+{
+	if (("N/A" == b1) && ("N/A" == b2))
+		return "BERR";
+
+	if ("N/A" == b1)
+		return "LERR";
+
+	if ("N/A" == b2)
+		return "RERR";
+
+	if (("?" == nf1) && ("?" == nf2))
+		return;
+
+	if ("?" == nf1)
+		return "LLIM";
+
+	if ("?" == nf2)
+		return "RLIM";
+
+	if (nf1 != nf2)
+		return "NENF";
+
+	if (beta(b1) != beta(b2))
+		return "BETA";
+}
+
+BEGIN {
+	FS = "\t";
+	OFS = "\t";
+}
+
+{
+	status = detect($2, $5, $3, $6);
+	if (status)
+		print status, $1, $2, $5, $3, $6;
+}
diff --git a/exhaust.js b/exhaust.js
new file mode 100644
index 0000000..9870940
--- /dev/null
+++ b/exhaust.js
@@ -0,0 +1,27 @@
+"use strict";
+
+function* sub(len, nv)
+{
+	if (len) {
+		--len;
+
+		for (const t of sub(len, nv + 1))
+			yield `(v${nv}: ${t})`;
+
+		for (let l = 0; l <= len; l++)
+			for (const t of sub(len - l, nv))
+				for (const u of sub(l, nv))
+					yield `(${t} ${u})`;
+	} else {
+		for (let i = 0; i < nv; i++)
+			yield `v${i}`;
+	}
+}
+
+function* exhaust(min, max)
+{
+	for (let len = min; len <= max; len++)
+		yield* sub(len, 0);
+}
+
+module.exports = exhaust;
diff --git a/generate.js b/generate.js
new file mode 100644
index 0000000..6b58e10
--- /dev/null
+++ b/generate.js
@@ -0,0 +1,11 @@
+"use strict";
+
+const exhaust = require("./exhaust");
+const fs = require("fs");
+
+const argv = process.argv;
+const max = parseInt(argv.pop());
+const min = parseInt(argv.pop());
+
+for (const term of exhaust(min, max))
+	fs.writeSync(1, `${term}\n`);
diff --git a/package.json b/package.json
new file mode 100644
index 0000000..bca7ec0
--- /dev/null
+++ b/package.json
@@ -0,0 +1,6 @@
+{
+	"dependencies": {
+		"@alexo/lambda": "0.3.7"
+	},
+	"private": true
+}
diff --git a/stats.awk b/stats.awk
new file mode 100644
index 0000000..8ed6882
--- /dev/null
+++ b/stats.awk
@@ -0,0 +1,28 @@
+BEGIN {
+	FS = "\t";
+	OFS = "\t";
+
+	total = 0;
+
+	fail = 0;
+	hard = 0;
+	good = 0;
+}
+
+{
+	++total;
+
+	if ("N/A" == $2)
+		++fail;
+	else if ("?" == $3)
+		++hard;
+	else
+		++good;
+
+	if (!(total % 10000))
+		print total, good, hard, fail;
+}
+
+END {
+	print total, good, hard, fail;
+}

From 8f32656cfb190d57c85ffb4abbc6688e33c438bc Mon Sep 17 00:00:00 2001
From: Anton Salikhmetov <anton.salikhmetov@gmail.com>
Date: Fri, 2 Mar 2018 15:40:11 +0200
Subject: [PATCH 2/6] Switch to @alexo/lambda@0.4.0

---
 README       | 53 ----------------------------------------------------
 README.md    | 32 +++++++++++++++++++++++++++++++
 package.json |  2 +-
 3 files changed, 33 insertions(+), 54 deletions(-)
 delete mode 100644 README
 create mode 100644 README.md

diff --git a/README b/README
deleted file mode 100644
index bc3673a..0000000
--- a/README
+++ /dev/null
@@ -1,53 +0,0 @@
-Exhaustive search through MLC inputs
-
-Usage:
-
-node generate.js min max >file.txt
-node compute.js algo limit min max >file.tsv
-tail -f -n +1 file.tsv | awk -f stats.awk
-paste left.tsv right.tsv | awk -f diff.awk
-
-where
-
-algo - MLC algorithm to use
-limit - maximum number of interactions per term
-min/max - minimum/maximum size for terms
-
-and
-
-size(x) = 0;
-size(x: M) = 1 + size(M);
-size(M N) = 1 + size(M) + size(N).
-
-The idea was suggested by Gabriel Scherer:
-http://lambda-the-ultimate.org/node/5487
-
-Number of closed lambda-terms of size n with size 0 for the variables:
-http://oeis.org/A220894
-
-All 69445532 closed terms of sizes 1-10:
-https://drive.google.com/open?id=1XjEa-N40wSqmSWnesahnxz6SXVUzzBig
-
-Results for "abstract", up to 250 interactions, sizes 1-9:
-https://drive.google.com/open?id=1O2aTULUXuLIl3LArehMtwmoQiIGB62-A
-
-Results for "optimal", up to 250 interactions, sizes 1-9:
-https://drive.google.com/open?id=16W_HSmwlRB6EAW5XxwVb4MqvkEZPf9HN
-
-Difference between results for "abstract" and "optimal":
-https://drive.google.com/open?id=1ldxxnbzdxZDk5-9VMDzLvS7BouxwbCfH
-
-Results for "standard", up to 250 interactions, sizes 1-9:
-https://drive.google.com/open?id=1k4HJTbafkhMJ6s2-vCs99YoKcJYdDhdl
-
-Difference between "abstract" and "standard", sizes 1-9:
-https://drive.google.com/open?id=1-acHtF-qmahPxzEzQGiPBcRj4EZ69V1l
-
-Results for "abstract", up to 250 interactions, size 10:
-https://drive.google.com/open?id=1irvjKZlKpXQykZvY2DPBWF7oYyES070I
-
-Results for "standard", up to 250 interactions, size 10:
-https://drive.google.com/open?id=1pyiiMKeCDdei9GJrRZmEV80axjE6karf
-
-Difference between "abstract" and "standard", size 10:
-https://drive.google.com/open?id=1zttDhqTHNrWZMBgXUndrFlWy0NC6eMBF
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..4fa7ecf
--- /dev/null
+++ b/README.md
@@ -0,0 +1,32 @@
+Exhaustive search through MLC inputs
+
+# Usage
+
+```
+node generate.js min max >file.txt
+node compute.js algo limit min max >file.tsv
+tail -f -n +1 file.tsv | awk -f stats.awk
+paste left.tsv right.tsv | awk -f diff.awk
+```
+
+where
+
+* `algo` is the MLC algorithm to use;
+* `limit` is the maximum number of interactions per term;
+* `min`/`max` is the minimum/maximum size for terms,
+
+and
+
+```
+size(x) = 0;
+size(x: M) = 1 + size(M);
+size(M N) = 1 + size(M) + size(N).
+```
+
+* * *
+
+The idea was suggested by Gabriel Scherer:
+http://lambda-the-ultimate.org/node/5487
+
+Number of closed lambda-terms of size n with size 0 for the variables:
+http://oeis.org/A220894
diff --git a/package.json b/package.json
index bca7ec0..adaf2b8 100644
--- a/package.json
+++ b/package.json
@@ -1,6 +1,6 @@
 {
 	"dependencies": {
-		"@alexo/lambda": "0.3.7"
+		"@alexo/lambda": "0.4.0"
 	},
 	"private": true
 }

From dd72b23547a7695e79958a381c19b79c647423e2 Mon Sep 17 00:00:00 2001
From: Anton Salikhmetov <anton.salikhmetov@gmail.com>
Date: Fri, 2 Mar 2018 16:12:35 +0200
Subject: [PATCH 3/6] Support user-defined contexts

---
 Makefile    |  6 ++++--
 README.md   |  7 ++++---
 compute.js  |  3 ++-
 exhaust.js  | 10 ++++++++--
 generate.js |  3 ++-
 5 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/Makefile b/Makefile
index 9310852..8f7295c 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,9 @@
+CTX = (x: x x) M
+
 all:
 	npm install
-	time -p node generate.js 1 8 >terms.txt
-	time -p node compute.js abstract 250 1 5 >abstract.tsv
+	node generate.js "$(CTX)" 1 8 >terms.txt
+	node compute.js abstract 250 "$(CTX)" 1 5 >abstract.tsv
 
 clean:
 	-rm -fr node_modules
diff --git a/README.md b/README.md
index 4fa7ecf..d6b1a84 100644
--- a/README.md
+++ b/README.md
@@ -3,17 +3,18 @@ Exhaustive search through MLC inputs
 # Usage
 
 ```
-node generate.js min max >file.txt
-node compute.js algo limit min max >file.tsv
+node generate.js ctx min max >file.txt
+node compute.js algo limit ctx min max >file.tsv
 tail -f -n +1 file.tsv | awk -f stats.awk
 paste left.tsv right.tsv | awk -f diff.awk
 ```
 
 where
 
+* `ctx` is a context `...M...` with one hole `M`;
+* `min`/`max` is the minimum/maximum size for terms;
 * `algo` is the MLC algorithm to use;
 * `limit` is the maximum number of interactions per term;
-* `min`/`max` is the minimum/maximum size for terms,
 
 and
 
diff --git a/compute.js b/compute.js
index f7290ec..e8952da 100644
--- a/compute.js
+++ b/compute.js
@@ -7,10 +7,11 @@ const fs = require("fs");
 const argv = process.argv;
 const max = parseInt(argv.pop());
 const min = parseInt(argv.pop());
+const ctx = argv.pop();
 const limit = parseInt(argv.pop());
 const algo = argv.pop();
 
-for (const term of exhaust(min, max)) {
+for (const term of exhaust(ctx, min, max)) {
 	let result;
 
 	try {
diff --git a/exhaust.js b/exhaust.js
index 9870940..4576ccd 100644
--- a/exhaust.js
+++ b/exhaust.js
@@ -18,10 +18,16 @@ function* sub(len, nv)
 	}
 }
 
-function* exhaust(min, max)
+function* wrap(ctx, len)
+{
+	for (const m of sub(len, 0))
+		yield ctx.replace("M", m);
+}
+
+function* exhaust(ctx, min, max)
 {
 	for (let len = min; len <= max; len++)
-		yield* sub(len, 0);
+		yield* wrap(ctx, len);
 }
 
 module.exports = exhaust;
diff --git a/generate.js b/generate.js
index 6b58e10..0058578 100644
--- a/generate.js
+++ b/generate.js
@@ -6,6 +6,7 @@ const fs = require("fs");
 const argv = process.argv;
 const max = parseInt(argv.pop());
 const min = parseInt(argv.pop());
+const ctx = argv.pop();
 
-for (const term of exhaust(min, max))
+for (const term of exhaust(ctx, min, max))
 	fs.writeSync(1, `${term}\n`);

From da70dba3429fab862e2968075a14c313fb4ab456 Mon Sep 17 00:00:00 2001
From: Anton Salikhmetov <anton.salikhmetov@gmail.com>
Date: Thu, 29 Mar 2018 15:56:36 +0300
Subject: [PATCH 4/6] Exhaust (w: w M w) (x: x x) for M of sizes 1-6

---
 Makefile     | 7 ++++---
 package.json | 2 +-
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index 8f7295c..cbaafb3 100644
--- a/Makefile
+++ b/Makefile
@@ -1,9 +1,10 @@
-CTX = (x: x x) M
+CTX = (w: w M w) (x: x x)
 
 all:
 	npm install
-	node generate.js "$(CTX)" 1 8 >terms.txt
-	node compute.js abstract 250 "$(CTX)" 1 5 >abstract.tsv
+	node generate.js "$(CTX)" 1 6 >terms.txt
+	node compute.js abstract 150 "$(CTX)" 1 6 >abstract.tsv
+	grep N/A abstract.tsv
 
 clean:
 	-rm -fr node_modules
diff --git a/package.json b/package.json
index adaf2b8..ec4ca0b 100644
--- a/package.json
+++ b/package.json
@@ -1,6 +1,6 @@
 {
 	"dependencies": {
-		"@alexo/lambda": "0.4.0"
+		"@alexo/lambda": "0.4.3"
 	},
 	"private": true
 }

From 2d5af478054fc8621665e0b40bb5c13f7aa41537 Mon Sep 17 00:00:00 2001
From: Anton Salikhmetov <anton.salikhmetov@gmail.com>
Date: Thu, 29 Mar 2018 23:41:44 +0300
Subject: [PATCH 5/6] Switch to @alexo/lambda@0.5.0

---
 Makefile     | 2 +-
 package.json | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index cbaafb3..7b66e38 100644
--- a/Makefile
+++ b/Makefile
@@ -4,7 +4,7 @@ all:
 	npm install
 	node generate.js "$(CTX)" 1 6 >terms.txt
 	node compute.js abstract 150 "$(CTX)" 1 6 >abstract.tsv
-	grep N/A abstract.tsv
+	awk -f stats.awk abstract.tsv
 
 clean:
 	-rm -fr node_modules
diff --git a/package.json b/package.json
index ec4ca0b..d2572cc 100644
--- a/package.json
+++ b/package.json
@@ -1,6 +1,6 @@
 {
 	"dependencies": {
-		"@alexo/lambda": "0.4.3"
+		"@alexo/lambda": "0.5.0"
 	},
 	"private": true
 }

From 0d19e3dec62400920c9bb22d63b279be8ac22f14 Mon Sep 17 00:00:00 2001
From: Anton Salikhmetov <anton.salikhmetov@gmail.com>
Date: Wed, 23 May 2018 09:34:04 +0300
Subject: [PATCH 6/6] Add a readline-based version of compute.js

---
 Makefile |  3 ++-
 line.js  | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 line.js

diff --git a/Makefile b/Makefile
index 7b66e38..6c663d8 100644
--- a/Makefile
+++ b/Makefile
@@ -3,9 +3,10 @@ CTX = (w: w M w) (x: x x)
 all:
 	npm install
 	node generate.js "$(CTX)" 1 6 >terms.txt
+	node line.js abstract 150 <terms.txt >output.tsv
 	node compute.js abstract 150 "$(CTX)" 1 6 >abstract.tsv
 	awk -f stats.awk abstract.tsv
 
 clean:
 	-rm -fr node_modules
-	-rm -f abstract.tsv terms.txt
+	-rm -f abstract.tsv terms.txt output.tsv
diff --git a/line.js b/line.js
new file mode 100644
index 0000000..9576a07
--- /dev/null
+++ b/line.js
@@ -0,0 +1,33 @@
+"use strict";
+
+const readline = require("readline");
+const mlc = require("@alexo/lambda");
+const fs = require("fs");
+
+const rl = readline.createInterface({
+	input: process.stdin
+});
+const argv = process.argv;
+const limit = parseInt(argv.pop());
+const algo = argv.pop();
+
+rl.on("line", term => {
+	let result;
+
+	try {
+		const output = mlc(term, algo, limit);
+		const total = output.total;
+		const beta = output.beta;
+		const stats = `${total}/${beta}`;
+		let nf = output.nf;
+
+		if (!nf)
+			nf = "?";
+
+		result = `${stats}\t${nf}`;
+	} catch (error) {
+		result = `N/A\t${error}`;
+	}
+
+	fs.writeSync(1, `${term}\t${result}\n`);
+});