Editing Function (mathematics) (section)

== In computer science ==
{{main|Function (computer programming)|Lambda calculus}}

In [[computer programming]], a [[Function (programming)|function]] is, in general, a [[subroutine]] which [[implementation|implements]] the abstract concept of function. That is, it is a program unit that produces an output for each input. [[Functional programming]] is the [[programming paradigm]] consisting of building programs by using only subroutines that behave like mathematical functions, meaning that they have no [[side effect (computer science)|side effect]]s and depend only on their arguments: they are [[Referential transparency|referentially transparent]]. For example, <code>if_then_else</code> is a function that takes three ([[nullary]]) functions as arguments, and, depending on the value of the first argument (''true'' or ''false''), returns the value of either the second or the third argument. An important advantage of functional programming is that it makes easier [[program proof]]s, as being based on a well founded theory, the [[lambda calculus]] (see below). However, side effects are generally necessary for practical programs, ones that perform [[input/output]]. There is a class of ''[[Purely functional programming|purely functional]]'' languages, such as [[Haskell]], which encapsulate the possibility of side effects in the type of a function. Others, such as the [[ML (programming language)|ML]] family, simply allow side effects.

In many [[programming language]]s, every subroutine is called a function, even when there is no output but only side effects, and when the functionality consists simply of modifying some data in the [[computer memory]].

Outside the context of programming languages, "function" has the usual mathematical meaning in [[computer science]]. In this area, a property of major interest is the [[computable function|computability]] of a function. For giving a precise meaning to this concept, and to the related concept of [[algorithm]], several [[models of computation]] have been introduced, the old ones being [[μ-recursive function|general recursive function]]s, [[lambda calculus]], and [[Turing machine]]. The fundamental theorem of [[computability theory]] is that these three models of computation define the same set of computable functions, and that all the other models of computation that have ever been proposed define the same set of computable functions or a smaller one. The [[Church–Turing thesis]] is the claim that every philosophically acceptable definition of a ''computable function'' defines also the same functions.

General recursive functions are [[partial function]]s from integers to integers that can be defined from 
* [[constant function]]s, 
* [[successor function|successor]], and
* [[projection function|projection]] functions 
via the operators
* [[#Function composition|composition]], 
* [[primitive recursion]], and 
* [[μ operator|minimization]].

Although defined only for functions from integers to integers, they can model any computable function as a consequence of the following properties:

* a computation is the manipulation of finite sequences of symbols (digits of numbers, formulas, etc.),
* every sequence of symbols may be coded as a sequence of [[bit]]s,
* a bit sequence can be interpreted as the [[binary representation]] of an integer.

[[Lambda calculus]] is a theory that defines computable functions without using [[set theory]], and is the theoretical background of functional programming. It consists of ''terms'' that are either variables, function definitions (''{{lambda}}''-terms), or applications of functions to terms. Terms are manipulated by interpreting its [[axiom]]s (the {{math|''α''}}-equivalence, the {{mvar|β}}-reduction, and the {{mvar|η}}-conversion) as [[rewriting]] rules, which can be used for computation.

In its original form, lambda calculus does not include the concepts of domain and codomain of a function. Roughly speaking, they have been introduced in the theory under the name of ''type'' in [[typed lambda calculus]]. Most kinds of typed lambda calculi can define fewer functions than untyped lambda calculus.