This post was written as part of the 2026 Research Fellowship for Dovetail Research. A massive thanks to Alex for directing this project, to Jose and Alfred for feedback and insights on this work, and to all the other fellows with whom wonderful discussions led to new ideas.
This work was funded by the Advanced Research + Invention Agency (ARIA) through project code MSAI-SE01-P005.
Declaration The proofs in this post have been formalised with assistance from Claude (Fable 5.0 & Opus 4.8). The ideas, writing, and proof verification have been done by me, a human.
TL;DR
Question Which features of an agent's world model are about the world itself, and which are consequences of the modelling choice?
Setting This project builds from the intuition of Wentworth's Natural Abstraction Hypothesis (NAH) on converging abstractions to propose a test for naturality: measuring the extent to which a given abstraction persists after changing the representation or model of the world could indicate just how natural it is.
Computability theory is a setting in which 'remodelling' is easy to construct and check, since translations between models are well-studied. We treat models of computation as a substitute for world models, congruences as abstractions, and translation maps between models as changes in representation.
Result 1 An abstraction that survives every change of representation is behavioural equivalence or coarser. (Too coarse to say anything about the model's internal structure.[1])
Result 2 An abstraction finer than behavioural equivalence can survive translation under three conditions:
there is no way of building a bigger program around a smaller one in the target model that forces two translated, previously-unmerged programs together.
Introduction
Most of us are familiar with the scenario of an agent that is "well-behaved" in its training environment, but when released in a new context (as in, one outside the tested distribution), it begins to exhibit unintended (and sometimes undesirable) behaviour. Testing behaviour alone can be blind to the internal variations in modelling that might yield these unexpected outputs, and abstractions[3] are one part of that internal story. As hidden differences in abstractions can surface as a differences in behaviour, understanding abstractions is a correspondingly important component of understanding alignment.
So, here's the problem. Two models, seeking to describe the same world, could opt for wildly different abstractions. These could constitute accurate reflections of structures in the world, or, alternatively, they might be artifacts of the choice of representation, or reflective of the modeller's perspective.
There needs to be some way to tell these apart.According to NAH, if an abstraction is "natural", then different observers should converge on it – that is, a natural abstraction will tend to show up across a variety of models.
That intuition, then, suggests a test for "naturality": which abstractions are preserved when you change how a world model is represented?
Given a translation and a coarse-graining , is there a matching abstraction on the target side?
To make that question precise enough to support investigation, I trade NAH's statistical setting for a more exact and deterministic one. If the framework presented here is correct, and if it carries over beyond the computational setting, it suggests that "naturality" might be better understood as a measure of how many (or what proportion of) re-modellings a given abstraction will survive.[4]
Related Work
Erik Jenner's research agenda proposes abstractions of computations as a tractable formal setting, and develops a framework for abstracting a single computation. In particular, Jenner notes that his framework says nothing about the encoding or representation of a computation, and leaves open whether it should be handled inside the framework or separately. This post can be seen as engaging with this idea, in which abstractions are held fixed and the representation varies.
Models of Computation
The task of translating between different models is rather unwieldy, especially as we start to consider all possible structures they might adopt. World models can range from automata to probabilistic or causal models, to neural representations and beyond, each residing in vastly different domains and exhibiting distinctive features. Transitioning between them requires some way to bridge these diverging descriptions.
It is therefore sensible to consider models for which such translations are straightforward to construct, or, even better, already exist. As foretold in the introduction, a candidate class of models can be found in computability theory.[5]
Models of computation are well-suited to this context.[6] The challenge of translation isn't a new one, and, indeed, the original strategy (going back to the 1930s) was to construct 'naturalmappings' between various models by hand.[7] The existence of translation maps between Turing-complete models turns out to be guaranteed[8] by a general theorem from computability theory. This is sufficient for us to get started.
Translating From One Model to Another
To understand what translations maps need to look like, we first need to fix what we mean by a 'model of computation'. Every model we'll consider decomposes into two essential parts:
The programs are just a set of static, finite objects. We assume nothing about their internal structure. The second component ("a way of running them") can be thought of as a partial function:
which takes a program together with some context[9] (an input, or a test to perform on it) and, if the program halts on that observable, returns the behaviour type(the observable or output) it exhibits; otherwise it returns nothing.
Thus, a computational system (or computational substrate, if you will) is a quadruple:
The following examples demonstrate how various Turing-complete models fit into the above definition.
Examples
These are not unique characterisations (e.g. you can define the function or the behaviour differently from what is shown here), and there might be aspects of models that are not represented (e.g. configurations of a computation). Rather, this definition is meant to capture what is common between them, and the essence of what makes them computational.
Model
Programs
"Running It"
Behaviour
Turing Machines
state transition tables
feed input and run transitions
contents of the tape at halting (or non-terminating)
-Calculus
closed -terms
apply input (optional) and β-reduction
halt at normal form (or non-terminating)
General Recursive Functions
closed syntactic definitions built from // by composition, primitive recursion, & μ-recursion
unwind the recursive definition on input
output natural number (or tuple), when defined
Cellular Automata
rule (e.g. Rule 150, Game of Life) + initial configuration
apply the rule synchronously to a given initial configuration, evolve forward
initial config evolution
(read off designated halting-observable)
JavaScript
JS source code
JS engine's usual call stack, memory heap, and event loop
return value / final state / console output
This is an operational view of computation,[10] and it is a characterisation that is general enough to describe any computational model on the table. Moreover, it predetermines what a translation must be: a map sending programs to programs that respects (under some agreed correspondence between observables) what "running them" means.
Definition. A translation is a map between computational substrates[11] that preserves program correctness, i.e.,:
for all admissible tests .
In other words, the translation must, minimally, ensure the output program does the same job as the input.[12]
The phrase "corresponds to" is deliberately left open: it stands in for whatever notion of matching outcomes that fits the two models' structure, and the specific choice has little consequence in the work to come. Two things must hold:
the correspondence is fixed once and shared across the entire class of translations from to under consideration, and
distinct source behaviours map to distinct target ones,[13] non-termination to non-termination.
Translations need be neither injective (distinct programs in can translate to the same point in ) nor surjective (there will be native programs in that do not have a counterpart in ).
Definition. Translation maps are not unique, so we can refer to the class of all correct translations, call it , between two substrates, and .
Abstractions
Abstraction, at its simplest, is a choice about which (features of) programs to treat as "the same" (this choice encapsulates what the abstraction forgets about distinct programs). The minimal structure capturing "which things get merged" is an equivalence relation,[14] which we will use to model the coarse-graining process here.
The central organising structure in this post is the lattice [15]of all equivalence relations (or partitions) on the set of all programs , ordered by ('finer than'). Each point is a different partition of , with every program appearing exactly once per point.
An approximate[16] representation of a sublattice of .
At the top, the trivial relation (a single partition) cannot distinguish between any program. At the bottom, the finest relation is the identity relation in which each program is in a partition of its own.
Not all equivalence relations make good abstractions – most merge elements no reasonable observer would treat as interchangeable.[17] We work with the full lattice anyway: a result proved for all of applies automatically to any restricted class defined later, so nothing is lost by deferring that choice.
Behavioural Equivalence
Definition. Two programs are behaviourally equivalent[18] () if and only if their behaviours agree[19] on all inputs:
for
Zooming in, a single point of this lattice is the set of all (infinitely many) programs. By the padding lemma[20], every partition defined by behavioural equivalence also contains infinitely many programs.
The relations that sit above (coarser than) behavioural equivalence () lump together programs with distinct behaviour. Here, we care more about relations strictly finer than behavioural equivalence which can distinguish behaviourally identical programs on the basis of internal structure.[21]
The blue area indicates (approximately) the region of the lattice that is most relevant to this investigation.
One Program at a Time
Another lattice worth studying in its own right is one that organises the coarse-grainings of a single program .
Example.
If is a deterministic finite automaton (DFA)[22] with two states never distinguishable by any input, then a coarse-graining might merge them into one state without changing 's behaviour.
This is an example of standard DFA minimisation. Quotienting by gives , the minimised automaton, and the set of all quotients can be ordered into a lattice.
This local lattice connects to : a relation "sees" the abstraction of when it places and in the same partition class.[23] Note that the local lattice is not a sublattice of the global lattice, so its structure doesn't transfer. Instead we track a program's coarse-grainings by how it relates to other programs across different points of , which is the more general question that is central to this project.
Which Abstractions are Model-Independent?
Recall our original question: which abstractions are preserved when changing how the world model is represented? Or, equivalently, which coarse-grainings are model-independent?
Placing this question within our mathematical framework:
Given a relation on , can it be recovered by some on ?
Definition. The pullback[24] of a relation on along a translation map is the set defined as follows:
The pullback is the relation in in which pairs of programs are mapped to the programs related by in under a specific translation .
If the pullback is equal to , then our question is answered. Fixing a single τ gives a complete answer:
If for some , then reflexivity of forces regardless of choice of The relation is unrecoverable.
:
If , define on the image of by relating and exactly when . This is well-defined precisely because never merges across -classes. Let everything outside the image be its own singleton class. Then , so is recovered.
Recoverability from one only shows that survives that particular encoding, without saying anything about why that rather than another. This condition is 'cheap' since can be chosen freely.
To remove the arbitrariness, we ask instead whether can be recovered no matter which correct translation was used:
Definition. For some class of correct translations , a relation on is -invariant if there is a single on that satisfies
for every .
This is our question is answered for the whole class . We take this as our working formalisation for "model-independent".[26] This definition restricts to a single in to ensure it is intrinsic to , and not freshly reverse-engineered for each translation.
Checking -invariance one candidate at a time would leave us iterating over an unbounded search. Instead of testing relations one by one, we can ask what's forced, no matter which we start with. That gives us a single, canonical relation to measure everything else against.
Definition. The free relation, , with respect to is the equivalence relation on generated by all pairs of programs such that for some .
The free relation collects all the pairs of programs in that -translations send to the same program. We will see that any -invariant abstraction is therefore forced to merge these pairs.
A translation can't un-identify programs it's already merged, so the pullback is never finer than what itself collapses. This holds for every simultaneously, so whatever we're testing, it's forced to contain every pair that contains.
Lemma I. Every -invariant relation is coarser than the free relation with respect to .
Proof.
Let be a -invariant relation on , witnessed by on with for all .
For a generating pair with , reflexivity of gives , so . This holds for every generator regardless of which produced it, since is fixed.
So, contains every generator of , and minimality of as the smallest equivalence relation containing them gives .
The grey area denotes a -invariant relation on Programs in the free relation can not be distinguished from one another after translation, so will always appear in the same equivalence class in the pullback.
So, is a lower bound on any -invariant abstraction. We can compute the free relation explicitly for the largest class of (correct) translations, .[27]
Lemma II. The free relation (with respect to ) is behavioural equivalence .
Proof.
If for correct , both must correspond to the same target value for any test. So, . Every generator of is already behaviourally related, so .
If , take any correct and redirect it at : set leaving elsewhere. Correctness survives, since and behave identically, so . Hence is a generator of , giving .
The direction says no correct translation merges behaviourally distinct programs: some test would separate them, and correctness preserves that. The direction says for any behaviourally-identical-but-distinct pair, some correct translation does merge them, after which nothing in can recover the distinction.
Theorem. A relation is translation-invariant if and only if it is behavioural equivalence () or coarser.
Proof.
(): By Lemma I, is coarser than . By Lemma II, . So, is finer than .
(): Assume is finer than .
Then -relatedness depends only on the behaviour class, not which representation is picked: if and , then transitivity through gives .
So descends to a well-defined relation on behaviour classes, via .
Define on by pulling back through behaviour: for , set iff the behaviour classes of any (equivalently, every) -preimages of and are -related. This is well-defined since any two correct translation agree on behaviour.
Then, for every , we have , simultaneously for all of . So, is -invariant.
Question. Given a relation on , can it be recovered by some on , regardless of which translation you used to get there?
Answer. Exactly when the relation is behavioural equivalence or coarser.
This is unsurprising: correctness was defined as preserving behaviour, so behaviour is what survives. It is worth considering whether this question actually aligns with what we want. Two things don't fit.
The answer describes the region of the lattice at or above behavioural equivalence. But our interests (mostly) don't live there. We want to understand the abstractions of individual models, which are relations that distinguish programs that behave identically, but identify pairs based on shared internal structure,[28] which is outside the scope of this result.
-invariance is a statement about every correct translation in at once. In theory, is enormous, and most of it contains translations that no one would ever build.[29] Even setting the first problem aside, knowing that some abstraction survives all of that tells us something very strong in aggregate, but it ignores whatever specific translations we actually have at hand.
Both problems suggest that we might be better served by an alternative approach. Previously, we removed arbitrariness in the choice of translation by considering all translations simultaneously. We can also remove arbitrariness by choosing a specific translation.
Under which conditions will a given abstraction transport to another model?
There's a trivial solution to this question: we can simply build a translation that respects any abstraction we like, by construction. Though true, this says nothing interesting about the translations or abstractions we might want to work with, and breaks down the moment we want to compose several coarse-graining maps together.
Besides, we're rarely in a position to invent from scratch[30], not to mention the number of existing translations present in the literature. It would be ambitious to reinvent translations every time we study new (or a different combination of) coarse-grainings.
Let us proceed by choosing a particular translation .
Motivating Example. An abstraction that coarse-grains a program's internal compositional structure could be preserved by some translation that keeps this structure visible on the target side.
The standard translation is built by structural recursion: each basic function gets a Turing machine gadget, and each combination gets a way of wiring gadgets together. For instance, composition becomes "run one machine, feed its output to the next." The translated program's wiring mirrors the source's build tree, as the figure shows. That mirrored shape is what makes a translation a good candidate for preserving abstractions.
Picture This
We can draw the whole setup as follows:
and are two models of computation, and is a translation between them.
is the formal encoding (the equivalence relation) of the abstraction we fixed on
it is the set of pairs that identifies.
is what you get by quotienting by through quotienting map
it collapses every -related pair into a single point (the partition).
is the induced translation map between equivalence classes in the quotiented sets.
The goal is to construct a corresponding set on the target side that respects the structure abstracted by . In other words, must send -related pairs in to some single, consistent equivalence class in , rather than scattering them. The square commutes exactly when respects this coarse-graining.
Forced Congruences
Not all equivalence relations make good abstractions, but we can sidestep that problem here by assuming represents a coarse-graining worth studying. For the rest of this section, I restrict to congruences. These areequivalence relations that also respect operations, which, in our case, means how programs are built, not just what they compute.[31] We make this precise via contexts in the next section, but for now, the idea is simple: identified programs should stay identified when the same larger program is built around each of them.
Our question can now be framed in the language of universal algebra:
Given a congruence on and a translation , what is the smallest congruence on that is coarser than ?
To begin, translate every pair that the relation merges:
Then take the smallest congruence on containing all of those pairs:
This is the forced congruence.[32] Two things to check:
It always exists.
The set of all congruences on coarser than is non-empty: e.g., the full/universal relation is trivially a congruence and is trivially coarser .
An intersection of congruences is again a congruence. So, , defined as the intersection of all congruences coarser than , is guaranteed to exist and be the smallest such congruence.
It is always non-empty.
Every congruence is reflexive by definition, therefore, must contain the diagonal .
is well-defined, and the main thing to understand is whether closing under the congruence axioms drags in pairs that it shouldn't. In other words, does stay faithful to , or blow up and identify everything?
We check this by walking through which pairs are added under closure:
Symmetry – trivial, no need to add anything: if , then .
Reflexivity – adds all[34] the identity pairs for all .
Trivial on , but not necessarily on : if for some , the single pair already pulls back to .
So the kernel condition (below) is forced by reflexivity, and transitivity is what turns that one stray pair into a cascade of identifications.
Transitivity – does not add extra pairs only if .
Take two pairs and in , such that .
Closing under transitivity forces to be added to .
If , then there are no issues: Since is transitive, we get , so translating the pair is always going to happen anyway.
The failure case is if : Here, the translation identifies despite . Transitive closure chains straight through, and ends up identifying and for no reason that can be attributed to .
This failure is only possible when the translation merges two -unrelated programs onto a single point in , which happens when .[35] The sufficient (and necessary) fix is to require
since means that , so is forced directly.
This gives us the kernel condition on our chosen translation and abstraction:
The next thing to check is whether respects the operations of , i.e., whether it is compatible with every input and environment a translated program might be run in.
Context is Everything
To make "respects testing and inputs" precise, we borrow the context formalism from the -calculus: a context is a program with a hole, becoming a genuine program once is plugged in.[36]
Example.
Church numerals encode the natural number as the term which means "apply to , times."
Let , where is the successor function.
Plugging in gives .
Plugging in gives .
Here, and are syntactically different terms that an abstraction might reasonably identify. If so, to be a congruence, it must also identify and for every context , not just .
This gives the precise condition:
E is a congruence if for all contexts
Placing -related programs in any shared context (the same larger program, the same input, the same environment, etc.) still can't tell them apart.
For a translation to respect this at all, it must be compositional:[37] translating a combined program must equal (or, more generally, be -related to) combining the translated pieces:
for the corresponding target-side context .
Two cases follow:
If is compositional, then every -context has a translated -counterpart under .
Since is a congruence in , and are related in and sit inside
Contexts native to that have no -counterpart[38] must be checked.
Suppose and for some .
Nothing forces since is invisible to by construction (it has no source-side origin). So, if , then has produced, on the target side, a translated pair that violates and the coarse-graining does not transport.
This gives the third and final condition:
Every native context , applied to a translated -related pair, and , must give one of two outcomes:
, or
and , for some .
This rules out two kinds of leakage: splitting the pair apart with no corresponding source merge, or sending one side into while the other escapes it.
Three Conditions on Abstractions & Translations
Question. Given a congruence on and a translation , under what conditions does a (forced) congruence on faithfully mirror (rather than cascading to something coarser) so that the original abstraction survives translation intact?
Answer.
The translation is compositional.
.
There is no way of building a bigger program around a smaller one on the target side that forces two translated, previously-unmerged programs together.
What does it look like to check these conditions in practice?
Compositionality is mechanical to check when is built structurally. Most literature encodings are, so it's close to free. For a known only to be correct, with no structural route, it can fail.
The kernel condition asks what merges, and whether already merges it. Structurally-built translations tend to be injective, making trivial and the condition automatic; otherwise the work is computing and checking it against .
The third condition is the bottleneck. It quantifies over 's native contexts, precisely the part of that the translation provides no information about. This mirrorsfull abstraction in the literature about compilers, where the hard part is showing target contexts can't observe more than source ones could. It's a useful source of technique and of warnings (full abstraction is notoriously hard to verify), so this condition remains open for further research.
One could make an argument for restricting the target model, , to the image of the translation, , to bypass the need for conditions (1) and (3) altogether. This could only work if the contexts are also restricted to pushed-forward source contexts. Then, yes, compositionality holds, but trivially so, because the target's context structure is defined to be a copy of the source's. Besides, the point of the exercise was to see whether 's structure genuinely preserves . This doesn't remove the need for the conditions but rather assumes them by construction.
A failure of (2) means itself identifies some pair of source programs that did not. A failure of (3) means some native context in can force a merge that no source context could have justified. Either way, once identifies a pair through one of these routes, the congruence closure can't tell that pair apart from any legitimate one. It becomes available as fuel for transitivity, which gets used to justify further merges, which justify more, and so on.
Condition (2) is necessary by the reflexivity argument above, but whether (1) and (3) are also necessary is still open: it hasn't been ruled out that could survive with one of them failing. Tightening this gap (or finding a counterexample) remains open work.
Conclusion
Which features of an agent's world model are about the world itself, and which are consequences of the modelling choice?
This project considered two readings of this question in the computational setting (models of computation as a substitute for world models):
If we demand that an abstraction must survive every correct change of representation, then only those relations that are behavioural equivalence or coarser remain intact after remodelling.
Specifically, the only way to learn about a program from outside is to run it on tests and observe what comes back. Features of programs that leave no trace on a test are invisible from the outside, and that is the information that a remodelling process is free to throw away.
A potential link worth exploring is to view "visible through testing" as a deterministic analogue of Wentworth's information at a distance. The claim, from his Telephone Theorem, is that the information a far-away observer can learn about a system is limited to whatever survives the noisy process of transporting the system to them. Swap "far away and noisy" for "outside and only reachable via tests", and the two might be pointing at the same underlying phenomenon: the information that can be preserved is bounded by what can actually travel along the channel connected to the observer.[39]
Behavioural equivalence compares world models from the outside, which is relevant if all we wanted was to know, say, when two models make the same predictions. In this project, however, we wanted to shed some light on what happens when abstracting a particular model in hand while maintaining it as a model of the same world. Those coarsenings are features inside the model, which are the relations finer than behavioural equivalence (which this result says nothing about). This matter led to the next result.
An abstraction finer than behavioural equivalence can survive translation under three conditions:
is compositional;
; and
no native target-side context opens a return path
with the forced congruence as its faithful image.
Checking condition (3) presents a major bottleneck and requires further research.
Whether the three conditions here are also necessary remains open, as does the asymmetry between translation directions (some encodings in the literature are compositional nearly for free, while the reverse direction[40] may not necessarily be so).
Naturality, then, is perhaps a relational and graded property, rather than a binary one that an abstraction either has or lacks. This framework measures the extent to which an abstraction is converged upon: how large a class of translations can it survive, and (unexplored here) how many target models it persists in at all. The three conditions of Result 2 are what decide membership in that class, one translation at a time.
Criticisms (& Open Problems)
Abstractions that are translation-invariant are not immediately independent of the observer•Observers that see the same world through different lenses are actually not constrained to agree on anything, whereas the translations defined here are, by construction, required to agree on behaviour on a fixed test set (for the first result).
Dependence on is not optional•The project has moved the question from "which model" to "which translations count as legitimate re-modellings". Result 1 would be more informative[41] if is restricted, which itself is a modelling decision. Additionally, Lemma II says that any class containing some translation that maps behaviourally-equivalent pairs to the same point loses information about all relations finer than ≃, so an informative must exclude such maps. In practice, this requires compositionality or stronger.[42] This sits awkwardly with NAH, where convergence toward an abstraction was meant to explain shared structure, not be assumed. At best this trades one arbitrary choice for a more tractable one: "which " is easier to argue about than "which model," and structural-recursion translations are a reasonable candidate.
Connecting the results to abstractions of a single program•Results 1 & 2 are about abstractions acting on all programs simultaneously. The bridge connecting the local and global lattices is informal (outlined earlier), so it's worth making this link explicit.
Do models of computation make good world models at all?•Can the features of computational models stand in for an agent's representation of a persisting environment? I aim to make this the topic of my next post.
In other words, the content of a program that is model-independent is its externally observable behaviour. So, abstractions of internal structure are never universally invariant.
Meaning that translating an assembled program from parts gives the same result as translating the pieces and assembling them on the target side ( commutes with program building).
an abstract model throws away or ignores information from the concrete model, but in such a way that we can still make reliable predictions about some aspects of the underlying system.
I won't delve too deeply into the concept of abstraction here, as this post and this one (amongst many others) already do that well.
A fuller comparison would also weigh in how many different target models an abstraction persists in at all (a second measure that this project doesn't cover, though the same methods here could plausibly extend to it).
We can be somewhat convinced that computational processes are worth studying in the context of agent foundations via the following argument: if agents are restricted to doing only computable things (as far as we know), their internal representation of the world must also be computable. Therefore, we can implement a model of computation to model said representation.
I concede that this is a departure from what we typically mean when we say "world model". Models of computation are formalisms for describing a computational process, and it is not clear how these map to some learned representation of the world.
This is a discussion big enough to deserve its own treatment, so I save it for a future post.
Technically speaking, this requires a bit more than Turing-completeness alone (you need a property called acceptability) since it's possible to construct strange counterexamples that compute exactly the same functions as a Turing machine but admit no translation from one.
To be absolutely precise, a translation is technically made up of a few components: a map between programs and a map between the testing environments . The relationship between and is defined via another map .
Throughout the post, we just write for all, because translations vary in how they encode programs, not in how they encode tests. We can do this safely by fixing the test-map and behaviour-map for the translation class , and remember that they are shared by every translation in .
A nice analogy for translations is to view them as compilers, which transform high-level programs (e.g. Python code) into binary or low-level machine code that a computer's CPU can execute. It is possible that the structure of the output program is nothing like the input's, because the only thing that really matters is that it behaves the same for all given inputs, and inside all environments it is placed in.
We could instead ask for a coarser notion of correspondence: e.g., behaviours that are 'close enough' under some similarity measure, rather than strict distinctness. I use the strict version here for simplicity and leave weaker notions of correspondence to future work.
Emphasis on approximate: the full partition lattice is countably infinite and incomparability is everywhere. Consider, for instance, that the equivalence classes "same number of states" and "same runtime complexity" do not refine each other, so the partitions sit side-by-side on the lattice.
For example, the relations that identify all programs which have the same length measured in bits, or those that have the same number of internal states, are perfectly valid relations, however they lump together programs with completely diverging behaviours.
The padding lemma covers Turing Machines and general recursive functions. Different arguments (which rely on each model's specific syntax) can be applied to find the result in other cases: e.g., for -calculus, wrapping a term in an identity redex, , gives the same trick.
Whether every behaviour class is always infinite isn't something I've checked for every possible model.
Jenner identifies these two regions (for a single computation) in his post:
There are (roughly speaking) two kinds of information we can throw away:
Details of the input-output behavior. [...]
Details of the internal implementation. [...]
Behavioural equivalence is the "hinge" between these in . If two programs appear in the same partition in a relation that is (strictly) coarser than behavioural equivalence, then some of their distinguishing input-output behaviour is merged and they are no longer identified as distinct.
Likewise, in relations finer than behavioural equivalence, merged programs behave identically by definition, so aspects of internal implementation are lost.
A DFA can be seen as a restricted Turing machine: it reads its input tape once, left to right, using only its finite set of states as memory. It cannot write to the tape or move backward, so it has no way to store or revisit information beyond what a state already encodes.
Of course, full model-independence, in the sense of not depending on the choice of (computational) model at all, would require this condition to hold across every pair of substrates , not just the one pair considered here.
Restricting the class away from (requiring translations to preserve more structure, not just behaviour) means that fewer identifications are forced, and the free relation shrinks. So, as intuition would suggest, a smaller makes it easier for a relation to be translation-invariant.
Our substrate definition deliberately assumed nothing about the internal structure of programs, so on a bare substrate, "congruence" isn't yet meaningful. It becomes meaningful once we equip each substrate with its program-forming operations (e.g., composition, primitive recursion and minimisation for general recursive functions, or term formation for the -calculus).
"Congruence" from here on always means "with respect to these operations."
alone (the raw pushforward of under ) need not be a congruence: it may fail to be transitive or compatible with the target's structure. is the congruence generated by closing under these properties, i.e. the smallest congruence containing it.
A congruence, by definition, is an equivalence relation on the whole underlying set, so , as a congruence on , must be reflexive on every, including programs that never hits. But that's not a problem since adding pairs can't ever merge two distinct elements.
One quick clarification: the contexts from our substrate definition are testing contexts: things fed in to the '' function alongside a program, in order to observe it. The contexts here are technically building contexts: ways of assembling a larger program around a smaller one, so is itself a program.
Behavioural equivalence is defined by testing contexts, and congruences are about building contexts. The two are related (running is one way of testing ) but they play slightly different roles.
In practice, this is an inductive check. Contexts are built compositionally from the basic operations of the substrate, so you need only to check compositional condition on the generators.
For example: consider a translation . The generating operations for general recursive functions are composition, primitive recursion, and minimisation. So, for each of these three operation-types, we need only to check that translating a composite function equals composing the translated pieces.
For composition itself:
where is "run one machine then feed output to another" on the Turing Machine side. Analogous checks would be done for the primitive recursion and minimisation operators.
This is often the case because often has structure that is not found in . Consider , for instance. There is a plethora of -terms that will not be the image of some Turing Machine under translation.
The example is a good one to keep in mind: it is built by structural recursion, so compositionality comes almost for free.
The reverse direction looks completely different. The standard route , by contrast, goes via the Kleene'sNormal Form Theorem. It isn't obviously compositional in the sense condition (1) needs (because it doesn't touch the machine's actual structure, and instead routes everything through one universal predicate and a single minimisation), and I have not checked whether some version of it is.
This is a claim about the class as a whole (which has to be restricted this way for the measure to be non-trivial at all), and it's what motivates condition (1): the per-instance check once and are both fixed.
Congruence closure can interleave context application with transitivity, so a merge like this can propagate through a chain of contexts, not just a single one. Checking single contexts suffices only because building contexts are closed under composition, which holds in every substrate we consider.
For example: suppose and compute the same value in isolation. Suppose additionally has a side effect, say, it writes to some shared state. Then, a context that runs (or ) alongside another program that can observe the side effect and produce different outputs depending on which one was plugged in. The equivalence relation that only checks "same output in isolation" fails to be a congruence, because this context pulls and apart.
This post was written as part of the 2026 Research Fellowship for Dovetail Research.
A massive thanks to Alex for directing this project, to Jose and Alfred for feedback and insights on this work, and to all the other fellows with whom wonderful discussions led to new ideas.
This work was funded by the Advanced Research + Invention Agency (ARIA) through project code MSAI-SE01-P005.
Declaration
The proofs in this post have been formalised with assistance from Claude (Fable 5.0 & Opus 4.8). The ideas, writing, and proof verification have been done by me, a human.
TL;DR
Question
Which features of an agent's world model are about the world itself, and which are consequences of the modelling choice?
Setting
This project builds from the intuition of Wentworth's Natural Abstraction Hypothesis (NAH) on converging abstractions to propose a test for naturality: measuring the extent to which a given abstraction persists after changing the representation or model of the world could indicate just how natural it is.
Computability theory is a setting in which 'remodelling' is easy to construct and check, since translations between models are well-studied. We treat models of computation as a substitute for world models, congruences as abstractions, and translation maps between models as changes in representation.
Result 1
An abstraction that survives every change of representation is behavioural equivalence or coarser. (Too coarse to say anything about the model's internal structure.[1])
Result 2
An abstraction
Introduction
Most of us are familiar with the scenario of an agent that is "well-behaved" in its training environment, but when released in a new context (as in, one outside the tested distribution), it begins to exhibit unintended (and sometimes undesirable) behaviour. Testing behaviour alone can be blind to the internal variations in modelling that might yield these unexpected outputs, and abstractions[3] are one part of that internal story. As hidden differences in abstractions can surface as a differences in behaviour, understanding abstractions is a correspondingly important component of understanding alignment.
So, here's the problem. Two models, seeking to describe the same world, could opt for wildly different abstractions. These could constitute accurate reflections of structures in the world, or, alternatively, they might be artifacts of the choice of representation, or reflective of the modeller's perspective.
There needs to be some way to tell these apart. According to NAH, if an abstraction is "natural", then different observers should converge on it – that is, a natural abstraction will tend to show up across a variety of models.
That intuition, then, suggests a test for "naturality": which abstractions are preserved when you change how a world model is represented?
Given a translation
To make that question precise enough to support investigation, I trade NAH's statistical setting for a more exact and deterministic one. If the framework presented here is correct, and if it carries over beyond the computational setting, it suggests that "naturality" might be better understood as a measure of how many (or what proportion of) re-modellings a given abstraction will survive.[4]
Related Work
Erik Jenner's research agenda proposes abstractions of computations as a tractable formal setting, and develops a framework for abstracting a single computation. In particular, Jenner notes that his framework says nothing about the encoding or representation of a computation, and leaves open whether it should be handled inside the framework or separately. This post can be seen as engaging with this idea, in which abstractions are held fixed and the representation varies.
Models of Computation
The task of translating between different models is rather unwieldy, especially as we start to consider all possible structures they might adopt. World models can range from automata to probabilistic or causal models, to neural representations and beyond, each residing in vastly different domains and exhibiting distinctive features. Transitioning between them requires some way to bridge these diverging descriptions.
It is therefore sensible to consider models for which such translations are straightforward to construct, or, even better, already exist. As foretold in the introduction, a candidate class of models can be found in computability theory.[5]
Models of computation are well-suited to this context.[6] The challenge of translation isn't a new one, and, indeed, the original strategy (going back to the 1930s) was to construct 'natural mappings' between various models by hand.[7] The existence of translation maps between Turing-complete models turns out to be guaranteed[8] by a general theorem from computability theory. This is sufficient for us to get started.
Translating From One Model to Another
To understand what translations maps need to look like, we first need to fix what we mean by a 'model of computation'. Every model we'll consider decomposes into two essential parts:
The programs are just a set
which takes a program together with some context[9] (an input, or a test to perform on it) and, if the program halts on that observable, returns the behaviour type (the observable or output) it exhibits; otherwise it returns nothing.
Thus, a computational system (or computational substrate, if you will) is a quadruple:
The following examples demonstrate how various Turing-complete models fit into the above definition.
Examples
These are not unique characterisations (e.g. you can define the
Model
Programs
"Running It"
Behaviour
Turing Machines
state transition tables
feed input and run transitions
contents of the tape at halting (or non-terminating)
closed
apply input (optional) and β-reduction
halt at normal form (or non-terminating)
General Recursive Functions
closed syntactic definitions built from
unwind the recursive definition on input
output natural number (or tuple), when defined
Cellular Automata
rule (e.g. Rule 150, Game of Life) + initial configuration
apply the rule synchronously to a given initial configuration, evolve forward
initial config
(read off designated halting-observable)
JavaScript
JS source code
JS engine's usual call stack, memory heap, and event loop
return value / final state / console output
This is an operational view of computation,[10] and it is a characterisation that is general enough to describe any computational model on the table. Moreover, it predetermines what a translation must be: a map sending programs to programs that respects (under some agreed correspondence between observables) what "running them" means.
In other words, the translation must, minimally, ensure the output program does the same job as the input.[12]
The phrase "corresponds to" is deliberately left open: it stands in for whatever notion of matching outcomes that fits the two models' structure, and the specific choice has little consequence in the work to come. Two things must hold:
Translations need be neither injective (distinct programs in
Abstractions
Abstraction, at its simplest, is a choice about which (features of) programs to treat as "the same" (this choice encapsulates what the abstraction forgets about distinct programs). The minimal structure capturing "which things get merged" is an equivalence relation,[14] which we will use to model the coarse-graining process here.
The central organising structure in this post is the lattice
An approximate[16] representation of a sublattice of
At the top, the trivial relation (a single partition) cannot distinguish between any program. At the bottom, the finest relation is the identity relation in which each program is in a partition of its own.
Not all equivalence relations make good abstractions – most merge elements no reasonable observer would treat as interchangeable.[17] We work with the full lattice anyway: a result proved for all of
Behavioural Equivalence
Zooming in, a single point of this lattice is the set
The relations that sit above (coarser than) behavioural equivalence (
The blue area indicates (approximately) the region of the lattice that is most relevant to this investigation.
One Program at a Time
Another lattice worth studying in its own right is one that organises the coarse-grainings of a single program
Example.
If
This is an example of standard DFA minimisation. Quotienting by
This local lattice connects to
Which Abstractions are Model-Independent?
Recall our original question: which abstractions are preserved when changing how the world model is represented? Or, equivalently, which coarse-grainings are model-independent?
Placing this question within our mathematical framework:
Given a relation
The pullback is the relation in
If the pullback is equal to
where
Proof.
If
If
Recoverability from one
To remove the arbitrariness, we ask instead whether
This is our question
Checking
The free relation collects all the pairs of programs in
A translation can't un-identify programs it's already merged, so the pullback
Proof.
Let
For a generating pair
So,
The grey area denotes a
So,
Proof.
Hence
The
Proof.
(
By Lemma I,
By Lemma II,
So,
(
Assume
Then
So
Define
Then, for every
Question. Given a relation
Answer. Exactly when the relation
This is unsurprising: correctness was defined as preserving behaviour, so behaviour is what survives. It is worth considering whether this question actually aligns with what we want. Two things don't fit.
Both problems suggest that we might be better served by an alternative approach. Previously, we removed arbitrariness in the choice of translation by considering all translations simultaneously. We can also remove arbitrariness by choosing a specific translation.
Under which conditions will a given abstraction transport to another model?
There's a trivial solution to this question: we can simply build a translation
Besides, we're rarely in a position to invent
Let us proceed by choosing a particular translation
Motivating Example. An abstraction that coarse-grains a program's internal compositional structure could be preserved by some translation
The standard translation
Picture This
We can draw the whole setup as follows:
The goal is to construct a corresponding set
Forced Congruences
Not all equivalence relations make good abstractions, but we can sidestep that problem here by assuming
Our question can now be framed in the language of universal algebra:
Given a congruence
To begin, translate every pair that the relation
Then take the smallest congruence on
This is the forced congruence.[32] Two things to check:
It always exists.
The set of all congruences on
An intersection of congruences is again a congruence. So,
It is always non-empty.
Every congruence is reflexive by definition, therefore,
i.e., pulling
Testing the Equivalence Conditions
We check this by walking through which pairs are added under closure:
Symmetry – trivial, no need to add anything: if
Reflexivity – adds all[34] the identity pairs
Trivial on
if
So the kernel condition (below) is forced by reflexivity, and transitivity is what turns that one stray pair into a cascade of identifications.
Transitivity – does not add extra pairs only if
Take two pairs
Closing under transitivity forces
Since
Here, the translation identifies
This failure is only possible when the translation
The sufficient (and necessary) fix is to require
since
This gives us the kernel condition on our chosen translation and abstraction:
The next thing to check is whether
Context is Everything
To make "respects testing and inputs" precise, we borrow the context formalism from the
Example.
Church numerals encode the natural number
which means "apply
Let
Plugging in
Plugging in
Here,
This gives the precise condition:
E is a congruence if
Placing
For a translation
for the corresponding target-side context
Two cases follow:
If
Since
Contexts native to
Suppose
and
Nothing forces
This gives the third and final condition:
Every native
This rules out two kinds of leakage:
Three Conditions on Abstractions & Translations
Question. Given a congruence
Answer.
What does it look like to check these conditions in practice?
One could make an argument for restricting the target model,
A failure of (2) means
Condition (2) is necessary by the reflexivity argument above, but whether (1) and (3) are also necessary is still open: it hasn't been ruled out that
Conclusion
Which features of an agent's world model are about the world itself, and which are consequences of the modelling choice?
This project considered two readings of this question in the computational setting (models of computation as a substitute for world models):
Specifically, the only way to learn about a program from outside is to run it on tests and observe what comes back. Features of programs that leave no trace on a test are invisible from the outside, and that is the information that a remodelling process is free to throw away.
A potential link worth exploring is to view "visible through testing" as a deterministic analogue of Wentworth's information at a distance. The claim, from his Telephone Theorem, is that the information a far-away observer can learn about a system is limited to whatever survives the noisy process of transporting the system to them. Swap "far away and noisy" for "outside and only reachable via tests", and the two might be pointing at the same underlying phenomenon: the information that can be preserved is bounded by what can actually travel along the channel connected to the observer.[39]
Behavioural equivalence compares world models from the outside, which is relevant if all we wanted was to know, say, when two models make the same predictions. In this project, however, we wanted to shed some light on what happens when abstracting a particular model in hand while maintaining it as a model of the same world. Those coarsenings are features inside the model, which are the relations finer than behavioural equivalence (which this result says nothing about). This matter led to the next result.
with the forced congruence
Checking condition (3) presents a major bottleneck and requires further research.
Whether the three conditions here are also necessary remains open, as does the asymmetry between translation directions (some encodings in the literature are compositional nearly for free, while the reverse direction[40] may not necessarily be so).
Naturality, then, is perhaps a relational and graded property, rather than a binary one that an abstraction either has or lacks. This framework measures the extent to which an abstraction is converged upon: how large a class of translations can it survive, and (unexplored here) how many target models it persists in at all. The three conditions of Result 2 are what decide membership in that class, one translation at a time.
Criticisms (& Open Problems)
In other words, the content of a program that is model-independent is its externally observable behaviour. So, abstractions of internal structure are never universally invariant.
Meaning that translating an assembled program from parts gives the same result as translating the pieces and assembling them on the target side (
In Wentworth's words:
I won't delve too deeply into the concept of abstraction here, as this post and this one (amongst many others) already do that well.
A fuller comparison would also weigh in how many different target models an abstraction persists in at all (a second measure that this project doesn't cover, though the same methods here could plausibly extend to it).
We can be somewhat convinced that computational processes are worth studying in the context of agent foundations via the following argument: if agents are restricted to doing only computable things (as far as we know), their internal representation of the world must also be computable. Therefore, we can implement a model of computation to model said representation.
I concede that this is a departure from what we typically mean when we say "world model". Models of computation are formalisms for describing a computational process, and it is not clear how these map to some learned representation of the world.
This is a discussion big enough to deserve its own treatment, so I save it for a future post.
There are plenty of modern constructions too. See this paper for further discussion.
Technically speaking, this requires a bit more than Turing-completeness alone (you need a property called acceptability) since it's possible to construct strange counterexamples that compute exactly the same functions as a Turing machine but admit no translation from one.
We will return to this!
As opposed to denotational, which would assign mathematical meaning via the function that is computed.
To be absolutely precise, a translation is technically made up of a few components: a map between programs
Throughout the post, we just write
A nice analogy for translations is to view them as compilers, which transform high-level programs (e.g. Python code) into binary or low-level machine code that a computer's CPU can execute. It is possible that the structure of the output program is nothing like the input's, because the only thing that really matters is that it behaves the same for all given inputs, and inside all environments it is placed in.
We could instead ask for a coarser notion of correspondence: e.g., behaviours that are 'close enough' under some similarity measure, rather than strict distinctness. I use the strict version here for simplicity and leave weaker notions of correspondence to future work.
The attribute that we're discussing here is essentially indistinguishability, which is reflexive, symmetric, and transitive.
We will use the shorthand
Emphasis on approximate: the full partition lattice
For example, the relations that identify all programs which have the same length measured in bits, or those that have the same number of internal states, are perfectly valid relations, however they lump together programs with completely diverging behaviours.
Any two correct translations
Since
The padding lemma covers Turing Machines and general recursive functions. Different arguments (which rely on each model's specific syntax) can be applied to find the result in other cases: e.g., for
Whether every behaviour class is always infinite isn't something I've checked for every possible model.
Jenner identifies these two regions (for a single computation) in his post:
Behavioural equivalence
Likewise, in relations finer than behavioural equivalence, merged programs behave identically by definition, so aspects of internal implementation are lost.
A DFA can be seen as a restricted Turing machine: it reads its input tape once, left to right, using only its finite set of states as memory. It cannot write to the tape or move backward, so it has no way to store or revisit information beyond what a state already encodes.
In other words, information that distinguished two programs,
Think of it this way:
Equivalently, if you prefer, it is preimage of
Put a pin in this kernel condition. We'll meet it again soon.
Of course, full model-independence, in the sense of not depending on the choice of (computational) model at all, would require this condition to hold across every pair of substrates
Restricting the class
"Below" behavioural equivalence:
I haven't checked, but I believe this class is infinite. It includes every conceivable correctness-preserving map, however superfluous or abnormal.
It's actually not that easy (and, IMO, quite tedious) to do so by hand.
Our substrate definition deliberately assumed nothing about the internal structure of programs, so on a bare substrate, "congruence" isn't yet meaningful. It becomes meaningful once we equip each substrate with its program-forming operations (e.g., composition, primitive recursion and minimisation for general recursive functions, or term formation for the
"Congruence" from here on always means "with respect to these operations."
Note:
This is the same recoverability question as before, now with a specific candidate relation,
A congruence, by definition, is an equivalence relation on the whole underlying set, so
Recall:
One quick clarification: the contexts
Behavioural equivalence is defined by testing contexts, and congruences are about building contexts. The two are related (running
In practice, this is an inductive check. Contexts are built compositionally from the basic operations of the substrate, so you need only to check compositional condition on the generators.
For example: consider a translation
For composition itself:
where
This is often the case because
I haven't checked how far the analogy holds, and the two settings differ in important ways, but I leave it here as a possibly interesting connection.
The
The reverse direction looks completely different. The standard route
As in, useful for understanding abstractions related to the internal structure of models.
This is a claim about the class
Congruence closure can interleave context application with transitivity, so a merge like this can propagate through a chain of contexts, not just a single one. Checking single contexts suffices only because building contexts are closed under composition, which holds in every substrate we consider.
Not every equivalence relation has this property.
For example: suppose
This is fairly similar to the idea of minimising a deterministic finite automaton.