From a3fe79ec9ad1c22eb288dd7fc32dfcea14b383b1 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Thu, 23 Jan 2025 15:34:04 +0100
Subject: Improve Parigot numbers

---
 std/Number/Parigot.bruijn | 69 ++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 62 insertions(+), 7 deletions(-)

(limited to 'std/Number/Parigot.bruijn')

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]]]
-- 
cgit v1.2.3