git.iko.soy/urbit.org
on 6d45ede help sign in
urbit.org/docs/nock/definition.md
168 lines 5.6 kB history raw
1---
2navhome: /docs
3sort: 1
4next: true
5title: Definition
6---
8# Definition
10The Nock VM is a Turing-complete function that maps a cell
11`{subject formula}` to a noun `product`, where `subject` is the
12data, `formula` is the code, and `product` is the result.
14To program in Hoon, this is all you need to know about Nock.
15It's probably at least worth skimming the definition, though.
17(Also, the Hoon programmer should know that (a) tail call
18elimination in Nock is straightforward; and (b) tail calls in
19Hoon always become tail calls in Nock.)
21## Rules
23Nock is a combinator interpreter defined by the spec below.
25This pseudocode (any system of axioms is properly defined in
26pseudocode) is a system of problem reduction rules. Variables
27match any noun; the first rule from the top matches.
29A problem that reduces to itself is an infinite loop, hence a
30crash ("bottom" in formal logic). Obviously a real interpreter
31can detect this crash and produce an out-of-band value instead.
33```
34?[a b] 0
35?a 1
36+[a b] +[a b]
37+a 1 + a
38=[a a] 0
39=[a b] 1
40=a =a
42/[1 a] a
43/[2 a b] a
44/[3 a b] b
45/[(a + a) b] /[2 /[a b]]
46/[(a + a + 1) b] /[3 /[a b]]
47/a /a
49*[a [b c] d] [*[a b c] *[a d]]
51*[a 0 b] /[b a]
52*[a 1 b] b
53*[a 2 b c] *[*[a b] *[a c]]
54*[a 3 b] ?*[a b]
55*[a 4 b] +*[a b]
56*[a 5 b] =*[a b]
58*[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0]
59 2 [1 2 3] [1 0] 4 4 b]
60*[a 7 b c] *[a 2 b 1 c]
61*[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
62*[a 9 b c] *[a 7 c 2 [0 1] 0 b]
63*[a 10 [b c] d] *[a 8 c 7 [0 3] d]
64*[a 10 b c] *[a c]
66*a *a
67```
69## Operators
71The pseudocode notation defines five prefix operators: `?`, `+`,
72`=`, `/`, and `*`.
74`?[x]` produces `0` if `x` is a cell, `1` if an atom.
76`+[x]` produces the atom `x` plus `1`.
78`=[x y]` produces `0` if `x` and `y` are the same noun, `1`
79otherwise.
81`/` (`slot`) is a tree addressing operator. The root of the tree
82is `1`; the left child of any node `n` is `2n`; the right child
83is `2n+1`. `/[x y]` is the subtree of `y` at address `x`.
85(For instance, `/[1 [531 25 99]]` is `[531 25 99]`; `/[2 [531 25
8699]]` is `531`; `/[3 [531 25 99]]` is `[25 99]`; `/[6 [531 25
8799]]` is `25`; `/[12 [531 25 99]]` crashes.)
89`*[x y]` is the Nock interpreter function. `x` is the subject,
90`y` is the formula.
92An invalid use of any operator (eg, incrementing a cell) crashes.
93This is specified as an infinite loop, but it's not actually an
94infinite loop.
96## Instructions
98A valid formula is always a cell. If the head of the formula is a
99cell, Nock treats both head and tail as formulas, resolves each
100against the subject, and produces the cell of their products. In
101other words, the Lisp program `(cons x y)` becomes the Nock
102formula `[x y]`.
104If the head of the formula is an atom, it's an instruction from
105`0` to `10`.
107A formula `[0 b]` produces the noun at tree address `b`
108in the subject.
110A formula `[1 b]` produces the constant noun `b`.
112A formula `[2 b c]` treats `b` and `c` as formulas, resolves each
113against the subject, then computes Nock again with the product of
114`b` as the subject, `c` as the formula.
116In formulas `[3 b]`, `[4 b]`, and `[5 b]`, `b` is another
117formula, whose product against the subject becomes the input to
118an axiomatic operator. `3` is `?`, `4` is `+`, `5` is `=`.
120Instructions `6` through `10` are macros; deleting them
121from Nock would decrease compactness, but not expressiveness.
123`[6 b c d]` is *if* `b`, *then* `c`, *else* `d`. Each of `b`,
124`c`, `d` is a formula against the subject. Remember that `0` is
125true and `1` is false.
127`[7 b c]` composes the formulas `b` and `c`.
129`[8 b c]` produces the product of formula `c`, against
130a subject whose head is the product of formula `b` with the
131original subject, and whose tail is the original subject. (Think
132of `8` as a "variable declaration" or "stack push.")
134`[9 b c]` computes the product of formula `c` with the current
135subject; from that product `d` it extracts a formula `e` at tree
136address `b`, then computes `*[d e]`. (`9` is designed to fit
137Hoon; `d` is a `core` (object), `e` points to an arm (method).)
139`[10 b c]` is a *hint* semantically equivalent to the formula
140`c`. If `b` is an atom, it's a *static hint*, which is just
141discarded. If `b` is a cell, it's a *dynamic* hint; the head of
142`b` is discarded, and the tail of `b` is executed as a formula
143against the current subject; the product of this is discarded.
145A practical interpreter can do anything with discarded data, so
146long as the result it computes complies with the semantics of
147Nock. For example, the simplest use of hints is the ordinary
148"debug printf." It is erroneous for an interpreter to skip
149computing dynamic hints; they might crash.
151## Implementation
153The reader might wonder how an interpreter whose only arithmetic
154operation is increment can ever be practical.
156The short answer is that a Nock interpreter doesn't have to use
157the algorithm above. It just has to get the *same result* as the
158algorithm above.
160The algorithm for decrementing an atom is to count up to it, an
161O(n) operation. But if the interpreter knows it's running a
162decrement formula, it can use the CPU to decrement directly.
164Detecting any Nock formula whose semantics match some function,
165like decrement, is a hard problem. But in practice there is only
166one decrement we run -- the decrement in the kernel library.
167Declaring this formula (with a hint, instruction `10` above)
168and recognizing it is not hard.