git.iko.soy/urbit.org
on dc20522 help sign in
urbit.org/tutorials/nock/definition.md
186 lines 6.6 kB history raw
1+++
2title = "Nock Definition"
3weight = 1
4template = "doc.html"
5aliases = ["docs/learn/nock/definition/"]
6+++
8Nock is a Turing-complete function that maps a cell
9`[subject formula]` to a noun `product`, where `subject` is the
10data, `formula` is the code, and `product` is the result.
12To program in Hoon, this is all you need to know about Nock.
13It's probably at least worth skimming the definition, though.
15(Also, the Hoon programmer should know that (a) tail call
16elimination in Nock is straightforward; and (b) tail calls in
17Hoon always become tail calls in Nock.)
19## Rules
21Nock is a combinator interpreter defined by the specification below.
23This pseudocode describes a system of reduction rules. Variables
24match any noun; the first rule from the top matches.
26A formula that reduces to itself is an infinite loop, which we define as a
27crash ("bottom" in formal logic). A real interpreter
28can detect this crash and produce an out-of-band value instead.
30```
31Nock 4K
33A noun is an atom or a cell. An atom is a natural number. A cell is an ordered pair of nouns.
35Reduce by the first matching pattern; variables match any noun.
37nock(a) *a
38[a b c] [a [b c]]
40?[a b] 0
41?a 1
42+[a b] +[a b]
43+a 1 + a
44=[a a] 0
45=[a b] 1
47/[1 a] a
48/[2 a b] a
49/[3 a b] b
50/[(a + a) b] /[2 /[a b]]
51/[(a + a + 1) b] /[3 /[a b]]
52/a /a
54#[1 a b] a
55#[(a + a) b c] #[a [b /[(a + a + 1) c]] c]
56#[(a + a + 1) b c] #[a [/[(a + a) c] b] c]
57#a #a
59*[a [b c] d] [*[a b c] *[a d]]
61*[a 0 b] /[b a]
62*[a 1 b] b
63*[a 2 b c] *[*[a b] *[a c]]
64*[a 3 b] ?*[a b]
65*[a 4 b] +*[a b]
66*[a 5 b c] =[*[a b] *[a c]]
68*[a 6 b c d] *[a *[[c d] 0 *[[2 3] 0 *[a 4 4 b]]]]
69*[a 7 b c] *[*[a b] c]
70*[a 8 b c] *[[*[a b] a] c]
71*[a 9 b c] *[*[a c] 2 [0 1] 0 b]
72*[a 10 [b c] d] #[b *[a c] *[a d]]
74*[a 11 [b c] d] *[[*[a c] *[a d]] 0 3]
75*[a 11 b c] *[a c]
77*a *a
78```
80## Operators
82The pseudocode notation defines six prefix operators: `?`, `+`,
83`=`, `/`, `#`, and `*`.
85`?[x]` reduces to `0` if `x` is a cell, `1` if an atom.
87`+[x]` reduces to the atom `x` plus `1`.
89`=[x y]` reduces to `0` if `x` and `y` are the same noun, `1`
90otherwise.
92`/` (`slot`) is a tree addressing operator. The root of the tree
93is `1`; the left child of any node `n` is `2n`; the right child
94is `2n+1`. `/[x y]` is the subtree of `y` at address `x`.
96For instance, `/[1 [531 25 99]]` is `[531 25 99]`; `/[2 [531 25
9799]]` is `531`; `/[3 [531 25 99]]` is `[25 99]`; `/[6 [531 25
9899]]` is `25`; `/[12 [531 25 99]]` crashes.
100`#` (`edit`) is for replacing part of a noun with another noun. `#[x y z]` replaces the value at slot `x` of `z` (i.e., `/[x z]`) with `y`.
102For instance, `#[2 11 [22 33]]` is `[11 33]`; `#[3 11 [22 33]]` is `[22 11]`; `#[4 11 [[22 33] 44]]` is `[[11 33] 44]`; and `#[5 11 [[22 33] 44]]` is `[[22 11] 44]`.
104`*[x y]` is the Nock interpreter function. `x` is the subject,
105`y` is the formula.
107An invalid use of any operator (eg, incrementing a cell) crashes.
108This is specified as an infinite loop, but in practice you get a crash.
110## Instructions
112A valid Nock formula is always a cell. If the head of the formula is a
113cell, Nock treats both head and tail as formulas, resolves each
114against the subject, and produces the cell of their products. In
115other words, the Lisp program `(cons x y)` becomes the Nock
116formula `[x y]`.
118If the head of the formula is an atom, it's an instruction from
119`0` to `11`.
121A formula `[0 b]` reduces to the noun at tree address `b`
122in the subject.
124A formula `[1 b]` reduces to the constant noun `b`.
126A formula `[2 b c]` treats `b` and `c` as formulas, resolves each
127against the subject, then computes Nock again with the product of
128`b` as the subject, `c` as the formula.
130In formulas `[3 b]` and `[4 b]`, `b` is another
131formula, whose product against the subject becomes the input to
132an axiomatic operator. `3` is `?` and `4` is `+`
134A formula `[5 b c]` treats `b` and `c` as formulas that become the input to another axiomatic operator, `=`.
136Instructions `6` through `11` are not strictly necessary for Turing completeness; deleting them
137from Nock would decrease compactness, but not expressiveness.
139`[6 b c d]` is **if** `b`, **then** `c`, **else** `d`. Each of `b`,
140`c`, `d` is a formula against the subject. Remember that `0` is
141true and `1` is false.
143`[7 b c]` composes the formulas `b` and `c`.
145`[8 b c]` produces the product of formula `c`, against
146a subject whose head is the product of formula `b` with the
147original subject, and whose tail is the original subject. (Think
148of `8` as a "variable declaration" or "stack push.")
150`[9 b c]` computes the product of formula `c` with the current
151subject; from that product `d` it extracts a formula `e` at tree
152address `b`, then computes `*[d e]`. (`9` is designed to fit
153Hoon; `d` is a `core` (object), `e` points to an arm (method).)
155In a formula `[10 [b c] d]`, `c` and `d` are computed with the current subject, and then `b` of the product of `d` is replaced with the product of `c`.
157`[11 b c]` is a **hint** semantically equivalent to the formula
158`c`. If `b` is an atom, it's a **static hint**, which is just
159discarded. If `b` is a cell, it's a **dynamic** hint; the head of
160`b` is discarded, and the tail of `b` is executed as a formula
161against the current subject; the product of this is discarded.
163A practical interpreter can do anything with discarded data, so
164long as the result it computes complies with the semantics of
165Nock. For example, the simplest use of hints is the ordinary
166"debug printf." It is erroneous for an interpreter to skip
167computing dynamic hints; they might crash.
169## Implementation
171The reader might wonder how an interpreter whose only arithmetic
172operation is increment can ever be practical.
174The short answer is that a Nock interpreter doesn't have to use
175the algorithm above. It just has to get the **same result** as the
176algorithm above.
178The algorithm for decrementing an atom is to count up to it, an
179O(n) operation. But if the interpreter knows it's running a
180decrement formula, it can use the CPU to decrement directly.
182Detecting any Nock formula whose semantics match some function,
183like decrement, is a hard problem. But in practice there is only
184one decrement we run -- the decrement in the kernel library.
185Declaring this formula (with a hint, instruction `11` above)
186and recognizing it is not hard.