Calculus Church s Calculus Brief History One of a number of approaches to a mathematical challenge at the time 1930 Constructibility What does it mean for an object e g a natural number to be constructible aka effective computability computability Work in parallel included Turing s work on Turing machines G del s work on general recursive functions History continued In late 30 s Church Kleene and Turing showed equivalence of their respective notions Led to Church s thesis notion of a computable function should be identified with the notion of a general recursive function Church s Lambda Calculus Formally specifies the difference between functions and forms Form specifies operations that are to be applied to the parameters of the form with corresponding free variables and constants e g of a form a X2 X Y X Y parameters a free variable not parameter to form 2 constant Forms Note if actual arguments are applied to form there is no way to specify their bindings P Q a X2 X Y P X Q Y P Y Q X Functions Lambda function resolves ambiguity and defines difference between functions and forms x y a x2 x y function with two parameters x y where first actual is to be bound to x and second to y Curried interpretation function of x which yields a function of y which Two interesting characteristics of lambda calculus 1 Church defined argument substitution assuming static scope and actuals bound by were to be unique throughout form Functions 2 Form can only contain applications of other functions not their definitions instances of other formal parameters bound to other lambdas cannot exist in a given lambda function functions cannot be used as arguments or function values because a function would appear where a form or object is expected McCarthy s LISP McCarthy s LISP 1958 1960 First language to be based on Lambda Calculus Two major differences 1 LISP used dynamic scope so Define poly X Y a X X X Y Define p1 a poly 2 3 Define p2 a poly 4 5 p1 10 p2 20 a has different bindings in poly when called by p1 p2 so LISP maintained a list continue McCarthy s LISP 2 LISP many versions before Scheme ML allowed functions as arguments quoted lambda expressions were passed as funargs passby name definitions each time funarg was referenced it caused evaluation of actual parameter s lambda definition in its defining scope Note Scheme ML Haskell allow functions as arguments they evaluate to themselves McCarthy has suggested that the reason LISP used dynamic scope was that he did not fully understand the Lambda Calculus of Church during the development of LISP Expressions exp constant variable exp exp variable exp built in constant variable names applications lambda abstractions Abstractions Purpose is to denote new functions x x 1 x x 1 That function of x which adds x to 1 Free and Bound Variables x x y x is bound by the but y is free x y y z 7 x x y are bound z is free x x x 1 4 first x is free second is bound Occurrence of variable is bound if an enclosing expression binds it and it is free otherwise Conversions BAH Beta abstraction and reduction reduction applying abstraction to an argument making new instance of abstraction body and substituting argument for free occurrence of formal abstraction going the opposite way Alpha changing names consistent formal parameter name change in expression Eta elimination of redundant abstractions Substitution E M x expression E with all free occurrences of x replaced by M x M x M c M x c where c is variable or constant other than x E F M x E M x F M x x E M x x E because no free occurrences of x y E M x where y is not x y E M x if x does not occur free in E or y does not occur free in M z E z y M x otherwise where z is new variable not free in E or M Conversions Summary x E M if y is not free in E then x E y E y x E M x if x is not free in E and E denotes a function then x E x E when applied left to right are called reductions and rules Beta Reduction Reducing an expression x 3 x x 4 x 5 x y y x 4 5 f f 3 x x 1 function argument 3 9 y y 4 5 5 4 1 x x 1 3 3 1 4 Alpha Conversion Ought to be equivalent x 1 x and indeed x 1 x y 1 y y 1 y as long as newly introduced name does not occur freely in body of original lambda expression Eta Conversion Ought to be equivalent x 1 x 1 and indeed x 1 x 1 In general x F x F provided x is not free in F and F is a function Normal Form Def When an expression contains no reducible expressions redexes There may be more than one route to normal form for an expression E e g 3 4 7 8 Not every expression has a normal form e g D D where D is x x x produces D D Some reductions may reach normal form while others do not e g x 3 D D OK not OK Normal Form CRT CRT I If E1 E1 E2 then there exists an E such that E and E2 E in words two expressions that can be converted to each other share a common normal form Corollary No expression can be convereted to two distinct normal forms CRT II If E1 E2 and E2 is in normal form then there exists a normal order reduction sequence from E 1 to E2 Normal order reduction reduce leftmost outermost redex first Calculus Utility Supports expression of recursion YH H YH Y a fixed point combinator takes a function H and produces a fixed point of H See Peyton Jones section 2 4 1 Supports typed untyped and polymorphic systems Underlies denotational semantics