diff options
| author | Marvin Borner | 2023-03-12 00:04:55 +0100 |
|---|---|---|
| committer | Marvin Borner | 2023-03-12 00:08:37 +0100 |
| commit | 5e5069c5228f2cd39de38ace9134f57293cc7e5d (patch) | |
| tree | 525f3a12f8ae5a8d093c756ac5a094a9ccedfe78 /benchmark.bruijn | |
| parent | e789e11f8e478fe5987101424cf5c9c32cc6a29b (diff) | |
Fun
Diffstat (limited to 'benchmark.bruijn')
| -rw-r--r-- | benchmark.bruijn | 66 |
1 files changed, 0 insertions, 66 deletions
diff --git a/benchmark.bruijn b/benchmark.bruijn deleted file mode 100644 index e870b29..0000000 --- a/benchmark.bruijn +++ /dev/null @@ -1,66 +0,0 @@ -# ================== -# Lennart -# From Lambda-n-ways -# ================== - -fix [[1 (0 0)] [1 (0 0)]] - -zero [[1]] - -succ [[[0 2]]] - -add fix [[[1 0 [succ (3 0 1)]]]] - -sumto fix [[0 zero [add 1 (2 0)]]] - -mul fix [[[1 zero [add 1 (3 0 1)]]]] - -one succ zero - -two succ one - -three succ two - -n6 add three three - -n703 sumto n37 - n37 succ (mul n6 n6) - -n17 add n6 (add n6 n5) - n5 add two three - -true [[0]] - -false [[1]] - -const [[1]] - -eqnat fix [[[1 (0 true (const false)) [1 false [4 1 0]]]]] - -n720 fac n6 - if [[[2 0 1]]] - pair [[[0 2 1]]] - fst [[1 0 [[1]]]] - snd [[1 0 [[0]]]] - fac fix [[0 one [mul 1 (2 0)]]] - -# this can take some time.. -# - should return true -:print eqnat n720 (add n703 n17) - -# ========= -# Ackermann -# From AIT -# ========= - -# ackerlike [0 ackify omega 0] -# two [[1 (1 0)]] -# omega [0 0] -# ackify [[0 1 0]] - -# this can take a VERY long while -# maybe even too long for benchmarking -# - should return exponential tower with 256 levels -# :print ackerlike two - -main [0] |