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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186

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

:test fst (pair [[0]] [[1]]) = [[0]]
:test snd (pair [[0]] [[1]]) = [[1]]

# TODO: contract-like type-checking
#       like: `+ ... : [[[[# 3]]]]`

# ===================================
# Ternary
# According to works of T.Æ. Mogensen
# ===================================

zero? [0 T [F] [F] I]
:test zero? +0 = T
:test zero? -1 = F
:test zero? +1 = F
:test zero? +42 = F

upNeg [[[[[2 (4 3 2 1 0)]]]]]
:test upNeg +0 = -1
:test upNeg -1 = -4
:test upNeg +42 = +125

upPos [[[[[1 (4 3 2 1 0)]]]]]
:test upPos +0 = +1
:test upPos -1 = -2
:test upPos +42 = +127

upZero [[[[[0 (4 3 2 1 0)]]]]]
:test upZero +0 = [[[[0 3]]]]
:test upZero +1 = +3
:test upZero +42 = +126

up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
# TODO: up is incorrect

negate [[[[[4 3 1 2 0]]]]]
:test negate +0 = +0
:test negate -1 = +1
:test negate +42 = -42

tritNeg [[[2]]]
tritPos [[[1]]]
tritZero [[[0]]]
lst [0 tritZero [tritNeg] [tritPos] [tritZero]]
:test lst +0 = tritZero
:test lst -1 = tritNeg
:test lst +1 = tritPos
:test lst +42 = tritZero

_stripZ pair +0 T
_stripANeg [0 [[pair (upNeg 1) F]]]
_stripAPos [0 [[pair (upPos 1) F]]]
_stripAZero [0 [[pair (0 +0 (upZero 1)) 0]]]
strip [fst (0 _stripZ _stripANeg _stripAPos _stripAZero)]
:test strip [[[[0 3]]]] = +0
:test strip [[[[2 (0 (0 (0 (0 3))))]]]] = -1
:test strip +42 = +42

# I believe Mogensen's Paper has an error in its succ/pred definitions.
# They use 3 abstractions in the _succ* functions, also we use switched +/0
# in comparison to their implementation, yet the order of neg/pos/zero is
# the same. Something's weird.

_succZ pair +0 +1
_succNeg [0 [[pair (upNeg 1) (upZero 1)]]]
_succZero [0 [[pair (upZero 1) (upPos 1)]]]
_succPos [0 [[pair (upPos 1) (upNeg 0)]]]
succ [snd (0 _succZ _succNeg _succPos _succZero)]
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

_predZ pair +0 -1
_predNeg [0 [[pair (upNeg 1) (upPos 0)]]]
_predZero [0 [[pair (upZero 1) (upNeg 1)]]]
_predPos [0 [[pair (upPos 1) (upZero 1)]]]
pred [snd (0 _predZ _predNeg _predPos _predZero)]
spred [strip (pred 0)]
:test pred -42 = -43
:test pred +0 = -1
:test spred (pred (pred (pred (pred +5)))) = +0
:test spred +1 = +0
:test pred +42 = +41

_absNeg [[[[[2 4]]]]]
_absPos [[[[[1 4]]]]]
_absZero [[[[[0 4]]]]]
abstractify [0 [[[[3]]]] _absNeg _absPos _absZero]
:test abstractify -3 = [[[[0 [[[[2 [[[[3]]]]]]]]]]]]
:test abstractify +0 = [[[[3]]]]
:test abstractify +3 = [[[[0 [[[[1 [[[[3]]]]]]]]]]]]

# solving recursion using Y/ω
_normalize [[0 +0 [upNeg ([3 3 0] 0)] [upPos ([3 3 0] 0)] [upZero ([3 3 0] 0)]]]
normalize ω _normalize
:test normalize [[[[3]]]] = +0
:test normalize (abstractify +42) = +42
:test normalize (abstractify -42) = -42

_eqZ [zero? (normalize 0)]
_eqNeg [[0 F [2 0] [F] [F]]]
_eqPos [[0 F [F] [2 0] [F]]]
_eqZero [[0 (1 0) [F] [F] [2 0]]]
_eqAbs [0 _eqZ _eqNeg _eqPos _eqZero]
eq [[_eqAbs 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
_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]]]