Böhm's Theorem

The technical significance of Bohm’s theorem suffices to deserve it a prominent place in any monograph on the theory of the ?-calculus and makes it a basic result that any researcher working on ?-calculus must know. In addition to its technical content, we think that behind this beautiful result there is something of interest for a much wider audience. The clear thread that starting from his thesis led Corrado Bohm to the research on ?-calculus and to the quest for an “internal” way to discriminate ?-terms, the deep analysis of the structures of ?-terms required by the proof of the theorem, the so-called Bohm-out technique, and the many unexpected consequences and applications of this technique clearly put Bohm’s theorem on a relevant position in the bookshelf of the main achievements of theoretical computer science. Moreover, as in the case of almost all the relevant results of Mathematics, the interest of Bohm’s theorem is not only in the statement that it asserts, but also, and maybe mainly, in the constructions required by its proof.