git.iko.soy/urbit.org
on 8e080d6 help sign in
urbit.org/docs/programming/core/nock.md
161 lines 5.2 kB history raw
1---
2sort: 5
3next: true
4---
6# Interpreter: `nock`
8The Nock VM 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 this 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 spec below.
23This pseudocode (any system of axioms is properly defined in
24pseudocode) is a system of problem reduction rules. Variables
25match any noun; the first rule from the top matches.
27A problem that reduces to itself is an infinite loop, hence a
28crash ("bottom" in formal logic). Obviously a real interpreter
29can detect this crash and produce an out-of-band value instead.
31```
32?[a b] 0
33?a 1
34+[a b] +[a b]
35+a 1 + a
36=[a a] 0
37=[a b] 1
38=a =a
40/[1 a] a
41/[2 a b] a
42/[3 a b] b
43/[(a + a) b] /[2 /[a b]]
44/[(a + a + 1) b] /[3 /[a b]]
45/a /a
47*[a [b c] d] [*[a b c] *[a d]]
49*[a 0 b] /[b a]
50*[a 1 b] b
51*[a 2 b c] *[*[a b] *[a c]]
52*[a 3 b] ?*[a b]
53*[a 4 b] +*[a b]
54*[a 5 b] =*[a b]
56*[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0]
57 2 [1 2 3] [1 0] 4 4 b]
58*[a 7 b c] *[a 2 b 1 c]
59*[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
60*[a 9 b c] *[a 7 c 2 [0 1] 0 b]
61*[a 10 [b c] d] *[a 8 c 7 [0 3] d]
62*[a 10 b c] *[a c]
64*a *a
65```
67## Operators
69The pseudocode notation defines five prefix operators: `?`, `+`,
70`=`, `/`, and `*`.
72`?[x]` produces `0` if `x` is a cell, `1` if an atom.
74`+[x]` produces the atom `x` plus `1`.
76`=[x y]` produces `0` if `x` and `y` are the same noun, `1`
77otherwise.
79`/` is a tree addressing operator. The root of the tree is `1`;
80the left child of any node `n` is `2n`; the right child is
81`2n+1`. `/[x y]` is the subtree of `y` at address `x`.
83(For instance, `/[1 [531 25 99]]` is `[531 25 99]`; `/[2 [531 25
8499]]` is `531`; `/[3 [531 25 99]]` is `[25 99]`; `/[6 [531 25
8599]]` is `25`; `/[12 [531 25 99]]` crashes.)
87`*[x y]` is the Nock interpreter function. `x` is the subject,
88`y` is the formula.
90An invalid use of any operator (eg, incrementing a cell) crashes.
91This is specified as an infinite loop, but it's not actually an
92infinite loop.
94## Instructions
96A valid formula is always a cell. If the head of the formula is a
97cell, Nock treats both head and tail as formulas, resolves each
98against the subject, and produces the cell of their products. In
99other words, the Lisp program `(cons x y)` becomes the Nock
100formula `[x y]`.
102If the head of the formula is an atom, it's an instruction from
103`0` to `10`.
105A formula `[0 b]` produces the noun at tree address `b`
106in the subject.
108A formula `[1 b]` produces the constant noun `b`.
110A formula `[2 b c]` treats `b` and `c` is formulas, resolves each
111against the subject, then computes Nock again with the product of
112`b` as the subject, `c` as the formula.
114In formulas `[3 b]`, `[4 b]`, and `[5 b]`, `b` is another
115formula, whose product against the subject becomes the input to
116an axiomatic operator. `3` is `?`, `4` is `+`, `5` is `=`.
118Instructions `6` through `10` are macros; deleting them
119from Nock would decrease compactness, but not expressiveness.
121`[6 b c d]` is *if* `b`, *then* `c`, *else* `d`. Each of `b`,
122`c`, `d` is a formula against the subject. Remember that `0` is
123true and `1` is false.
125`[7 b c]` composes the formulas `b` and `c`.
127`[8 b c]` produces the product of formula `c`, against
128a subject whose head is the product of formula `b` with the
129original subject, and whose tail is the original subject. (Think
130of `8` as a ``variable declaration'' or ``stack push.'')
132`[9 b c]` computes the product of formula `c` with the
133current subject; from that product `d` it extracts a formula
134`e` at tree address `b`, then computes `*[d e]`.
135(Think, very roughly, of `d` as an object and `e` as a
136method.)
138`[10 b c]` is a *hint* semantically equivalent to the formula
139`c`. If `b` is an atom, it's a *static hint*, which is just
140discarded. If `b` is a cell, it's a *dynamic* hint; the head of
141`b` is discarded, and the tail of `b` is executed as a formula
142against the current subject; the product of this is discarded.
144A practical interpreter can do anything with discarded data, so
145long as the result it computes complies with the semantics of
146Nock. For example, the simplest use of hints is the ordinary
147"debug printf." It is erroneous for an interpreter to skip
148computing dynamic hints; they might crash.
150## Implementation
152The reader might wonder how an interpreter whose only arithmetic
153operation is increment can ever be practical.
155The short answer is that a Nock interpreter doesn't have to use
156the algorithm above; it just has to get the same result as the
157algorithm above.
159The algorithm for decrementing an atom is to count up to it, an
160O(n) operation. But if we know we are running a decrement
161formula,