Nock

32 thoughts
last posted Oct. 18, 2013, 4:24 p.m.
0
get stream as: markdown or atom
0

Once of the first things that intrigued me about Urbit was the Nock language.

0

Nock immediately reminded me a lot of combinatory logic but with a willingness to relax a small amount of purity to gain (slightly) more practicality.

0

You can read more about Nock in the Crash course in Nock on the Urbit site.

0

Of course, I had to go implement it in Python as pynock but since I did that, David Eyk has started a much better version.

0

The Nock 5K spec is:

1  ::    nock(a)           *a
2  ::    [a b c]           [a [b c]]
3  ::
4  ::    ?[a b]            0
5  ::    ?a                1
6  ::    +[a b]            +[a b]
7  ::    +a                1 + a
8  ::    =[a a]            0
9  ::    =[a b]            1
10 ::    =a                =a   
11 ::
12 ::    /[1 a]            a
13 ::    /[2 a b]          a
14 ::    /[3 a b]          b
15 ::    /[(a + a) b]      /[2 /[a b]]
16 ::    /[(a + a + 1) b]  /[3 /[a b]]
17 ::    /a                /a
18 ::
19 ::    *[a [b c] d]      [*[a b c] *[a d]]
20 ::
21 ::    *[a 0 b]          /[b a]
22 ::    *[a 1 b]          b
23 ::    *[a 2 b c]        *[*[a b] *[a c]]
24 ::    *[a 3 b]          ?*[a b]
25 ::    *[a 4 b]          +*[a b]
26 ::    *[a 5 b]          =*[a b]
27 ::
28 ::    *[a 6 b c d]      *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
29 ::    *[a 7 b c]        *[a 2 b 1 c]
30 ::    *[a 8 b c]        *[a 7 [[7 [0 1] b] 0 1] c]
31 ::    *[a 9 b c]        *[a 7 c 2 [0 1] 0 b]
32 ::    *[a 10 [b c] d]   *[a 8 c 7 [0 3] d]
33 ::    *[a 10 b c]       *[a c]
34 ::
35 ::    *a                *a
0

It should be possible to recast these without line 2 and just write out the cells in full.

0

Nock spec with explicit cells, not lists:

1  ::    nock(a)           *a
3  ::
4  ::    ?[a b]            0
5  ::    ?a                1
6  ::    +[a b]            +[a b]
7  ::    +a                1 + a
8  ::    =[a a]            0
9  ::    =[a b]            1
10 ::    =a                =a   
11 ::
12 ::    /[1 a]            a
13 ::    /[2 [a b]]          a
14 ::    /[3 [a b]]          b
15 ::    /[(a + a) b]      /[2 /[a b]]
16 ::    /[(a + a + 1) b]  /[3 /[a b]]
17 ::    /a                /a
18 ::
19 ::    *[a [[b c] d]]      [*[a [b c]] *[a d]]
20 ::
21 ::    *[a [0 b]]          /[b a]
22 ::    *[a [1 b]]          b
23 ::    *[a [2 [b c]]]        *[*[a b] *[a c]]
24 ::    *[a [3 b]]          ?*[a b]
25 ::    *[a [4 b]]          +*[a b]
26 ::    *[a [5 b]]          =*[a b]
27 ::
28 ::    *[a [6 [b [c d]]]]      *[a [2 [[0 1] [2 [[1 [c d]] [[1 0] [2 [[1 [2 3]] [[1 0] [4 [4 b]]]]]]]]]]]
29 ::    *[a [7 [b c]]]        *[a [2 [b [1 c]]]]
30 ::    *[a [8 [b c]]]        *[a [7 [[[7 [[0 1] b]] [0 1]] c]]]
31 ::    *[a [9 [b c]]]        *[a [7 [c [2 [[0 1] [0 b]]]]]]
32 ::    *[a [10 [[b c] d]]]   *[a [8 [c [7 [[0 3] d]]]]]
33 ::    *[a [10 [b c]]]       *[a c]
34 ::
35 ::    *a                *a
0

As pointed out in the Nock crash course, lines 28 thru 32 are just macros so they could be expanded.

I wonder to what extent lines 24 thru 26 can be too.

0

It's possible lines 24 thru 26 can't be expanded because of the * operator.

For example, *[a [3 b]] will evaluate to 1 if and only if *[a b] evaluates to an atom.

0

Similarly, the recursion in lines 15 and 16 means I don't think line 21 could be expanded.

0

Because nouns are either atoms (unsigned integers) or cells and cells are pairs of nouns, the only structure in Nock is a binary tree of unsigned integers.

0

[0 n] is a "function" that, when applied to one of these trees, evaluates to a particular leaf or subtree given by n. This is implemented by lines 12 thru 17 plus 21.

0

[1 a] is a "function" that, when applied to anything, evaluates to a.

0

[3 b] is a "function" that, when applied to a, firstly applies b to a then evaluates to 0 if the result is a cell and 1 if the result is an atom.

0

[4 b] is a "function" that, when applied to a, firstly applies b to a then, if the result is an atom, evaluates to that atom plus one.

0

[5 b] is a "function" that, when applied to a, firstly applies b to a then, evaluates to 0 if the result is a cell with equal items and 1 if the result is a cell with non-equal items.

I presume it crashes if the result of applying b to a is an atom.

0

[2 [b c]] is a "function" that, when applied to a, firstly applies c to a then applies the resulting product to the product of applying b to a.

0

[7 [b c]] is a "function" that, when applied to a, firstly applies b to a then applies c to the result. It is therefore just function composition.

Here is a reduction:

*[a [7 [b c]]] =>
*[a [2 [b [1 c]]]] =>
*[*[a b] *[a [1 c]]] =>
*[*[a b] c]
0

[8 [b c]] is a "function" that, when applied to a, firstly applies b to a then applies c to the ordered pair of that result and the original subject a.

In other words: *[[*[a b] a] c]

To do a reduction from line 30, we're going to need to make use of line 19, though, because after the first two steps:

*[a [8 [b c]]] =>
*[a [7 [[[7 [[0 1] b]] [0 1]] c]]] =>
*[*[a [[7 [[0 1] b]] [0 1]]] c] =>

we end up needing to know how to apply a formula whose left noun is a cell, not just an atom like we've been dealing with up until this point.

0

Line 19 basically says that a formula that doesn't start with an atom is treated as a list of formulas to apply, kind of like map would.

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

Now we can continue our reduction of line 30:

*[a [8 [b c]]] =>
*[a [7 [[[7 [[0 1] b]] [0 1]] c]]] =>
*[*[a [[7 [[0 1] b]] [0 1]]] c] =>
*[[*[a [7 [[0 1] b ]]] *[a [0 1]]] c] =>
*[[*[*[a [0 1]] b] *[a [0 1]]] c] =>
*[[*[a b] a] c]
0

You may have noticed that the formula [0 1] is the identity operator. That is, *[a [0 1]] is a. This is clear from lines 21 and 12.

0

A note on terminology:

* takes a noun. A noun is either an atom (an unsigned integer) or a cell. A cell is an ordered pair of nouns.

*a crashes (hangs) if a is an atom (an unsigned integer) so it should be given a cell. The components of a cell given to * are the subject and the formula.

0

It's not made explicit in the spec, but a formula must be a cell otherwise * will crash.

As explained above, line 19 handles the case where a formula doesn't start with an atom. Lines 21 thru 33 handle the case where the formula starts with an atom between 0 and 10.

* will crash if given a formula that starts with an atom greater than 10.

0

[9 [b c]] is a "function" that, when applied to a, firstly applies c to a. The result is taken to contain within it a formula (at address b) that is then applied to that result.

Here is the reduction:

*[a [9 [b c]]] =>
*[*[a c] [2 [[0 1] [0 b]]]] =>
*[*[*[a c] [0 1]] *[*[a c] [0 b]]] =>
*[*[a c] *[*[a c] [0 b]]]
0

[10 [b c]] is a "function" that throws away b and just applies c to the subject.

However, if b is a cell, its second component is applied to the subject first (before also being thrown away).

This reduction makes this a little clearer:

*[a [10 [[b c] d]]] =>
*[a [8 [c [7 [[0 3] d]]]]] =>
*[[*[a c] a] [7 [[0 3] d]]] =>
*[*[[*[a c] a] [0 3]] d] =>
*[a d]

although I'm still a little confused how this would be used in practice.

0

[6 [b [c d]]] is a "function" that, when applied to a, is equivalent to c if *[a b] is 0 and d if *[a b] is 1. It is therefore a basic if construct.

Much of the complexity is due to handling the case where b is neither 0 nor 1 (crashing rather than giving a bogus result that tries to apply a subtree of c or d to a).

Let's try a reduction:

*[a [6 [b [c d]]]] =>
*[a [2 [[0 1] [2 [[1 [c d]] [[1 0] [2 [[1 [2 3]] [[1 0] [4 [4 b]]]]]]]]]]]
*[*[a [0 1]] *[a [2 [[1 [c d]] [[1 0] [2 [[1 [2 3]] [[1 0] [4 [4 b]]]]]]]]]]
*[a *[a [2 [[1 [c d]] [[1 0] [2 [[1 [2 3]] [[1 0] [4 [4 b]]]]]]]]]]
*[a *[*[a [1 [c d]]] *[a [[1 0] [2 [[1 [2 3]] [[1 0] [4 [4 b]]]]]]]]]
*[a *[[c d] *[a [[1 0] [2 [[1 [2 3]] [[1 0] [4 [4 b]]]]]]]]]
*[a *[[c d] [*[a [1 0]] *[a [2 [[1 [2 3]] [[1 0] [4 [4 b]]]]]]]]]
*[a *[[c d] [0 *[a [2 [[1 [2 3]] [[1 0] [4 [4 b]]]]]]]]]
*[a *[[c d] [0 *[*[a [1 [2 3]]] *[a [[1 0] [4 [4 b]]]]]]]]
*[a *[[c d] [0 *[[2 3] *[a [[1 0] [4 [4 b]]]]]]]]
*[a *[[c d] [0 *[[2 3] [*[a [1 0]] *[a [4 [4 b]]]]]]]]
*[a *[[c d] [0 *[[2 3] [0 *[a [4 [4 b]]]]]]]]
*[a *[[c d] [0 *[[2 3] [0 +*[a [4 b]]]]]]]
*[a *[[c d] [0 *[[2 3] [0 ++*[a b]]]]]]

If *[a b] evaluates to 0 then ++*[a b] will be 2. If *[a b] evaluates to 1 then ++*[a b] will be 3.

This is then used as a tree-address into [2 3]. Because [0 2] selects the left noun of a cell, *[[2 3] [0 2]] is just 2. And because [o 3] selects the right noun of a cell, *[[2 3] [0 3]] is just 3.

This may seem like an identity operation but it insures the correct behaviour if b is neither 0 nor 1. if x is an atom greater than 3 or if x is a cell, *[[2 3] [0 x]] crashes.

We can now use the sanitized tree address into [c d] and either get c or d as appropriate without risk that some subtree of c or d will be applied to a.

0

Why does *[[2 3] [0 x]] crash if x is a cell? Well no other rule but line 17 applies.

Why does *[[2 3] [0 x]] crash if x is, say 4?

/[4 [2 3]] =>
/[2 /[2 [2 3]] =>
/[2 2]

which crashes because, at that point, no other rule but line 17 applies.

0

In the Noon crash course, a core is defined as a cell whose tail is data (possibly containing other cores) and whose head is code containing one or more formulas. The head of a core is call the battery and the tail of a core is called the payload.

A formula in the battery of a core is called an arm of the core.

An arm is evaluated by applying it to the core it's part of, sort of like a method on a Python class taking only self.

0

I've been wondering how you can extract the SKI combinators out of Nock.

We've already seen that [0 1] is the identity operator I. So Ix is *[x [0 1]].

Turns out K and S are simple:

Recall Kxy = x. i.e. Kx is a function that takes y and returns x. Sounds a lot like *[y [1 x]].

Sxyz = xz(yz). S takes three arguments and then returns the first argument applied to the third, which is then applied to the result of the second argument applied to the third. Sounds a lot like *[*[z y] *[z x]] which is *[z 2 y x].

0

So [2 [b c]], [1 a] and [0 1] are analogous to the S, K and I combinators respectively. They are not, however, exactly equivalent (at least in the case of [2 [b c]]). The difference seems to lie in the use of the * operator.

The * operator in the definition of *[a [2 [b c]]] prevents it from being treated as a true combinator.

0

This would also seem to explain why [7 [b c]], which is analogous to the B combinator, can be more simply defined.

As we previously saw,

*[a [7 [b c]]] => *[a [2 [b [1 c]]]]

where as

B => S (K S) K