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