Exhaustive search through MLC inputs

README

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

compute.js

"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.awk

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;
}

exhaust.js

"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;

generate.js

"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`);

Makefile

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

package.json

{
	"dependencies": {
		"@alexo/lambda": "0.3.7"
	},
	"private": true
}

stats.awk

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;
}