diff options
Diffstat (limited to 'std.bruijn')
| -rw-r--r-- | std.bruijn | 179 |
1 files changed, 107 insertions, 72 deletions
@@ -15,71 +15,118 @@ 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 +:test I = i i +:test K = i (i (i i)) +:test S = i (i (i (i i))) # ===== # Pairs # ===== +# pairs two expressions into one pair [[[0 2 1]]] -fst [0 T] -snd [0 F] +# extracts first expression from pair +fst [0 T] :test fst (pair [[0]] [[1]]) = [[0]] + +# extracts second expression from pair +snd [0 F] :test snd (pair [[0]] [[1]]) = [[1]] -# TODO: contract-like type-checking -# like: `+ ... : [[[[# 3]]]]` +# TODO: investigate currying and chaining functions +# -> WHNF things? +# chain [[[2 (1 0)]]] # =================================== # Ternary # According to works of T.Æ. Mogensen # =================================== +# checks whether balanced ternary number is zero zero? [0 T [F] [F] I] :test zero? +0 = T :test zero? -1 = F :test zero? +1 = F :test zero? +42 = F +trit-neg [[[2]]] +trit-pos [[[1]]] +trit-zero [[[0]]] + +# shifts a negative trit into a balanced ternary number up-neg [[[[[2 (4 3 2 1 0)]]]]] :test up-neg +0 = -1 :test up-neg -1 = -4 :test up-neg +42 = +125 +# shifts a positive trit into a balanced ternary number up-pos [[[[[1 (4 3 2 1 0)]]]]] :test up-pos +0 = +1 :test up-pos -1 = -2 :test up-pos +42 = +127 +# shifts a zero trit into a balanced ternary number up-zero [[[[[0 (4 3 2 1 0)]]]]] :test up-zero +0 = [[[[0 3]]]] :test up-zero +1 = +3 :test up-zero +42 = +126 +# shifts a specified trit into a balanced ternary number up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]] -# TODO: up is incorrect +:test up trit-neg +42 = up-neg +42 +:test up trit-pos +42 = up-pos +42 +:test up trit-zero +42 = up-zero +42 +# negates a balanced ternary number negate [[[[[4 3 1 2 0]]]]] :test negate +0 = +0 :test negate -1 = +1 :test negate +42 = -42 -trit-neg [[[2]]] -trit-pos [[[1]]] -trit-zero [[[0]]] +# extracts least significant trit from balanced ternary numbers lst [0 trit-zero [trit-neg] [trit-pos] [trit-zero]] :test lst +0 = trit-zero :test lst -1 = trit-neg :test lst +1 = trit-pos :test lst +42 = trit-zero +# converts the normal balanced ternary representation into abstract +# -> the abstract representation is used in add/sub/mul +_abs-neg [[[[[2 4]]]]] +_abs-pos [[[[[1 4]]]]] +_abs-zero [[[[[0 4]]]]] +abstractify [0 [[[[3]]]] _abs-neg _abs-pos _abs-zero] +:test abstractify -3 = [[[[0 [[[[2 [[[[3]]]]]]]]]]]] +:test abstractify +0 = [[[[3]]]] +:test abstractify +3 = [[[[0 [[[[1 [[[[3]]]]]]]]]]]] + +# converts the abstracted balanced ternary representation back to normal +# using Y/ω to solve recursion +_normalize [[0 +0 [up-neg ([3 3 0] 0)] [up-pos ([3 3 0] 0)] [up-zero ([3 3 0] 0)]]] +normalize ω _normalize +:test normalize [[[[3]]]] = +0 +:test normalize (abstractify +42) = +42 +:test normalize (abstractify -42) = -42 + +# checks whether two balanced ternary numbers are equal +# -> removes leading 0s! +_eq-z [zero? (normalize 0)] +_eq-neg [[0 F [2 0] [F] [F]]] +_eq-pos [[0 F [F] [2 0] [F]]] +_eq-zero [[0 (1 0) [F] [F] [2 0]]] +_eq-abs [0 _eq-z _eq-neg _eq-pos _eq-zero] +eq? [[_eq-abs 1 (abstractify 0)]] +:test eq? -42 -42 = T +:test eq? -1 -1 = T +:test eq? -1 +0 = F +:test eq? +0 +0 = T +:test eq? +1 +0 = F +:test eq? +1 +1 = T +:test eq? +42 +42 = T +:test eq? [[[[(1 (0 (0 (0 (0 3)))))]]]] +1 = T + +# strips leading 0s from balanced ternary number _strip-z pair +0 T _strip-neg [0 [[pair (up-neg 1) F]]] _strip-pos [0 [[pair (up-pos 1) F]]] @@ -94,18 +141,20 @@ strip [fst (0 _strip-z _strip-neg _strip-pos _strip-zero)] # in comparison to their implementation, yet the order of neg/pos/zero is # the same. Something's weird. +# adds +1 to a balanced ternary number (can introduce leading 0s) _succ-z pair +0 +1 _succ-neg [0 [[pair (up-neg 1) (up-zero 1)]]] _succ-zero [0 [[pair (up-zero 1) (up-pos 1)]]] _succ-pos [0 [[pair (up-pos 1) (up-neg 0)]]] succ [snd (0 _succ-z _succ-neg _succ-pos _succ-zero)] ssucc [strip (succ 0)] -:test succ -42 = -41 -:test ssucc -1 = +0 -:test succ +0 = +1 -:test succ (succ (succ (succ (succ +0)))) = +5 -:test succ +42 = +43 +:test eq? (succ -42) -41 = T +:test eq? (succ -1) +0 = T +:test eq? (succ +0) +1 = T +:test eq? (succ (succ (succ (succ (succ +0))))) +5 = T +:test eq? (succ +42) +43 = T +# subs +1 from a balanced ternary number (can introduce leading 0s) _pred-z pair +0 -1 _pred-neg [0 [[pair (up-neg 1) (up-pos 0)]]] _pred-zero [0 [[pair (up-zero 1) (up-neg 1)]]] @@ -118,62 +167,47 @@ spred [strip (pred 0)] :test spred +1 = +0 :test pred +42 = +41 -_abs-neg [[[[[2 4]]]]] -_abs-pos [[[[[1 4]]]]] -_abs-zero [[[[[0 4]]]]] -abstractify [0 [[[[3]]]] _abs-neg _abs-pos _abs-zero] -:test abstractify -3 = [[[[0 [[[[2 [[[[3]]]]]]]]]]]] -:test abstractify +0 = [[[[3]]]] -:test abstractify +3 = [[[[0 [[[[1 [[[[3]]]]]]]]]]]] - -# solving recursion using Y/ω -_normalize [[0 +0 [up-neg ([3 3 0] 0)] [up-pos ([3 3 0] 0)] [up-zero ([3 3 0] 0)]]] -normalize ω _normalize -:test normalize [[[[3]]]] = +0 -:test normalize (abstractify +42) = +42 -:test normalize (abstractify -42) = -42 - -_eq-z [zero? (normalize 0)] -_eq-neg [[0 F [2 0] [F] [F]]] -_eq-pos [[0 F [F] [2 0] [F]]] -_eq-zero [[0 (1 0) [F] [F] [2 0]]] -_eq-abs [0 _eq-z _eq-neg _eq-pos _eq-zero] -eq? [[_eq-abs 1 (abstractify 0)]] -:test eq? -42 -42 = T -:test eq? -1 -1 = T -:test eq? -1 +0 = F -:test eq? +0 +0 = T -:test eq? +1 +0 = F -:test eq? +1 +1 = T -:test eq? +42 +42 = T - -# TODO: Much zero/one switching needed -_add-z [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]] +# adds two balanced ternary numbers (can introduce leading 0s) _add-c [[1 0 trit-zero]] -_add-b-neg2 [1 (up-zero (3 0 trit-neg)) (up-pos (3 0 trit-neg)) (up-neg (3 0 trit-zero))] -_add-b-neg [1 (up-pos (3 0 trit-neg)) (up-neg (3 0 trit-zero)) (up-zero (3 0 trit-zero))] +_add-b-neg2 [1 (up-zero (3 0 trit-neg)) (up-neg (3 0 trit-zero)) (up-pos (3 0 trit-neg))] +_add-b-neg [1 (up-pos (3 0 trit-neg)) (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-zero))] _add-b-zero [up 1 (3 0 trit-zero)] -_add-b-pos [1 (up-zero (3 0 trit-zero)) (up-pos (3 0 trit-zero)) (up-neg (3 0 trit-pos))] -_add-b-pos2 [1 (up-pos (3 0 trit-zero)) (up-neg (3 0 trit-pos)) (up-zero (3 0 trit-pos))] -_add-a-neg [[[1 (_add-b-neg 1) _add-b-neg2 _add-b-neg _add-b-zero]]] -_add-a-zero [[[1 (_add-b-zero 1) _add-b-neg _add-b-zero _add-b-pos]]] -_add-a-pos [[[1 (_add-b-pos 1) _add-b-zero _add-b-pos _add-b-pos2]]] -_add-abs [_add-c (0 _add-z _add-a-neg _add-a-pos _add-a-neg)] +_add-b-pos [1 (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-pos)) (up-pos (3 0 trit-zero))] +_add-b-pos2 [1 (up-pos (3 0 trit-zero)) (up-zero (3 0 trit-pos)) (up-neg (3 0 trit-pos))] +_add-a-neg [[[1 (_add-b-neg 1) _add-b-neg2 _add-b-zero _add-b-neg]]] +_add-a-pos [[[1 (_add-b-pos 1) _add-b-zero _add-b-pos2 _add-b-pos]]] +_add-a-zero [[[1 (_add-b-zero 1) _add-b-neg _add-b-pos _add-b-zero]]] +_add-z [[0 (pred (normalize 1)) (succ (normalize 1)) (normalize 1)]] +_add-abs [_add-c (0 _add-z _add-a-neg _add-a-pos _add-a-zero)] add [[_add-abs 1 (abstractify 0)]] -:test add -42 -1 = -43 -:test add -5 +6 = +1 -:test add -1 +0 = -1 -:test add +0 +0 = +0 -:test add +1 +2 = +3 -:test add +42 +1 = +43 - +sadd [[strip (add 1 0)]] +:test eq? (add -42 -1) -43 = T +:test eq? (add -5 +6) +1 = T +:test eq? (add -1 +0) -1 = T +:test eq? (add +0 +0) +0 = T +:test eq? (add +1 +2) +3 = T +:test eq? (add +42 +1) +43 = T + +# subs two balanced ternary numbers (can introduce leading 0s) sub [[add 1 (negate 0)]] -:test sub -42 -1 = -41 -:test sub -5 +6 = -11 -:test sub -1 +0 = -1 -:test sub +0 +0 = +0 -:test sub +1 +2 = -1 -:test sub +42 +1 = +41 +ssub [[strip (sub 1 0)]] +:test eq? (sub -42 -1) -41 = T +:test eq? (sub -5 +6) -11 = T +:test eq? (sub -1 +0) -1 = T +:test eq? (sub +0 +0) +0 = T +:test eq? (sub +1 +2) -1 = T +:test eq? (sub +42 +1) +41 = T + +# muls two balanced ternary numbers (can introduce leading 0s) +_mul-neg [sub (up-zero 0) 1] +_mul-pos [add (up-zero 0) 1] +_mul-zero [up-zero 0] +mul [[1 +0 _mul-neg _mul-pos _mul-zero]] +smul [[strip (mul 1 0)]] +:test eq? (mul +42 +0) +0 = T +:test eq? (mul -1 +42) -42 = T +:test eq? (mul +3 +11) +33 = T +:test eq? (mul +42 -4) -168 = T # =============== # Boolean algebra @@ -184,6 +218,7 @@ and [[1 0 F]] or [[1 T 0]] xor [[1 (not 0) 0]] if [[[2 1 0]]] +:test not (or (and false true) true) = false # =============== # Church numerals |