5 Synthesis, and why one has to run things
(ns meme-constructor.computing.post-i3-synthesis
(:require [scicloj.kindly.v4.kind :as kind]
[meme-constructor.synthesis.system :as sys]
[meme-constructor.synthesis.synth :as sy]
[meme-constructor.figures :as fig]))Post I.3 of Part I, “A Constructor Theory of Computing and Design”.
Synthesis is the task whose product is a program. Two things follow from Rice’s theorem. A decoder that reads a meme off a brain state is a verifier of the brain’s programs, so it cannot exist for a receptive host. And no procedure, however clever, can confirm more of a candidate than finitely many input-output pairs witness: one can test a program, never certify it.
Both results need the language to be acceptable, not merely universal. We use post I.1’s vocabulary: computing system (C1) and the abstract constructor \(K_\sigma\) (Definition I.1.6).
5.1 1. Synthesis as a task
Fix a programming language \(L\): a decidable set of program texts with a semantics \(\llbracket p \rrbracket\), a partial function from inputs to outputs. Push3 with its interpreter is one such language.
Definition I.3.1 (Specification). A specification \(\sigma\) is a set of partial functions. A program meets it, \(\llbracket p \rrbracket \models \sigma\), iff \(\llbracket p \rrbracket \in \sigma\). An example specification \(\sigma_E\) is given by finitely many pairs \(E = \{x_i \mapsto y_i\}\): it contains every \(f\) with \(f(x_i) = y_i\) for all pairs in \(E\).
A specification depends only on what a program does, never on its text. The programs meeting \(\sigma\) form the abstract constructor \(K_\sigma\).
Definition I.3.2 (Synthesis (C4)). On the composite substrate of a specification medium and a program medium, the synthesis task for \(\sigma\) is
\[\mathrm{Synth}_\sigma = \{\, (\sigma, x_0) \to (\sigma, p) \,\} \quad \text{with} \quad \llbracket p \rrbracket \models \sigma .\]
Here \(x_0\) holds no program meeting \(\sigma\), and the specification is not consumed. A synthesiser is a constructor for \(\mathrm{Synth}_\sigma\) for every \(\sigma\) in some class.
The product of synthesis is an abstract constructor, so a synthesiser is a constructor that builds constructors. The contrast is Marletto’s (2015) programmable constructor P.
Where the design of \(p\) comes from is the question of the adaptive synthesis task (C5) in post I.5. Program synthesis is older (Manna & Waldinger 1980, Gulwani 2011). What we add is the reading as a task in Deutsch’s (2013) sense.
5.2 2. What can be confirmed
5.2.1 2.1 Verification
A synthesiser that is not correct by construction must verify candidates: decide \(\llbracket p \rrbracket \models \sigma\). Call a language acceptable if every standard numbering \(\varphi_e\) of the partial computable functions translates into it by a total computable map \(e \mapsto p_e\) with \(\llbracket p_e \rrbracket = \varphi_e\). In words: given any program text, one can compute a program of \(L\) that does the same. This is post 2’s effective receptivity (Definition 2.4), stated for a language. Push3 is acceptable if we ignore its clamped integers and bounded stacks.
Proposition I.3.3 (Verification is undecidable). Let \(L\) be acceptable and \(\sigma\) a specification that some partial computable function meets and some other does not. Then
\[V_\sigma = \{\, p \in L \mid \llbracket p \rrbracket \models \sigma \,\}\]
is undecidable. This covers every non-empty example specification.
Proof. A decider for \(V_\sigma\), composed with \(e \mapsto p_e\), would decide the index set of \(\sigma\), contrary to Rice’s (1953) theorem. An example specification with \(E \neq \emptyset\) is met by a finite table and not by the empty function. \(\square\)
Rice rules out a decision. A sharper theorem says what can be confirmed at all.
Proposition I.3.4 (Only finitely witnessed properties can be confirmed). Let \(L\) be acceptable.
- For an example specification, \(V_{\sigma_E}\) is semi-decidable: run \(p\) on each \(x_i\), and accept when all have halted with \(y_i\). The procedure never accepts a wrong program.
- If \(V_\sigma\) is semi-decidable by any procedure at all, then a function meets \(\sigma\) iff some finite subfunction of it does (the Rice–Shapiro theorem; Rice 1956, Shapiro 1956).
- Hence for a total function \(f\), the specification “equals \(f\) on every input” is not semi-decidable. No procedure confirms total correctness of arbitrary candidates.
Proof. Part 1 is immediate. Part 2 is the theorem, transported to \(L\) by the translation map as in Proposition I.3.3. For part 3, \(\{f\}\) contains \(f\) but no finite subfunction of \(f\), since those are not total. \(\square\)
- run p on each xᵢ, accept when all halt with yᵢ
- never accepts a wrong program
This is the precise content of “one has to run things”. Whatever method a verifier uses, it can only confirm what finitely many input-output pairs witness, and running is the one method that produces such pairs for every candidate. Total correctness, the property one wants, can only be tested, and a candidate may pass a finite test by luck.
Three things do not follow.
5.2.2 2.2 A decoder is a verifier
A decoder for a question \(P\) on a host \(H\) answers “does \(T(s)\) lie in \(P\)” correctly for every reachable state (post 2, Definition 2.3). Read the reachable states \(R_H\), with the dynamics \(\mathrm{exec}\), as a language whose programs are states.
Proposition I.3.5 (A decoder is a verifier). A decoder for \(P\) on \(H\) is exactly a decider of \(V_P\) for the language \((R_H, \mathrm{exec})\). The finite-task question “answers \(o\) to \(i\)” is the example specification \(\{i \mapsto o\}\), and for finite \(T_m\) “carries \(m\)” is the example specification given by \(T_m\).
Proof. Unfold the definitions. Post 2’s repertoire \(T(s)\) is the graph of \(\mathrm{exec}(s, \cdot)\), so \(T(s) \in P\) iff \(\llbracket s \rrbracket \models P\). \(\square\)
Corollary I.3.6 (Proposition 2.7 recovered). If \(H\) is effectively receptive, no non-trivial question has a decoder on \(H\).
Proof. Effective receptivity says \((R_H, \mathrm{exec})\) is acceptable, with the installation map as translation. Apply Proposition I.3.3 and then Proposition I.3.5. \(\square\)
So decoding a brain and verifying a candidate program are one problem.
The half of the decoder dichotomy (F7) that post 2 proved is the verification half of synthesis, applied to the host’s own language.
The word “acceptable” cannot be weakened to “universal”. A Friedberg numbering is universal, every partial computable function occurs in it exactly once, and it has a decidable non-trivial question (post 2, Section 4.2). What a decoder needs to be impossible is not that every program is present, but that programs can be translated in. The corollary also does not give the converse: in a total, non-universal language, example specifications are decidable, yet “outputs 0 everywhere” need not be (Proposition 2.13).
5.3 3. Evolution as synthesis
Natural selection can be cast as synthesis.
The environment always answers, because every organism dies: a lifetime is a timer, and a candidate that has not delivered by then is scored like a wrong one.
What Rice says about evolution is modest. Selection on genomes without vehicles would need a computable predictor of the environment’s score from the genome. If it were right for every genome of an acceptable genotype space, it would be a decider of the kind Proposition I.3.3 rules out. So evolution builds vehicles, science runs experiments and synthesis runs tests for one shared reason: no procedure that skips running is right about every candidate of an open space. Whether genotype spaces are acceptable is an untested premise.
5.4 4. Evidence: a criterion, and in closed spaces a source
Copying is the case of synthesis where the specification is another constructor’s repertoire, and the copier sees only part of it.
Definition I.3.7 (Copy task, fidelity). Let \(o\) be an original, a program or any other constructor, with repertoire \(T(o)\) (Definition I.1.6), and let \(\mu\) be a measure on tasks that weights them by importance. The copy task for \(o\) takes evidence \(e_o\), finitely many of \(o\)’s answers, and a receiver in a state \(x_0\) to the same evidence and a receiver that performs every task of \(o\):
\[\mathrm{Copy}_o = \{\, (e_o, x_0) \to (e_o, x) \,\} \quad \text{with} \quad T(o) \subseteq T(x) .\]
The fidelity of a copy \(x\) is the weighted share of the original’s tasks that it keeps:
\[\varphi(o, x) = \frac{\mu\big(T(o) \cap T(x)\big)}{\mu\big(T(o)\big)} .\]
A copy is faithful when \(\varphi = 1\). For a \(\mu\) with full support, that holds iff \(x\) performs the copy task. Fidelity measures loss only: a faithful copy can add tasks of its own. The copy task is synthesis (Definition I.3.2) for \(\sigma = T(o)\) with only \(\sigma_{e_o}\) in hand, so the copier is given a weaker specification than the one it has to meet. Post 1 takes the original to be a meme and the receiver a brain.
In generate-and-test the examples only filter. In an acceptable language that is forced.
Proposition I.3.8 (Examples never fix the class in an acceptable language). For every finite example set \(E\) and every partial computable \(g\) that extends \(E\), some program meets \(\sigma_E\) and computes \(g\). So the programs meeting \(\sigma_E\) fall into infinitely many classes.
Proof. Acceptability gives a program for every partial computable function, and infinitely many of them extend a finite table. \(\square\)
A synthesiser that returns one program from \(E\) therefore makes a choice that \(E\) does not make. The choice comes from the generator’s bias: size, enumeration order, a prior. For the function of culture memes, a copy is synthesis from examples, and this is post 1’s underdetermination (Proposition 1.11): the evidence \(e_m\) rejects reconstructions but does not produce them.
The contrast case is a closed language, where the knowledge sits in the language itself. The closed level of a meme is of this kind, and an ape meme is nothing but that level: the fixed behaviour alphabet is shared, so the receiver parses what it sees into it.
Proposition I.3.9 (Evidence as source in a closed language). In the polynomial language below, let the target have degree at most \(d\) and let \(E\) contain \(d+1\) examples at distinct inputs. Then every program of degree at most \(d\) that meets \(\sigma_E\) has the target’s class, and Lagrange interpolation computes such a program from \(E\) directly.
Proof. Two distinct polynomials of degree at most \(d\) agree on at most \(d\) points. \(\square\)
Here a fixed procedure turns examples into the right program, with no search and no test. The degree bound that makes this possible is not in the evidence but in the language. FlashFill works this way: Gulwani’s (2011) algorithm builds, for each example, a compact structure of all consistent programs of its string language, intersects these, and ranks the result.
- examples filter, never fix the class (Prop. I.3.8)
- the choice comes from the generator's bias
- d+1 examples fix a polynomial of degree ≤ d (Prop. I.3.9)
- the knowledge sits in the language
The language has one variable, two literals and three operators,
\[e ::= x \mid 1 \mid 2 \mid (e + e) \mid (e - e) \mid (e \times e),\]
and every program denotes an integer polynomial. The decoder computes that polynomial from the syntax without running anything. We synthesise the target \(x^3 - 2\) from two, three and four examples, twice: the enumerative synthesiser returns the smallest consistent program, the interpolating one the polynomial of lowest degree.
(def target [:- [:* :x [:* :x :x]] 2])(kind/table
(for [xs [[0 1] [0 1 2] [0 1 2 3]]]
(let [sigma (into {} (map (fn [x] [x (sy/dsl-eval target x)])) xs)
en (sy/enumerative-synth sigma 7)
ip (sy/interpolation-synth sigma)]
{:inputs xs
:enumerative (sy/normal-form (:program en))
:enumerative-correct? (sy/dsl-meets? (:program en) {:poly (sy/normal-form target)})
:interpolation (sy/normal-form ip)
:interpolation-correct? (sy/dsl-meets? ip {:poly (sy/normal-form target)})})))| inputs | enumerative | enumerative-correct? | interpolation | interpolation-correct? |
|---|---|---|---|---|
|
|
false | |
false |
|
|
true | |
false |
|
|
true | |
true |
Observation I.3.10 (no seed; deterministic). Normal forms map degree to coefficient. With two examples both synthesisers return the line \(3x - 2\). With three, the enumerative one finds \(x^3 - 2\), because it is small, and the interpolating one returns \(3x^2 - 2x - 2\), because it has the lowest degree. Both fit the evidence. The evidence did not choose between them; the bias did. With four examples both return the target, as Proposition I.3.9 says, and the decoder confirms it over all integers without running anything.
5.5 5. An open language: generate-and-test over Push3
Over Push3 no decoder exists, and the only verifier is an oracle that runs each candidate on the examples within a step budget (sys/perform from post I.1). It answers :undetermined when some run was cut off and none refuted the candidate. The generator draws flat Push programs of length 1 to 6 over thirteen symbols, including loops and the never-ending :exec_y, and never sees the examples.
We draw one pool of 10,000 candidates (seed 1), run each once on the example inputs 2, 3, 5 and 7 with 512 steps, and read off the verdict at smaller budgets. That is exact, since a run that halts within \(B\) steps halts at the same step under any larger budget.
(def examples-at [2 3 5 7])(defn examples-of [f] (into {} (map (fn [x] [x (f x)])) examples-at))(def pool (sy/random-pool 1 10000 sy/push-alphabet 6))(def tables (sy/tabulate-pool pool examples-at 512))(def step-budgets [2 8 32 128 512])(def targets
{"2n+1" #(inc (* 2 %))
"n²" #(* % %)
"n(n+1)" #(* % (inc %))
"n(n+1)/2" #(quot (* % (inc %)) 2)})(kind/table
(mapv #(update-vals % (fn [v] (if (double? v) (/ (Math/round (* 1000 v)) 1000.0) v)))
(sy/verdict-fractions tables (examples-of (targets "2n+1")) step-budgets)))| budget | accept | reject | undetermined |
|---|---|---|---|
| 2 | 0.0 | 0.14 | 0.86 |
| 8 | 0.001 | 0.672 | 0.327 |
| 32 | 0.001 | 0.797 | 0.202 |
| 128 | 0.001 | 0.8 | 0.199 |
| 512 | 0.001 | 0.8 | 0.199 |
(def held-out (range 0 16))(kind/table
(for [[nm f] targets]
(let [acc (keep (fn [[p t]] (when (= :accept (sy/verdict t (examples-of f) 512)) p))
(map vector pool tables))]
{:target nm
:accepted-at-512 (count acc)
:correct-but-undetermined-at-32 (count (sy/late-deciders pool tables (examples-of f) 32 512))
:accepted-but-wrong-on-0-to-15 (pr-str (vec (remove #(sy/generalises? (sy/run-table % held-out 4096) f held-out) acc)))})))| target | accepted-at-512 | correct-but-undetermined-at-32 | accepted-but-wrong-on-0-to-15 |
|---|---|---|---|
| 2n+1 | 11 | 1 | [] |
| n² | 42 | 4 | [(:integer_swap :in1 :exec_do*times :in1 :integer_*)] |
| n(n+1) | 6 | 0 | [] |
| n(n+1)/2 | 5 | 5 | [] |
Observation I.3.11 (seed 1, 10,000 candidates). For \(2n+1\), 86 % of the candidates are undetermined at 2 steps and about a fifth at 32 steps, and the share then stops moving. The plateau consists of loops, through :exec_y or like (:exec_dup :exec_dup), where each copy of :exec_dup copies the next one. Every correct program for \(n(n+1)/2\) in the pool needs more than 32 steps, so a budget of 32 makes a solvable problem look unsolvable, and from inside the run the two cases look the same. And one accepted program is wrong: (:integer_swap :in1 :exec_do*times :in1 :integer_*) computes \(n^2\) for \(n \ge 1\) and gives no output for \(n = 0\), which the examples did not include.
That is the contrast with Section 4. There the decoder settled every candidate on all inputs. Here the oracle settles candidates only on the examples, only within its budget, and leaves a remainder. (The fragment is finite and its loops can be recognised from the text, so this shows the oracle’s position, not Rice’s theorem itself.)
5.6 6. What synthesis says about persons
One might define an AGI as a system that performs synthesis on itself, universally: every pattern is a possible product of its own steps. It does not hold, because a laptop running a program enumerator does exactly that, and no condition on what a system can reach separates it from a person (post I.2, Proposition I.2.14).
- tests its patterns, never confirms them (Prop. I.3.4)
- what it installs is partly its own bias (Prop. I.3.8)
What synthesis does settle is one property every such system has. A system that synthesises its own patterns over an acceptable language can test them but never confirm them (Proposition I.3.4), and what it installs is always partly its own bias (Proposition I.3.8). It cannot certify any of its ideas as final. What it needs beyond that, criticism whose keeping depends on the world, is the subject of post I.6.
5.7 Summary
- Synthesis (C4) is the task \((\sigma, x_0) \to (\sigma, p)\) with \(\llbracket p \rrbracket \models \sigma\). Its product is the abstract constructor \(K_\sigma\).
- Over an acceptable language, verification is undecidable (Rice), and only properties witnessed by finitely many input-output pairs can be confirmed at all (Rice–Shapiro). That is the precise sense of “one has to run things”.
- A decoder is a verifier for the host’s own language, so the proved half of the decoder dichotomy (F7) is a corollary. It needs “acceptable”; “universal” is not enough (Friedberg).
- Evidence is a criterion in an acceptable language. In a closed one it can be the source, because the knowledge sits in the language.
- Universal self-synthesis does not define a person: an enumerator has it.
5.8 Open problems
- A quantitative Rice–Shapiro. How many examples does a given generator bias need before its acceptances generalise?
- Are genotype spaces acceptable? The argument that evolution must build vehicles rests on it.
5.9 References
- Deutsch, D. (2013). Constructor theory. Synthese 190(18), 4331–4359. arXiv:1210.7439. (not re-checked)
- Gulwani, S. (2011). Automating string processing in spreadsheets using input-output examples. Proc. 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011), 317–330. (verified: bibliographic data; the description of the algorithm as a version-space construction with intersection across examples and ranking was checked in secondary sources, not in the paper’s full text)
- Manna, Z. & Waldinger, R. (1980). A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems 2(1), 90–121. doi:10.1145/357084.357090. (verified: bibliographic data and abstract, synthesis as theorem proving)
- Marletto, C. (2015). Constructor theory of life. J. R. Soc. Interface 12(104): 20141226. arXiv:1407.0681. (not re-checked)
- Rice, H. G. (1953). Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society 74(2), 358–366. doi:10.1090/S0002-9947-1953-0053041-6. (verified: bibliographic data)
- Rice, H. G. (1956). On completely recursively enumerable classes and their key arrays. Journal of Symbolic Logic 21, 304–308. (verified: bibliographic data)
- Shapiro, N. (1956). Degrees of computability. Transactions of the American Mathematical Society 82, 281–299. (verified: bibliographic data. The Rice–Shapiro statement used in Proposition I.3.4 was checked in its standard textbook form, not in the two 1956 papers.)
source: book2/notebooks/meme_constructor/computing/post_i3_synthesis.clj