Formalizing quantum computation

Many different models of computation were defined in the beginning of computer science: Turing machines (TM), cellular automata (CA), Boolean circuits, etc. And yet today one can buy a PC, a Macintosh, etc., but no Turing machine. But in fact the definition of all complexity classes are based on TMs. So should one conclude from this that complexity theory is useless? No, since, as the famous Church-Turing thesis states, all reasonable models of computation (which can be simulated with a sheet of paper and a pencil in a finite amount of time) are equivalent, in the sense that they can simulate each other. Thus compatibility, the fact that a function is computable, is device-independent. Since in practice it makes no difference whether a program never stops or stops only in a hundred years, one is more interested in efficient algorithms, i.e. where the running time is polynomial in the size of the input. Fortunately all known reasonable models simulate each other with only polynomial overhead. This is known as the modern version of the Church-Turing thesis