no-cloning theorem



physics, mathematical physics, philosophy of physics

Surveys, textbooks and lecture notes

theory (physics), model (physics)

experiment, measurement, computable physics

Monoidal categories

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




In quantum physics the no-cloning theorem is the statement that one cannot produce a second copy of an arbitrary given quantum state by a quantum physical process.

More in detail, in its original version the statement is that given a quantum system with Hilbert space HH and with a chosen initial pure quantum state eHe \in H, then there is no unitary operator on the tensor product HHH \otimes H which would take states of the form (ψ,e)(\psi, e) to (ψ,ψ)(\psi,\psi).

Of course this cannot exist, because such a map would not even be linear. Often the statement is relaxed to observing that if there is a unitary that takes (ψ,e)(\psi,e) to (ψ,ψ)(\psi,\psi) and (ϕ,e)(\phi,e) to (ϕ,ϕ)(\phi,\phi) for any two states ϕ,ψH\phi,\psi \in H, then either ϕ=ψ\phi= \psi or ϕψ\phi \perp \psi (since it follows from unitarity that in this case ϕ|ψ=ϕ|ψ 2\langle\phi | \psi \rangle = \langle\phi | \psi \rangle^2 ).

There is a slightly more substantial generalization of this observation to mixed quantum states, then called the no-broadcasting theorem. Dually, there is also a no-deleting theorem.

Formally, when quantum physics is axiomatized by quantum logic in the guise of linear logic/linear type theory, the content of “no-cloning” and “no-deleting” is the very “linearity” of this logic, the absence of a diagonal map and of a projection map for the non-cartesian tensor product in the categorical semantics given by non-cartesian symmetric monoidal categories such as that of Hilbert spaces. See also at finite quantum mechanics in terms of dagger-compact categories.

From this perspective one gets a more interesting statement if one turns this around and asks which conditions are imposed on a symmetric monoidal category if its tensor product is assumed to admit a diagonal map (for “cloning”) or projection maps (for “deleting”) or both. These turn out to be very strong conditions. For instance in order for a diagonal to exist for the tensor product of a compact closed category implies that every endomorphism on every object in the category is a multiple of the identity (Abramsky 09, in generalization of “Joyal’s lemma”). This is clearly false in any category in which one could find interesting quantum mechanics, certainly in that of (finite dimensional) Hilbert spaces.


The original articles are

General reviews include

Discussion from the point of view of monoidal category-theory (finite quantum mechanics in terms of dagger-compact categories) includes

  • Samson Abramsky, No-Cloning in categorical quantum mechanics, (2008) in I. Mackie and S. Gay (eds), Semantic Techniques for Quantum Computation , Cambridge University Press (arXiv:0910.2401)

Revised on May 19, 2017 17:30:21 by David Corfield (