# ================== # Common combinators # ================== S [[[2 0 (1 0)]]] K [[1]] I [0] B [[[2 (1 0)]]] C [[[2 0 1]]] T [[1]] F [[0]] ω [0 0] Ω ω ω 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 # ===== pair [[[0 2 1]]] 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]] # # _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 # =============== not [0 F T] and [[1 0 F]] or [[1 T 0]] xor [[1 (not 0) 0]] if [[[2 1 0]]] # =============== # Church numerals # =============== churchZero [[0]] churchSucc [[[1 (2 1 0)]]] churchAdd [[[[3 1 (2 1 0)]]]] churchMul [[[2 (1 0)]]] churchExp [[0 1]] main [[[0 2 1]]]