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.