Revisiting the notion of function

AbstractFunctions play a central role in type theory, logic and computation. We describe how the notions of functionalisation (the way in which functions can be constructed) and instantiation (the process of applying a function to an argument) have been developed in the last century. We explain how both processes were implemented in Frege’s Begriffschrift, Russell’s Ramified Type Theory, and the λ-calculus (originally introduced by Church) showing that the λ-calculus misses a crucial aspect of functionalisation. We then pay attention to some special forms of function abstraction that do not exist in the λ-calculus and we show that various logical constructs (e.g., let expressions and definitions and the use of parameters in mathematics), can be seen as forms of the missing part of functionalisation. Our study of the function concept leads to: (a) an extension of the Barendregt cube [4] with all of definitions, Π-reduction and explicit substitutions giving all their advantages in one system; and (b) a natural refinement of the cube with parameters. We show that in the refined Barendregt cube, systems like Automath, LF, and ML, can be described more naturally and accurately than in the original cube