Definition

Nock is a Turing-complete function that maps a cell [subject formula] to a noun product, where subject is the data, formula is the code, and product is the result.

To program in Hoon, this is all you need to know about Nock. It's probably at least worth skimming the definition, though.

(Also, the Hoon programmer should know that (a) tail call elimination in Nock is straightforward; and (b) tail calls in Hoon always become tail calls in Nock.)

Rules

Nock is a combinator interpreter defined by the specification below.

This pseudocode describes a system of reduction rules. Variables match any noun; the first rule from the top matches.

A formula that reduces to itself is an infinite loop, which we define as a crash ("bottom" in formal logic). A real interpreter can detect this crash and produce an out-of-band value instead.

Nock 4K

A noun is an atom or a cell.  An atom is a natural number.  A cell is an ordered pair of nouns.

Reduce by the first matching pattern; variables match any noun.

nock(a)             *a
[a b c]             [a [b c]]

?[a b]              0
?a                  1
+[a b]              +[a b]
+a                  1 + a
=[a a]              0
=[a b]              1

/[1 a]              a
/[2 a b]            a
/[3 a b]            b
/[(a + a) b]        /[2 /[a b]]
/[(a + a + 1) b]    /[3 /[a b]]
/a                  /a

#[1 a b]            a
#[(a + a) b c]      #[a [b /[(a + a + 1) c]] c]
#[(a + a + 1) b c]  #[a [/[(a + a) c] b] c]
#a                  #a

*[a [b c] d]        [*[a b c] *[a d]]

*[a 0 b]            /[b a]
*[a 1 b]            b
*[a 2 b c]          *[*[a b] *[a c]]
*[a 3 b]            ?*[a b]
*[a 4 b]            +*[a b]
*[a 5 b c]          =[*[a b] *[a c]]

*[a 6 b c d]        *[a *[[c d] 0 *[[2 3] 0 *[a 4 4 b]]]]
*[a 7 b c]          *[*[a b] c]
*[a 8 b c]          *[[*[a b] a] c]
*[a 9 b c]          *[*[a c] 2 [0 1] 0 b]
*[a 10 [b c] d]     #[b *[a c] *[a d]]

*[a 11 [b c] d]     *[[*[a c] *[a d]] 0 3]
*[a 11 b c]         *[a c]

*a                  *a

Operators

The pseudocode notation defines six prefix operators: ?, +, =, /, #, and *.

?[x] reduces to 0 if x is a cell, 1 if an atom.

+[x] reduces to the atom x plus 1.

=[x y] reduces to 0 if x and y are the same noun, 1 otherwise.

/ (slot) is a tree addressing operator. The root of the tree is 1; the left child of any node n is 2n; the right child is 2n+1. /[x y] is the subtree of y at address x.

For instance, /[1 [531 25 99]] is [531 25 99]; /[2 [531 25 99]] is 531; /[3 [531 25 99]] is [25 99]; /[6 [531 25 99]] is 25; /[12 [531 25 99]] crashes.

# (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.

For 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].

*[x y] is the Nock interpreter function. x is the subject, y is the formula.

An invalid use of any operator (eg, incrementing a cell) crashes. This is specified as an infinite loop, but in practice you get a crash.

Instructions

A valid Nock formula is always a cell. If the head of the formula is a cell, Nock treats both head and tail as formulas, resolves each against the subject, and produces the cell of their products. In other words, the Lisp program (cons x y) becomes the Nock formula [x y].

If the head of the formula is an atom, it's an instruction from 0 to 11.

A formula [0 b] reduces to the noun at tree address b in the subject.

A formula [1 b] reduces to the constant noun b.

A formula [2 b c] treats b and c as formulas, resolves each against the subject, then computes Nock again with the product of b as the subject, c as the formula.

In formulas [3 b] and [4 b], b is another formula, whose product against the subject becomes the input to an axiomatic operator. 3 is ? and 4 is +

A formula [5 b c] treats b and c as formulas that become the input to another axiomatic operator, =.

Instructions 6 through 11 are not strictly necessary for Turing completeness; deleting them from Nock would decrease compactness, but not expressiveness.

[6 b c d] is if b, then c, else d. Each of b, c, d is a formula against the subject. Remember that 0 is true and 1 is false.

[7 b c] composes the formulas b and c.

[8 b c] produces the product of formula c, against a subject whose head is the product of formula b with the original subject, and whose tail is the original subject. (Think of 8 as a "variable declaration" or "stack push.")

[9 b c] computes the product of formula c with the current subject; from that product d it extracts a formula e at tree address b, then computes *[d e]. (9 is designed to fit Hoon; d is a core (object), e points to an arm (method).)

In 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.

[11 b c] is a hint semantically equivalent to the formula c. If b is an atom, it's a static hint, which is just discarded. If b is a cell, it's a dynamic hint; the head of b is discarded, and the tail of b is executed as a formula against the current subject; the product of this is discarded.

A practical interpreter can do anything with discarded data, so long as the result it computes complies with the semantics of Nock. For example, the simplest use of hints is the ordinary "debug printf." It is erroneous for an interpreter to skip computing dynamic hints; they might crash.

Implementation

The reader might wonder how an interpreter whose only arithmetic operation is increment can ever be practical.

The short answer is that a Nock interpreter doesn't have to use the algorithm above. It just has to get the same result as the algorithm above.

The algorithm for decrementing an atom is to count up to it, an O(n) operation. But if the interpreter knows it's running a decrement formula, it can use the CPU to decrement directly.

Detecting any Nock formula whose semantics match some function, like decrement, is a hard problem. But in practice there is only one decrement we run -- the decrement in the kernel library. Declaring this formula (with a hint, instruction 11 above) and recognizing it is not hard.