From e2c3965f929556dda9f779c237f4ba96c8f6c542 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Fri, 2 Aug 2024 00:26:21 +0200
Subject: Improved Parigot data types

---
 std/Number/Parigot.bruijn | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

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

diff --git a/std/Number/Parigot.bruijn b/std/Number/Parigot.bruijn
index 9a23fd4..51ae178 100644
--- a/std/Number/Parigot.bruijn
+++ b/std/Number/Parigot.bruijn
@@ -1,20 +1,29 @@
 # MIT License, Copyright (c) 2024 Marvin Borner
-# see "on the representation of data in lambda-calculus" #5
+# see "on the representation of data in lambda-calculus" (Parigot 1989)
 # has a "one-step" predecessor *and* addition function
-# has 2x space complexity compared to unary/Church
 
-zero [0]
+# zero Parigot number
+zero [0] ⧗ Parigot
 
-inc [[[0 2 1]]]
+# increments Parigot number
+inc [[[0 (2 1)]]] ⧗ Parigot → Parigot
 
 ++‣ inc
 
-dec [[1 0 [0]]]
+# decrements Parigot number
+dec [[1 0 [0]]] ⧗ Parigot → Parigot
 
 --‣ dec
 
 :test (dec (inc zero)) (zero)
 
+# adds two Parigot numbers
+add [[[2 (1 0)]]] ⧗ Parigot → Parigot → Parigot
+
+…+… add
+
+:test (add (inc (zero)) (inc (inc zero))) (inc (inc (inc zero)))
+
 iter [[[0 ι ρ ρ]]]
 	ρ [[3 (1 0 0)]]
 	ι [[4]]
-- 
cgit v1.2.3