std.bruijn


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106

# ==================
# 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]

# =====
# Pairs
# =====

pair [[[0 2 1]]]
fst [0 T]
snd [0 F]

# ===================================
# 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)]]

# ===============
# 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 I F