Salvador Lucas (Universitat Politècnica de València) expose ses travaux le jeudi 22 mai à 13h30 en salle 301
Church defined lambda calculus computations as symbolic transformation processes which are expected to halt. In sharp contrast, Turing's landmark 1936 paper introducing his machines and associated notion of computation did not pay attention to any halting notion. Furthermore, halting was implicitly considered as an *unsatisfactory* behavior. Thus, although it is part of the current standard description of computation with Turing Machines, halting is not intrinsic to computation. Interestingly, this dichotomy is alive in existing functional languages today. For instance, termination (or halting) is part of the computational description of eager functional languages like ML or Scheme. However, the developers of lazy functional languages like Haskell are often proud of allowing for the use of infinite data structures produced by means of non-terminating reduction processes. The presentation will provide a brief historical overview of these issues, hopefully leading to a further clarification and answer to "Should computations halt?".
