Revisiting the notion of function

Fairouz Kamareddine, Twan Laan, Rob Nederpelt

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

Functions 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. © 2002 Elsevier Science Inc. All rights reserved.

Original languageEnglish
Pages (from-to)65-107
Number of pages43
JournalJournal of Logic and Algebraic Programming
Volume54
Issue number1-2
DOIs
Publication statusPublished - Jan 2002

Keywords

  • Π-reduction
  • Automath
  • Explicit substitution
  • Function abstraction and application

Fingerprint Dive into the research topics of 'Revisiting the notion of function'. Together they form a unique fingerprint.

  • Cite this