Once of the first things that intrigued me about [Urbit](http://www.urbit.org) was the **Nock** language. ---- 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. ---- You can read more about Nock in the [Crash course in Nock](http://www.urbit.org/2013/08/22/Chapter-2-nock.html) on the Urbit site. ---- Of course, I had to go implement it in Python as [pynock](https://github.com/jtauber/pynock) but since I did that, David Eyk has started a [much better version](https://github.com/eykd/nock). ---- 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 ---- It should be possible to recast these without line 2 and just write out the cells in full. ---- 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 ---- 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. ---- 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. ---- Similarly, the recursion in lines 15 and 16 means I don't think line 21 could be expanded. ---- 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 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. ---- `[1 a]` is a "function" that, when applied to anything, evaluates to `a`. ---- `[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. ---- `[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. ---- `[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. ---- `[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`. ---- `[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] ---- `[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. ---- 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]] ---- 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] ---- 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. ---- 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**. ---- 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`. ---- `[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]]] ---- `[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. ---- `[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`. ---- 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. ---- 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`. ---- 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 **I**x is `*[x [0 1]]`. Turns out **K** and **S** are simple: Recall **K**xy = x. i.e. **K**x is a function that takes y and returns x. Sounds a lot like `*[y [1 x]]`. **S**xyz = 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]`. ---- 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. ---- 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**