Improve Parigot numbers

2 files changed, 71 insertions, 7 deletions

diff --git a/std/Number/Conversion.bruijn b/std/Number/Conversion.bruijn
index 01c7e9f..2f6681a 100644
--- a/std/Number/Conversion.bruijn
+++ b/std/Number/Conversion.bruijn
@@ -5,6 +5,7 @@
 :import std/Number/Unary U
 :import std/Number/Binary B
 :import std/Number/Ternary T
+:import std/Number/Parigot P
 
 # converts unary numbers to ternary
 unary→ternary [0 T.inc (+0t)] ⧗ Unary → Ternary
@@ -24,6 +25,14 @@ ternary→unary [T.apply 0 U.inc (+0u)] ⧗ Ternary → Unary
 :test (³¹(+0t)) ((+0u))
 :test (³¹(+2t)) ((+2u))
 
+# converts Parigot numbers to unary
+parigot→unary [[[P.iter 0 1 2]]] ⧗ Parigot → Unary
+
+ᵖ¹‣ parigot→unary
+
+:test (ᵖ¹P.zero) ((+0u))
+:test (ᵖ¹(P.inc (P.inc P.zero))) ((+2u))
+
 # converts binary numbers to ternary
 # constructs reversed path of composed functions and applies to ternary
 binary→ternary [y [[[rec]]] [0] 0 (+0t)] ⧗ Binary → Ternary
diff --git a/std/Number/Parigot.bruijn b/std/Number/Parigot.bruijn
index 51ae178..108d2b7 100644
--- a/std/Number/Parigot.bruijn
+++ b/std/Number/Parigot.bruijn
@@ -2,32 +2,87 @@
 # see "on the representation of data in lambda-calculus" (Parigot 1989)
 # has a "one-step" predecessor *and* addition function
 
+# Compared to unary/church, they're also faster in many reducers
+
+:import std/Combinator .
+:import std/Logic .
+
 # zero Parigot number
-zero [0] ⧗ Parigot
+zero i ⧗ Parigot
+
+# returns true if Parigot number is zero
+zero? [0 [true] [false]] ⧗ Parigot → Boolean
+
+=?‣ zero?
+
+:test (=?zero) (true)
+:test (=?[[0 1]]) (false)
+:test (=?[[0 [0 2]]]) (false)
 
 # increments Parigot number
-inc [[[0 (2 1)]]] ⧗ Parigot → Parigot
+inc q''' ⧗ Parigot → Parigot
 
 ++‣ inc
 
+:test (++zero) ([[0 1]])
+:test (++[[0 1]]) ([[0 [0 2]]])
+
 # decrements Parigot number
-dec [[1 0 [0]]] ⧗ Parigot → Parigot
+dec r i ⧗ Parigot → Parigot
 
 --‣ dec
 
-:test (dec (inc zero)) (zero)
+:test (--(++zero)) (zero)
+:test (--[[0 [0 2]]]) ([[0 1]])
+
+# decrements Parigot number with `dec 0 = 0`
+dec' [0 [[[0]]] [[0]] [1 0 [0]]] ⧗ Parigot → Parigot
 
 # adds two Parigot numbers
-add [[[2 (1 0)]]] ⧗ Parigot → Parigot → Parigot
+add b ⧗ Parigot → Parigot → Parigot
 
 …+… add
 
 :test (add (inc (zero)) (inc (inc zero))) (inc (inc (inc zero)))
 
-iter [[[0 ι ρ ρ]]]
+# multiplies two Parigot numbers
+# [[iter zero (add 1) 0]]
+mul [[[1 [[[0]]] 0 0] [[[4 (2 1 1 0)]]]]] ⧗ Parigot → Parigot → Parigot
+
+…⋅… mul
+
+:test ((inc zero) ⋅ zero) (zero)
+:test ((inc zero) ⋅ (inc (inc zero))) (inc (inc zero))
+:test ((inc (inc (inc zero))) ⋅ (inc (inc zero))) (inc (inc (inc (inc (inc (inc zero))))))
+
+# subtracts two Parigot numbers
+# will not give correct results when b>a in a-b (use sub' then)
+# [[iter 1 dec 0]]
+sub [[[1 [[4]] 0 0] [[[2 1 1 0 [0]]]]]] ⧗ Parigot → Parigot → Parigot
+
+…-… sub
+
+:test ((inc zero) - zero) (inc zero)
+:test ((inc (inc (inc zero))) - (inc zero)) (inc (inc zero))
+
+# subtracts two Parigot numbers such that a-b=0 if b>a
+sub' [[[0 [[3]] 2 2]]] [[dec' (1 0 0)]] ⧗ Parigot → Parigot → Parigot
+
+…-*… sub'
+
+:test ((inc zero) -* zero) (inc zero)
+:test ((inc (inc (inc zero))) -* (inc zero)) (inc (inc zero))
+:test ((inc zero) -* (inc (inc zero))) (zero)
+
+# returns true if Parigot number is greater than other Parigot number
+gt? not! ∘∘ (zero? ∘∘ sub') ⧗ Parigot → Parigot → Parigot
+
+iter [[[0 ι ρ ρ]]] ⧗ a → (a → a) → Parigot → a
 	ρ [[3 (1 0 0)]]
 	ι [[4]]
 
-rec [[[0 ι ρ ρ --0]]]
+:test (iter zero inc (inc (inc (inc zero)))) (inc (inc (inc zero)))
+
+rec [[[0 ι ρ ρ --0]]] ⧗ Parigot → (Parigot → Boolean) → Parigot → Parigot
 	ρ [[[4 0 (2 1 1)]]]
 	ι [[[5]]]