Create a gist now

Instantly share code, notes, and snippets.

@codedot /Makefile
Last active Feb 13, 2018

What would you like to do?
Exhaustive search through MLC inputs
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
"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`);
}
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;
}
"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;
"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`);
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
{
"dependencies": {
"@alexo/lambda": "0.3.7"
},
"private": true
}
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;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment