First let's do the proof for the classical case: ------------------ Def: torev f = \ (a,b) -> (a, xor (f a) b) Claim: \ (a,b) -> torev f (torev f (a,b)) = id Proof: \ (a,b) -> torev f (a, xor (f a) b) = \ (a,b) -> (a, xor (f a) (xor (f a) b)) = \ (a,b) -> (a, xor b (xor (f a) (f a))) = \ (a,b) -> (a, xor b False) = \ (a,b) -> (a, b) = id ------------------ Let's try to generalize to the quantum case: Def: torev f = \ (a,b) -> f a @>>= \ b' -> vreturn (a, xor b b') Claim: \ (a0,b0) -> torev f (a0,b0) @>>= \ (a1,b1) -> torev f (a1,b1) = \ (a0,b0) -> vreturn (a0,b0) Proof: \ (a0,b0) -> torev f (a0,b0) @>>= \ (a1,b1) -> torev f (a1,b1) = \ (a0,b0) -> f a0 @>>= \ b' -> vreturn (a0, xor b0 b') @>>= \ (a1,b1) -> f a1 @>>= \ b'' -> vreturn (a1, xor b1 b'') = \ (a0,b0) -> f a0 @>>= \ b' -> f a0 @>>= \ b'' -> vreturn (a0, xor (xor b0 b') b'') Assume that two applications of f to the same value return the same result. This is not true in some monads. It would need to be proved for the two monads we consider: Classical and Quantum. = \ (a0,b0) -> f a0 @>>= \ b' -> vreturn (a0, xor (xor b0 b') b') = \ (a0,b0) -> f a0 @>>= \ b' -> vreturn (a0, xor b0 (xor b' b')) = \ (a0,b0) -> f a0 @>>= \ b' -> vreturn (a0, b0) = \ (a0,b0) -> f a0 @>>= \ _ -> vreturn (a0, b0) Assume that it is ok to throw away the result of applying a function. This is not true in some monads. It would need to be proved for the two monads we consider: Classical and Quantum. = \ (a0,b0) -> vreturn (a0, b0)