27b9eda · urbit.org · git.iko.soy

git.iko.soy/urbit.org

quick refresh of nock pages for 4k spec

commit27b9eda2f28d078b7ad00f4d6869cb84571d0482 authorjoshuareagan <joshuareagan@gmail.com> dateThu 4 Oct 2018, 12:48 (8 years ago) parent69fd46f

4 files changed+215−109

compare with master

unifiedsplit

docs/tutorials/nock.umd+1−1 docs/tutorials/nock/definition.umd+68−47 docs/tutorials/nock/explanation.umd+76−35 docs/tutorials/nock/implementations.umd+70−26

docs/tutorials/nock.umd+1−1

@@ -7,7 +7,7 @@

88# Nock

10−> Last major revision of this tutorial: 2016

10+> Last major revision of this tutorial: 2016. Minor revisions were made in October 2018 to bring it in line with the new Nock 4K spec.

1111

1212Nock is the low-level functional programming language that is interpreted by Vere. You don't need to know Nock to write Hoon, or even to work on most parts of Vere. But if you want to understand the foundations of Urbit and are mathematically-inclined, dive right in.

1313

docs/tutorials/nock/definition.umd+68−47

@@ -23,54 +23,67 @@ Hoon always become tail calls in Nock.)

2323

2424Nock is a combinator interpreter defined by the specification below.

2525

26−This pseudocode (any system of axioms is properly defined in

27−pseudocode) is a system of problem reduction rules. Variables

26+This pseudocode describes a system of reduction rules. Variables

2827match any noun; the first rule from the top matches.

2928

30−A formula that reduces to itself is an infinite loop, hence a

31−crash ("bottom" in formal logic). Obviously a real interpreter

29+A formula that reduces to itself is an infinite loop, which we define as a

30+crash ("bottom" in formal logic). A real interpreter

3231can detect this crash and produce an out-of-band value instead.

3332

3433```

35−?[a b] 0

36−?a 1

37−+[a b] +[a b]

38−+a 1 + a

39−=[a a] 0

40−=[a b] 1

41−=a =a

42−

43−/[1 a] a

44−/[2 a b] a

45−/[3 a b] b

46−/[(a + a) b] /[2 /[a b]]

47−/[(a + a + 1) b] /[3 /[a b]]

48−/a /a

49−

50−*[a [b c] d] [*[a b c] *[a d]]

51−

52−*[a 0 b] /[b a]

53−*[a 1 b] b

54−*[a 2 b c] *[*[a b] *[a c]]

55−*[a 3 b] ?*[a b]

56−*[a 4 b] +*[a b]

57−*[a 5 b] =*[a b]

58−

59−*[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0]

60− 2 [1 2 3] [1 0] 4 4 b]

61−*[a 7 b c] *[a 2 b 1 c]

62−*[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]

63−*[a 9 b c] *[a 7 c 2 [0 1] 0 b]

64−*[a 10 [b c] d] *[a 8 c 7 [0 3] d]

65−*[a 10 b c] *[a c]

66−

67−*a *a

34+Nock 4K

35+

36+A noun is an atom or a cell. An atom is a natural number. A cell is an ordered pair of nouns.

37+

38+Reduce by the first matching pattern; variables match any noun.

39+

40+nock(a) *a

41+[a b c] [a [b c]]

42+

43+?[a b] 0

44+?a 1

45++[a b] +[a b]

46++a 1 + a

47+=[a a] 0

48+=[a b] 1

49+

50+/[1 a] a

51+/[2 a b] a

52+/[3 a b] b

53+/[(a + a) b] /[2 /[a b]]

54+/[(a + a + 1) b] /[3 /[a b]]

55+/a /a

56+

57+#[1 a b] a

58+#[(a + a) b c] #[a [b /[(a + a + 1) c]] c]

59+#[(a + a + 1) b c] #[a [/[(a + a) c] b] c]

60+#a #a

61+

62+*[a [b c] d] [*[a b c] *[a d]]

63+

64+*[a 0 b] /[b a]

65+*[a 1 b] b

66+*[a 2 b c] *[*[a b] *[a c]]

67+*[a 3 b] ?*[a b]

68+*[a 4 b] +*[a b]

69+*[a 5 b c] =[*[a b] *[a c]]

70+

71+*[a 6 b c d] *[a *[[c d] 0 *[[2 3] 0 *[a 4 4 b]]]]

72+*[a 7 b c] *[*[a b] c]

73+*[a 8 b c] *[[*[a b] a] c]

74+*[a 9 b c] *[*[a c] 2 [0 1] 0 b]

75+*[a 10 [b c] d] #[b *[a c] *[a d]]

76+

77+*[a 11 [b c] d] *[[*[a c] *[a d]] 0 3]

78+*[a 11 b c] *[a c]

79+

80+*a *a

6881```

6982

7083## Operators

7184

72−The pseudocode notation defines five prefix operators: `?`, `+`,

73−`=`, `/`, and `*`.

85+The pseudocode notation defines six prefix operators: `?`, `+`,

86+`=`, `/`, `#`, and `*`.

7487

7588`?[x]` reduces to `0` if `x` is a cell, `1` if an atom.

7689

@@ -83,9 +96,13 @@ otherwise.

8396is `1`; the left child of any node `n` is `2n`; the right child

8497is `2n+1`. `/[x y]` is the subtree of `y` at address `x`.

8598

86−(For instance, `/[1 [531 25 99]]` is `[531 25 99]`; `/[2 [531 25

99+For instance, `/[1 [531 25 99]]` is `[531 25 99]`; `/[2 [531 25

8710099]]` is `531`; `/[3 [531 25 99]]` is `[25 99]`; `/[6 [531 25

88−99]]` is `25`; `/[12 [531 25 99]]` crashes.)

101+99]]` is `25`; `/[12 [531 25 99]]` crashes.

102+

103+`#` (`edit`) is for replacing part of a noun with another noun. `#[x y z]` replaces the value at slot `x` of `z` (i.e., `/[x z]`) with `y`.

104+

105+For instance, `#[2 11 [22 33]]` is `[11 33]`; `#[3 11 [22 33]]` is `[22 11]`; `#[4 11 [[22 33] 44]]` is `[[11 33] 44]`; and `#[5 11 [[22 33] 44]]` is `[[22 11] 44]`.

89106

90107`*[x y]` is the Nock interpreter function. `x` is the subject,

91108`y` is the formula.

@@ -95,14 +112,14 @@ This is specified as an infinite loop, but in practice you get a crash.

95112

96113## Instructions

97114

98−A valid formula is always a cell. If the head of the formula is a

115+A valid Nock formula is always a cell. If the head of the formula is a

99116cell, Nock treats both head and tail as formulas, resolves each

100117against the subject, and produces the cell of their products. In

101118other words, the Lisp program `(cons x y)` becomes the Nock

102119formula `[x y]`.

103120

104121If the head of the formula is an atom, it's an instruction from

105−`0` to `10`.

122+`0` to `11`.

106123

107124A formula `[0 b]` reduces to the noun at tree address `b`

108125in the subject.

@@ -113,11 +130,13 @@ A formula `[2 b c]` treats `b` and `c` as formulas, resolves each

113130against the subject, then computes Nock again with the product of

114131`b` as the subject, `c` as the formula.

115132

116−In formulas `[3 b]`, `[4 b]`, and `[5 b]`, `b` is another

133+In formulas `[3 b]` and `[4 b]`, `b` is another

117134formula, whose product against the subject becomes the input to

118−an axiomatic operator. `3` is `?`, `4` is `+`, `5` is `=`.

135+an axiomatic operator. `3` is `?` and `4` is `+`

136+

137+A formula `[5 b c]` treats `b` and `c` as formulas that become the input to another axiomatic operator, `=`.

119138

120−Instructions `6` through `10` are macros; deleting them

139+Instructions `6` through `11` are not strictly necessary for Turing completeness; deleting them

121140from Nock would decrease compactness, but not expressiveness.

122141

123142`[6 b c d]` is *if* `b`, *then* `c`, *else* `d`. Each of `b`,

@@ -136,7 +155,9 @@ subject; from that product `d` it extracts a formula `e` at tree

136155address `b`, then computes `*[d e]`. (`9` is designed to fit

137156Hoon; `d` is a `core` (object), `e` points to an arm (method).)

138157

139−`[10 b c]` is a *hint* semantically equivalent to the formula

158+In a formula `[10 [b c] d]`, `c` and `d` are computed with the current subject, and then `b` of the product of `d` is replaced with the product of `c`.

159+

160+`[11 b c]` is a *hint* semantically equivalent to the formula

140161`c`. If `b` is an atom, it's a *static hint*, which is just

141162discarded. If `b` is a cell, it's a *dynamic* hint; the head of

142163`b` is discarded, and the tail of `b` is executed as a formula

docs/tutorials/nock/explanation.umd+76−35

@@ -210,6 +210,52 @@ is `[14 15]`

210210

211211Hopefully this isn't terribly hard to follow.

212212

213+### Editing a Noun, `#`

214+

215+```

216+#[1 a b] a

217+#[(a + a) b c] #[a [b /[(a + a + 1) c]] c]

218+#[(a + a + 1) b c] #[a [/[(a + a) c] b] c]

219+```

220+

221+The `#` operator replaces part of a noun with another noun. `#[x y z]` replaces address `x` of `z` with the noun `y`.

222+

223+Take some noun, say, `[22 33 44 55]`. Let's replace part of it with another noun, `[123 456]`. We can replace the entire original noun as follows:

224+

225+```

226+#[1 [123 456] [22 33 44 55]]

227+```

228+

229+is

230+

231+```

232+[123 456]

233+```

234+

235+If we only want to replace the value at address `2`:

236+

237+```

238+#[2 [123 456] [22 33 44 55]]

239+```

240+

241+is

242+

243+```

244+[[123 456] 33 44 55]

245+```

246+

247+And we can replace address `3`:

248+

249+```

250+#[3 [123 456] [22 33 44 55]]

251+```

252+

253+is

254+

255+```

256+[22 123 456]

257+```

258+

213259## Instructions

214260

215261These rules define Nock itself - ie, the `*` operator.

@@ -227,6 +273,7 @@ Note that we're using Hoon syntax here. Since we do not use Nock

227273from Hoon all that often (it's sort of like embedding assembly in

228274C), we've left it a little cumbersome. In Hoon, instead of

229275writing `*[a 0 b]`, we write

276+

230277```

231278.*(a [0 b])

232279```

@@ -281,10 +328,10 @@ This gives the same `[153 218]`

281328```

282329*[a 3 b] ?*[a b]

283330*[a 4 b] +*[a b]

284−*[a 5 b] =*[a b]

331+*[a 5 b c] =[*[a b] *[a c]]

285332```

286333

287−In lines 23-25, we meet our axiomatic functions again:

334+These are axiomatic functions:

288335

289336For instance, if `x` is a formula that calculates some product,

290337`[4 x]` calculates that product plus one. Hence:

@@ -322,7 +369,7 @@ We could write this line less formally:

322369In other words, if you have two Nock formulas `x` and `y`, a

323370formula that computes the pair of them is just `[x y]`. We can

324371recognize this because no atom is a valid formula, and

325−every formula that *does not* use line 19 has an atomic head.

372+every formula that *does not* use distribution has an atomic head.

326373

327374If you know Lisp, you can think of this feature as a sort of

328375"implicit cons." Where in Lisp you would write `(cons x y)`,

@@ -353,45 +400,45 @@ we get

353400[43 1]

354401```

355402

356−Except for the crash defaults (lines 6, 10, 17, and 35), we've actually

403+Except for the crash defaults, we've actually

357404completed all the _essential_ aspects of Nock. The instructions up

358405through 5 provide all necessary computational functionality.

359406Nock, though very simple, is actually much more complex than it

360407formally needs to be.

361408

362−Operators 6 through 10 are macros. They exist because Nock is

409+Operators 6 through 11 are sugar. They exist because Nock is

363410not a toy, but a practical interpreter. Let's see them all

364411together:

365412

366−## Macros

413+## Sugar

367414

368415```

369−*[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]

370−*[a 7 b c] *[a 2 b 1 c]

371−*[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]

372−*[a 9 b c] *[a 7 c 2 [0 1] 0 b]

373−*[a 10 [b c] d] *[a 8 c 7 [0 3] d]

374−*[a 10 b c] *[a c]

416+*[a 6 b c d] *[a *[[c d] 0 *[[2 3] 0 *[a 4 4 b]]]]

417+*[a 7 b c] *[*[a b] c]

418+*[a 8 b c] *[[*[a b] a] c]

419+*[a 9 b c] *[*[a c] 2 [0 1] 0 b]

420+*[a 10 [b c] d] #[b *[a c] *[a d]]

421+

422+*[a 11 [b c] d] *[[*[a c] *[a d]] 0 3]

423+*[a 11 b c] *[a c]

375424```

376425

377−Notice that instructions `6` through `10` are macros: each just

378−expands to a larger formula. Let's try to figure out what these

379−macros do, simplest first:

426+Let's try to figure out what these do, simplest first:

380427

381−### `10`, hint

428+### `11`, hint

382429

383430```

384−*[a 10 b c] *[a c]

431+*[a 11 b c] *[a c]

385432```

386433

387434If `x` is an atom and `y` is a formula, the formula `[10 x y]`

388435appears to be equivalent to... `y`. For instance:

389436

390437```

391−.*([132 19] [10 37 [4 0 3]])

438+.*([132 19] [11 37 [4 0 3]])

392439```

393440

394−Why would we want to do this? `10` is actually a hint instruction.

441+Why would we want to do this? `11` is actually a hint instruction.

395442The `37` in this example is discarded information - it is not

396443used, formally, in the computation. It may help the interpreter

397444compute the expression more efficiently, however.

@@ -403,13 +450,13 @@ the Nock spec. Some are defined in Hoon. Indeed, a naive Nock

403450interpreter not optimized for Hoon will run Hoon quite poorly.

404451When it gets the product, however, the product will be right.

405452

406−There is another instruction `10` rule:

453+There is another instruction `11` rule:

407454

408455```

409−*[a 10 [b c] d] *[a 8 c 7 [0 3] d]

456+*[a 11 [b c] d] *[[*[a c] *[a d]] 0 3]

410457```

411458

412−Once we see what `7` and `8` do, we'll see that this complex hint

459+This complex hint

413460throws away an arbitrary `b`, but computes the formula `c`

414461against the subject and... throws away the product. This formula

415462is simply equivalent to `d`. Of course, in practice the product

@@ -418,12 +465,12 @@ wind up as a side effect.

418465

419466(Why do we even care that `c` is computed? Because `c` could

420467crash. A correct Nock cannot simply ignore it, and treat both

421−variants of `10` as equivalent.)

468+variants of `11` as equivalent.)

422469

423470### `7`, compose

424471

425472```

426−*[a 7 b c] *[a 2 b 1 c]

473+*[a 7 b c] *[*[a b] c]

427474```

428475

429476Suppose we have two formulas, `b` and `c`. What is the formula

@@ -435,13 +482,13 @@ Suppose we have two formulas, `b` and `c`. What is the formula

435482```

436483

437484Good old composition, on Nock formulas. It's easy to see how

438−this is built out of `2`. The data to evaluate is simply `b`,

485+this is a variant of Nock `2`. The data to evaluate is simply `b`,

439486and the formula is `c` quoted.

440487

441488### `8`, extend

442489

443490```

444−*[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]

491+*[a 8 b c] *[[*[a b] a] c]

445492```

446493

447494`8` is `7`, except that the subject for `c` is not simply the

@@ -464,22 +511,16 @@ likely to generate an `8`, because the variable is computed

464511against the present subject, and used in a calculation which

465512depends both on the original subject and the new variable.

466513

467−For extra credit, explain why we can't just define

468−

469−```

470−*[a 8 b c] *[a 7 [b 0 1] c]

471−```

472−

473514### `9`, invoke

474515

475516`9` is a calling convention:

476517

477518```

478−*[a 9 b c] *[a 7 c 2 [0 1] 0 b]

519+*[a 9 b c] *[*[a c] 2 [0 1] 0 b]

479520```

480521

481522With `c`, we produce a noun which contains both code and data - a

482−*core*. We use this core as the subject, and evaulate the

523+*core*. We use this core as the subject, and evaluate the

483524formula within it at slot `b`.

484525

485526### `6`, if-then-else

@@ -487,7 +528,7 @@ formula within it at slot `b`.

487528This looks much scarier than it is:

488529

489530```

490−*[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]

531+*[a 6 b c d] *[a *[[c d] 0 *[[2 3] 0 *[a 4 4 b]]]]

491532```

492533

493534If `b` evaluates to `0`, we produce `c`; if `b` evaluates to `1`,

docs/tutorials/nock/implementations.umd+70−26

@@ -12,10 +12,10 @@ and manual reference counting. More about the C environment can be found

1212in the [runtime system documentation](../../../vere/runtime).

1313

1414```

15−/* nock(): produce .*(bus fol). Do not virtualize.

15+/* _n_nock_on(): produce .*(bus fol). Do not virtualize.

1616*/

1717static u3_noun

18−nock(u3_noun bus, u3_noun fol)

18+_n_nock_on(u3_noun bus, u3_noun fol)

1919{

2020 u3_noun hib, gal;

2121

@@ -23,11 +23,15 @@ nock(u3_noun bus, u3_noun fol)

2323 hib = u3h(fol);

2424 gal = u3t(fol);

2525

26+#ifdef U3_CPU_DEBUG

27+ u3R->pro.nox_d += 1;

28+#endif

29+

2630 if ( c3y == u3r_du(hib) ) {

2731 u3_noun poz, riv;

2832

29− poz = nock(u3k(bus), u3k(hib));

30− riv = nock(bus, u3k(gal));

33+ poz = _n_nock_on(u3k(bus), u3k(hib));

34+ riv = _n_nock_on(bus, u3k(gal));

3135

3236 u3a_lose(fol);

3337 return u3i_cell(poz, riv);

@@ -57,8 +61,8 @@ nock(u3_noun bus, u3_noun fol)

5761 c3_assert(!"not reached");

5862

5963 case 2: {

60− u3_noun nex = nock(u3k(bus), u3k(u3t(gal)));

61− u3_noun seb = nock(bus, u3k(u3h(gal)));

64+ u3_noun nex = _n_nock_on(u3k(bus), u3k(u3t(gal)));

65+ u3_noun seb = _n_nock_on(bus, u3k(u3h(gal)));

6266

6367 u3a_lose(fol);

6468 bus = seb;

@@ -70,7 +74,7 @@ nock(u3_noun bus, u3_noun fol)

7074 case 3: {

7175 u3_noun gof, pro;

7276

73− gof = nock(bus, u3k(gal));

77+ gof = _n_nock_on(bus, u3k(gal));

7478 pro = u3r_du(gof);

7579

7680 u3a_lose(gof); u3a_lose(fol);

@@ -81,7 +85,7 @@ nock(u3_noun bus, u3_noun fol)

8185 case 4: {

8286 u3_noun gof, pro;

8387

84− gof = nock(bus, u3k(gal));

88+ gof = _n_nock_on(bus, u3k(gal));

8589 pro = u3i_vint(gof);

8690

8791 u3a_lose(fol);

@@ -90,7 +94,7 @@ nock(u3_noun bus, u3_noun fol)

9094 c3_assert(!"not reached");

9195

9296 case 5: {

93− u3_noun wim = nock(bus, u3k(gal));

97+ u3_noun wim = _n_nock_on(bus, u3k(gal));

9498 u3_noun pro = u3r_sing(u3h(wim), u3t(wim));

9599

96100 u3a_lose(wim); u3a_lose(fol);

@@ -103,7 +107,7 @@ nock(u3_noun bus, u3_noun fol)

103107

104108 u3x_trel(gal, &b_gal, &c_gal, &d_gal);

105109 {

106− u3_noun tys = nock(u3k(bus), u3k(b_gal));

110+ u3_noun tys = _n_nock_on(u3k(bus), u3k(b_gal));

107111 u3_noun nex;

108112

109113 if ( 0 == tys ) {

@@ -124,7 +128,7 @@ nock(u3_noun bus, u3_noun fol)

124128

125129 u3x_cell(gal, &b_gal, &c_gal);

126130 {

127− u3_noun bod = nock(bus, u3k(b_gal));

131+ u3_noun bod = _n_nock_on(bus, u3k(b_gal));

128132 u3_noun nex = u3k(c_gal);

129133

130134 u3a_lose(fol);

@@ -140,7 +144,7 @@ nock(u3_noun bus, u3_noun fol)

140144

141145 u3x_cell(gal, &b_gal, &c_gal);

142146 {

143− u3_noun heb = nock(u3k(bus), u3k(b_gal));

147+ u3_noun heb = _n_nock_on(u3k(bus), u3k(b_gal));

144148 u3_noun bod = u3nc(heb, bus);

145149 u3_noun nex = u3k(c_gal);

146150

@@ -157,18 +161,29 @@ nock(u3_noun bus, u3_noun fol)

157161

158162 u3x_cell(gal, &b_gal, &c_gal);

159163 {

160− u3_noun seb = nock(bus, u3k(c_gal));

164+ u3_noun seb = _n_nock_on(bus, u3k(c_gal));

165+ u3_noun pro;

161166

162− if ( c3n == u3r_ud(b_gal) ) {

163− return u3m_bail(c3__exit);

164− }

165− else {

166− u3_noun nex = u3k(u3at(b_gal, seb));

167+ u3t_off(noc_o);

168+ pro = u3j_kick(seb, b_gal);

169+ u3t_on(noc_o);

167170

171+ if ( u3_none != pro ) {

168172 u3a_lose(fol);

169− bus = seb;

170− fol = nex;

171− continue;

173+ return pro;

174+ }

175+ else {

176+ if ( c3n == u3r_ud(b_gal) ) {

177+ return u3m_bail(c3__exit);

178+ }

179+ else {

180+ u3_noun nex = u3k(u3at(b_gal, seb));

181+

182+ u3a_lose(fol);

183+ bus = seb;

184+ fol = nex;

185+ continue;

186+ }

172187 }

173188 }

174189 }

@@ -187,7 +202,7 @@ nock(u3_noun bus, u3_noun fol)

187202 u3_noun d_gal = q_gal;

188203

189204 zep = u3k(b_gal);

190− hod = nock(u3k(bus), u3k(c_gal));

205+ hod = _n_nock_on(u3k(bus), u3k(c_gal));

191206 nex = u3k(d_gal);

192207 }

193208 else {

@@ -199,10 +214,39 @@ nock(u3_noun bus, u3_noun fol)

199214 nex = u3k(c_gal);

200215 }

201216

202− u3a_lose(zep);

203− u3a_lose(hod);

217+ u3a_lose(fol);

218+ return _n_hint(zep, hod, bus, nex);

219+ }

220+ }

221+

222+ case 11: {

223+ u3_noun ref = _n_nock_on(u3k(bus), u3k(u3h(gal)));

224+ u3_noun gof = _n_nock_on(bus, u3k(u3t(gal)));

225+ u3_noun val;

204226

205− return nock(bus, nex);

227+ u3t_off(noc_o);

228+ val = u3m_soft_esc(ref, u3k(gof));

229+ u3t_on(noc_o);

230+

231+ if ( !_(u3du(val)) ) {

232+ u3m_bail(u3nt(1, gof, 0));

233+ }

234+ if ( !_(u3du(u3t(val))) ) {

235+ //

236+ // replace with proper error stack push

237+ //

238+ u3t_push(u3nc(c3__hunk, _n_mush(gof)));

239+ return u3m_bail(c3__exit);

240+ }

241+ else {

242+ u3_noun pro;

243+

244+ u3z(gof);

245+ u3z(fol);

246+ pro = u3k(u3t(u3t(val)));

247+ u3z(val);

248+

249+ return pro;

206250 }

207251 }

208252 c3_assert(!"not reached");

@@ -211,6 +255,6 @@ nock(u3_noun bus, u3_noun fol)

211255}

212256```

213257

214−Building a Nock interpreter in another language is a fun exercise. Check out our community Nock implementations:

258+Building a Nock interpreter in another language is a fun exercise. Check out our community Nock implementations. (Note: these were written for a slightly older version of Nock, Nock 5K. The current version is Nock 4K.):

215259

216260;list(src "../../nock/implementations");