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
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.
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].
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.
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.
[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.
[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.
[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]]]
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.
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.
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.
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]
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]]
[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.
[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]
[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.
[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.
[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.
[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.
[1 a] is a "function" that, when applied to anything, evaluates to a.
[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.
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.
Similarly, the recursion in lines 15 and 16 means I don't think line 21 could be expanded.
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.
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.
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
It should be possible to recast these without line 2 and just write out the cells in full.
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
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.
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.