Semantic Uniqueness and Non-Uniqueness of Machine Realizations

Semantic realizations

Let $\mathcal{C}$ be an $\infty$ -category whose objects are computational realizations (machines, programs, agents, or other executable systems), and let

\mathrm{Op} \colon \mathcal{C} \longrightarrow \mathcal{X}

be an operational semantics into an $\infty$ -topos $\mathcal{X}$ . Fix $n \geq -2$ . Let

\tau_{\leq n} \colon \mathcal{X} \longrightarrow \mathcal{X}_{\leq n}

denote the $n$ -truncation functor. Define the semantic realization functor

Q_n := \tau_{\leq n} \circ \mathrm{Op} \colon \mathcal{C} \longrightarrow \mathcal{X}_{\leq n}.

Definition 1.1.

For $M, N \in \mathcal{C}$ , write

M \equiv_n N

if there is an equivalence

Q_n(M) \simeq Q_n(N)

in $\mathcal{X}_{\leq n}$ . We call $\equiv_n$ semantic equivalence at level $n$ .

Thus $\equiv_n$ identifies realizations which are indistinguishable after passage to the chosen homotopy $n$ -type.

Definition 1.2.

The $n$ -semantic class of a realization $M$ is the equivalence class

[M]_n

determined by $Q_n(M)$ in the appropriate homotopy category of $\mathcal{X}_{\leq n}$ .

The distinction between realization and semantic class is therefore

M \in \mathcal{C} \qquad \longmapsto \qquad [M]_n \in \pi_0(\mathcal{X}_{\leq n}).

Non-uniqueness of realizations

The essential mathematical point is that truncation is generally a localization and therefore need not be conservative.

Definition 2.1.

A functor

F \colon \mathcal{C} \to \mathcal{D}

is conservative if, for every morphism $f$ of $\mathcal{C}$ ,

F(f)\text{ is an equivalence} \quad\Longrightarrow\quad f\text{ is an equivalence}.

Equivalently, $F$ reflects equivalences.

Theorem 2.2 (Semantic equivalence does not imply realization uniqueness).

Let

Q_n = \tau_{\leq n} \circ \mathrm{Op} \colon \mathcal{C} \to \mathcal{X}_{\leq n}.

Suppose there exist realizations $M, N \in \mathcal{C}$ such that

Q_n(M) \simeq Q_n(N)

while

M \not\simeq N.

Then $M$ and $N$ determine the same semantic $n$ -class but are inequivalent realizations:

[M]_n = [N]_n, \qquad M \not\simeq N.

In particular, whenever $Q_n$ fails to reflect equivalences on the full subcategory of realizers under consideration, semantic uniqueness does not imply uniqueness of realization.

Proof. By definition,

Q_n(M) \simeq Q_n(N)

means precisely that $M$ and $N$ are semantically equivalent at level $n$ , hence

[M]_n = [N]_n.

The hypothesis

M \not\simeq N

states that the realizations themselves are not equivalent in $\mathcal{C}$ . Thus the same object of the localized semantic category $\mathcal{X}_{\leq n}$ has at least two inequivalent realizations in $\mathcal{C}$ . Hence the semantic class is unique while its realization is not.

If $Q_n$ is non-conservative on the relevant class of realizers, such a pair can occur by definition of non-conservativity: there exists an equivalence after applying $Q_n$ which does not arise from an equivalence before applying $Q_n$ .

Remark 2.3.

The conclusion is stronger than the statement that presentations need not be literally equal. It permits

M \not\simeq N

even in the homotopy theory of realizations. Thus the distinction is not merely syntactic. It can persist after quotienting the category of machines by its own equivalences.

Why truncation permits non-uniqueness

The preceding phenomenon is intrinsic to truncation.

Proposition 3.1.

For $n \geq -1$ , the truncation functor

\tau_{\leq n} \colon \mathcal{X} \to \mathcal{X}_{\leq n}

does not in general reflect equivalences.

Proof. Consider, for example, spaces in the $\infty$ -category $\mathcal{S}$ . Let

X = S^{n+1}, \qquad Y = *.

The canonical map

S^{n+1} \longrightarrow *

induces an equivalence after $n$ -truncation:

\tau_{\leq n} S^{n+1} \simeq \tau_{\leq n} * \simeq *.

However,

S^{n+1} \not\simeq *

because

\pi_{n+1}(S^{n+1}) \cong \mathbb{Z}, \qquad \pi_{n+1}(*) = 0.

Hence $\tau_{\leq n}$ does not reflect equivalences.

Consequently, equality in the localized semantics forgets all homotopy information above degree $n$ . In particular,

\tau_{\leq n} X \simeq \tau_{\leq n} Y

does not imply

X \simeq Y.

Realizers of a finite specification

Let $P$ be a finite presentation of an operation. Write

\mathrm{Real}(P) \subseteq \mathcal{C}

for the full $\infty$ -subcategory of realizations of $P$ . Assume that the specification determines a semantic $n$ -type

p_P \in \mathcal{X}_{\leq n}

such that every realization of $P$ satisfies

Q_n(M) \simeq p_P, \qquad M \in \mathrm{Real}(P).

Theorem 4.1 (Uniqueness of the semantic class).

Under the preceding hypotheses, $P$ determines a unique semantic operation class

[P]_n := p_P,

in the sense that

\forall\, M, N \in \mathrm{Real}(P), \qquad Q_n(M) \simeq Q_n(N).

This does not imply that $\mathrm{Real}(P)$ is contractible, nor even that all of its objects are equivalent.

Proof. For $M, N \in \mathrm{Real}(P)$ ,

Q_n(M) \simeq p_P \simeq Q_n(N),

and therefore

Q_n(M) \simeq Q_n(N).

Thus all realizers determine the same semantic $n$ -class. No assertion has been made that

M \simeq N.

Such an assertion would require additional hypotheses, for example conservativity of $Q_n$ on $\mathrm{Real}(P)$ . Hence uniqueness of the semantic class does not entail uniqueness of the realization category.

Corollary 4.2 (Unique class, non-unique machines).

Suppose there exist

M, N \in \mathrm{Real}(P)

such that

M \not\simeq N.

Then

Q_n(M) \simeq Q_n(N) \simeq [P]_n,

so the specification has a unique semantic operation class but at least two inequivalent machine realizations.

Traces and operational classes

Let

\mathrm{Trace}

denote the space of executable traces. A trace is not treated merely as an external observation; rather, assume the operational semantics provides a trace map

\mathrm{tr} \colon \mathcal{C} \to \mathrm{Trace}

and a semantic reification map

\operatorname{class}_n \colon \mathrm{Trace} \longrightarrow \mathcal{X}_{\leq n}

such that

Q_n = \operatorname{class}_n \circ \mathrm{tr}.

Thus a realized operation is represented by the composite

M \xmapsto{\ \mathrm{tr}\ } \mathrm{tr}(M) \xmapsto{\ \operatorname{class}_n\ } [M]_n.

The trace is therefore an operational object, while the map $\operatorname{class}_n$ performs the passage from an executable trace to its semantic operation class. In particular,

\operatorname{class}_n(\mathrm{tr}(M)) \simeq \operatorname{class}_n(\mathrm{tr}(N))

does not entail

M \simeq N

unless the composite

Q_n = \operatorname{class}_n \circ \mathrm{tr}

is conservative on the realizers under consideration.

Cofinality of realizers

Let $I$ be a directed index category and let

M \colon I \to \mathcal{C}

be a timeline of machines. Suppose this timeline is $n$ -cofinal in $\mathrm{Real}(P)$ , meaning that

\forall R \in \mathrm{Real}(P)\; \exists i \in I \quad\text{such that}\quad Q_n(M_i) \simeq Q_n(R).

Theorem 6.1 (Eventual realization up to semantic type).

If $\mathrm{Real}(P) \neq \varnothing$ and the machine timeline is $n$ -cofinal in $\mathrm{Real}(P)$ , then there exists $i \in I$ such that

Q_n(M_i) \simeq [P]_n.

Proof. Choose any

R \in \mathrm{Real}(P),

which exists by assumption. Since the timeline is $n$ -cofinal, there is an $i \in I$ satisfying

Q_n(M_i) \simeq Q_n(R).

Since $R$ realizes $P$ ,

Q_n(R) \simeq [P]_n.

Therefore

Q_n(M_i) \simeq [P]_n.

Hence stage $i$ realizes the specification up to the chosen homotopy $n$ -type.

Recursive self-improvement

Let

\mathcal{O}_n := \tau_{\leq n}\mathcal{O}

be the $n$ -truncated $\infty$ -type of agent operations. Suppose self-improvement induces an internal endomorphism

F \colon \mathcal{O}_n \to \mathcal{O}_n.

For an initial semantic operation

o_0 \in \mathcal{O}_n,

define recursively

o_{k+1} := F(o_k).

Then

o_k = F^k(o_0).

A family of machines $(M_k)_{k \geq 0}$ realizes this recursive process up to semantic level $n$ precisely when

Q_n(M_k) \simeq o_k

for all $k$ . There is no requirement that

M_{k+1} \simeq M_k.

Indeed, if the fibers of $Q_n$ are nontrivial, there may exist many inequivalent realizers satisfying

Q_n(M_k) \simeq o_k.

Thus recursive self-improvement is naturally an operation on semantic classes:

\mathcal{O}_n \xrightarrow{\ F\ } \mathcal{O}_n,

rather than necessarily an endomorphism of a uniquely determined machine presentation.

Main conclusion

The preceding results establish the following separation:

\boxed{\begin{array}{c} \text{finite presentation} \\[2mm] \Downarrow \\[2mm] \text{semantic operation class }[P]_n \\[2mm] \Downarrow \\[2mm] \text{possibly many inequivalent realizers }M \end{array}}

More precisely,

M \longmapsto Q_n(M)

is a semantic localization. If it is non-conservative on the relevant realization category, then

Q_n(M) \simeq Q_n(N) \quad\not\Rightarrow\quad M \simeq N.

Hence the appropriate uniqueness statement is

the operation class is unique up to

n

-equivalence, whereas its machine realization need not be unique.

The non-uniqueness is therefore not an artifact of comparing different syntactic presentations. It is a structural consequence of passing from realizations to a truncated semantic localization.

Typeset in the browser with KaTeX. The wording follows the source note; statements are numbered within each section, as in the original.