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