More math

MAATHTHAHHAHA

6 files changed, 90 insertions, 1 deletions

diff --git a/std/Number/Conversion.bruijn b/std/Number/Conversion.bruijn
index 52f3c9e..01c7e9f 100644
--- a/std/Number/Conversion.bruijn
+++ b/std/Number/Conversion.bruijn
@@ -14,6 +14,8 @@ unary→ternary [0 T.inc (+0t)] ⧗ Unary → Ternary
 :test (¹³(+0u)) ((+0t))
 :test (¹³(+2u)) ((+2t))
 
+binary→unary [[0 (+0u) [U.inc (2 0)] 1]] (U.mul (+2u)) ⧗ Binary → Unary
+
 # converts ternary numbers to unary
 ternary→unary [T.apply 0 U.inc (+0u)] ⧗ Ternary → Unary
 
diff --git a/std/Number/Parigot.bruijn b/std/Number/Parigot.bruijn
new file mode 100644
index 0000000..9a23fd4
--- /dev/null
+++ b/std/Number/Parigot.bruijn
@@ -0,0 +1,24 @@
+# MIT License, Copyright (c) 2024 Marvin Borner
+# see "on the representation of data in lambda-calculus" #5
+# has a "one-step" predecessor *and* addition function
+# has 2x space complexity compared to unary/Church
+
+zero [0]
+
+inc [[[0 2 1]]]
+
+++‣ inc
+
+dec [[1 0 [0]]]
+
+--‣ dec
+
+:test (dec (inc zero)) (zero)
+
+iter [[[0 ι ρ ρ]]]
+	ρ [[3 (1 0 0)]]
+	ι [[4]]
+
+rec [[[0 ι ρ ρ --0]]]
+	ρ [[[4 0 (2 1 1)]]]
+	ι [[[5]]]
diff --git a/std/Number/Scott.bruijn b/std/Number/Scott.bruijn
new file mode 100644
index 0000000..bc776d8
--- /dev/null
+++ b/std/Number/Scott.bruijn
@@ -0,0 +1,31 @@
+# MIT License, Copyright (c) 2023 Marvin Borner
+
+:import std/Combinator .
+:import std/Logic .
+
+zero [[1]] ⧗ Scott
+
+inc [[[0 2]]] ⧗ Scott → Scott
+
+:test (inc zero) ([[0 zero]])
+:test (inc (inc zero)) ([[0 [[0 zero]]]])
+:test (inc (inc (inc zero))) ([[0 [[0 [[0 zero]]]]]])
+
+dec [0 zero [0]] ⧗ Scott → Scott
+
+:test (dec zero) (zero)
+:test (dec (inc zero)) (zero)
+:test (dec (inc (inc zero))) (inc zero)
+
+zero? [0 true [false]] ⧗ Scott → Boolean
+
+:test (zero? zero) (true)
+:test (zero? (inc zero)) (false)
+:test (zero? (inc (inc zero))) (false)
+
+add z [[[1 0 [inc (3 0 1)]]]] ⧗ Scott → Scott → Scott
+
+:test (add zero zero) (zero)
+:test (add zero (inc zero)) (inc zero)
+:test (add (inc zero) zero) (inc zero)
+:test (add (inc zero) (inc zero)) (inc (inc zero))
diff --git a/std/Number/Ternary.bruijn b/std/Number/Ternary.bruijn
index 27da643..2ad5059 100644
--- a/std/Number/Ternary.bruijn
+++ b/std/Number/Ternary.bruijn
@@ -328,7 +328,7 @@ abs [<?0 -0 0] ⧗ Number → Number
 :test (|(-1)) ((+1))
 :test (|(+42)) ((+42))
 
-# apply a function n times to a value
+# applies a function n times to a value
 # ~> substitute church numbers
 apply z [[[rec]]] ⧗ Number → (a → a) → a → a
 	rec =?1 case-end case-apply
@@ -382,6 +382,12 @@ log₃ log₃* ∘ strip ⧗ Number → Number
 :test (log₃ (+5)) ((+3))
 :test (log₃ (+42)) ((+5))
 
+# amount of non-zero trits
+hamming-weight [0 (+0) inc inc [0]] ⧗ Number → Number
+
+:test ((hamming-weight (+5)) =? (+3)) (true)
+:test ((hamming-weight (+6)) =? (+2)) (true)
+
 # returns the smallest number in a range such that a predicate is true
 binary-search z [[[[rec]]]] ⧗ (Number → Boolean) → Number → Number → Number
 	rec (0 =? 1) case-end case-search
diff --git a/std/Number/Unary.bruijn b/std/Number/Unary.bruijn
index ae54c19..b764e87 100644
--- a/std/Number/Unary.bruijn
+++ b/std/Number/Unary.bruijn
@@ -143,6 +143,9 @@ pow [[0 [[3 (1 0)]] pow*]] ⧗ Unary → Unary → Unary
 :test ((+2u) ^ (+3u)) ((+8u))
 :test ((+3u) ^ (+2u)) ((+9u))
 
+# also note that
+# [0 ..i.. 0] (+nu) = n^..i..^n
+
 # fibonacci sequence
 # index +1 vs std/Math fib
 fib [0 [[[2 0 [2 (1 0)]]]] [[1]] [0]] ⧗ Unary → Unary
diff --git a/std/Number/Wadsworth.bruijn b/std/Number/Wadsworth.bruijn
new file mode 100644
index 0000000..00bd3c3
--- /dev/null
+++ b/std/Number/Wadsworth.bruijn
@@ -0,0 +1,23 @@
+# MIT License, Copyright (c) 2023 Marvin Borner
+# from Wadsworth's "some unusual numeral systems" (p224, see refs in README)
+
+:import std/Combinator .
+
+zero [0 [k]] ⧗ Wadsworth
+
+# increment Wadsworth number
+inc [[[2 [2 (1 0) 1]]]] ⧗ Wadsworth → Wadsworth
+
+:test (inc (inc zero)) ([[[2 (1 (0 (k [[1]]))) 1 0]]])
+
+# decrement Wadsworth number
+dec [[1 [k (1 0)] i]] ⧗ Wadsworth → Wadsworth
+
+:test (dec (dec (inc (inc zero)))) (zero)
+
+# returns true if Wadsworth number is zero
+zero? [0 i (k (k [[0]]))] ⧗ Wadsworth → Bool
+
+:test (zero? zero) ([[1]])
+:test (zero? (inc zero)) ([[0]])
+:test (zero? (inc (inc zero))) ([[0]])