# MIT License, Copyright (c) 2022 Marvin Borner # According to works of T.Æ. Mogensen :import std/Combinator . :import std/Pair . :import std/Logic . # negative trit indicating coeffecient of (-1) trit-neg [[[2]]] # returns whether a trit is negative trit-neg? [0 T F F] # positive trit indicating coeffecient of (+1) trit-pos [[[1]]] # returns whether a trit is positive trit-pos? [0 F T F] # zero trit indicating coeffecient of 0 trit-zero [[[0]]] # returns whether a trit is zero trit-zero? [0 F F T] :test (trit-neg? trit-neg) (T) :test (trit-neg? trit-pos) (F) :test (trit-neg? trit-zero) (F) :test (trit-pos? trit-neg) (F) :test (trit-pos? trit-pos) (T) :test (trit-pos? trit-zero) (F) :test (trit-zero? trit-neg) (F) :test (trit-zero? trit-pos) (F) :test (trit-zero? trit-zero) (T) # shifts a negative trit into a balanced ternary number up-neg [[[[[2 (4 3 2 1 0)]]]]] ^<( up-neg :test (^<(+0)) ((-1)) :test (^<(-1)) ((-4)) :test (^<(+42)) ((+125)) # shifts a positive trit into a balanced ternary number up-pos [[[[[1 (4 3 2 1 0)]]]]] ^>( up-pos :test (^>(+0)) ((+1)) :test (^>(-1)) ((-2)) :test (^>(+42)) ((+127)) # shifts a zero trit into a balanced ternary number up-zero [[[[[0 (4 3 2 1 0)]]]]] ^=( up-zero :test (^=(+0)) ([[[[0 3]]]]) :test (^=(+1)) ((+3)) :test (^=(+42)) ((+126)) # shifts a specified trit into a balanced ternary number up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]] :test (up trit-neg (+42)) (^<(+42)) :test (up trit-pos (+42)) (^>(+42)) :test (up trit-zero (+42)) (^=(+42)) # shifts the least significant trit out - basically div by 3 down [snd (0 z neg pos zero)] z pair (+0) (+0) neg [0 [[pair (^<1) 1]]] pos [0 [[pair (^>1) 1]]] zero [0 [[pair (^=1) 1]]] # negates a balanced ternary number negate [[[[[4 3 1 2 0]]]]] -( negate :test (-(+0)) ((+0)) :test (-(-1)) ((+1)) :test (-(+42)) ((-42)) # converts a balanced ternary number to a list of trits list! [0 z neg pos zero] z F neg [[pair trit-neg 1]] pos [[pair trit-pos 1]] zero [[pair trit-zero 1]] # TODO: Tests! # strips leading 0s from balanced ternary number strip [fst (0 z neg pos zero)] z pair (+0) T neg [0 [[pair (^<1) F]]] pos [0 [[pair (^>1) F]]] zero [0 [[pair (0 (+0) (^=1)) 0]]] ~( strip :test (~[[[[0 3]]]]) ((+0)) :test (~[[[[2 (0 (0 (0 (0 3))))]]]]) ((-1)) :test (~(+42)) ((+42)) # 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) # extracts most significant trit from balanced ternary numbers # TODO: Find a more elegant way to do this # mst [fix (List.last (list! (strip 0)))] # fix [if (or (trit-neg? 0) (or (trit-pos? 0) (trit-zero? 0))) 0 [[0]]] # TODO: Fix list import loop mst [trit-zero] :test (mst (+0)) (trit-zero) :test (mst (-1)) (trit-neg) :test (mst (+1)) (trit-pos) :test (mst (+42)) (trit-pos) # returns whether balanced ternary number is negative negative? [trit-neg? (mst 0)] ?( positive? :test (>?(+0)) (F) :test (>?(-1)) (F) :test (>?(+1)) (T) :test (>?(+42)) (T) # checks whether balanced ternary number is zero zero? [0 T [F] [F] I] =?( zero? :test (=?(+0)) (T) :test (=?(-1)) (F) :test (=?(+1)) (F) :test (=?(+42)) (F) # converts the normal balanced ternary representation into abstract # -> the abstract representation is used in add/sub/mul abstract! [0 z neg pos zero] z (+0) neg [[[[[2 4]]]]] pos [[[[[1 4]]]]] zero [[[[[0 4]]]]] :test (abstract! (-3)) ([[[[0 [[[[2 [[[[3]]]]]]]]]]]]) :test (abstract! (+0)) ([[[[3]]]]) :test (abstract! (+3)) ([[[[0 [[[[1 [[[[3]]]]]]]]]]]]) # converts the abstracted balanced ternary representation back to normal # using ω to solve recursion normal! ω rec rec [[0 (+0) [^<([3 3 0] 0)] [^>([3 3 0] 0)] [^=([3 3 0] 0)]]] :test (normal! [[[[3]]]]) ((+0)) :test (normal! (abstract! (+42))) ((+42)) :test (normal! (abstract! (-42))) ((-42)) # checks whether two balanced ternary numbers are equal # -> ignores leading 0s! eq? [[abs 1 (abstract! 0)]] z [zero? (normal! 0)] neg [[0 F [2 0] [F] [F]]] pos [[0 F [F] [2 0] [F]]] zero [[0 (1 0) [F] [F] [2 0]]] abs [0 z neg pos zero] (=?) eq? :test ((-42) =? (-42)) (T) :test ((-1) =? (-1)) (T) :test ((-1) =? (+0)) (F) :test ((+0) =? (+0)) (T) :test ((+1) =? (+0)) (F) :test ((+1) =? (+1)) (T) :test ((+42) =? (+42)) (T) :test ([[[[(1 (0 (0 (0 (0 3)))))]]]] =? (+1)) (T) # I believe Mogensen's Paper has an error in its inc/dec/add/mul/eq definitions. # They use 3 instead of 2 abstractions in the functions, also we use switched # +/0 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) inc [snd (0 z neg pos zero)] z pair (+0) (+1) neg [0 [[pair (^<1) (^=1)]]] zero [0 [[pair (^=1) (^>1)]]] pos [0 [[pair (^>1) (^<0)]]] ++( inc # adds (+1) to a balanced ternary number and strips leading 0s ssinc [~(++0)] :test ((++(-42)) =? (-41)) (T) :test ((++(-1)) =? (+0)) (T) :test ((++(+0)) =? (+1)) (T) :test ((++(++(++(++(++(+0)))))) =? (+5)) (T) :test ((++(+42)) =? (+43)) (T) # subs (+1) from a balanced ternary number (can introduce leading 0s) dec [snd (0 dec-z dec-neg dec-pos dec-zero)] dec-z pair (+0) (-1) dec-neg [0 [[pair (^<1) (^>0)]]] dec-zero [0 [[pair (^=1) (^<1)]]] dec-pos [0 [[pair (^>1) (^=1)]]] --( dec # subs (+1) from a balanced ternary number and strips leading 0s ssub [~(--0)] :test ((--(-42)) =? (-43)) (T) :test ((--(+0)) =? (-1)) (T) :test ((--(--(--(--(--(+5)))))) =? (+0)) (T) :test ((--(+1)) =? (+0)) (T) :test ((--(+42)) =? (+41)) (T) # adds two balanced ternary numbers (can introduce leading 0s) add [[abs 1 (abstract! 0)]] c [[1 0 trit-zero]] b-neg2 [1 (^=(3 0 trit-neg)) (^<(3 0 trit-zero)) (^>(3 0 trit-neg))] b-neg [1 (^>(3 0 trit-neg)) (^=(3 0 trit-zero)) (^<(3 0 trit-zero))] b-zero [up 1 (3 0 trit-zero)] b-pos [1 (^=(3 0 trit-zero)) (^<(3 0 trit-pos)) (^>(3 0 trit-zero))] b-pos2 [1 (^>(3 0 trit-zero)) (^=(3 0 trit-pos)) (^<(3 0 trit-pos))] a-neg [[[1 (b-neg 1) b-neg2 b-zero b-neg]]] a-pos [[[1 (b-pos 1) b-zero b-pos2 b-pos]]] a-zero [[[1 (b-zero 1) b-neg b-pos b-zero]]] z [[0 (--(normal! 1)) (++(normal! 1)) (normal! 1)]] abs [c (0 z a-neg a-pos a-zero)] (+) add # adds two balanced ternary numbers and strips leading 0s sadd [[~(1 + 0)]] :test (((-42) + (-1)) =? (-43)) (T) :test (((-5) + (+6)) =? (+1)) (T) :test (((-1) + (+0)) =? (-1)) (T) :test (((+0) + (+0)) =? (+0)) (T) :test (((+1) + (+2)) =? (+3)) (T) :test (((+42) + (+1)) =? (+43)) (T) # subs two balanced ternary numbers (can introduce leading 0s) sub [[1 + -0]] (-) sub # subs two balanced ternary numbers and strips leading 0s ssub [[~(1 - 0)]] :test (((-42) - (-1)) =? (-41)) (T) :test (((-5) - (+6)) =? (-11)) (T) :test (((-1) - (+0)) =? (-1)) (T) :test (((+0) - (+0)) =? (+0)) (T) :test (((+1) - (+2)) =? (-1)) (T) :test (((+42) - (+1)) =? (+41)) (T) # returns whether number is greater than other number gre? [[negative? (sub 0 1)]] (>?) gre? # returns whether number is less than or equal to other number leq? [[not (gre? 1 0)]] (<=?) leq? # muls two balanced ternary numbers (can introduce leading 0s) mul [[1 (+0) neg pos zero]] neg [(^=0) - 1] pos [(^=0) + 1] zero [^=0] (*) mul smul [[strip (mul 1 0)]] :test (((+42) * (+0)) =? (+0)) (T) :test (((-1) * (+42)) =? (-42)) (T) :test (((+3) * (+11)) =? (+33)) (T) :test (((+42) * (-4)) =? (-168)) (T)