diff options
| -rw-r--r-- | samples/fun/goldbach.bruijn | 20 | ||||
| -rw-r--r-- | samples/fun/halting_problem.bruijn | 10 | ||||
| -rw-r--r-- | samples/fun/huge.bruijn | 16 | ||||
| -rw-r--r-- | std/Math/Real.bruijn | 12 |
4 files changed, 56 insertions, 2 deletions
diff --git a/samples/fun/goldbach.bruijn b/samples/fun/goldbach.bruijn new file mode 100644 index 0000000..2592a40 --- /dev/null +++ b/samples/fun/goldbach.bruijn @@ -0,0 +1,20 @@ +# Tromp's version, will reduce to [0] iff Goldbach conjecture is false +:import std/Combinator . + +zero [[1]] + +one [[0]] + +sieve y [[[0 one (2 sn1 f)]]] + f y [sn2 0] + sn2 [[0 (0 4 1)] [[[[0 2 (1 3)]]]]] + sn1 [[0 (0 3 1)] [[[[0 2 (1 3)]]]]] + +zeroS [[[[0 zero (1 3)]]]] + +primes sieve zeroS + +check y [[[[[primes 0 (1 (4 0))] testp1]]]] + testp1 [0 0 2 [0 4] 0] + +main primes (check [[[[0]]]]) diff --git a/samples/fun/halting_problem.bruijn b/samples/fun/halting_problem.bruijn new file mode 100644 index 0000000..dd7e6d6 --- /dev/null +++ b/samples/fun/halting_problem.bruijn @@ -0,0 +1,10 @@ +:import std/Logic . + +# hypothetical halting decider (shall not loop) +# assuming (Program Arg) reduces to boolean +halting [[halts (1 0)]] ⧗ Program → Arg → Boolean + halts [0 true false] + +# basically y combinator +# paradox! +e halting [¬(halting 0 0)] [¬(halting 0 0)] diff --git a/samples/fun/huge.bruijn b/samples/fun/huge.bruijn index 2d963ad..2f36dc1 100644 --- a/samples/fun/huge.bruijn +++ b/samples/fun/huge.bruijn @@ -1,4 +1,18 @@ # "bruijn huge.bruijn" +# some of the fastest growing functions per blc length + # 55 bits inflating to 65536 bits, John Tromp +huge-55 [[0 0 0 0 [[0 [[0]] 1]]] (+2u) + +# 64 bits inflating to ??? bits, John Tromp +huge-64 [0 0 h 0 0 0] (+2u) + h [[[0 2 1 0]]] + +# 79 bits inflating to ??? bits, John Tromp and Bertram Felgenhauer +huge-79 [0 0 e 0] (+2u) + e [0 g [[0]] d0 0] + g [[1 (d 0) (0 [0])]] + d [[[2 [2 0 1]]]] + d0 [[1 0 0]] -main [[0 0 0 0 [[0 [[0]] 1]]] [[1 (1 0)]]] +main huge-64 diff --git a/std/Math/Real.bruijn b/std/Math/Real.bruijn index 28bc512..4b3e7d0 100644 --- a/std/Math/Real.bruijn +++ b/std/Math/Real.bruijn @@ -151,9 +151,19 @@ hypot [[sqrt ((0 ⋅ 0) + (1 ⋅ 1))]] ⧗ Real → Real → Real denom [N.mul 2 (N.mul 0 N.++0)] (N.mul (+2) 5) # ratio of circle's circumference to its diameter -# TODO: Gauss-Legendre π π/2 ⋅ (+2.0r) ⧗ Real +# Gauss-Legendre, quadratic convergence +# Chudnovsky would be even faster but is ugly (i.e. magic numbers) +π-gauss [L.nth-iterate &[[[[op]]]] start 0 final] + start [0 (+1.0q) Q.~(sqrt (+2.0r) 1) (+0.25q) (+1.0q)] + op [[1 0 b t p] a] + a Q.div (Q.add 4 3) (+2.0q) + b sqrt [Q.mul 6 5] 6 + t Q.sub 3 (Q.mul 2 (Q.pow-n (Q.sub 5 0) (+2))) + p Q.mul (+2.0q) 2 + final [[[[Q.div (Q.pow-n (Q.add 3 2) (+2)) (Q.mul (+4.0q) 1)]]]] + # arctan by Taylor expansion, only for |x|<=1 # tex: \sum_{n=0}^\infty(-1)^n \frac{x^{2n+1}}{2n+1} arctan* [[[L.nth-iterate &[[[[op]]]] start 1] (1 0) [[[[3]]]]]] ⧗ Real → Real |