docs/misc/words.txt

   1 Some notes on definitions.
   2
   3 Let's work out the definition of the step combinator in Joy:
   4
   5        [] [P] step
   6     -----------------
   7
   8
   9          [X|Xs] [P] step
  10     -----------------------
  11        X P [Xs] [P] step
  12
  13 In terms of branch and x:
  14
  15      step == [F] x
  16
  17 So:
  18
  19         [L] [P] step
  20      ------------------
  21         [L] [P] [F] x
  22      ------------------
  23         [L] [P] [F] F
  24
  25 First, get the flag value and roll< it to the top for a branch:
  26
  27      F  == F′ F″
  28      F′ == [?] dipd roll<
  29
  30         [L] [P] [F] F
  31      ---------------------------
  32         [L] [P] [F′ F″] F′ F″
  33      ---------------------------------------
  34         [L] [P] [F′ F″] [?] dipd roll< F″
  35
  36 How that works out:
  37
  38      [L]   [P] [F] [?] dipd roll< F″
  39      [L] ? [P] [F]          roll< F″
  40      [L] b [P] [F]          roll< F″
  41      [L]   [P] [F] b              F″
  42
  43 Now we can write a branch:
  44
  45      F″ == [Ff] [Ft] branch
  46
  47         [L] [P] [F] b F″
  48      ------------------------------------
  49         [L] [P] [F] b [Ff] [Ft] branch
  50
  51 The false case is easy:
  52
  53      Ff == pop popop
  54
  55      ... [] [P] [F] Ff
  56      ... [] [P] [F] pop popop
  57      ... [] [P]         popop
  58      ...
  59
  60
  61 The true case is a little more fun:
  62
  63      ... [X|Xs] [P] [F] Ft
  64
  65 We need to uncons that first term, run a copy of P, and recur (recurse?
  66 I think re-curse means to "curse again" so it must be "recur".)
  67
  68      Ft == Ft′ Ft″
  69      Ft′ == [uncons] dipd
  70
  71      ... [X|Xs]        [P] [F] [uncons] dipd Ft″
  72      ... [X|Xs] uncons [P] [F]               Ft″
  73      ... X [Xs]        [P] [F]               Ft″
  74
  75 So now we run a copy of P:
  76
  77      ... X [Xs] [P] [F] Ft″
  78
  79      Ft″ == [dup dipd] dip Ft‴
  80
  81      ... X   [Xs] [P]          [F] Ft″
  82      ... X   [Xs] [P]          [F] [dup dipd] dip Ft‴
  83      ... X   [Xs] [P] dup dipd [F] Ft‴
  84      ... X   [Xs] [P] [P] dipd [F] Ft‴
  85      ... X P [Xs] [P]          [F] Ft‴
  86
  87 And now all that remains is to recur on F:
  88
  89      Ft‴ == x
  90
  91      ... X P [Xs] [P] [F] x
  92
  93
  94 Collecting the definitions, we have:
  95
  96      step == [F] x
  97        F  == F′ [Ff] [Ft] branch
  98        F′ == [?] dipd roll<
  99        Ff == pop popop
 100        Ft == Ft′ Ft″ x
 101       Ft′ == [uncons] dipd
 102       Ft″ == [dup dipd] dip
 103
 104
 105 QED.
 106
 107 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
 108
 109        x [P] dupdip
 110     ------------------
 111          x P x
 112
 113
 114     x     [P] [dup] dip dip
 115     x dup [P]           dip
 116     x x   [P]           dip
 117
 118
 119     dupdip [dup] dip dip
 120
 121
 122 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
 123
 124
 125 3 true [-- [0 >] nullary] loop
 126
 127 5 [1 <] [] [dup --] [i +] genrec
 128
 129 ′ ″ ‴ ⁗
 130
 131 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
 132
 133 map
 134      in terms of genrec:
 135
 136                     [F] map
 137      -------------------------------------
 138         [] [P] [E] [[F] R0] [R1] genrec
 139      -------------------------------------  w/ K == [P] [E] [[F] R0] [R1] genrec
 140         [] [P] [E] [[F] R0 [K] R1] ifte
 141
 142
 143 P is applied nullary so it will just be:
 144
 145      P == pop bool
 146
 147 to check the non-emptiness of the input list.  When the input list is
 148 empty, the output list is ready, but in the reverse order, so:
 149
 150      E == popd reverse
 151
 152 That leaves the non-empty case:
 153
 154     [X|Xs] [Ys] [F] R0 [K] R1
 155
 156 Here we want to uncons that X term, prepend it to a copy of the stack for
 157 using infra on F, put the result on [Ys], and recur.
 158
 159 Let's keep it simple:
 160
 161     R0 == [R0′] dipd R0″
 162
 163     [X|Xs]     [Ys] [F] [R0′] dipd R0″ [K] R1
 164     [X|Xs] R0′ [Ys] [F]            R0″ [K] R1
 165
 166 Let's concentrate on R0′:
 167
 168     R0′ == [stack] dip shift
 169
 170     ... [X|Xs] R0′
 171     ... [X|Xs] [stack] dip shift
 172     ... [...] [X|Xs] shift
 173     ... [X|...] [Xs]
 174
 175 okay, so:
 176
 177     ... [X|...] [Xs] [Ys] [F] R0″ [K] R1
 178
 179 We want to use F on that stack we just made:
 180
 181     R0″ == [infra first] cons dipd R0‴
 182
 183     ... [X|...]                 [Xs] [Ys] [F] R0″                     R0‴ [K] R1
 184     ... [X|...]                 [Xs] [Ys] [F] [infra first] cons dipd R0‴ [K] R1
 185     ... [X|...]                 [Xs] [Ys] [[F] infra first]      dipd R0‴ [K] R1
 186     ... [X|...] [F] infra first [Xs] [Ys]                             R0‴ [K] R1
 187     ... [Y|...]           first [Xs] [Ys]                             R0‴ [K] R1
 188     ...  Y                      [Xs] [Ys]                             R0‴ [K] R1
 189
 190 And:
 191
 192     R0‴ == roll< swons
 193
 194     ... Y [Xs] [Ys] R0‴         [K] R1
 195     ... Y [Xs] [Ys] roll< swons [K] R1
 196     ... [Xs] [Ys] Y       swons [K] R1
 197     ... [Xs] [Y|Ys]             [K] R1
 198
 199 That just leaves R1:
 200
 201     R1 == i
 202
 203     ... [Xs] [Y|Ys] [K] R1
 204     ... [Xs] [Y|Ys] [K] i
 205     ... [Xs] [Y|Ys]  K
 206     ... [Xs] [Y|Ys] [P] [E] [[F] R0] [R1] genrec
 207
 208 ::
 209
 210
 211       P == pop bool
 212       E == popd reverse
 213      R0 == [R0′] dipd R0″
 214     R0′ == [stack] dip shift
 215     R0″ == [infra first] cons dipd R0‴
 216     R0‴ == roll< swons
 217      R1 == i
 218
 219 Now that we have the parts, we need to make the map combinator that takes
 220 [F] and builds the genrec function:
 221
 222                     [F] map
 223      -------------------------------------
 224         [] [P] [E] [[F] R0] [R1] genrec
 225
 226 Working backwards:
 227
 228     [] [P] [E] [[F] R0]                       [R1] genrec
 229                [[F] R0]      [[] [P] [E]] dip [R1] genrec
 230                [F] [R0] cons [[] [P] [E]] dip [R1] genrec
 231
 232 Ergo:
 233
 234     map == [R0] cons [[] [P] [E]] dip [R1] genrec
 235
 236 So the source would be:
 237
 238     map [_map0] cons [[] [_map?] [_mape]] dip [i] genrec
 239     _map? pop bool
 240     _mape popd reverse
 241     _map0 [_map1] dipd _map2
 242     _map1 [stack] dip shift
 243     _map2 [infra first] cons dipd _map3
 244     _map3 roll< swons
 245
 246
 247 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
 248
 249 Minimal Basis
 250 ----------------
 251
 252 This is a tight set of primitives from the POV of implementation.  You
 253 can get nice performance improvements by implementing some additional
 254 words (like uncons and rest) but these along with the defs.txt file are
 255 good to go:
 256
 257 and bool branch concat cons dip dup first i loop or pop stack swaack swap
 258 + - * / % < > = >= <= <>
 259
 260
 261 Integer Math
 262 ----------------
 263 + - * / %
 264
 265
 266 Binary Boolean Logic
 267 ----------------
 268 < > = >= <= <>
 269 and or bool
 270
 271
 272 Stack Manipulation
 273 ----------------
 274 dup pop stack swaack swap
 275
 276
 277 Combinators
 278 ----------------
 279 branch loop i dip
 280
 281
 282 List Manipulation
 283 ----------------
 284 concat cons first
 285
 286