Semantic Uniqueness and Non-Uniqueness of Machine Realizations

1

Semantic realizations

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

Op ⁣:C⟶X\\mathrm{Op} \\colon \\mathcal{C} \\longrightarrow \\mathcal{X}Op:C⟶X

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

τ≤n ⁣:X⟶X≤n\\tau\{\\leq n} \\colon \\mathcal{X} \\longrightarrow \\mathcal{X}\{\\leq n}τ≤n​:X⟶X≤n​

denote the nnn\-truncation functor. Define the semantic realization functor

Qn:=τ≤n∘Op ⁣:C⟶X≤n.Q\n := \\tau\{\\leq n} \\circ \\mathrm{Op} \\colon \\mathcal{C} \\longrightarrow \\mathcal{X}\_{\\leq n}.Qn​:=τ≤n​∘Op:C⟶X≤n​.

Definition 1.1.

For M,N∈CM, N \\in \\mathcal{C}M,N∈C, write

M≡nNM \\equiv\_n NM≡n​N

if there is an equivalence

Qn(M)≃Qn(N)Q\_n(M) \\simeq Q\_n(N)Qn​(M)≃Qn​(N)

in X≤n\\mathcal{X}\_{\\leq n}X≤n​. We call ≡n\\equiv\_n≡n​ semantic equivalence at level nnn.

Thus ≡n\\equiv\_n≡n​ identifies realizations which are indistinguishable after passage to the chosen homotopy nnn\-type.

Definition 1.2.

The nnn\-semantic class of a realization MMM is the equivalence class

\[M\]n\[M\]\_n\[M\]n​

determined by Qn(M)Q\n(M)Qn​(M) in the appropriate homotopy category of X≤n\\mathcal{X}\{\\leq n}X≤n​.

The distinction between realization and semantic class is therefore

M∈C⟼\[M\]n∈π0(X≤n).M \\in \\mathcal{C} \\qquad \\longmapsto \\qquad \[M\]\n \\in \\pi\_0(\\mathcal{X}\{\\leq n}).M∈C⟼\[M\]n​∈π0​(X≤n​).

2

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 ⁣:C→DF \\colon \\mathcal{C} \\to \\mathcal{D}F:C→D

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

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

Equivalently, FFF reflects equivalences.

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

Let

Qn=τ≤n∘Op ⁣:C→X≤n.Q\n = \\tau\{\\leq n} \\circ \\mathrm{Op} \\colon \\mathcal{C} \\to \\mathcal{X}\_{\\leq n}.Qn​\=τ≤n​∘Op:C→X≤n​.

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

Qn(M)≃Qn(N)Q\_n(M) \\simeq Q\_n(N)Qn​(M)≃Qn​(N)

while

M≄N.M \\not\\simeq N.M≃N.

Then MMM and NNN determine the same semantic nnn\-class but are inequivalent realizations:

\[M\]n=\[N\]n,M≄N.\[M\]\_n = \[N\]\_n, \\qquad M \\not\\simeq N.\[M\]n​\=\[N\]n​,M≃N.

In particular, whenever QnQ\_nQn​ fails to reflect equivalences on the full subcategory of realizers under consideration, semantic uniqueness does not imply uniqueness of realization.

Proof. By definition,

Qn(M)≃Qn(N)Q\_n(M) \\simeq Q\_n(N)Qn​(M)≃Qn​(N)

means precisely that MMM and NNN are semantically equivalent at level nnn, hence

\[M\]n=\[N\]n.\[M\]\_n = \[N\]\_n.\[M\]n​\=\[N\]n​.

The hypothesis

M≄NM \\not\\simeq NM≃N

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

If QnQ\_nQn​ 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 QnQ\_nQn​ which does not arise from an equivalence before applying QnQ\_nQn​.

Remark 2.3.

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

M≄NM \\not\\simeq NM≃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.

3

Why truncation permits non-uniqueness

The preceding phenomenon is intrinsic to truncation.

Proposition 3.1.

For n≥−1n \\geq -1n≥−1, the truncation functor

τ≤n ⁣:X→X≤n\\tau\{\\leq n} \\colon \\mathcal{X} \\to \\mathcal{X}\{\\leq n}τ≤n​:X→X≤n​

does not in general reflect equivalences.

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

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

The canonical map

Sn+1⟶∗S^{n+1} \\longrightarrow \*Sn+1⟶∗

induces an equivalence after nnn\-truncation:

τ≤nSn+1≃τ≤n∗≃∗.\\tau\{\\leq n} S^{n+1} \\simeq \\tau\{\\leq n} \ \\simeq \.τ≤n​Sn+1≃τ≤n​∗≃∗.

However,

Sn+1≄∗S^{n+1} \\not\\simeq \*Sn+1≃∗

because

πn+1(Sn+1)≅Z,πn+1(∗)=0.\\pi\{n+1}(S^{n+1}) \\cong \\mathbb{Z}, \\qquad \\pi\{n+1}(\*) = 0.πn+1​(Sn+1)≅Z,πn+1​(∗)\=0.

Hence τ≤n\\tau\_{\\leq n}τ≤n​ does not reflect equivalences.

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

τ≤nX≃τ≤nY\\tau\{\\leq n} X \\simeq \\tau\{\\leq n} Yτ≤n​X≃τ≤n​Y

does not imply

X≃Y.X \\simeq Y.X≃Y.

4

Realizers of a finite specification

Let PPP be a finite presentation of an operation. Write

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

for the full ∞\\infty∞\-subcategory of realizations of PPP. Assume that the specification determines a semantic nnn\-type

pP∈X≤np\P \\in \\mathcal{X}\{\\leq n}pP​∈X≤n​

such that every realization of PPP satisfies

Qn(M)≃pP,M∈Real(P).Q\_n(M) \\simeq p\_P, \\qquad M \\in \\mathrm{Real}(P).Qn​(M)≃pP​,M∈Real(P).

Theorem 4.1 (Uniqueness of the semantic class).

Under the preceding hypotheses, PPP determines a unique semantic operation class

\[P\]n:=pP,\[P\]\_n := p\_P,\[P\]n​:=pP​,

in the sense that

∀ M,N∈Real(P),Qn(M)≃Qn(N).\\forall\\, M, N \\in \\mathrm{Real}(P), \\qquad Q\_n(M) \\simeq Q\_n(N).∀M,N∈Real(P),Qn​(M)≃Qn​(N).

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

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

Qn(M)≃pP≃Qn(N),Q\_n(M) \\simeq p\_P \\simeq Q\_n(N),Qn​(M)≃pP​≃Qn​(N),

and therefore

Qn(M)≃Qn(N).Q\_n(M) \\simeq Q\_n(N).Qn​(M)≃Qn​(N).

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

M≃N.M \\simeq N.M≃N.

Such an assertion would require additional hypotheses, for example conservativity of QnQ\_nQn​ on Real(P)\\mathrm{Real}(P)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∈Real(P)M, N \\in \\mathrm{Real}(P)M,N∈Real(P)

such that

M≄N.M \\not\\simeq N.M≃N.

Then

Qn(M)≃Qn(N)≃\[P\]n,Q\_n(M) \\simeq Q\_n(N) \\simeq \[P\]\_n,Qn​(M)≃Qn​(N)≃\[P\]n​,

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

5

Traces and operational classes

Let

Trace\\mathrm{Trace}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

tr ⁣:C→Trace\\mathrm{tr} \\colon \\mathcal{C} \\to \\mathrm{Trace}tr:C→Trace

and a semantic reification map

class⁡n ⁣:Trace⟶X≤n\\operatorname{class}\n \\colon \\mathrm{Trace} \\longrightarrow \\mathcal{X}\{\\leq n}classn​:Trace⟶X≤n​

such that

Qn=class⁡n∘tr.Q\_n = \\operatorname{class}\_n \\circ \\mathrm{tr}.Qn​\=classn​∘tr.

Thus a realized operation is represented by the composite

M↦ tr tr(M)↦ class⁡n \[M\]n.M \\xmapsto{\\ \\mathrm{tr}\\ } \\mathrm{tr}(M) \\xmapsto{\\ \\operatorname{class}\_n\\ } \[M\]\_n.M tr ​tr(M) classn​ ​\[M\]n​.

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

class⁡n(tr(M))≃class⁡n(tr(N))\\operatorname{class}\_n(\\mathrm{tr}(M)) \\simeq \\operatorname{class}\_n(\\mathrm{tr}(N))classn​(tr(M))≃classn​(tr(N))

does not entail

M≃NM \\simeq NM≃N

unless the composite

Qn=class⁡n∘trQ\_n = \\operatorname{class}\_n \\circ \\mathrm{tr}Qn​\=classn​∘tr

is conservative on the realizers under consideration.

6

Cofinality of realizers

Let III be a directed index category and let

M ⁣:I→CM \\colon I \\to \\mathcal{C}M:I→C

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

∀R∈Real(P) ∃i∈Isuch thatQn(Mi)≃Qn(R).\\forall R \\in \\mathrm{Real}(P)\\; \\exists i \\in I \\quad\\text{such that}\\quad Q\_n(M\_i) \\simeq Q\_n(R).∀R∈Real(P)∃i∈Isuch thatQn​(Mi​)≃Qn​(R).

Theorem 6.1 (Eventual realization up to semantic type).

If Real(P)≠∅\\mathrm{Real}(P) \\neq \\varnothingReal(P)\=∅ and the machine timeline is nnn\-cofinal in Real(P)\\mathrm{Real}(P)Real(P), then there exists i∈Ii \\in Ii∈I such that

Qn(Mi)≃\[P\]n.Q\_n(M\_i) \\simeq \[P\]\_n.Qn​(Mi​)≃\[P\]n​.

Proof. Choose any

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

which exists by assumption. Since the timeline is nnn\-cofinal, there is an i∈Ii \\in Ii∈I satisfying

Qn(Mi)≃Qn(R).Q\_n(M\_i) \\simeq Q\_n(R).Qn​(Mi​)≃Qn​(R).

Since RRR realizes PPP,

Qn(R)≃\[P\]n.Q\_n(R) \\simeq \[P\]\_n.Qn​(R)≃\[P\]n​.

Therefore

Qn(Mi)≃\[P\]n.Q\_n(M\_i) \\simeq \[P\]\_n.Qn​(Mi​)≃\[P\]n​.

Hence stage iii realizes the specification up to the chosen homotopy nnn\-type.

7

Recursive self-improvement

Let

On:=τ≤nO\\mathcal{O}\n := \\tau\{\\leq n}\\mathcal{O}On​:=τ≤n​O

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

F ⁣:On→On.F \\colon \\mathcal{O}\_n \\to \\mathcal{O}\_n.F:On​→On​.

For an initial semantic operation

o0∈On,o\_0 \\in \\mathcal{O}\_n,o0​∈On​,

define recursively

ok+1:=F(ok).o\_{k+1} := F(o\_k).ok+1​:=F(ok​).

Then

ok=Fk(o0).o\_k = F^k(o\_0).ok​\=Fk(o0​).

A family of machines (Mk)k≥0(M\k)\{k \\geq 0}(Mk​)k≥0​ realizes this recursive process up to semantic level nnn precisely when

Qn(Mk)≃okQ\_n(M\_k) \\simeq o\_kQn​(Mk​)≃ok​

for all kkk. There is no requirement that

Mk+1≃Mk.M\_{k+1} \\simeq M\_k.Mk+1​≃Mk​.

Indeed, if the fibers of QnQ\_nQn​ are nontrivial, there may exist many inequivalent realizers satisfying

Qn(Mk)≃ok.Q\_n(M\_k) \\simeq o\_k.Qn​(Mk​)≃ok​.

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

On→ F On,\\mathcal{O}\_n \\xrightarrow{\\ F\\ } \\mathcal{O}\_n,On​ F ​On​,

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

8

Main conclusion

The preceding results establish the following separation:

finite presentation⇓semantic operation class \[P\]n⇓possibly many inequivalent realizers M\\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}}finite presentation⇓semantic operation class \[P\]n​⇓possibly many inequivalent realizers M​​

More precisely,

M⟼Qn(M)M \\longmapsto Q\_n(M)M⟼Qn​(M)

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

Qn(M)≃Qn(N)⇏M≃N.Q\_n(M) \\simeq Q\_n(N) \\quad\\not\\Rightarrow\\quad M \\simeq N.Qn​(M)≃Qn​(N)⇒M≃N.

Hence the appropriate uniqueness statement is

the operation class is unique up to nnn\-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.