The Combinator Approach#
Combinators are a foundational approach to mathematical logic. Expressions are built out of variables like x and y; combinators like S and K; and function applications like (S K). Books like Raymond Smullyan’s To Mock a Mockingbird explore the kinds of complex systems that can be built out of combinator calculi.
There are several different (compatible) formulations of combinatory logic, such as SKI and BCKW. Many authors have preferred to work with one of the most parsimonious systems, SKI, and Nock at its heart is SKI dressed up with some machinery to handle nouns. (Since SKI is a Turing-complete computational system, this demonstrates that Nock is Turing-complete without further ado.)
Nock opcodes 2, 1, and 0 correspond to S, K, and I combinators, so let’s start there. We’ll look at what the combinators do on their own and then as a part of the Nock system.
I Identity Combinator#
The I combinator simply returns its (single) argument:
I x = x
Iterated applications simply reduce one step at a time:
I I x = I x = x
In Nock, our format is a little different because of how opcodes are set up. (Think of this like grammar.) Opcode 0 provides noun addressing, with slot 1 referring to the entire noun. Thus:
[a 0 1] = a
K Constant Combinator#
The K combinator accepts two arguments and discards the second.
K x y = x
Like
K K x y z = K x z = x
K K x y = K x = x
The latter case is interesting. Why does it stop evaluating forward? There is insufficient information to