diff options
Diffstat (limited to 'std')
| -rw-r--r-- | std/Boolean.bruijn | 60 | ||||
| -rw-r--r-- | std/Church.bruijn | 7 | ||||
| -rw-r--r-- | std/Combinator.bruijn | 22 | ||||
| -rw-r--r-- | std/Number.bruijn | 173 | ||||
| -rw-r--r-- | std/Option.bruijn | 39 | ||||
| -rw-r--r-- | std/Pair.bruijn | 26 | ||||
| -rw-r--r-- | std/Result.bruijn | 21 |
7 files changed, 348 insertions, 0 deletions
diff --git a/std/Boolean.bruijn b/std/Boolean.bruijn new file mode 100644 index 0000000..36d11bd --- /dev/null +++ b/std/Boolean.bruijn @@ -0,0 +1,60 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +:import std/Combinator . + +not [0 F T] +:test not T = F +:test not F = T + +and [[1 0 F]] +:test and T T = T +:test and T F = F +:test and F T = F +:test and F F = F + +nand [[1 0 1 F T]] +:test nand T T = F +:test nand T F = T +:test nand F T = T +:test nand F F = T + +or [[1 T 0]] +:test or T T = T +:test or T F = T +:test or F T = T +:test or F F = F + +nor [[1 1 0 F T]] +:test nor T T = F +:test nor T F = F +:test nor F T = F +:test nor F F = T + +xor [[1 (not 0) 0]] +:test xor T T = F +:test xor T F = T +:test xor F T = T +:test xor F F = F + +xnor [[1 0 (not 0)]] +:test xnor T T = T +:test xnor T F = F +:test xnor F T = F +:test xnor F F = T + +if [[[2 1 0]]] +:test if T T F = T +:test if F T F = F + +implies [[or (not 1) 0]] +:test implies T T = T +:test implies T F = F +:test implies F T = T +:test implies F F = T + +iff [[and (implies 1 0) (implies 0 1)]] +:test iff T T = T +:test iff T F = F +:test iff F T = F +:test iff F F = T + diff --git a/std/Church.bruijn b/std/Church.bruijn new file mode 100644 index 0000000..40807dd --- /dev/null +++ b/std/Church.bruijn @@ -0,0 +1,7 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +church-zero [[0]] +church-succ [[[1 (2 1 0)]]] +church-add [[[[3 1 (2 1 0)]]]] +church-mul [[[2 (1 0)]]] +church-exp [[0 1]] diff --git a/std/Combinator.bruijn b/std/Combinator.bruijn new file mode 100644 index 0000000..95338a6 --- /dev/null +++ b/std/Combinator.bruijn @@ -0,0 +1,22 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +S [[[2 0 (1 0)]]] +K [[1]] +I [0] +B [[[2 (1 0)]]] +C [[[2 0 1]]] +W [[1 0 0]] +T [[1]] +F [[0]] +ω [0 0] +Ω ω ω +Y [[1 (0 0)] [1 (0 0)]] +Θ [[0 (1 1 0)]] [[0 (1 1 0)]] +i [0 S K] + +:test I = i i +:test K = i (i (i i)) +:test S = i (i (i (i i))) +:test B = S (K S) K +:test C = S (S (K (S (K S) K)) S) (K K) +:test W = S S (S K) diff --git a/std/Number.bruijn b/std/Number.bruijn new file mode 100644 index 0000000..5bc95a1 --- /dev/null +++ b/std/Number.bruijn @@ -0,0 +1,173 @@ +# MIT License, Copyright (c) 2022 Marvin Borner +# According to works of T.Æ. Mogensen + +:import std/Combinator . +:import std/Pair . + +# checks whether balanced ternary number is zero +zero? [0 T [F] [F] I] +:test zero? +0 = T +:test zero? -1 = F +:test zero? +1 = F +:test zero? +42 = F + +trit-neg [[[2]]] +trit-pos [[[1]]] +trit-zero [[[0]]] + +# shifts a negative trit into a balanced ternary number +up-neg [[[[[2 (4 3 2 1 0)]]]]] +:test up-neg +0 = -1 +:test up-neg -1 = -4 +:test up-neg +42 = +125 + +# shifts a positive trit into a balanced ternary number +up-pos [[[[[1 (4 3 2 1 0)]]]]] +:test up-pos +0 = +1 +:test up-pos -1 = -2 +:test up-pos +42 = +127 + +# shifts a zero trit into a balanced ternary number +up-zero [[[[[0 (4 3 2 1 0)]]]]] +:test up-zero +0 = [[[[0 3]]]] +:test up-zero +1 = +3 +:test up-zero +42 = +126 + +# shifts a specified trit into a balanced ternary number +up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]] +:test up trit-neg +42 = up-neg +42 +:test up trit-pos +42 = up-pos +42 +:test up trit-zero +42 = up-zero +42 + +# negates a balanced ternary number +negate [[[[[4 3 1 2 0]]]]] +:test negate +0 = +0 +:test negate -1 = +1 +:test negate +42 = -42 + +# extracts least significant trit from balanced ternary numbers +lst [0 trit-zero [trit-neg] [trit-pos] [trit-zero]] +:test lst +0 = trit-zero +:test lst -1 = trit-neg +:test lst +1 = trit-pos +:test lst +42 = trit-zero + +# converts the normal balanced ternary representation into abstract +# -> the abstract representation is used in add/sub/mul +_abs-neg [[[[[2 4]]]]] +_abs-pos [[[[[1 4]]]]] +_abs-zero [[[[[0 4]]]]] +abstractify [0 [[[[3]]]] _abs-neg _abs-pos _abs-zero] +:test abstractify -3 = [[[[0 [[[[2 [[[[3]]]]]]]]]]]] +:test abstractify +0 = [[[[3]]]] +:test abstractify +3 = [[[[0 [[[[1 [[[[3]]]]]]]]]]]] + +# converts the abstracted balanced ternary representation back to normal +# using Y/ω to solve recursion +_normalize [[0 +0 [up-neg ([3 3 0] 0)] [up-pos ([3 3 0] 0)] [up-zero ([3 3 0] 0)]]] +normalize ω _normalize +:test normalize [[[[3]]]] = +0 +:test normalize (abstractify +42) = +42 +:test normalize (abstractify -42) = -42 + +# checks whether two balanced ternary numbers are equal +# -> removes leading 0s! +_eq-z [zero? (normalize 0)] +_eq-neg [[0 F [2 0] [F] [F]]] +_eq-pos [[0 F [F] [2 0] [F]]] +_eq-zero [[0 (1 0) [F] [F] [2 0]]] +_eq-abs [0 _eq-z _eq-neg _eq-pos _eq-zero] +eq? [[_eq-abs 1 (abstractify 0)]] +:test eq? -42 -42 = T +:test eq? -1 -1 = T +:test eq? -1 +0 = F +:test eq? +0 +0 = T +:test eq? +1 +0 = F +:test eq? +1 +1 = T +:test eq? +42 +42 = T +:test eq? [[[[(1 (0 (0 (0 (0 3)))))]]]] +1 = T + +# strips leading 0s from balanced ternary number +_strip-z pair +0 T +_strip-neg [0 [[pair (up-neg 1) F]]] +_strip-pos [0 [[pair (up-pos 1) F]]] +_strip-zero [0 [[pair (0 +0 (up-zero 1)) 0]]] +strip [fst (0 _strip-z _strip-neg _strip-pos _strip-zero)] +:test strip [[[[0 3]]]] = +0 +:test strip [[[[2 (0 (0 (0 (0 3))))]]]] = -1 +:test strip +42 = +42 + +# I believe Mogensen's Paper has an error in its succ/pred definitions. +# They use 3 abstractions in the _succ* functions, also we use switched +/0 +# in comparison to their implementation, yet the order of neg/pos/zero is +# the same. Something's weird. + +# adds +1 to a balanced ternary number (can introduce leading 0s) +_succ-z pair +0 +1 +_succ-neg [0 [[pair (up-neg 1) (up-zero 1)]]] +_succ-zero [0 [[pair (up-zero 1) (up-pos 1)]]] +_succ-pos [0 [[pair (up-pos 1) (up-neg 0)]]] +succ [snd (0 _succ-z _succ-neg _succ-pos _succ-zero)] +ssucc [strip (succ 0)] +:test eq? (succ -42) -41 = T +:test eq? (succ -1) +0 = T +:test eq? (succ +0) +1 = T +:test eq? (succ (succ (succ (succ (succ +0))))) +5 = T +:test eq? (succ +42) +43 = T + +# subs +1 from a balanced ternary number (can introduce leading 0s) +_pred-z pair +0 -1 +_pred-neg [0 [[pair (up-neg 1) (up-pos 0)]]] +_pred-zero [0 [[pair (up-zero 1) (up-neg 1)]]] +_pred-pos [0 [[pair (up-pos 1) (up-zero 1)]]] +pred [snd (0 _pred-z _pred-neg _pred-pos _pred-zero)] +spred [strip (pred 0)] +:test pred -42 = -43 +:test pred +0 = -1 +:test spred (pred (pred (pred (pred +5)))) = +0 +:test spred +1 = +0 +:test pred +42 = +41 + +# adds two balanced ternary numbers (can introduce leading 0s) +_add-c [[1 0 trit-zero]] +_add-b-neg2 [1 (up-zero (3 0 trit-neg)) (up-neg (3 0 trit-zero)) (up-pos (3 0 trit-neg))] +_add-b-neg [1 (up-pos (3 0 trit-neg)) (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-zero))] +_add-b-zero [up 1 (3 0 trit-zero)] +_add-b-pos [1 (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-pos)) (up-pos (3 0 trit-zero))] +_add-b-pos2 [1 (up-pos (3 0 trit-zero)) (up-zero (3 0 trit-pos)) (up-neg (3 0 trit-pos))] +_add-a-neg [[[1 (_add-b-neg 1) _add-b-neg2 _add-b-zero _add-b-neg]]] +_add-a-pos [[[1 (_add-b-pos 1) _add-b-zero _add-b-pos2 _add-b-pos]]] +_add-a-zero [[[1 (_add-b-zero 1) _add-b-neg _add-b-pos _add-b-zero]]] +_add-z [[0 (pred (normalize 1)) (succ (normalize 1)) (normalize 1)]] +_add-abs [_add-c (0 _add-z _add-a-neg _add-a-pos _add-a-zero)] +add [[_add-abs 1 (abstractify 0)]] +sadd [[strip (add 1 0)]] +:test eq? (add -42 -1) -43 = T +:test eq? (add -5 +6) +1 = T +:test eq? (add -1 +0) -1 = T +:test eq? (add +0 +0) +0 = T +:test eq? (add +1 +2) +3 = T +:test eq? (add +42 +1) +43 = T + +# subs two balanced ternary numbers (can introduce leading 0s) +sub [[add 1 (negate 0)]] +ssub [[strip (sub 1 0)]] +:test eq? (sub -42 -1) -41 = T +:test eq? (sub -5 +6) -11 = T +:test eq? (sub -1 +0) -1 = T +:test eq? (sub +0 +0) +0 = T +:test eq? (sub +1 +2) -1 = T +:test eq? (sub +42 +1) +41 = T + +# muls two balanced ternary numbers (can introduce leading 0s) +_mul-neg [sub (up-zero 0) 1] +_mul-pos [add (up-zero 0) 1] +_mul-zero [up-zero 0] +mul [[1 +0 _mul-neg _mul-pos _mul-zero]] +smul [[strip (mul 1 0)]] +:test eq? (mul +42 +0) +0 = T +:test eq? (mul -1 +42) -42 = T +:test eq? (mul +3 +11) +33 = T +:test eq? (mul +42 -4) -168 = T + + diff --git a/std/Option.bruijn b/std/Option.bruijn new file mode 100644 index 0000000..e33cbb5 --- /dev/null +++ b/std/Option.bruijn @@ -0,0 +1,39 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +:import std/Combinator . + +# empty option +none T + +# encapsulates value in option +some [[[0 2]]] + +# checks whether option is none +none? [0 T [F]] +:test none? none = T +:test none? (some [[0]]) = F + +# checks whether option is some +some? [0 F [T]] +:test some? none = F +:test some? (some [[0]]) = T + +# applies a function to the value in a option +map [[0 none [some (2 0)]]] +:test map [[1]] (some [[0]]) = some [[[0]]] +:test map [[1]] none = none + +# applies a function to the value in a option or returns first arg if none +map-or [[[0 2 1]]] +:test map-or [[[2]]] [[1]] (some [[0]]) = [[[0]]] +:test map-or [[[2]]] [[1]] none = [[[2]]] + +# extracts value from option or returns first argument if none +unwrap-or [[0 1 I]] +:test unwrap-or F (some T) = T +:test unwrap-or F none = F + +# applies encapsulated value to given function +apply [[1 none 0]] +:test apply none [some ([[1]] 0)] = none +:test apply (some [[0]]) [some ([[1]] 0)] = some [[[0]]] diff --git a/std/Pair.bruijn b/std/Pair.bruijn new file mode 100644 index 0000000..75d8680 --- /dev/null +++ b/std/Pair.bruijn @@ -0,0 +1,26 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +:import std/Combinator . + +# pairs two expressions into one +pair [[[0 2 1]]] + +# extracts first expression from pair +fst [0 T] +:test fst (pair [[0]] [[1]]) = [[0]] + +# extracts second expression from pair +snd [0 F] +:test snd (pair [[0]] [[1]]) = [[1]] + +# applies both elements of a pair to a function +uncurry [[1 (fst 0) (snd 0)]] +:test uncurry W (pair [[0]] [[1]]) = [[1]] + +# applies a function to the pair of two values +curry [[[2 (pair 1 0)]]] +:test curry fst [[0]] [[1]] = [[0]] + +# swaps the values of a pair +swap [pair (snd 0) (fst 0)] +:test swap (pair [[0]] [[1]]) = pair [[1]] [[0]] diff --git a/std/Result.bruijn b/std/Result.bruijn new file mode 100644 index 0000000..28b8181 --- /dev/null +++ b/std/Result.bruijn @@ -0,0 +1,21 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +:import std/Combinator . + +# encapsulates a value in ok +ok [[[1 2]]] +:test ok [[0]] = [[1 [[0]]]] + +# encapsulates a value in err +err [[[0 2]]] +:test err [[0]] = [[0 [[0]]]] + +# checks whether result is ok +ok? [0 [T] [F]] +:test ok? (ok [[0]]) = T +:test ok? (err [[0]]) = F + +# checks whether result is not ok +err? [0 [F] [T]] +:test err? (ok [[0]]) = F +:test err? (err [[0]]) = T |