Last active
February 13, 2018 22:40
-
-
Save codedot/3b99edd504678e160999f12cf30da420 to your computer and use it in GitHub Desktop.
Exhaustive search through MLC inputs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| "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`); | |
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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; | |
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| "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; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| "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`); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "dependencies": { | |
| "@alexo/lambda": "0.3.7" | |
| }, | |
| "private": true | |
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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