Lambda Calculus: a Theory of Functions

Processes of definition and abstraction one of the most important skills in programming is the ability to identify and "abstract out" common parts or patterns of expression from texts (i.e., programs)

Lambda Calculus: a Theory of Functions

	Processes of definition and abstraction
	Lambda abstraction and beta-conversion lambda abstraction is a linguistic form which directly realizes the abstraction/instantiation process

Lambda Calculus: a Theory of Functions

	Processes of definition and abstraction
	Lambda abstraction and beta-conversion
	Abstraction as inverse of function application we can also view abstraction as a symmetric "opposite" of function application, arising as a means of solving equations directly for functions

Lambda Calculus: a Theory of Functions

	Processes of definition and abstraction
	Lambda abstraction and beta-conversion
	Abstraction as inverse of function application
	A calculus of pure functions the language of pure lambda calculus includes only variables, abstraction and application; it captures a very general notion of function (including all computable ones)

Lambda Calculus: a Theory of Functions

	Processes of definition and abstraction
	Lambda abstraction and beta-conversion
	Abstraction as inverse of function application
	A calculus of pure functions
	Calculation-as-reduction and normal forms we formalize calculation as the process of substituting terms for lambda-bound variables until all abs/app "pairs" are resolved; this results in a term-rewriting or tree-transformation view of computation

Lambda Calculus: a Theory of Functions

	Processes of definition and abstraction
	Lambda abstraction and beta-conversion
	Abstraction as inverse of function application
	A calculus of pure functions
	Calculation-as-reduction and normal forms
	Representation results by standard techniques we can represent values such as numbers, truth-values, pairs, etc. as functions, thus encoding all entities of logic and mathematics

Lambda Calculus: a Theory of Functions

	Processes of definition and abstraction
	Lambda abstraction and beta-conversion
	Abstraction as inverse of function application
	A calculus of pure functions
	Calculation-as-reduction and normal forms
	Representation results
	Self-application and non-termination we can even encode (i.e., define) recursion, through the self-application of functions, but this raises the spectre of non-termination