diff options
-rw-r--r-- | bruijn.cabal | 2 | ||||
-rw-r--r-- | std/Logic.bruijn | 104 | ||||
-rw-r--r-- | std/Logic/Binary.bruijn | 102 | ||||
-rw-r--r-- | std/Logic/Ternary.bruijn | 62 |
4 files changed, 169 insertions, 101 deletions
diff --git a/bruijn.cabal b/bruijn.cabal index 7b92d04..e2909c1 100644 --- a/bruijn.cabal +++ b/bruijn.cabal @@ -35,6 +35,8 @@ data-files: std/String.bruijn std/test_all.sh std/AIT/Beavers.bruijn + std/Logic/Binary.bruijn + std/Logic/Ternary.bruijn std/Number/Binary.bruijn std/Number/Bruijn.bruijn std/Number/Conversion.bruijn diff --git a/std/Logic.bruijn b/std/Logic.bruijn index b16595c..171b52b 100644 --- a/std/Logic.bruijn +++ b/std/Logic.bruijn @@ -1,102 +1,4 @@ -# MIT License, Copyright (c) 2022 Marvin Borner +# MIT License, Copyright (c) 2024 Marvin Borner +# this is just a reference to the boolean implementation -:import std/Combinator . - -# true -true k ⧗ Boolean - -# false -false ki ⧗ Boolean - -# inverts boolean value -# equivalent of [0 ⇒ false] -not! c ⧗ Boolean → Boolean - -¬‣ not! - -:test (¬true) (false) -:test (¬false) (true) - -# true if both args are true -and? [[0 1 0]] ⧗ Boolean → Boolean → Boolean - -…⋀?… and? - -:test (true ⋀? true) (true) -:test (true ⋀? false) (false) -:test (false ⋀? true) (false) -:test (false ⋀? false) (false) - -# true if not both args are true -nand? [[1 0 1 false true]] ⧗ Boolean → Boolean → Boolean - -:test (nand? true true) (false) -:test (nand? true false) (true) -:test (nand? false true) (true) -:test (nand? false false) (true) - -# true if one of the args is true -or? m ⧗ Boolean → Boolean → Boolean - -…⋁?… or? - -:test (true ⋁? true) (true) -:test (true ⋁? false) (true) -:test (false ⋁? true) (true) -:test (false ⋁? false) (false) - -# true if both args are false -nor? [[1 1 0 false true]] ⧗ Boolean → Boolean → Boolean - -:test (nor? true true) (false) -:test (nor? true false) (false) -:test (nor? false true) (false) -:test (nor? false false) (true) - -# true if args are not same bools -xor? [[0 (1 false 0) 1]] ⧗ Boolean → Boolean → Boolean - -:test (xor? true true) (false) -:test (xor? true false) (true) -:test (xor? false true) (true) -:test (xor? false false) (false) - -# true if both args are same bools -xnor? [[0 1 (1 0 true)]] ⧗ Boolean → Boolean → Boolean - -:test (xnor? true true) (true) -:test (xnor? true false) (false) -:test (xnor? false true) (false) -:test (xnor? false false) (true) - -# 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]]] ⧗ Boolean → a → b → c - -…?…:… if - -:test (if true true false) (true) -:test (true ? true : false) (true) -:test (if false true false) (false) -:test (false ? true : false) (false) - -# mathematical implies definition -implies [[1 0 true]] ⧗ Boolean → Boolean → Boolean - -…⇒?… implies - -:test (true ⇒? true) (true) -:test (true ⇒? false) (false) -:test (false ⇒? true) (true) -:test (false ⇒? false) (true) - -# mathematical iff (if and only if) definition -iff xnor? ⧗ Boolean → Boolean → Boolean - -…⇔?… iff - -:test (true ⇔? true) (true) -:test (true ⇔? false) (false) -:test (false ⇔? true) (false) -:test (false ⇔? false) (true) +:input std/Logic/Binary . diff --git a/std/Logic/Binary.bruijn b/std/Logic/Binary.bruijn new file mode 100644 index 0000000..b16595c --- /dev/null +++ b/std/Logic/Binary.bruijn @@ -0,0 +1,102 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +:import std/Combinator . + +# true +true k ⧗ Boolean + +# false +false ki ⧗ Boolean + +# inverts boolean value +# equivalent of [0 ⇒ false] +not! c ⧗ Boolean → Boolean + +¬‣ not! + +:test (¬true) (false) +:test (¬false) (true) + +# true if both args are true +and? [[0 1 0]] ⧗ Boolean → Boolean → Boolean + +…⋀?… and? + +:test (true ⋀? true) (true) +:test (true ⋀? false) (false) +:test (false ⋀? true) (false) +:test (false ⋀? false) (false) + +# true if not both args are true +nand? [[1 0 1 false true]] ⧗ Boolean → Boolean → Boolean + +:test (nand? true true) (false) +:test (nand? true false) (true) +:test (nand? false true) (true) +:test (nand? false false) (true) + +# true if one of the args is true +or? m ⧗ Boolean → Boolean → Boolean + +…⋁?… or? + +:test (true ⋁? true) (true) +:test (true ⋁? false) (true) +:test (false ⋁? true) (true) +:test (false ⋁? false) (false) + +# true if both args are false +nor? [[1 1 0 false true]] ⧗ Boolean → Boolean → Boolean + +:test (nor? true true) (false) +:test (nor? true false) (false) +:test (nor? false true) (false) +:test (nor? false false) (true) + +# true if args are not same bools +xor? [[0 (1 false 0) 1]] ⧗ Boolean → Boolean → Boolean + +:test (xor? true true) (false) +:test (xor? true false) (true) +:test (xor? false true) (true) +:test (xor? false false) (false) + +# true if both args are same bools +xnor? [[0 1 (1 0 true)]] ⧗ Boolean → Boolean → Boolean + +:test (xnor? true true) (true) +:test (xnor? true false) (false) +:test (xnor? false true) (false) +:test (xnor? false false) (true) + +# 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]]] ⧗ Boolean → a → b → c + +…?…:… if + +:test (if true true false) (true) +:test (true ? true : false) (true) +:test (if false true false) (false) +:test (false ? true : false) (false) + +# mathematical implies definition +implies [[1 0 true]] ⧗ Boolean → Boolean → Boolean + +…⇒?… implies + +:test (true ⇒? true) (true) +:test (true ⇒? false) (false) +:test (false ⇒? true) (true) +:test (false ⇒? false) (true) + +# mathematical iff (if and only if) definition +iff xnor? ⧗ Boolean → Boolean → Boolean + +…⇔?… iff + +:test (true ⇔? true) (true) +:test (true ⇔? false) (false) +:test (false ⇔? true) (false) +:test (false ⇔? false) (true) diff --git a/std/Logic/Ternary.bruijn b/std/Logic/Ternary.bruijn new file mode 100644 index 0000000..71fb5ac --- /dev/null +++ b/std/Logic/Ternary.bruijn @@ -0,0 +1,62 @@ +# MIT License, Copyright (c) 2023 Marvin Borner + +# true +true [[[0]]] + +# maybe (true-ish) +maybe [[[1]]] + +# false +false [[[2]]] + +# inverts trit value +¬‣ [0 true maybe false] ⧗ Trit → Trit + +:test (¬true) (false) +:test (¬maybe) (maybe) +:test (¬false) (true) + +# true if both args are true-ish +and? [[1 (0 1 1 1) (0 0 0 1) (0 0 0 0)]] ⧗ Trit → Trit → Trit + +…⋀?… and? + +:test (true ⋀? true) (true) +:test (true ⋀? maybe) (maybe) +:test (true ⋀? false) (false) +:test (maybe ⋀? true) (maybe) +:test (maybe ⋀? maybe) (maybe) +:test (maybe ⋀? false) (false) +:test (false ⋀? true) (false) +:test (false ⋀? maybe) (false) +:test (false ⋀? false) (false) + +# true if one of the args is true-ish +or? [[1 (0 0 0 0) (0 1 0 0) (0 1 1 1)]] ⧗ Trit → Trit → Trit + +…⋁?… or? + +:test (true ⋁? true) (true) +:test (true ⋁? maybe) (true) +:test (true ⋁? false) (true) +:test (maybe ⋁? true) (true) +:test (maybe ⋁? maybe) (maybe) +:test (maybe ⋁? false) (maybe) +:test (false ⋁? true) (true) +:test (false ⋁? maybe) (maybe) +:test (false ⋁? false) (false) + +# mathematical iff (if and only if) definition +iff [[1 (0 true 0 1) (0 1 1 1) (0 0 0 0)]] ⧗ Trit → Trit → Trit + +…⇔?… iff + +:test (true ⇔? true) (true) +:test (true ⇔? maybe) (maybe) +:test (true ⇔? false) (false) +:test (maybe ⇔? true) (maybe) +:test (maybe ⇔? maybe) (maybe) +:test (maybe ⇔? false) (maybe) +:test (false ⇔? true) (false) +:test (false ⇔? maybe) (maybe) +:test (false ⇔? false) (true) |