nLab dynamic lifting

Contents

Context

Computation

Quantum systems

quantum logic


quantum physics


quantum probability theoryobservables and states


quantum information


quantum computation

quantum algorithms:

Contents

Idea

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).

References

General

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:

Last revised on December 7, 2022 at 10:35:09. See the history of this page for a list of all contributions to it.