 Turing (1936–7) and, separately, Church (1936) proved that the answer is negative: there is no such algorithm. To show this, they offered precise characterizations of the informal notion of an effectively computable function. Turing did so in terms of so-called Turing machines (TMs)—devices that manipulate discrete symbols written on a tape in accordance with finitely many instructions. Other logicians did the same thing—they formalized the notion of effectively computable function—in terms of other notions, such as λ-definable functions and general recursive functions.