.. title: Computer Theoretical Implications of the Many-worlds Interpretation
.. slug: computer-theoretical-implications-of-the-many-worlds-interpretation
.. date: 2026-08-27 16:50:16 UTC+02:00
.. tags: 
.. category: 
.. link: 
.. description: 
.. type: text
.. has_math: True

Recently, my collaborators and I published an article in the proceedings of the
ACM on programming languages for the PLDI 2026 conference. 

    | Hybrid Path-Sums for Hybrid Quantum Programs
    | `doi:10.1145/3808314 <https://doi.org/10.1145/3808314>`_ `arXiv:2604.24578 <https://arxiv.org/abs/2604.24578>`_
    | Christophe Chareton, Jad Issa, Mathieu Nguyen, Nicolas Blanco, and
      Sébastien Bardin.

International programming language conferences like PLDI are often not great
fans of philosophical observations and references to potentially metaphysical
questions, and that's usually great, as the intent is exclusively to explain the
technical contributions. However, in fields like programming language design
where there is often a lot of structure and formalism, I find that authors are
often inspired and guided by less rigid philosophical ideas, or in the least,
might consider these ideas as intuition for their constructs, and it's a shame
not to share these intuitions. This is precisely what happened to us in the
writing of the article above, and the inspiration is the many-worlds
interpretation of quantum mechanics. So, in this post, I re-earn the chance to
discuss those fun, inspiring, and enlightening perspectives on what is now a
purely technical work.

.. TEASER_END

The Measurement Problem
-----------------------

A major problem of intuition that physicists find in the formalism of quantum
mechanics is the so-called measurement problem. According to experimental
evidence, a quantum system in a superposition of states, say :math:`|\psi\rangle
= \alpha |0\rangle + \beta |1\rangle`,
when measured as either :math:`|0\rangle` or :math:`|1\rangle`, will report
either 0 or 1 and the superposition will collapse to the measured state. There
are many reasons why this is an issue. The first and most fundamental is
probably that this makes a categorical distinction between the object being
observed and the subject observing it. However, the subject is also a quantum
system that evolves and can be observed by another observer. There is no
reasonable solution to this issue: if one considers the line of interactions
from the observed system to the 'conscious' observation (whatever that means)
and passing through all the measurement apparatus and human biology, there is no
single point where the system changed from object to subject. This is not a
matter of continuity vs discreteness or something special about consciousness
either as demonstrated by the Wigner's friend thought experiment. In the
experiment, Wigner stands outside a room where his friend performs a quantum
measurement on a system. Wigner's friend then observes the collapse of the
wavefunction; however, Wigner, who is outside the room, has not measured
anything; therefore, he still considers the system's evolution to be unitary and
when Wigner measures the system himself, he is supposed to still possibly
observe a different outcome than his friend's. 

A solution to this problem is to forget the conscious observer and consider that
everything and everyone (the entire Universe) is a single composite quantum
system. In this case, the apparent collapse of the wavefunction is nothing more
than an entanglement between the observed system and the observer within the
Hilbert space of the Universe as a whole. Therefore, what Wigner sees is that
the system experiment-friend still follows unitary evolutions, but the state of
Wigner's friend and that of the system can no longer be faithfully described
independently of one another. This is known as the many-worlds interpretation.
The reason it's called many-worlds is, at least in my way of seeing it, that
since we cannot possibly describe the state of the entire Universe as a whole,
we can gradually, at each measurement, augment the system we are describing by
tensoring it with a new and entangled "copy" of itself. This "copy" represents
part of the observer which has now become entangled with the observed system.
Since it is not part of the system per se, we can imagine that the world has
split into many, one for each possible outcome of the measurement and that the
"conscious" observation is in only one of them. The advantage of this view is
that, while the worlds are technically still in a superposition, we are not
supposed to be able to apply transformations involving the observer, as it is
not part of the system in question; therefore, worlds cannot interfere in any
interesting ways. This is very informal, but bear with me, there is a formal
version of each statement here, separately, but the notion of 'worlds' is
metaphysical anyway, and it doesn't mean much, formally, beyond refuting
collapse and using a universal wavefunction instead.

Path-sums and Hybrid Path-sums
------------------------------

Another, though indirect, inspiration for our work is the path-integral
formulation of quantum mechanics, in particular, a discrete version of it known
as path-sums [Amy18]_. Path-sums exist in many forms, balanced [Amy18]_,
unbalanced [Amy23]_, "double-sided" [Vilmart22]_, and, in our work, hybrid
[CIN+26]_, but the basic idea is quite simple. Let's say you're a high-school
student, which you may be, (with educational inflation, you might need to be a
bachelor's or even master's student, I guess), and you just learned some linear
algebra and the basics of quantum computing: gates and circuits. Now, you have
just seen the circuit for the quantum Fourier transform on :math:`10` qubits,
and it starts with a parallel Hadamard gate on all :math:`10` qubits and you
want to run through it to see its output on some input basis state
:math:`|x_1\cdots x_{10}\rangle`. With all certainty, you will not explicitly
write down :math:`2^{10} = 1024` terms of the decomposition over the
computational basis.  Instead, you will likely write the following:

.. math::

   \vert\psi\rangle = \frac{1}{\sqrt{2^{10}}} \sum_{y_1,\ldots,y_{10}\in\{0,1\}}
   e^{2\pi i (x_1 y_1 / 2 + \cdots + x_{10} y_{10}/2)} \vert y_1\cdots y_{10}\rangle
  
This is a path-sum. It is simply a symbolic sum describing a vector or a matrix
or some other linear "object" compactly, without expanding all its terms. How
you define its precise syntax and semantics gives you all the variations and is
central to a computational application, but whatever you do, this is what a
path-sum is. The *paths* are each of the assignments of the variables
:math:`y_1,\ldots,y_{10}`, which are referred to as *path variables*. 

Does this remind you of anything? The paths existing in parallel and in a
superposition resemble, quite a lot, the worlds that exist in superposition in
the many-worlds interpretation. Here's a question: how would you describe the
state after measuring the first 5 qubits of :math:`|\psi\rangle`? You could list
the :math:`2^5 = 32` possible outcomes, and the respective projections of the
state, but more likely than not, you would also want to find a shortcut. If we
look back at the interpretation of the measurement in the many-worlds model, we
realize that all we need to do is to augment the system with 5 new "qubits"
representing the parts of the measurement apparatus that needs to get entangled
with the measured qubits, let's denote them :math:`|-\rangle_{A_1}\cdots
|-\rangle_{A_5}`. We can entangle these qubits with the qubits of the system by
copying the :math:`|y_i\rangle` values into them. Indeed, in the path where the
state of the first qubit is :math:`|y_i\rangle`, the measurement outcome is
:math:`y_i`. As such, we get the following *hybrid path-sum*:

.. math::
   \vert\psi'\rangle = \frac{1}{\sqrt{2^{10}}} \sum_{y_1,\ldots,y_{10}\in\{0,1\}}
   e^{2\pi i (x_1 y_1 / 2 + \cdots + x_{10} y_{10}/2)} \vert y_1\cdots y_{10}\rangle
   \vert y_1\rangle_{A_1}\cdots \vert y_5\rangle_{A_5}

Then, you can interpret this hybrid path-sum by considering that the :math:`A_i`
qubits are not really accessible. This gives you a set of :math:`2^5` worlds,
in each of which, the state can be described by a sum over the remaining 5 path
variables:

.. math::
   \vert \psi_{a_1\cdots a_5}\rangle = \frac{1}{\sqrt{2^{10}}}
   \sum_{y_6,\ldots,y_{10}\in\{0,1\}} 
   e^{2\pi i (x_1 a_1 / 2 + \cdots + x_5 a_5 / 2 + x_6 y_6 / 2 + \cdots + x_{10}
   y_{10}/2)} \vert a_1\cdots a_5 y_6\cdots
   y_{10}\rangle


More generally, if the content of the :math:`A_i` qubits was not just a
standalone variable, but some more involved boolean function
:math:`f_i(y_1,\ldots,y_{10})` of the path variables, the splitting into worlds
corresponds to a partition of the path space into :math:`2^5` sets, with the
projected (subnormalized) states being given by

.. math::
   \vert \varphi_{a_1\cdots a_5}\rangle = \frac{1}{\sqrt{2^{10}}}
   \sum_{\substack{y_1,\ldots,y_{10}\in\{0,1\} \\ f_1(y_1,\ldots,y_{10}) = a_1
   \\ \cdots \\ f_5(y_1,\ldots,y_{10}) = a_5}} 
   e^{2\pi i (x_1 y_1 / 2 + \cdots + x_{10} y_{10}/2)}
   \vert y_1\cdots y_{10}\rangle

And voilà, that's our work! Well, of course not, but that's the core idea.

Equivalence and refinement
--------------------------

If this ancilla system, the :math:`A_i` qubits, is seen as a set of classical
bits, the hybrid path-sum becomes a compact representation of a
quantum-classical system. That, in itself, is quite great, but to unlock its
full potential, we need methods to manipulate, simplify, and check the
equivalence of these path-sums. By being able to check the equivalence of two
hybrid-path sums, we can check the equivalence of two quantum-classical
programs, an essential task for the verification of a range of tasks, from
quantum circuit optimization to compilation, and more. Furthermore, if we can
describe the specification of a quantum-classical program itself as a hybrid
path-sum, equivalence checking becomes functional verification. Another approach
is to relate hybrid path-sums with a "refinement" relation :math:`h_1 \preceq h_2` which
says, roughly speaking, that the hybrid path-sum :math:`h_1` is a more detailed
description of the system than :math:`h_2`. In this context, specifications no
longer need to be exact, but the verification can still be done by tools similar
to equivalence checking.

Practically speaking, the tools we are talking about concern a rewriting system
given by a set of concrete rules of the form :math:`h_1 \to h_2` where if some
pattern is found in :math:`h_1`, then, :math:`h_1` can be replaced by an
equivalent path-sum :math:`h_2`. If there is a path of rewrites from some
specification path-sum :math:`h_s` to the path-sum of the program :math:`h_p`,
then, :math:`h_s` and :math:`h_p` are equivalent, and the program satisfies its
specification. Similarly, we can define a set of refinement rules where
:math:`h_p \to h_s` means that :math:`h_p` is a refinement of :math:`h_s` and
the program, again, satisfies its specification. 

I do not wish to elaborate more on the technical aspects here and instead refer
the reader to the article itself [CIN+26]_ as well as the implementation of the
corresponding tool, HQbricks, available on `GitHub
<https://github.com/Qbricks/hqbricks>`_.


Bibliography
------------

.. [Amy18] Matthew Amy. Towards large-scale functional verification of
   universal quantum circuits. `arXiv:1805.06908 <https://arxiv.org/abs/1805.06908>`_, 2018.
.. [Amy23] Matthew Amy. Complete equational theories for the sum-over-paths with
   unbalanced amplitudes. `arXiv:2306.16369
   <https://arxiv.org/abs/2306.16369>`_, 2023.
.. [Vilmart22] Renaud Vilmart. Completeness of sum-over-paths for Toffoli-Hadamard and the
   dyadic fragments of quantum computation.  `arXiv:2205.02600
   <https://arxiv.org/abs/2205.02600>`_, 2022.
.. [CIN+26] Chareton, C., Issa, J., Nguyen, M., Blanco, N., & Bardin, S. (2026).
   Hybrid Path-Sums for Hybrid Quantum Programs. In Proceedings of the ACM on
   Programming Languages (Volume 10, Issue PLDI, pp. 1687--1713). ACM.
   `doi:10.1145/3808314 <https://doi.org/10.1145/3808314>`_ `arXiv:2604.24578
   <https://arxiv.org/abs/2604.24578>`_