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