Foundations of Theory of Programming Languages: Introduction to Lambda CalculusLecture OutlineLambda Calculus. History.Function CreationHistory of NotationMore on Lisp and Lambda...Preview: Function ApplicationIt sounds too dumb!! Why Study Lambda Calculus?Is lambda calculus a programming language?A prediction come trueSyntax of Lambda CalculusSyntax of Lambda Calculus in LispExamples of Lambda ExpressionsNotational Conventions which primarily serve to confuse.Notational Conventions in Lisp require no precedence to parseScope of VariablesFree and Bound VariablesFree and Bound Variables Lisp notationFree and Bound Variables Lisp notationFree and Bound Variables (Cont.)Renaming Bound VariablesRenaming Bound Variables (Cont.)What can we do with lambda calculus expressions?SubstitutionEvaluation of l-termsExamples of EvaluationExamples of Evaluation in Lisp notationFunctions with Multiple ArgumentsFunctions with Multiple ArgumentsFunctions with Multiple Arguments, some of which are MISSINGEvaluation and Static ScopeThe Order of EvaluationOrder of Evaluation (Cont.)Call by NameCall by ValueCall by Name and Call by ValueLambda Calculus and Programming LanguagesEncoding Booleans in Lambda CalculusEncoding Booleans in Lambda Calculus Lisp notationEncoding Pairs in Lambda CalculusEncoding Natural Numbers in Lambda CalculusEncoding Natural Numbers in LispComputing with Natural NumbersComputing with Natural Numbers in lisp notationComputing with Natural Numbers. ExampleComputing with Natural Numbers. ExampleExpressiveness of Lambda CalculusWe’ll quit here for lack of timeProf. Fateman CS 164 Lecture 23 1Foundations of Theory of Programming Languages:Introduction to Lambda CalculusLecture 23Prof. Fateman CS 164 Lecture 23 2Lecture Outline•Some History• Why study lambda calculus?• What IS lambda calculus?• How extensions relate to explaining Lisp, Tiger, Java etc. semanticsProf. Fateman CS 164 Lecture 23 3Lambda Calculus. History.• A framework developed in 1930s by Alonzo Church to study computations with functions• Church wanted a minimal notation– to expose only what is essential• Two operations with functions are essential:– function creation– function application• Um, what has this to do with (integral?) calculus?Prof. Fateman CS 164 Lecture 23 4Function Creation• Church introduced the notationλx. E to denote a function with formal argument x and with body E• Functions do not have names– names are not essential for the computation• Functions have a single argument– once we understand how functions with one argument work we can generalize to multiple args.Prof. Fateman CS 164 Lecture 23 5History of Notation• Whitehead & Russell (Principia Mathematica) used the notation ŷ P to denote the set of y’s such that P holds.• Church borrowed the notation but moved ˆ down to create ∧yE• Which later turned into λy. E and the calculus became known as lambda calculus• John McCarthy, inventor of Lisp, who later admitted he didn’t really “understand” lambda calculus at the time, appropriated the notation lambda[y](E), later changed to (lambda(y) E) for an “anonymous” function.Prof. Fateman CS 164 Lecture 23 6More on Lisp and Lambda...• We will find it useful to use lisp notation in these slides because logicians muck up their formal notation with implicit operators (just putting items next to each other) and expecting the reader to figure out precedence.Prof. Fateman CS 164 Lecture 23 7Preview: Function Application•The only thing that we can do with a function is to apply it to an argument• Church used the notationE1E2…in lisp, (E1E2)to denote the application of function E1to actual argument E2• All functions are applied to a single argument• Even so, THIS IS ENOUGH TO COMPUTE ANYTHING.Prof. Fateman CS 164 Lecture 23 8It sounds too dumb!! Why Study Lambda Calculus?• λ-calculus has had a tremendous influence on the theory and analysis of programming languages• Comparable to Turing machines• Provides a PL framework:– Realistic languages are too large and complex to study from scratch as a whole– Typical approach is to modularize the study into one feature at a time• E.g., recursion, looping, exceptions, objects, etc.– Then we assemble the features togetherProf. Fateman CS 164 Lecture 23 9Is lambda calculus a programming language?• λ-calculus as a concept is the standard testbed for studying programming language features– Because of its minimality– Despite its syntactic simplicity the λ-calculus can easily encode:• numbers, recursive data types, modules, imperative features, exceptions, etc.• Certain language features necessitate more substantial extensions to λ-calculus:– for distributed & parallel languages: π-calculus– for object oriented languages: σ-calculus• But as will be evident shortly, the bare lambda calculus is not a PL in a practical sense.Prof. Fateman CS 164 Lecture 23 10A prediction come true“Whatever the next 700 languages turn out to be, they will surely be variants of lambda calculus.”(Peter Landin 1966)Prof. Fateman CS 164 Lecture 23 11Syntax of Lambda Calculus• Syntax: Only three kinds of expressionsE Æ x variables| E1 E2function application| λx. E function creation•The form λx. E is also called lambda abstraction, or simply abstraction•Eare called λ-terms or λ-expressionsProf. Fateman CS 164 Lecture 23 12Syntax of Lambda Calculus in Lisp• Only three kinds of LISP expressionsE → x variables| (E1 E2) function application| (lambda(x) E) function creation•The form (lambda(x)E) is also called lambda abstraction, or simply abstraction•Eare called s-expressions or termsProf. Fateman CS 164 Lecture 23 13Examples of Lambda Expressions• The identity function:I =defλx. x …(lambda(x) x)• A function that given an argument y discards it and computes the identity function:λy. (λx. x) ... (lambda(y)(lambda(x)x))• A function that given a function f invokes it on the identity function λf. f (λ x. x) …(lambda(f)(f(lambda(x)x))) {actually, that’s Scheme. In CL we need…(lambda(f)(funcall f (lambda(x)x))) }Prof. Fateman CS 164 Lecture 23 14Notational Conventions which primarily serve to confuse.• Application associates to the leftx y z parses as (x y) z• Abstraction extends to the right as far as possibleλx. x λy. x y z parses as λ x. (x (λy. ((x y) z)))•
View Full Document
Unlocking...