Class 08: Lambda Calculus

Back to McCarthy's LISP. On to Continuation Basics.

Held: Wednesday, February 8, 2006

Summary: Today we consider the basics of the lambda calculus, a notation (and way of thinking about functions) that underlies most modern functional languages.

Assignments

Notes:

• A few of you have asked for extensions on the homework, or at least time to talk to me. It is now due a week from Friday.

Overview:

• Historical aspects.
• Notation basics.
• Currying.

Historical Aspects

• As you saw in the papers from McCarthy, lambda notation has been a part of functional programming since the first version of Lisp.
• Lambda notation predates Lisp by a number of years.
• Lambda notation was developed by Alonzo Church, a logician, in the early part of the 20th century.
• Logicians at the time were trying to understand (a) how mathematicians reason and (b) computation.
• Church designed lambda notation as a way of thinking and writing about functions. He observed that mathematicians often speak of functions anonymously, as in a function that given an input, x, computes ....
• The lambda notation he developed provided a way for reasoning about functions and about computation.
• You may have heard of the Church-Turing thesis, which is phrased in a number of ways (according to a number of pages, mostly incorrect ways). Here are some fun variations:
• Any function that is computable under a reasonable model of computation is computable by (a Turing machine; the lambda calculus)
• Any sufficiently powerful model of computation is equivalent to all other models of computation.

Notation Basics

• So, what is this amazing notation?
• It's fairly straightforward, particularly if you remember the a function that, given input x, computes some expression.
• Church chose to write that long phrase as λ x . some-expression
• What can the expression look like? It can use atomic symbols and other lambdas.
• For example, λ x . cons x nil
• Of course, we might eventually need a way to think about what those constants mean.
• In Lisp, we have built-in meanings for some symbols.
• Church tried to avoid them.
• Note that the x is a local variable for the body.
• Church was careful to clarify that a symbol means different things at different points, depending on the most recent binding.
• We won't go through the details, just remember that they are like local variables.
• We typically write multiple-parameter functions by putting all the variables before the period, as in λ x y z . some-expression
• Lambda notation is incredibly powerful. You can represent conditionals, numbers, arithmetic, etc., with just lambdas and symbols.
• Here are conditionals (along with true and false)
• if: λ b t f . b t f
• true: λ t f . t
• false: λ t f . f
• Note that truth values are functions rather than constants. Writing functions for even simple values is one of the halmarks of the lambda calculus.
• We can also define the normal boolean operations
• not: λ b . (&lambda t f . b f t)
• or: λ b1 b2 . (&lambda t f . b1 t (bt t f))
• and is left as an exercise to the reader

Currying

• He suggested that there is little difference between &lambda x y . exp and λ x . λ y . exp
• In a Curried version of the lambda calculus, it is perfectly acceptable to fill in only some of the parameters to a multiple-parameter method.
• The result of such an operation is a function.
• We'll do some examples.

Back to McCarthy's LISP. On to Continuation Basics.

Disclaimer: I usually create these pages on the fly, which means that I rarely proofread them and they may contain bad grammar and incorrect details. It also means that I tend to update them regularly (see the history for more details). Feel free to contact me with any suggestions for changes.

This document was generated by Siteweaver on Wed May 10 09:02:46 2006.
The source to the document was last modified on Thu Jan 12 09:00:37 2006.
This document may be found at `http://www.cs.grinnell.edu/~rebelsky/Courses/CS302/2006S/Outlines/outline.08.html`.

You may wish to validate this document's HTML ; ; Check with Bobby

Samuel A. Rebelsky, rebelsky@grinnell.edu