## Saturday, January 9, 2010

### Maxwell's equations of software (Nock)

This post, although by me and not by him, was generously hosted by my good friend Mencius Moldbug.

I love Mencius to death, but let's face it - he's a strange guy. And his blog is even stranger. Frankly, I'd stay off it.

So here's a copy of the original UR post - the Nock spec, plus some mysterious non-clarification:
```1 Context This spec defines one function, Nock. 2 Structures A noun is an atom or a cell. An atom is any unsigned integer. A cell is an ordered pair of any two nouns. 3 Pseudocode Brackets enclose cells. [a b c] is [a [b c]]. *a is Nock(a). Reductions match top-down. 4 Reductions ?[a b] => 0 ?a => 1 ^[a b] => ^[a b] ^a => (a + 1) =[a a] => 0 =[a b] => 1 =a => =a /[1 a] => a /[2 a b] => a /[3 a b] => b /[(a + a) b] => /[2 /[a b]] /[(a + a + 1) b] => /[3 /[a b]] /a => /a *[a 0 b] => /[b a] *[a 1 b] => b *[a 2 b c d] => *[a 3 [0 1] 3 [1 c d] [1 0] 3 [1 2 3] [1 0] 5 5 b] *[a 3 b] => **[a b] *[a 4 b] => ?*[a b] *[a 5 b] => ^*[a b] *[a 6 b] => =*[a b] *[a [b c] d] => [*[a b c] *[a d]] *a => *a ```

For context and comparison, see this or this or this. Here at UR, axioms are axioms - we leave no "niceties such as arithmetic" to the programmer's imagination. Just sayin'.

To grok Nock, construct a formula `f` such that `*[s f]` equals `(s - 1)` for any atomic nonzero subject `s`. The equivalent formula for `(s + 1)` is `[5 0 1]`. The first 16 people who mail me a correct answer may (or may not) win a prize, which may (or may not) be valuable. (Please include your interpreter - in any language, it should fit on a page. Please do not post the answer here or anywhere, and let me know if you see it posted. This is not a difficult problem.)

As you'll quickly see if you try this exercise, raw Nock is not a usable programming language. But nor is it an esoteric language or automaton, like SK combinators. Rather, Nock is a tool for defining higher-level languages - comparable to the lambda calculus, but meant as foundational system software rather than foundational metamathematics.

To define a language with Nock, construct two nouns, `q` and `r`, such that `*[q r]` equals `r`, and `*[s *[p r]]` is a useful functional language. In this description, `p` is the function source; `q` is your language definition, as source; `r` is your language definition, as data; `s` is the input data. You will find this a tractable and entertaining problem.