From chaos to undefinedness

Manfred Broy

pp. 476-496

in: Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer (eds), Algebra, meaning, and computation, Berlin, Springer, 2006

Abstract

The semantic and logical treatment of recursion and of recursive definitions in computer science, in particular in requirements specification, in programming languages and related formalisms such as λ-calculus or recursively defined functions is one of the key issues of the semantic theory of programming and programming languages. As it has been recognised already in the early days of the theory of programming there are several options to formalise and give a theory of the semantics of recursive function declarations. In different branches of computer science, logics, and mathematics various techniques for dealing with the semantics of recursion have been developed and established. We outline, compare, and shortly discuss advantages and disadvantages of these different possibilities, illustrate them by a simple running example, and relate these approaches.