nLab dynamic lifting




Quantum systems

quantum logic

quantum physics

quantum probability theoryobservables and states

quantum information

quantum computation


quantum algorithms:

quantum sensing

quantum communication



In quantum computation the term “dynamic lifting” (mostly used in the Quipper-community, starting around Green et al (2013), p. 5) refers to the outcome of quantum measurement-results — which can be known only during runtime (ie. “dynamically”), due to the intrinsic stochastic nature of quantum physics — being turned into (ie. “lifted” back to) variables on which subsequent classical computation may be conditioned, which may then in turn control further quantum circuits, etc.:

SQRAM model adapted from Nagarajan, Papanikolaou Williams 2007, Fig 1

Dynamic lifting is thought (eg. Rand (2018),p. 52) to be optional in cases like the quantum teleportation protocol but necessary for applications like

There have been several (partial) proposals for the precise categorical semantics of this idea, see the references below. Another formalization, via monadic effects of potentiality modalities in dependent linear type theory, is discussed at quantum circuits via dependent linear types (CQTS 2022, see there).



The general but informal idea of quantum computation with classical control that may itself be conditioned on quantum measurement results (see also at Quantum Computation – Classical control and quantum data) may be argued to be implicit already in Knill (1996).

Explicit discussion includes:

  • Rajagopal Nagarajan, Nikolaos Papanikolaou, David Williams, Simulating and Compiling Code for the Sequential Quantum Random Access Machine, Electronic Notes in Theoretical Computer Science Volume 170, 6 March 2007, Pages 101-124 [doi:10.1016/j.entcs.2006.12.014]

The term “dynamic lifting” is mainly used in discussion of the quantum programming language Quipper. Its first (brief) appearance might be that in:

More in-depth discussion of “dynamic lifting” is in:

Categorical semantics

Proposals for categorical semantics of “dynamic lifting”, mostly following along the lines of some dependent linear type theory, such as found in Quipper:

Last revised on November 13, 2023 at 17:36:34. See the history of this page for a list of all contributions to it.