Maxwell’s equations of software
I haz dem:
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.