git.iko.soy/urbit.org
on d452c09 help sign in
urbit.org/docs/programming/core/nock.md
160 lines 5.2 kB history raw
1---
2sort: 5
3---
5# Interpreter: `nock`
7The Nock VM is a Turing-complete function that maps a cell
8`{subject formula}` to a noun `product`, where `subject` is the
9data, `formula` is the code, and `product` is the result.
11To program in Hoon, this is all you need to know about Nock.
12It's probably at least worth skimming this definition, though.
14(Also, the Hoon programmer should know that (a) tail call
15elimination in Nock is straightforward; and (b) tail calls in
16Hoon always become tail calls in Nock.)
18## Rules
20Nock is a combinator interpreter defined by the spec below.
22This pseudocode (any system of axioms is properly defined in
23pseudocode) is a system of problem reduction rules. Variables
24match any noun; the first rule from the top matches.
26A problem that reduces to itself is an infinite loop, hence a
27crash ("bottom" in formal logic). Obviously a real interpreter
28can detect this crash and produce an out-of-band value instead.
30```
31?[a b] 0
32?a 1
33+[a b] +[a b]
34+a 1 + a
35=[a a] 0
36=[a b] 1
37=a =a
39/[1 a] a
40/[2 a b] a
41/[3 a b] b
42/[(a + a) b] /[2 /[a b]]
43/[(a + a + 1) b] /[3 /[a b]]
44/a /a
46*[a [b c] d] [*[a b c] *[a d]]
48*[a 0 b] /[b a]
49*[a 1 b] b
50*[a 2 b c] *[*[a b] *[a c]]
51*[a 3 b] ?*[a b]
52*[a 4 b] +*[a b]
53*[a 5 b] =*[a b]
55*[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0]
56 2 [1 2 3] [1 0] 4 4 b]
57*[a 7 b c] *[a 2 b 1 c]
58*[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
59*[a 9 b c] *[a 7 c 2 [0 1] 0 b]
60*[a 10 [b c] d] *[a 8 c 7 [0 3] d]
61*[a 10 b c] *[a c]
63*a *a
64```
66## Operators
68The pseudocode notation defines five prefix operators: `?`, `+`,
69`=`, `/`, and `*`.
71`?[x]` produces `0` if `x` is a cell, `1` if an atom.
73`+[x]` produces the atom `x` plus `1`.
75`=[x y]` produces `0` if `x` and `y` are the same noun, `1`
76otherwise.
78`/` is a tree addressing operator. The root of the tree is `1`;
79the left child of any node `n` is `2n`; the right child is
80`2n+1`. `/[x y]` is the subtree of `y` at address `x`.
82(For instance, `/[1 [531 25 99]]` is `[531 25 99]`; `/[2 [531 25
8399]]` is `531`; `/[3 [531 25 99]]` is `[25 99]`; `/[6 [531 25
8499]]` is `25`; `/[12 [531 25 99]]` crashes.)
86`*[x y]` is the Nock interpreter function. `x` is the subject,
87`y` is the formula.
89An invalid use of any operator (eg, incrementing a cell) crashes.
90This is specified as an infinite loop, but it's not actually an
91infinite loop.
93## Instructions
95A valid formula is always a cell. If the head of the formula is a
96cell, Nock treats both head and tail as formulas, resolves each
97against the subject, and produces the cell of their products. In
98other words, the Lisp program `(cons x y)` becomes the Nock
99formula `[x y]`.
101If the head of the formula is an atom, it's an instruction from
102`0` to `10`.
104A formula `[0 b]` produces the noun at tree address `b`
105in the subject.
107A formula `[1 b]` produces the constant noun `b`.
109A formula `[2 b c]` treats `b` and `c` is formulas, resolves each
110against the subject, then computes Nock again with the product of
111`b` as the subject, `c` as the formula.
113In formulas `[3 b]`, `[4 b]`, and `[5 b]`, `b` is another
114formula, whose product against the subject becomes the input to
115an axiomatic operator. `3` is `?`, `4` is `+`, `5` is `=`.
117Instructions `6` through `10` are macros; deleting them
118from Nock would decrease compactness, but not expressiveness.
120`[6 b c d]` is *if* `b`, *then* `c`, *else* `d`. Each of `b`,
121`c`, `d` is a formula against the subject. Remember that `0` is
122true and `1` is false.
124`[7 b c]` composes the formulas `b` and `c`.
126`[8 b c]` produces the product of formula `c`, against
127a subject whose head is the product of formula `b` with the
128original subject, and whose tail is the original subject. (Think
129of `8` as a ``variable declaration'' or ``stack push.'')
131`[9 b c]` computes the product of formula `c` with the
132current subject; from that product `d` it extracts a formula
133`e` at tree address `b`, then computes `*[d e]`.
134(Think, very roughly, of `d` as an object and `e` as a
135method.)
137`[10 b c]` is a *hint* semantically equivalent to the formula
138`c`. If `b` is an atom, it's a *static hint*, which is just
139discarded. If `b` is a cell, it's a *dynamic* hint; the head of
140`b` is discarded, and the tail of `b` is executed as a formula
141against the current subject; the product of this is discarded.
143A practical interpreter can do anything with discarded data, so
144long as the result it computes complies with the semantics of
145Nock. For example, the simplest use of hints is the ordinary
146"debug printf." It is erroneous for an interpreter to skip
147computing dynamic hints; they might crash.
149## Implementation
151The reader might wonder how an interpreter whose only arithmetic
152operation is increment can ever be practical.
154The short answer is that a Nock interpreter doesn't have to use
155the algorithm above; it just has to get the same result as the
156algorithm above.
158The algorithm for decrementing an atom is to count up to it, an
159O(n) operation. But if we know we are running a decrement
160formula,