Some binary magic

1 files changed, 98 insertions, 55 deletions

diff --git a/std.bruijn b/std.bruijn
index a27dabb..b4d4be8 100644
--- a/std.bruijn
+++ b/std.bruijn
@@ -15,6 +15,14 @@ Y [[1 (0 0)] [1 (0 0)]]
 Θ [[0 (1 1 0)]] [[0 (1 1 0)]]
 i [0 S K]
 
+# =================
+# Alternative names
+# =================
+
+true T
+false F
+id I
+
 # =====
 # Pairs
 # =====
@@ -24,64 +32,99 @@ fst [0 T]
 snd [0 F]
 
 # ===================================
+# Binary
+# According to works of T.Æ. Mogensen
+# ===================================
+
+# TODO: contract-like type-checking
+#       like: `+ ... : [[[[# 3]]]]`
+
+# TODO: Fix for negative 4x abstraction
+
+upZero [[[[1 (3 2 1 0)]]]]
+upOne [[[[0 (3 2 1 0)]]]]
+up [[[[[4 1 0 (3 2 1 0)]]]]]
+
+zero? [0 T I [F]]
+
+binZero [[[2]]]
+binOne [[[0 2]]]
+
+_succZ (pair binZero binOne)
+_succA [0 [[pair (upZero 1) (upOne 1)]]]
+_succB [0 [[pair (upOne 1) (upZero 0)]]]
+succ [snd (0 _succZ _succA _succB)]
+
+_predZ (pair binZero binZero)
+_predA [0 [[pair (upZero 1) (upOne 0)]]]
+_predB [0 [[pair (upOne 1) (upZero 1)]]]
+pred [snd (0 _predZ _predA _predB)]
+
+# ===================================
 # Ternary
 # According to works of T.Æ. Mogensen
 # ===================================
 
-zero? [0 T [F] I [F]]
-upNeg [[[[[2 (4 3 2 1 0)]]]]]
-upZero [[[[[1 (4 3 2 1 0)]]]]]
-upPos [[[[[0 (4 3 2 1 0)]]]]]
-up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
-
-negate [[[[[4 3 0 1 2]]]]]
-
-tritNeg [[[2]]]
-tritZero [[[1]]]
-tritPos [[[0]]]
-lst [0 tritZero [tritNeg] [tritZero] [tritPos]]
-
-_succZ (pair +0 +1)
-_succANeg [0 [[[pair (upNeg 2) (upZero 2)]]]]
-_succAZero [0 [[[pair (upZero 2) (upPos 2)]]]]
-_succAPos [0 [[[pair (upPos 2) (upNeg 1)]]]]
-succ [snd (0 _succZ _succANeg _succAZero _succAPos)]
-
-_predZ (pair +0 -1)
-_predANeg [0 [[[pair (upNeg 2) (upPos 1)]]]]
-_predAZero [0 [[[pair (upZero 2) (upNeg 2)]]]]
-_predAPos [0 [[[pair (upPos 2) (upZero 2)]]]]
-pred [snd (0 _predZ _predANeg _predAZero _predAPos)]
-
-_absNeg [[[[[2 4]]]]]
-_absZero [[[[[1 4]]]]]
-_absPos [[[[[0 4]]]]]
-abstractify [0 [[[[3]]]] _absNeg _absZero _absPos]
-
-_normalize [[0 [ +0 ] [[upNeg (1 1 0)]] [[upZero (1 1 0)]] [[upPos (1 1 0)]] 1]]
-normalize ω _normalize
-
-_eqZero? [zero? (normalize 0)]
-_eqNeg [[0 F [2 0] [F] [F]]]
-_eqZero [[0 (1 0) [F] [2 0] [F]]]
-_eqPos [[0 F [F] [F] [2 0]]]
-_eqAbs [0 _eqZero? _eqNeg _eqZero _eqPos]
-eq [[_eqAbs 1 (abstractify 0)]]
-
-_addZ [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]]
-_addC [[1 0 tritZero]]
-_addBNeg2 [1 (upZero (3 0 tritNeg)) (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero))]
-_addBNeg [1 (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero)) (upZero (3 0 tritZero))]
-_addBZero [up 1 (3 0 tritZero)]
-_addBPos [1 (upZero (3 0 tritZero)) (upPos (3 0 tritZero)) (upNeg (3 0 tritPos))]
-_addBPos2 [1 (upPos (3 0 tritZero)) (upNeg (3 0 tritPos)) (upZero (3 0 tritPos))]
-_addANeg [[[1 (_addBNeg 1) _addBNeg2 _addBNeg _addBZero]]]
-_addAZero [[[1 (_addBZero 1) _addBNeg _addBZero _addBPos]]]
-_addAPos [[[1 (_addBPos 1) _addBZero _addBPos _addBPos2]]]
-_addAbs [_addC (0 _addZ _addANeg _addAZero _addAPos)]
-add [[_addAbs 1 (abstractify 0)]]
-
-sub [[add 1 (negate 0)]]
+# zero? [0 T [F] I [F]]
+# upNeg [[[[[2 (4 3 2 1 0)]]]]]
+# upZero [[[[[1 (4 3 2 1 0)]]]]]
+# upPos [[[[[0 (4 3 2 1 0)]]]]]
+# up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
+# 
+# negate [[[[[4 3 0 1 2]]]]]
+# 
+# tritNeg [[[2]]]
+# tritZero [[[1]]]
+# tritPos [[[0]]]
+# lst [0 tritZero [tritNeg] [tritZero] [tritPos]]
+# 
+# _stripZ pair +0 T
+# _stripANeg [0 [[pair (0 +0 (upNeg 1)) 0]]]
+# _stripAZero [0 [[pair (upZero 1) F]]]
+# _stripAPos [0 [[pair (upPos 1) F]]]
+# strip [fst (0 _stripZ _stripANeg _stripAZero _stripAPos)]
+# 
+# _succZ pair +0 +1
+# _succANeg [0 [[[pair (upNeg 2) (upZero 2)]]]]
+# _succAZero [0 [[[pair (upZero 2) (upPos 2)]]]]
+# _succAPos [0 [[[pair (upPos 2) (upNeg 1)]]]]
+# succ [snd (0 _succZ _succANeg _succAZero _succAPos)]
+# 
+# _predZ pair +0 -1
+# _predANeg [0 [[[pair (upNeg 2) (upPos 1)]]]]
+# _predAZero [0 [[[pair (upZero 2) (upNeg 2)]]]]
+# _predAPos [0 [[[pair (upPos 2) (upZero 2)]]]]
+# pred [snd (0 _predZ _predANeg _predAZero _predAPos)]
+# 
+# _absNeg [[[[[2 4]]]]]
+# _absZero [[[[[1 4]]]]]
+# _absPos [[[[[0 4]]]]]
+# abstractify [0 [[[[3]]]] _absNeg _absZero _absPos]
+# 
+# _normalize [[0 [ +0 ] [[upNeg (1 1 0)]] [[upZero (1 1 0)]] [[upPos (1 1 0)]] 1]]
+# normalize ω _normalize
+# 
+# _eqZero? [zero? (normalize 0)]
+# _eqNeg [[0 F [2 0] [F] [F]]]
+# _eqZero [[0 (1 0) [F] [2 0] [F]]]
+# _eqPos [[0 F [F] [F] [2 0]]]
+# _eqAbs [0 _eqZero? _eqNeg _eqZero _eqPos]
+# eq [[_eqAbs 1 (abstractify 0)]]
+# 
+# _addZ [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]]
+# _addC [[1 0 tritZero]]
+# _addBNeg2 [1 (upZero (3 0 tritNeg)) (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero))]
+# _addBNeg [1 (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero)) (upZero (3 0 tritZero))]
+# _addBZero [up 1 (3 0 tritZero)]
+# _addBPos [1 (upZero (3 0 tritZero)) (upPos (3 0 tritZero)) (upNeg (3 0 tritPos))]
+# _addBPos2 [1 (upPos (3 0 tritZero)) (upNeg (3 0 tritPos)) (upZero (3 0 tritPos))]
+# _addANeg [[[1 (_addBNeg 1) _addBNeg2 _addBNeg _addBZero]]]
+# _addAZero [[[1 (_addBZero 1) _addBNeg _addBZero _addBPos]]]
+# _addAPos [[[1 (_addBPos 1) _addBZero _addBPos _addBPos2]]]
+# _addAbs [_addC (0 _addZ _addANeg _addAZero _addAPos)]
+# add [[_addAbs 1 (abstractify 0)]]
+# 
+# sub [[add 1 (negate 0)]]
 
 # ===============
 # Boolean algebra
@@ -103,4 +146,4 @@ churchAdd [[[[3 1 (2 1 0)]]]]
 churchMul [[[2 (1 0)]]]
 churchExp [[0 1]]
 
-main I F
+main [[[0 2 1]]]