diff options
| -rw-r--r-- | std/List.bruijn | 95 | ||||
| -rw-r--r-- | std/Logic.bruijn | 24 | ||||
| -rw-r--r-- | std/Math.bruijn | 43 |
3 files changed, 79 insertions, 83 deletions
diff --git a/std/List.bruijn b/std/List.bruijn index bce9463..c3f36b2 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -7,17 +7,17 @@ :import std/Number . # empty list element -empty false +empty false ⧗ (List a) # returns true if a list is empty -empty? [0 [[[false]]] true] +empty? [0 [[[false]]] true] ⧗ (List a) → Boolean ∅?‣ empty? :test (∅?empty) (true) # prepends an element to a list -cons P.pair +cons P.pair ⧗ a → (List a) → (List a) …:… cons @@ -25,21 +25,21 @@ cons P.pair :test (∅?((+2) : empty)) (false) # returns the head of a list or empty -head P.fst +head P.fst ⧗ (List a) → a ^‣ head :test (^((+1) : ((+2) : empty))) ((+1)) # returns the tail of a list or empty -tail P.snd +tail P.snd ⧗ (List a) → (List a) ~‣ tail :test (~((+1) : ((+2) : empty))) ((+2) : empty) # returns the length of a list in balanced ternary -length z [[[rec]]] (+0) +length z [[[rec]]] (+0) ⧗ (List a) → Number rec ∅?0 case-end case-inc case-inc 2 ++1 ~0 case-end 1 @@ -50,7 +50,7 @@ length z [[[rec]]] (+0) :test (∀empty) ((+0)) # returns the element at index in list -index z [[[rec]]] +index z [[[rec]]] ⧗ (List a) → Number → a rec ∅?0 case-end case-index case-index =?1 ^0 (2 --1 ~0) case-end empty @@ -63,7 +63,7 @@ index z [[[rec]]] :test (((+1) : ((+2) : ((+3) : empty))) !! (+3)) (empty) # applies a left fold on a list -foldl z [[[[rec]]]] +foldl z [[[[rec]]]] ⧗ (b → a → b) → b → (List a) → b rec ∅?0 case-end case-fold case-fold 3 2 (2 1 ^0) ~0 case-end 1 @@ -72,10 +72,10 @@ foldl z [[[[rec]]]] :test ((foldl …-… (+6) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) # foldl without starting value -foldl1 [[foldl 1 ^0 ~0]] +foldl1 [[foldl 1 ^0 ~0]] ⧗ (a → a → a) → (List a) → a # applies a right fold on a list -foldr [[[z [[rec]] 0]]] +foldr [[[z [[rec]] 0]]] ⧗ (a → b → b) → b → (List b) → b rec ∅?0 case-end case-fold case-fold 4 ^0 (1 ~0) case-end 3 @@ -84,10 +84,10 @@ foldr [[[z [[rec]] 0]]] :test ((foldr …-… (+2) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) # foldr without starting value -foldr1 [[foldl 1 ^0 ~0]] +foldr1 [[foldl 1 ^0 ~0]] ⧗ (a → a → a) → (List a) → a # applies or to all list elements -lor? foldr or? false +lor? foldr or? false ⧗ (List Boolean) → Boolean ⋁?‣ lor? @@ -96,7 +96,7 @@ lor? foldr or? false :test (⋁?(false : (false : empty))) (false) # applies and to all list elements -land? foldr and? true +land? foldr and? true ⧗ (List Boolean) → Boolean ⋀?‣ land? @@ -105,7 +105,7 @@ land? foldr and? true :test (⋀?(false : (false : empty))) (false) # reverses a list -reverse foldl \cons empty +reverse foldl \cons empty ⧗ (List a) → (List a) <~>‣ reverse @@ -113,17 +113,18 @@ reverse foldl \cons empty # creates list out of n terms # TODO: fix for balanced ternary -list [0 [[[2 (0 : 1)]]] reverse empty] +# TODO: fix/remove incorrect type? +list [0 [[[2 (0 : 1)]]] reverse empty] ⧗ (List a) → Unary → b → (List b) # creates list with single element -singleton [0 : empty] +singleton [0 : empty] ⧗ a → (List a) {…} singleton :test ({ (+1) }) ((+1) : empty) # appends two lists -append z [[[rec]]] +append z [[[rec]]] ⧗ (List a) → (List a) → (List a) rec ∅?1 case-end case-append case-append ^1 : (2 ~1 0) case-end 0 @@ -133,7 +134,7 @@ append z [[[rec]]] :test (((+1) : ((+2) : ((+3) : empty))) ++ ((+4) : empty)) ((+1) : ((+2) : ((+3) : ((+4) : empty)))) # appends an element to a list -snoc [[1 ++ ({ 0 })]] +snoc [[1 ++ ({ 0 })]] ⧗ (List a) → a → (List a) …;… snoc @@ -141,7 +142,7 @@ snoc [[1 ++ ({ 0 })]] :test (((+1) : empty) ; (+2)) ((+1) : ((+2) : empty)) # maps each element to a function -map z [[[rec]]] +map z [[[rec]]] ⧗ (a → b) → (List a) → (List b) rec ∅?0 case-end case-map case-map (1 ^0) : (2 1 ~0) case-end empty @@ -151,7 +152,7 @@ map z [[[rec]]] :test (++‣ <$> ((+1) : ((+2) : ((+3) : empty)))) ((+2) : ((+3) : ((+4) : empty))) # filters a list based on a predicate -filter z [[[rec]]] +filter z [[[rec]]] ⧗ (a → Boolean) → (List a) → (List a) rec ∅?0 case-end case-filter case-filter 1 ^0 (cons ^0) i (2 1 ~0) case-end empty @@ -167,14 +168,14 @@ filter z [[[rec]]] # case-last ∅?(~0) ^0 (1 ~0) # case-end empty # - taking the first element of the reversed list is actually way faster because laziness -last ^‣ ∘ <~>‣ +last ^‣ ∘ <~>‣ ⧗ (List a) → a _‣ last :test (_((+1) : ((+2) : ((+3) : empty)))) ((+3)) # returns everything but the last element of a list -init z [[rec]] +init z [[rec]] ⧗ (List a) → (List a) rec ∅?0 case-end case-init case-init ∅?(~0) empty (^0 : (1 ~0)) case-end empty @@ -182,7 +183,7 @@ init z [[rec]] :test (init ((+1) : ((+2) : ((+3) : empty)))) ((+1) : ((+2) : empty)) # concatenates a list of lists to one list -concat foldr append empty +concat foldr append empty ⧗ (List a) → (List a) → (List a) # TODO: ? # :test (concat ((((+1) : ((+2) : empty)) : ((+3) : ((+4) : empty))) : empty)) ((+1) : ((+2) : ((+3) : ((+4) : empty)))) @@ -190,12 +191,12 @@ concat foldr append empty :test (concat ("a" : ("b" : empty))) ("ab") # maps a function returning list of list and concatenates -concat-map concat ∘∘ map +concat-map concat ∘∘ map ⧗ (a → (List b)) → (List a) → (List b) :test (concat-map [-0 : (0 : empty)] ((+1) : ((+2) : empty))) ((-1) : ((+1) : ((-2) : ((+2) : empty)))) # zips two lists discarding excess elements -zip z [[[rec]]] +zip z [[[rec]]] ⧗ (List a) → (List b) → (List (Pair a b)) rec ∅?1 case-end case-zip case-zip ∅?0 empty ((^1 : ^0) : (2 ~1 ~0)) case-end empty @@ -203,7 +204,7 @@ zip z [[[rec]]] :test (zip ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) (((+1) : (+2)) : (((+2) : (+1)) : empty)) # applies pairs of the zipped list as arguments to a function -zip-with z [[[[rec]]]] +zip-with z [[[[rec]]]] ⧗ (a → b → c) → (List a) → (List b) → (List c) rec ∅?1 case-end case-zip case-zip ∅?0 empty ((2 ^1 ^0) : (3 2 ~1 ~0)) case-end empty @@ -211,17 +212,17 @@ zip-with z [[[[rec]]]] :test (zip-with …+… ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) ((+3) : ((+3) : empty)) # list comprehension -{…|…} map +{…|…} map ⧗ (a → b) → (List a) → (List b) :test ({ ++‣ | ((+0) : ((+2) : empty)) }) ((+1) : ((+3) : empty)) # doubled list comprehension -{…|…,…} zip-with +{…|…,…} zip-with ⧗ (a → b → c) → (List a) → (List b) → (List c) :test ({ …+… | ((+0) : ((+2) : empty)) , ((+1) : ((+3) : empty)) }) ((+1) : ((+5) : empty)) # returns first n elements of a list -take z [[[rec]]] +take z [[[rec]]] ⧗ Number → (List a) → (List a) rec ∅?0 case-end case-take case-take =?1 empty (^0 : (2 --1 ~0)) case-end empty @@ -229,7 +230,7 @@ take z [[[rec]]] :test (take (+2) ((+1) : ((+2) : ((+3) : empty)))) ((+1) : ((+2) : empty)) # takes elements while a predicate is satisfied -take-while z [[[rec]]] +take-while z [[[rec]]] ⧗ (a → Boolean) → (List a) → (List a) rec ∅?0 case-end case-take case-take 1 ^0 (^0 : (2 1 ~0)) empty case-end empty @@ -237,7 +238,7 @@ take-while z [[[rec]]] :test (take-while zero? ((+0) : ((+0) : ((+1) : empty)))) ((+0) : ((+0) : empty)) # removes first n elements of a list -drop z [[[rec]]] +drop z [[[rec]]] ⧗ Number → (List a) → (List a) rec ∅?0 case-end case-drop case-drop =?1 0 (2 --1 ~0) case-end empty @@ -245,7 +246,7 @@ drop z [[[rec]]] :test (drop (+2) ((+1) : ((+2) : ((+3) : empty)))) ((+3) : empty) # removes elements from list while a predicate is satisfied -drop-while z [[[rec]]] +drop-while z [[[rec]]] ⧗ (a → Boolean) → (List a) → (List a) rec ∅?0 case-end case-drop case-drop 1 ^0 (2 1 ~0) 0 case-end empty @@ -253,7 +254,7 @@ drop-while z [[[rec]]] :test (drop-while zero? ((+0) : ((+0) : ((+1) : empty)))) ((+1) : empty) # returns pair of take-while and drop-while -span z [[[rec]]] +span z [[[rec]]] ⧗ (a → Boolean) → (List a) → (Pair (List a) (List a)) rec ∅?0 case-end case-drop case-drop 1 ^0 ((^0 : ^recced) : ~recced) (empty : 0) recced 2 1 ~0 @@ -262,12 +263,12 @@ span z [[[rec]]] :test (span (\les? (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty))) # same as span but with inverted predicate -break span ∘ (…∘… ¬‣) +break span ∘ (…∘… ¬‣) ⧗ (a → Boolean) → (List a) → (Pair (List a) (List a)) :test (break (\gre? (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty))) # splits a list into two lists based on predicate -split-at z [[[rec]]] +split-at z [[[rec]]] ⧗ (a → Boolean) → (List a) → (Pair (List a) (List a)) rec ∅?dropped case-end case-split dropped drop-while 1 0 case-split ^broken : (2 1 ~broken) @@ -277,32 +278,32 @@ split-at z [[[rec]]] :test (split-at (…=?… (+1)) ((+2) : ((+1) : ((+3) : ((+2) : empty))))) ((((+2) : empty) : (((+3) : ((+2) : empty)) : empty))) # returns true if any element in a list matches a predicate -any? ⋁?‣ ∘∘ map +any? ⋁?‣ ∘∘ map ⧗ (a → Boolean) → (List a) → Boolean :test (any? (\gre? (+2)) ((+1) : ((+2) : ((+3) : empty)))) (true) :test (any? (\gre? (+2)) ((+1) : ((+2) : ((+2) : empty)))) (false) # returns true if all elements in a list match a predicate -all? ⋀?‣ ∘∘ map +all? ⋀?‣ ∘∘ map ⧗ (a → Boolean) → (List a) → Boolean :test (all? (\gre? (+2)) ((+3) : ((+4) : ((+5) : empty)))) (true) :test (all? (\gre? (+2)) ((+4) : ((+3) : ((+2) : empty)))) (false) # returns true if element is part of a list based on eq predicate -in? …∘… any? +in? …∘… any? ⧗ (a → a → Boolean) → a → (List a) → Boolean :test (in? …=?… (+3) ((+1) : ((+2) : ((+3) : empty)))) (true) :test (in? …=?… (+0) ((+1) : ((+2) : ((+3) : empty)))) (false) # returns true if all elements of one list are equal to corresponding elements of other list -eq? ⋀?‣ ∘∘∘ zip-with +eq? ⋀?‣ ∘∘∘ zip-with ⧗ (a → a → Boolean) → (List a) → Boolean :test (eq? …=?… ((+1) : ((+2) : empty)) ((+1) : ((+2) : empty))) (true) :test (eq? …=?… ((+1) : ((+2) : empty)) ((+2) : ((+2) : empty))) (false) :test (eq? …=?… empty empty) (true) # removes first element that match an eq predicate -remove z [[[[rec]]]] +remove z [[[[rec]]]] ⧗ (a → a → Boolean) → a → (List a) → (List a) rec ∅?0 case-end case-remove case-remove (2 ^0 1) ~0 (^0 : (3 2 1 ~0)) case-end empty @@ -310,7 +311,7 @@ remove z [[[[rec]]]] :test (remove …=?… (+2) ((+1) : ((+2) : ((+3) : ((+2) : empty))))) ((+1) : ((+3) : ((+2) : empty))) # removes duplicates from list based on eq predicate (keeps first occurrence) -nub z [[[rec]]] +nub z [[[rec]]] ⧗ (a → a → Boolean) → (List a) → (List a) rec ∅?0 case-end case-nub case-nub ^0 : (2 1 (~0 <#> [¬(2 0 ^1)])) case-end empty @@ -318,25 +319,25 @@ nub z [[[rec]]] :test (nub …=?… ((+1) : ((+2) : ((+3) : empty)))) (((+1) : ((+2) : ((+3) : empty)))) :test (nub …=?… ((+1) : ((+2) : ((+1) : empty)))) (((+1) : ((+2) : empty))) -# returns a list with infinite-times a element -repeat z [[rec]] +# returns a list with infinite-times an element +repeat z [[rec]] ⧗ a → (List a) rec 0 : (1 0) :test (take (+3) (repeat (+4))) ((+4) : ((+4) : ((+4) : empty))) -# returns a list with n-times a element -replicate \(g take repeat) +# returns a list with n-times an element +replicate \(g take repeat) ⧗ Number → a → (List a) :test (replicate (+3) (+4)) ((+4) : ((+4) : ((+4) : empty))) # returns an infinite list repeating a finite list -cycle z [[rec]] +cycle z [[rec]] ⧗ (List a) → (List a) rec 0 ++ (1 0) :test (take (+6) (cycle "ab")) ("ababab") # returns a list with infinite-times previous (or start) value applied to a function -iterate z [[[rec]]] +iterate z [[[rec]]] ⧗ (a → a) → a → (List a) rec 0 : (2 1 (1 0)) :test (take (+5) (iterate ++‣ (+0))) (((+0) : ((+1) : ((+2) : ((+3) : ((+4) : empty)))))) diff --git a/std/Logic.bruijn b/std/Logic.bruijn index 06a08eb..e6f205c 100644 --- a/std/Logic.bruijn +++ b/std/Logic.bruijn @@ -3,14 +3,14 @@ :import std/Combinator . # true -true k +true k ⧗ Boolean # false -false ki +false ki ⧗ Boolean # inverts boolean value # equivalent of [0 ⇒ false] -not! [0 false true] +not! [0 false true] ⧗ Boolean → Boolean ¬‣ not! @@ -18,7 +18,7 @@ not! [0 false true] :test (¬false) (true) # true if both args are true -and? [[1 0 false]] +and? [[1 0 false]] ⧗ Boolean → Boolean → Boolean …⋀?… and? @@ -28,7 +28,7 @@ and? [[1 0 false]] :test (false ⋀? false) (false) # true if not both args are true -nand? [[1 0 1 false true]] +nand? [[1 0 1 false true]] ⧗ Boolean → Boolean → Boolean :test (nand? true true) (false) :test (nand? true false) (true) @@ -36,7 +36,7 @@ nand? [[1 0 1 false true]] :test (nand? false false) (true) # true if one of the args is true -or? [[1 true 0]] +or? [[1 true 0]] ⧗ Boolean → Boolean → Boolean …⋁?… or? @@ -46,7 +46,7 @@ or? [[1 true 0]] :test (false ⋁? false) (false) # true if both args are false -nor? [[1 1 0 false true]] +nor? [[1 1 0 false true]] ⧗ Boolean → Boolean → Boolean :test (nor? true true) (false) :test (nor? true false) (false) @@ -54,7 +54,7 @@ nor? [[1 1 0 false true]] :test (nor? false false) (true) # true if args are not same bools -xor? [[1 ¬0 0]] +xor? [[1 ¬0 0]] ⧗ Boolean → Boolean → Boolean :test (xor? true true) (false) :test (xor? true false) (true) @@ -62,7 +62,7 @@ xor? [[1 ¬0 0]] :test (xor? false false) (false) # true if both args are same bools -xnor? [[1 0 ¬0]] +xnor? [[1 0 ¬0]] ⧗ Boolean → Boolean → Boolean :test (xnor? true true) (true) :test (xnor? true false) (false) @@ -72,7 +72,7 @@ xnor? [[1 0 ¬0]] # if first arg is true, exec first exp; else second exp # this function is generally redundant # I personally just write (exp? case-T case-F) directly -if [[[2 1 0]]] +if [[[2 1 0]]] ⧗ Boolean → a → b → c …?…:… if @@ -82,7 +82,7 @@ if [[[2 1 0]]] :test (false ? true : false) (false) # mathematical implies definition -implies [[¬1 ⋁? 0]] +implies [[¬1 ⋁? 0]] ⧗ Boolean → Boolean → Boolean …⇒?… implies @@ -92,7 +92,7 @@ implies [[¬1 ⋁? 0]] :test (false ⇒? false) (true) # mathematical iff (if and only if) definition -iff [[(1 ⇒? 0) ⋀? (0 ⇒? 1)]] +iff [[(1 ⇒? 0) ⋀? (0 ⇒? 1)]] ⧗ Boolean → Boolean → Boolean …⇔?… iff diff --git a/std/Math.bruijn b/std/Math.bruijn index 7cf0af0..7b94283 100644 --- a/std/Math.bruijn +++ b/std/Math.bruijn @@ -1,27 +1,28 @@ # MIT License, Copyright (c) 2022 Marvin Borner :import std/List . + :input std/Number . # adds all values in list -sum foldl add (+0) +sum foldl add (+0) ⧗ (List Number) → Number ∑‣ sum :test (∑((+1) : ((+2) : ((+3) : empty)))) ((+6)) # returns max value of list -lmax foldl1 max +lmax foldl1 max ⧗ (List Number) → Number :test (lmax ((+1) : ((+3) : ((+2) : empty)))) ((+3)) # returns min value of list -lmin foldl1 min +lmin foldl1 min ⧗ (List Number) → Number :test (lmin ((+2) : ((+1) : ((+0) : empty)))) ((+0)) # list from num to num -{…→…} z [[[rec]]] +{…→…} z [[[rec]]] ⧗ Number → Number → (List Number) rec (1 =? ++0) case-end case-list case-list 1 : (2 ++1 0) case-end empty @@ -29,7 +30,7 @@ lmin foldl1 min :test ({ (+0) → (+2) }) ((+0) : ((+1) : ((+2) : empty))) # equivalent of mathematical sum function -∑…→…|… z [[[[[rec]]]]] (+0) +∑…→…|… z [[[[[rec]]]]] (+0) ⧗ Number → Number → (Number → Number) → Number rec (2 =? ++1) case-end case-sum case-sum 4 (3 + (0 2)) ++2 1 0 case-end 3 @@ -37,22 +38,22 @@ lmin foldl1 min :test (∑ (+1) → (+3) | ++‣) ((+9)) # multiplies all values in list -product foldl mul (+1) +product foldl mul (+1) ⧗ (List Number) → Number Π product :test (Π ((+1) : ((+2) : ((+3) : empty)))) ((+6)) # equivalent of mathematical product function -∏…→…|… z [[[[[rec]]]]] (+1) +∏…→…|… z [[[[[rec]]]]] (+1) ⧗ Number → Number → (Number → Number) → Number rec (2 =? ++1) case-end case-sum - case-sum 4 (3 * (0 2)) ++2 1 0 + case-sum 4 (3 ⋅ (0 2)) ++2 1 0 case-end 3 :test (∏ (+1) → (+3) | ++‣) ((+24)) # greatest common divisor -gcd z [[[(1 =? 0) case-eq ((1 >? 0) case-gre case-les)]]] +gcd z [[[(1 =? 0) case-eq ((1 >? 0) case-gre case-les)]]] ⧗ Number → Number → Number case-eq 1 case-gre 2 (1 - 0) 0 case-les 2 1 (0 - 1) @@ -62,40 +63,33 @@ gcd z [[[(1 =? 0) case-eq ((1 >? 0) case-gre case-les)]]] :test ((gcd (+3) (+8)) =? ((+1))) (true) # power function -pow […!!… (iterate (…*… 0) (+1))] +pow […!!… (iterate (…⋅… 0) (+1))] ⧗ Number → Number → Number …**… pow :test (((+2) ** (+3)) =? ((+8))) (true) -# power function using ternary exponentiation -# a 1 → b 0 -# pow' z [[[rec]]] -# rec =?0 case-end case-pow -# case-pow =?(lst 0) (mult ⊩r) ((mult ⊩r) ⋅ 1) -# mult [0 ⋅ 0 ⋅ 0] -# r 2 1 /³0 -# case-end (+1) -pow' z [[[rec]]] +# power function using ternary exponentiation (TODO: slow..) +pow' z [[[rec]]] ⧗ Number → Number → Number rec =?0 case-end case-pow case-pow =?(lst 0) (r ⋅ r ⋅ r) (r ⋅ r ⋅ r ⋅ 1) r 2 1 /³0 case-end (+1) # prime number sequence -primes nub ((…≠?… (+1)) ∘∘ gcd) (iterate ++‣ (+2)) +primes nub ((…≠?… (+1)) ∘∘ gcd) (iterate ++‣ (+2)) ⧗ (List Number) # factorial function # TODO: faster fac? -fac [∏ (+1) → 0 | i] +fac [∏ (+1) → 0 | i] ⧗ Number → Number :test ((fac (+3)) =? (+6)) (true) # fibonacci sequence # TODO: faster fib? -fibs fst <$> (iterate [~0 : (^0 + ~0)] ((+0) : (+1))) +fibs head <$> (iterate [~0 : (^0 + ~0)] ((+0) : (+1))) ⧗ (List Number) -fib [fibs !! ++0] +fib [fibs !! ++0] ⧗ Number :test (fib (+5)) ((+8)) @@ -106,7 +100,8 @@ pascal iterate [zip-with …+… ({ (+0) } ++ 0) (0 ; (+0))] ({ (+1) }) # π # q 3, r 2, t 1, i 0 # translation of unbounded spigot algorithm by Jeremy Gibbons -π g (+1) (+180) (+60) (+2) +# TODO: Fix/faster +π g (+1) (+180) (+60) (+2) ⧗ (List Number) g y [[[[[calc]]]]] calc b : (4 q r t i) a ↑⁰(↑⁺0 ⋅ (↑⁰0 + (+2))) |