on 01ac191 help sign in
1045 lines 30 kB history raw
1---
2sort: 2
3next: true
4title: Tutorial
5---
7# Nock tutorial
9So let's learn Nock! But wait - why learn Nock? After all,
10we're going to be programming in Hoon, not Nock.
12Like JVM bytecode, Nock is as inscrutable as assembly language.
13In fact, you can think of it as a sort of "functional assembly
14language." There are sometimes reasons to program in real
15assembly language. There is never a reason to program in Nock.
16Except to learn Nock.
18Indeed, it is not necessary for the Hoon programmer to learn
19Nock. We recommend it strongly, however, because Hoon has a very
20special relationship with Nock - not unlike the relationship
21between C and assembly language.
23Just as C is a very shallow layer over the raw CPU, Hoon is a
24very shallow layer over raw Nock - often little more than a
25macro. If you try to learn C without understanding the CPU under
26it, you will be forever bemused by why it works the way it does.
28So let's learn Nock! But wait - which Nock? Nock, though more
29frozen than Walt Disney, does have versions. Nock versions are
30measured by integer degrees Kelvin, newer being colder. The
31newest, Nock 5K - roughly the temperature of Neptune. No change
32is anticipated between 5K and absolute zero, though you never
33know. Any such change would certainly be quite painful.
35#1.1 Definition#
37The best way to learn Nock is to read the spec and write your own
38naive interpreter. Here is Nock 5K:
40**1. Structures**
42 A noun is an atom or a cell. An atom is a natural number.
43 A cell is an ordered pair of nouns.
45**2. Pseudocode**
47 1 :: nock(a) *a
48 2 :: [a b c] [a [b c]]
49 3 ::
50 4 :: ?[a b] 0
51 5 :: ?a 1
52 6 :: +[a b] +[a b]
53 7 :: +a 1 + a
54 8 :: =[a a] 0
55 9 :: =[a b] 1
56 10 :: =a =a
57 11 ::
58 12 :: /[1 a] a
59 13 :: /[2 [a b]] a
60 14 :: /[3 [a b]] b
61 15 :: /[(a + a) b] /[2 /[a b]]
62 16 :: /[(a + a + 1) b] /[3 /[a b]]
63 17 :: /a /a
64 18 ::
65 19 :: *[a [[b c] d]] [*[a [b c]] *[a d]]
66 20 ::
67 21 :: *[a [0 b]] /[b a]
68 22 :: *[a [1 b]] b
69 23 :: *[a [2 [b c]]] *[*[a b] *[a c]]
70 24 :: *[a [3 b]] ?*[a b]
71 25 :: *[a [4 b]] +*[a b]
72 26 :: *[a [5 b]] =*[a b]
73 27 ::
74 28 :: *[a [6 [b [c d]]]] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
75 29 :: *[a [7 [b c]]] *[a 2 b 1 c]
76 30 :: *[a [8 [b c]]] *[a 7 [[7 [0 1] b] 0 1] c]
77 31 :: *[a [9 [b c]]] *[a 7 c 2 [0 1] 0 b]
78 32 :: *[a [10 [[b c] d]]] *[a 8 c 7 [0 3] d]
79 33 :: *[a [10 [b c]]] *[a c]
80 34 ::
81 35 :: *a *a
83Your interpreter should be no more than a page of code in
84any language. For extra credit, `6`-`10` are macros; implement
85them directly. For extra extra credit, optimize tail calls.
86To test your code, write a decrement formula b such that
87`*[a b]` is `a - 1` for any atomic nonzero `a`.
89#1.2 Installation#
91The second best way to learn Nock is to boot up your own Arvo
92virtual computer. See the Arvo tutorial for instructions.
94#1.3 Nock#
96To make Nock make sense, let's work through Nock 5K line by line.
97First the data model:
99##1. Structures##
101 A noun is an atom or a cell. An atom is any natural number.
102 A cell is any ordered pair of nouns.
104Nouns are the dumbest data model ever. Nouns make JSON look like
105XML and XML look like ASN.1. It may also remind you of Lisp's
106S-expressions - you can think of nouns as "S-expressions without
107the S."
109To be exact, a noun _is_ an S-expression, except that classic
110S-expressions have multiple atom types ("S" is for "symbol").
111Since Nock is designed to be used with a higher-level type system
112(such as Hoon's), it does not need low-level types. An atom is
113just an unsigned integer of any size.
115For instance, it's common to represent strings (or even whole
116text files) as atoms, arranging them LSB first - so "foo" becomes
117`0x6f6f66`. How do we know to print this as "foo", not `0x6f6f66`?
118We need external information - such as a Hoon type. Similarly,
119other common atomic types - signed integers, floating point, etc
120- are all straightforward to map into atoms.
122It's also important to note that, unlike Lisp, Nock cannot create
123cyclical data structures. It is normal and common for nouns in a
124Nock runtime system to have acyclic structure - shared subtrees.
125But there is no Nock computation that can make a child point to
126its parent. One consequence: Nock has no garbage collector.
127(Nor can dag structure be detected, as with Lisp `eq`.)
129There is also no single syntax for nouns. If you have nouns you
130have Nock; if you have Nock you have Hoon; if you have Hoon, you
131can write whatever parser you like.
133Let's continue:
135##2. Pseudocode##
137It's important to recognize that the pseudocode of the Nock spec
138is just that: pseudocode. It looks a little like Hoon. It isn't
139Hoon - it's just pseudocode. Or in other words, just English.
140At the bottom of every formal system is a system of axioms, which
141can only be written in English. (Why pseudocode, not Hoon? Since
142Hoon is defined in Nock, this would only give a false impression
143of nonexistent precision.)
145The logic of this pseudocode is a pattern-matching reduction,
146matching from the top down. To compute Nock, repeatedly reduce
147with the first line that matches. Let's jump right in!
149##Line 1:##
151 1 :: nock(a) *a
153Nock is a pure (stateless) function from noun to noun. In our
154pseudocode (and only in our pseudocode) we express this with the
155prefix operator `*`.
157This function is defined for every noun, but on many nouns it
158does nothing useful. For instance, if `a` is an atom, `*a`
159reduces to... `*a`. In theory, this means that Nock spins
160forever in an infinite loop. In other words, Nock produces no
161result - and in practice, your interpreter will stop.
163(Another way to see this is that Nock has "crash-only" semantics.
164There is no exception mechanism. The only way to catch Nock
165errors is to simulate Nock in a higher-level virtual Nock -
166which, in fact, we do all the time. A simulator (or a practical
167low-level interpreter) can report, out of band, that Nock would
168not terminate. It cannot recognize all infinite loops, of
169course, but it can catch the obvious ones - like `*42`.)
171Normally `a` in `nock(a)` is a cell `[s f]`, or as we say
173 [subject formula]
175Intuitively, the formula is your function and the subject is
176its argument. We call them something different because Hoon,
177or any other high-level language built on Nock, will build its
178own function calling convention which *does not* map directly
179to `*[subject formula]`.
181##Line 2:##
183 2 :: [a b c] [a [b c]]
185Ie, brackets (in our pseudocode, as in Hoon) associate to the
186right. For those with Lisp experience, it's important to note
187that Nock and Hoon use tuples or "improper lists" much more
188heavily than Lisp. The list terminator, normally 0, is never
189automatic. So the Lisp list
191 (a b c)
193becomes the Nock noun
195 [a b c 0]
197which is equivalent to
199 [a [b [c 0]]]
201Note that we can and do use unnecessary brackets anyway, for
202emphasis.
204Let's move on to the axiomatic functions.
206##Lines 4-10:##
208 4 :: ?[a b] 0
209 5 :: ?a 1
210 6 :: +[a b] +[a b]
211 7 :: +a 1 + a
212 8 :: =[a a] 0
213 9 :: =[a b] 1
215Here we define more pseudocode operators, which we'll use in
216reductions further down. So far we have four built-in functions:
217`*` meaning Nock itself, `?` testing whether a noun is a cell or
218an atom, `+` incrementing an atom, and `=` testing for equality.
219Again, no rocket science here.
221We should note that in Nock and Hoon, `0` (pronounced "yes") is
222true, and `1` ("no") is false. Why? It's fresh, it's different,
223it's new. And it's annoying. And it keeps you on your toes.
224And it's also just intuitively right.
227##Lines 12-16:##
229 12 :: /[1 a] a
230 13 :: /[2 a b] a
231 14 :: /[3 a b] b
232 15 :: /[(a + a) b] /[2 /[a b]]
233 16 :: /[(a + a + 1) b] /[3 /[a b]]
235Slightly more interesting is our tree numbering. Every noun is of course a tree. The `/` operator - pronounced
236"slot" - imposes an address space on that tree, mapping every
237nonzero atom to a tree position.
2391 is the root. The head of every node `n` is `2n`; the tail is
240`2n+1`. Thus a simple tree:
242 1
243 2 3
244 4 5 6 7
245 14 15
247If the value of every leaf is its tree address, this tree is
249 [[4 5] [6 14 15]]
251and, for some examples of addressing:
253 /[1 [[4 5] [6 14 15]]]
255is `[[4 5] [6 14 15]]`
257 /[2 [[4 5] [6 14 15]]]
259is `[4 5]`
261 /[3 [[4 5] [6 14 15]]]
263is `[6 14 15]`, and
265 /[7 [[4 5] [6 14 15]]]
267is `[14 15]`
269I do hope this isn't so terribly hard to follow.
271##Line 21:##
273Now we enter the definition of Nock itself - ie, the `*`
274operator.
276 21 :: *[a 0 b] /[b a]
278`0` is simply Nock's tree-addressing operator. Let's try it out
279from the Arvo command line.
281Note that we're using Hoon syntax here. Since we do not use Nock
282from Hoon all that often (it's sort of like embedding assembly in
283C), we've left it a little cumbersome. In Hoon, instead of
284writing `*[a 0 b]`, we write
286 .*(a [0 b])
288So, to reuse our slot example, let's try the interpreter:
290 ~tasfyn-partyv> .*([[4 5] [6 14 15]] [0 7])
292gives, while the sky remains blue and the sun rises in the east:
294 [14 15]
296Even stupider is line 21:
298##Line 21:##
300 21 :: *[a 1 b] b
302`1` is the constant operator. It produces its argument without
303reference to the subject. So
305 ~tasfyn-partyv> .*(42 [1 153 218])
307yields
309 [153 218]
312##Line 23:##
314 23 :: *[a 2 b c] *[*[a b] *[a c]]
316Line 22 brings us the essential magic of recursion.
317`2` is the Nock operator. If you can compute a subject and a
318formula, you can evaluate them in the interpreter. In most
319fundamental languages, like Lisp, `eval` is a curiosity. But
320Nock has no `apply` - so all our work gets done with `2`.
322Let's convert the previous example into a stupid use of `2`:
324 ~tasfyn-partyv> .*(77 [2 [1 42] [1 1 153 218]])
326with a constant subject and a constant formula, gives the same
328 [153 218]
330Like so:
332 *[77 [2 [1 42] [1 1 153 218]]]
334 22 :: *[a 2 b c] *[*[a b] *[a c]]
336 *[*[77 [1 42]] *[77 [1 1 153 218]]]
338 21 :: *[a 1 b] b
340 *[42 *[77 [1 1 153 218]]]
342 *[42 1 153 218]
344 [153 218]
346##Lines 24-26:##
348 24 :: *[a 3 b] ?*[a b]
349 25 :: *[a 4 b] +*[a b]
350 26 :: *[a 5 b] =*[a b]
352In lines 23-25, we meet our axiomatic functions again:
354For instance, if `x` is a formula that calculates some product,
355`[4 x]` calculates that product plus one. Hence:
357 ~tasfyn-partyv> .*(57 [0 1])
358 57
360and
362 ~tasfyn-partyv> .*([132 19] [0 3])
363 19
365and
367 ~tasfyn-partyv> .*(57 [4 0 1])
368 58
370and
372 ~tasfyn-partyv> .*([132 19] [4 0 3])
373 20
375If this seems obvious, you're doin' good. Finally, we jump back up
376to line 18, the trickiest in the spec:
378##Line 19:##
380 19 :: *[a [b c] d] [*[a b c] *[a d]]
382Um, what?
384Since Nock of an atom just crashes, the practical domain of the
385Nock function is always a cell. Conventionally, the head of this
386cell is the "subject," the tail is the "formula," and the result
387of Nocking it is the "product." Basically, the subject is your
388data and the formula is your code.
390We could write line 19 less formally:
392 *[subject [formula-x formula-y]]
393 => [*[subject formula-x] *[subject formula-y]]
395In other words, if you have two Nock formulas `x` and `y`, a
396formula that computes the pair of them is just `[x y]`. We can
397recognize this because no atom is a valid formula, and
398every formula that _does not_ use line 19 has an atomic head.
400If you know Lisp, you can think of this feature as a sort of
401"implicit cons." Where in Lisp you would write `(cons x y)`,
402in Nock you write `[x y]`.
404For example,
406 ~tasfyn-partyv> .*(42 [4 0 1])
408where `42` is the subject (data) and `[4 0 1]` is the formula
409(code), happens to evaluate to `43`. Whereas
411 ~tasfyn-partyv> .*(42 [3 0 1])
413is `1`. So if we evaluate
415 ~tasfyn-partyv> .*(42 [[4 0 1] [3 0 1]])
417we get
419 [43 1]
421Except for the crash defaults (lines 6, 10, 17, and 35), we've actually
422completed all the _essential_ aspects of Nock. The operators up
423through 5 provide all necessary computational functionality.
424Nock, though very simple, is actually much more complex than it
425formally needs to be.
427Operators 6 through 10 are macros. They exist because Nock is
428not a toy, but a practical interpreter. Let's see them all
429together:
431##Lines 28-33:##
433 28 :: *[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
434 29 :: *[a 7 b c] *[a 2 b 1 c]
435 30 :: *[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
436 31 :: *[a 9 b c] *[a 7 c 2 [0 1] 0 b]
437 32 :: *[a 10 [b c] d] *[a 8 c 7 [0 3] d]
438 33 :: *[a 10 b c] *[a c]
440Whoa! Have we entered rocket-science territory? Let's try to
441figure out what these strange formulas do - simplest first.
442The simplest is clearly line 33:
444 33 :: *[a 10 b c] *[a c]
446If `x` is an atom and `y` is a formula, the formula `[10 x y]`
447appears to be equivalent to... `y`. For instance:
449 ~tasfyn-partyv> .*([132 19] [10 37 [4 0 3]])
450 20
452Why would we want to do this? `10` is actually a hint operator.
453The `37` in this example is discarded information - it is not
454used, formally, in the computation. It may help the interpreter
455compute the expression more efficiently, however.
457Every Nock computes the same result - but not all at the same
458speed. What hints are supported? What do they do? Hints are a
459higher-level convention which do not, and should not, appear in
460the Nock spec. Some are defined in Hoon. Indeed, a naive Nock
461interpreter not optimized for Hoon will run Hoon quite poorly.
462When it gets the product, however, the product will be right.
464There is another reduction for hints - line 32:
466 32 :: *[a 10 [b c] d] *[a 8 c 7 [0 3] d]
468Once we see what `7` and `8` do, we'll see that this complex hint
469throws away an arbitrary `b`, but computes the formula `c`
470against the subject and... throws away the product. This formula
471is simply equivalent to `d`. Of course, in practice the product
472of `c` will be put to some sordid and useful use. It could even
473wind up as a side effect, though we try not to get _that_ sordid.
475(Why do we even care that `c` is computed? Because `c` could
476crash. A correct Nock cannot simply ignore it, and treat both
477variants of `10` as equivalent.)
479We move on to the next simplest operator, `7`. Line 29:
481 29 :: *[a 7 b c] *[a 2 b 1 c]
483Suppose we have two formulas, `b` and `c`. What is the formula
484`[7 b c]`? This example will show you:
486 ~tasfyn-partyv> .*(42 [7 [4 0 1] [4 0 1]])
487 44
489`7` is an old mathematical friend, function composition. It's
490easy to see how this is built out of `2`. The data to evaluate
491is simply `b`, and the formula is `c` quoted.
493Line 30 looks very similar:
495 30 :: *[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
497Indeed, `8` is `7`, except that the subject for `c` is not simply
498the product of `b`, but the ordered pair of the product of `b`
499and the original subject. Hence:
501 ~tasfyn-partyv> .*(42 [8 [4 0 1] [0 1]])
502 [43 42]
504and
506 ~tasfyn-partyv> .*(42 [8 [4 0 1] [4 0 3]])
507 43
509Why would we want to do this? Imagine a higher-level language
510in which the programmer declares a variable. This language is
511likely to generate an `8`, because the variable is computed
512against the present subject, and used in a calculation which
513depends both on the original subject and the new variable.
515For extra credit, explain why we can't just define
517 *[a 8 b c] *[a 7 [b 0 1] c]
519Another simple macro is line 31:
521 31 :: *[a 9 b c] *[a 7 c 2 [0 1] 0 b]
523`9` is a calling convention. With `c`, we produce a noun which
524contains both code and data - a _core_. We use this core as the
525subject, and apply the formula within it at slot `b`.
527And finally, we come to the piece de resistance - line 28:
529 28 :: *[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
531Great giblets! WTF is this doing? It seems we've finally
532arrived at some real rocket science.
534Actually, `6` is a primitive known to every programmer - good old
535"if." If `b` evaluates to `0`, we produce `c`; if `b` evaluates
536to `1`, we produce `d`; otherwise, we crash.
538For instance:
540 ~tasfyn-partyv> .*(42 [6 [1 0] [4 0 1] [1 233]])
541 43
543and
545 ~tasfyn-partyv> .*(42 [6 [1 1] [4 0 1] [1 233]])
546 233
548In real life, of course, the Nock implementor knows that `6` is
549"if" and implements it as such. There is no practical sense in
550reducing through this macro, or any of the others. We could have
551defined "if" as a built-in function, like increment - except that
552we can write "if" as a macro. If a funky macro.
554It's a good exercise, however, to peek inside the funk.
556We can actually simplify the semantics of `6`, at the expense of
557breaking the system a little, by creating a macro that works as
558"if" only if `b` is a proper boolean and produces `0` or `1`.
559Perhaps we have a higher-level type system which checks this.
561This simpler "if" would be:
563 *[a 6 b c d] *[a [2 [0 1] [2 [1 c d] [[1 0] [4 4 b]]]]]
565Or without so many unnecessary brackets:
567 *[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] [4 4 b]]
569How does this work? We've replaced `[6 b c d]` with the formula
570`[2 [0 1] [2 [1 c d] [[1 0] [4 4 b]]]]`. We see two uses of `2`,
571our evaluation operator - an outer and an inner.
573Call the inner one `i`. So we have `[2 [0 1] i]`. Which means
574that, to calculate our product, we use `[0 1]` - that is, the
575original subject - as the subject; and the product of `i` as
576the formula.
578Okay, cool. So `i` is `[2 [1 c d] [[1 0] [4 4 b]]]`. We compute
579Nock with subject `[1 c d]`, formula `[[1 0] [4 4 b]]`.
581Obviously, `[1 c d]` produces just `[c d]` - that is, the ordered
582pair of the "then" and "else" formulas. `[[1 0] [4 4 b]]` is a
583line 19 cell - its head is `[1 0]`, producing just `0`, its tail
584`[4 4 b]`, producing... what? Well, if `[4 b]` is `b` plus `1`,
585`[4 4 b]` is `b` plus `2`.
587We're assuming that `b` produces either `0` or `1`. So `[4 4 b]`
588yields either `2` or `3`. `[[1 0] [4 4 b]]` is either `[0 2]` or
589`[0 3]`. Applied to the subject `[c d]`, this gives us either
590`c` or `d` - the product of our inner evaluation `i`. This is
591applied to the original subject, and the result is "if."
593But we need the full power of the funk, because if `b` produces,
594say, `7`, all kinds of weirdness will result. We'd really like
595`6` to just crash if the test product is not a boolean. How can
596we accomplish this? This is an excellent way to prove to
597yourself that you understand Nock: figure out what the real `6`
598does. Or you could just agree that `6` is "if," and move on.
600(It's worth noting that in practical, compiler-generated Nock, we
601never do anything as funky as these `6` macro internals. There's
602no reason we couldn't build formulas at runtime, but we have no
603reason to and we don't - except when actually metaprogramming.
604As in most languages, normally code is code and data is data.)
606#1.4 Decrement in Nock#
608A good practice exercise for Nock is a decrement formula. Ie, a
609formula `f` which implements the partial function that produces
610`(s - 1)` if `s` is a nonzero atom, and otherwise does not
611terminate.
613The normal Hoon programmer has written one Nock formula: this
614one. Since decrement uses all the Nock techniques the Hoon
615compiler uses, the exercise is a good foundation. After you
616write decrement (or just follow this example), you'll never need
617to deal with Nock again.
619As we know, the equivalent formula for increment is
621 [4 0 1]
623Thus:
625 ~>tasfyn-partyv .*(42 [4 0 1])
626 43
628Of course, increment is built into Nock. So, ha, that's easy.
630How do we decrement? A good way to start is to gaze fondly on
631how we'd do it if we actually had a real language, ie, Hoon.
632Here is a minimal decrement in Hoon:
634 => a=. :: line 1
635 =+ b=0 :: line 2
636 |- :: line 3
637 ?: =(a +(b)) :: line 4
638 b :: line 5
639 $(b +(b)) :: line 6
641Or for fun, on one line:
643 =>(a=. =+(b=0 |-(?:(=(a +(b)) b $(b +(b))))))
645Does Hoon actually work?
647 ~tasfyn-partyv> =>(42 =>(a=. =+(b=0 |-(?:(=(a +(b)) b $(b +(b)))))))
648 41
650Let's translate this into English. How do we decrement the
651subject? First (line 1), we rename the subject `a`. Second
652(line 2), we add a variable, `b`, an atom with value `0`.
653Third (line 3), we loop. Fourth, we test if `a` equals `b` plus
6541 (line 4), produce `b` if it does (line 5), repeat the loop with
655`b` set to `b` plus 1 (line 6) if it doesn't. Obviously, while
656the syntax is unusual, the algorithm is anything but deep. We
657are calculating `b` minus one by counting up from `0`.
659(Obviously, this is an O(n) algorithm. Is there a better way?
660There is not. Do we actually do this in practice? Yes and no.)
662Unfortunately we are missing a third of our Rosetta stone. We
663have decrement in Hoon and we have it in English. How do we
664express this in Nock? What will the Hoon compiler generate from
665the code above? Let's work through it line by line.
667Nock has no types, variable names, etc. So line 1 is a no-op.
669How do we add a variable (line 2)? We compute a new subject,
670which is a cell of the present subject and the variable. With
671this new subject, we execute another formula.
673Since `0` is a constant, a formula that produces it is
675 [1 0]
677To combine `0` with the subject, we compute
679 [[1 0] [0 1]]
681which, if our subject is 42, gives us
683 [0 42]
685which we can use as the subject for an inner formula, `g`.
686Composing our new variable with `g`, we have `f` as
688 [2 [[1 0] [0 1]] [1 g]]
690which seems a little funky for something so simple. But we
691can simplify it with the composition macro, `7`:
693 [7 [[1 0] [0 1]] g]
695and still further with the augmentation macro, `8`:
697 [8 [1 0] g]
699If you refer back to the Nock definition, you'll see that all
700these formulas are semantically equivalent.
702Let's continue with our decrement. So what's `g`? We seem to
703loop. Does Nock have a loop operator? It most certainly does
704not. So what do we do?
706We build a noun called a _core_ - a construct which is behind any
707kind of interesting control flow in Hoon. Of course, the Nock
708programmer is not constrained to use the same techniques as the
709Hoon compiler, but it is probably a good idea.
711In Hoon, all the flow structures from your old life as an Earth
712programmer become cores. Functions and/or closures are cores,
713objects are cores modules are cores, even loops are cores.
715The core is just a cell whose tail is data (possibly containing
716other cores) and whose head is code (containing one or more
717formulas). The tail is the _payload_ and the head is the
718_battery_. Hence your core is
720 [bat pay]
722To activate a core, pick a formula out of the battery, and use
723the entire core (_not_ just the payload) as the subject.
725(A core formula is called an _arm_. An arm is almost like an
726object-oriented method, but not quite - a method would be an arm
727that produces a function on an argument. The arm is just a
728function of the core, ie, a computed attribute.)
730Of course, because we feed it the entire core, our arm can
731invoke itself (or any other formula in the battery). Hence, it
732can loop. And this is what a loop is - the simplest of cores.
734We need to do two things with this core: create it, and activate
735it. To be precise, we need two formulas: a formula which
736produces the core, and one which activates its subject. We can
737compose these functions with the handy `7` operator:
739 [8 [1 0] [7 p a]]
741`p` produces our core, `a` activates it. Let's take these in
742reverse order. How do we activate a core?
744Since we have only one formula, it's the battery itself.
745Thus we want to execute Nock with the whole core (already the
746subject, and the entire battery (slot `2`). Hence, `a` is
748 [2 [0 1] [0 2]]
750We could also use the handy `9` macro - which almost seems
751designed for firing arms on cores:
753 [9 2 [0 1]]
755Which leaves us seeking
757 [8 [1 0] [7 p [9 2 0 1]]]
759And all we have to do is build the core, `p`. How do we build a
760core? We add code to the subject, just as we added a variable
761above. The initial value of our counter was a constant, `0`.
762The initial (and permanent) value of our battery is a constant,
763the loop formula `l`. So `p` is
765 [8 [1 l] [0 1]]
767Which would leave us seeking
769 [8 [1 0] [7 [8 [1 l] [0 1]] [9 2 0 1]]]
771except that we have duplicated the `8` pattern again, since we
772know
774 [7 [8 [1 l] [0 1]] [9 2 0 1]]
776is equivalent to
778 [8 [1 l] [9 2 0 1]]
780so the full value of `f` is
782 [8 [1 0] [8 [1 l] [9 2 0 1]]]
784Thus our only formula to compose is the loop body, `l`.
785Its subject is the loop core:
787 [bat pay]
789where `bat` is just the loop formula, and `pay` is the pair `[a
790b]`, `a` being the input subject, and `b` the counter. Thus we
791could also write this subject as
793 [l b a]
795and we see readily that `a` is at slot `7`, `b` `6`, `l` `2`.
796With this subject, we need to express the Hoon loop body
798 ?: =(a +(b)) :: line 4
799 b :: line 5
800 $(b +(b)) :: line 6
802This is obviously an if statement, and it calls for `6`. Ie:
804 [6 t y n]
806Giving our decrement program as:
808 [8 [1 0] [8 [1 6 t y n] [9 2 0 1]]]
810For `t`, how do we compute a flag that is yes (`0`) if `a` equals
811`b` plus one? Equals, we recall, is `5`. So `t` can only be
813 [5 [0 7] [4 0 6]]
815If so, our product `y` is just the counter `b`:
817 [0 6]
819And if not? We have to re-execute the loop with the counter
820incremented. If we were executing it with the same counter,
821obviously an infinite loop, we could use the same core:
823 [9 2 0 1]
825But instead we need to construct a new core with the counter
826incremented:
828 [l +(b) a]
830ie,
832 [[0 2] [4 0 6] [0 7]]
834and `n` is:
836 [9 2 [[0 2] [4 0 6] [0 7]]]
838Hence our complete decrement. Let's reformat vertically so we
839can actually read it:
841 [8
842 [1 0]
843 [ 8
844 [ 1
845 [ 6
846 t
847 y
848 n
849 ]
850 ]
851 [9 2 0 1]
852 ]
853 ]
855which becomes
857 [8
858 [1 0]
859 [ 8
860 [ 1
861 [ 6
862 [5 [0 7] [4 0 6]]
863 [0 6]
864 [9 2 [[0 2] [4 0 6] [0 7]]]
865 ]
866 ]
867 [9 2 0 1]
868 ]
869 ]
871or, on one line without superfluous brackets:
873 [8 [1 0] 8 [1 6 [5 [0 7] 4 0 6] [0 6] 9 2 [0 2] [4 0 6] 0 7] 9 2 0 1]
875which works for the important special case, 42:
877 ~tasfyn-partyv> .*(42 [8 [1 0] 8 [1 6 [5 [0 7] 4 0 6] [0 6] 9 2 [0 2] [4 0 6] 0 7] 9 2 0 1])
878 41
880If you understood this, you understand Nock. At least in principle!
882If you want to play around more with Nock, the command line will
883start getting unwieldy. Fortunately, the standard install
884contains the above Nock decrement packaged as an Arvo app, which
885you can edit and change if you'd like to get ambitious. Just run
887 ~tasfyn-partyv> :toy/ndec 19
888 18
890The file driving this is
892 hub/$seat/toy/app/ndec.holw
894Edit this file, ignoring everything above the Nock formula, and
895hit return in the console to see it update:
897 ~tasfyn-partyv>
898 : ~tasfyn-partyv/toy/app/ndec/holw/
900If decrement seems fun - why not write add? I wrote a Nock adder
901a long, long time ago. But I've forgotten where I put it. There
902is absolutely no use in this exercise, except to prove to
903yourself that you've mastered Nock.
905#Appendix A: Operator Reductions#
907##`6` Reduction:##
909 28 :: *[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
911 *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
913 23 :: *[a 2 b c] *[*[a b] *[a c]]
915 *[*[a 0 1] *[a 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]]
917 21 :: *[a 0 b] /[b a]
919 *[a *[a 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]]
921 23 :: *[a 2 b c] *[*[a b] *[a c]]
923 *[a *[*[a [1 c d]] *[a [1 0] 2 [1 2 3] [1 0] 4 4 b]]]
925 22 :: *[a 1 b] b
927 19 :: *[a [b c] d] [*[a b c] *[a d]]
929 *[a *[[c d] [*[a 1 0] *[a 2 [1 2 3] [1 0] 4 4 b]]]]
931 22 :: *[a 1 b] b
933 *[a *[[c d] [0 *[a 2 [1 2 3] [1 0] 4 4 b]]]]
935 23 :: *[a 2 b c] *[*[a b] *[a c]]
937 *[a *[[c d] [0 *[*[a [1 2 3]] *[a [1 0] 4 4 b]]]]]
939 22 :: *[a 1 b] b
941 *[a *[[c d] [0 *[[2 3] *[a [1 0] 4 4 b]]]]]
943 19 :: *[a [b c] d] [*[a b c] *[a d]]
945 *[a *[[c d] [0 *[[2 3] [*[a [1 0]] *[a 4 4 b]]]]]]
947 22 :: *[a 1 b] b
949 *[a *[[c d] [0 *[[2 3] [0 *[a 4 4 b]]]]]]
951 25 :: *[a 4 b] +*[a b]
953 *[a *[[c d] [0 *[[2 3] [0 ++*[a b]]]]]]
955**`6` Reduced:**
957 6r :: *[a 6 b c d] *[a *[[c d] [0 *[[2 3] [0 ++*[a b]]]]]]
959##`7` Reduction:##
961 29 :: *[a 7 b c] *[a 2 b 1 c]
963 *[a 2 b 1 c]
965 23 :: *[a 2 b c] *[*[a b] *[a c]]
967 *[*[a b] *[a 1 c]]
969 22: *[a 1 b] b
971 *[*[a b] c]
973**`7` Reduced:**
975 7r :: *[a 7 b c] *[*[a b] c]
977##`8` Reduction:##
979 30 :: *[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
981 *[a 7 [[7 [0 1] b] 0 1] c]
983 7r :: *[a 7 b c] *[*[a b] c]
985 *[*[a [7 [0 1] b] 0 1]] c]
987 19 :: *[a [b c] d] [*[a b c] *[a d]]
989 *[[*[a [7 [0 1] b]] *[a 0 1]] c]
991 21 :: *[a 0 b] /[b a]
993 *[[*[a [7 [0 1] b]] /[1 a]] c]
995 12 :: /[1 a] a
997 *[[*[a [7 [0 1] b]] a] c]
999 7r :: *[a 7 b c] *[*[a b] c]
1001 *[[*[*[a 0 1]] b] a] c]
1003**`8` Reduced:**
1005 8r :: *[a 8 b c] *[[*[a b] a] c]
1008##`9` Reduction:##
1010 31 :: *[a 9 b c] *[a 7 c [2 [0 1] [0 b]]]
1012 *[a 7 c [2 [0 1] [0 b]]]
1014 7r :: *[a 7 b c] *[*[a b] c]
1016 *[*[a c] [2 [0 1] [0 b]]]
1018 23 :: *[a 2 b c] *[*[a b] *[a c]]
1020 *[*[*[a c] [0 1]] *[*[a c] [0 b]]]
1022 21 :: *[a 0 b] /[b a]
1024**`9` Reduced:**
1026 9r :: *[a 9 b c] *[*[a c] *[*[a c] 0 b]]
1029##`10` Reduction:##
1031 *[a 10 [b c] d] *[a 8 c 7 [0 3] d]
1033 8r :: *[a 8 b c] [[*[a b] a] c]
1035 *[[*[a c] a] 7 [0 2] d]
1037 7r :: *[a 7 b c] *[*[a b] c]
1039 *[*[[*[a c] a] 0 3] d]
1041 21 :: *[a 0 b] /[b a]
1043**`10` reduced:**
1045 10r :: *[a 10 [b c] d] *[a d]