l CalculusChurch’s l Calculus: Brief HistoryHistory (continued)Church's Lambda Calculus:Formsl FunctionsSlide 7McCarthy’s LISP(continue) McCarthy's LISPl Expressionsl AbstractionsFree and Bound VariablesConversions, BAH!SubstitutionConversions SummaryBeta ReductionAlpha ConversionEta ConversionNormal FormNormal Form (CRT)l Calculus Utility CalculusChurch’sChurch’s Calculus: Brief HistoryCalculus: 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 functionsHistory (continued)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: 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: constantFormsForms•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 ? FunctionsFunctions–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) FunctionsFunctions2) 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 LISPMcCarthy’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(continue) McCarthy's LISP•2) LISP (many versions before Scheme, ML) allowed functions as arguments.–quoted lambda expressions were passed as "funargs." (pass-by-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... ExpressionsExpressions<exp> ::= <constant> built-in constant | <variable> variable names | <exp> <exp> applications |  <variable> . <exp> lambda abstractions AbstractionsAbstractions•Purpose is to denote new functions: (x . + x 1)(x . + x 1)That function of x which adds x to 1Free and Bound VariablesFree 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!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  abstractionsSubstitutionSubstitution E[M/x] -- expression E with all free occurrences of x replaced by Mx [M/x] = Mc [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 MConversions SummaryConversions Summary• : (x . E) M E[M/x]• : if y is not free in E then (x . E) (y . E[y/x])• : if x is not free in E and E denotes a function then (x . E x) E•when applied left to right ( ), andrules are called reductions•Reducing an expression:(x . 3) x 3(x . + 4 x) 5 9(x . (y . - y x)) 4 5 (y . - y 4) 5 - 5 41(f . f 3) (x . + x 1) (x . + x 1) 3+ 3 14Beta ReductionBeta Reductionfunctionargument•Ought to be equivalent...(x . + 1 x) & (y . + 1 y)and, indeed…(x . + 1 x) (y . + 1 y)...as long as newly introduced name does not occur freely in body of original lambda expression.Alpha ConversionAlpha 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 functionEta ConversionEta Conversion•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 )Normal FormNormal FormOKnotOK•(CRT-I): If E1 E2 then