X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek2_lambda_intro.mdwn;h=6bbb53991b855a73c57de344a56d24c0756ea83b;hp=486a75b434f6266ca91e1d6b722b5ea05f06eca8;hb=20c3705983ac428fecca3a33b472431371e6b347;hpb=e1f4de77bd03fe51fa8c432c82bc4a098c9d6298 diff --git a/topics/week2_lambda_intro.mdwn b/topics/week2_lambda_intro.mdwn index 486a75b4..6bbb5399 100644 --- a/topics/week2_lambda_intro.mdwn +++ b/topics/week2_lambda_intro.mdwn @@ -1,13 +1,12 @@ -## Syntax of Lambda Calculus ## +# Introduction to the Lambda Calculus # We often talk about "*the* Lambda Calculus", as if there were just one; but in fact, there are many, many variations. The one we will start with, and will explore in some detail, is often called "the pure" -or "the untyped" Lambda Calculus. Actually, there are many variations even under -that heading. But all of the variations share a strong family +or "the untyped" Lambda Calculus. Actually, there are many variations even under that heading. But all of the variations share a strong family resemblance, so what we learn now will apply to all of them. -> Fussy note: calling this/these the "pure" lambda calculus is entrenched terminology, +> Fussy note: calling this the "pure" Lambda Calculus is entrenched terminology, but it coheres imperfectly with other uses of "pure" we'll encounter. There are three respects in which the lambda calculus we'll be presenting might claim to deserve the name "pure": (1) it has no pre-defined constants and a very spare @@ -15,16 +14,12 @@ syntax; (2) it has no types; (3) it has no side-effects, and is insensitive to the order of evaluation. > Sense (3) corresponds most closely to the other uses of "pure" you'll -see in the surrounding literature. With respect to this point, it may be true that -this lambda calculus has no side effects. (Let's revisit that assumption -at the end of term.) But as we'll see next week, it is *not* true that it's insensitive -to the order of evaluation. So if that's what we mean by "pure", this lambda -calculus isn't as pure as you might hope to get. Some *typed* lambda calculi will -turn out to be more pure in that respect. +see in the surrounding literature. With respect to this point, it may be true that the Lambda Calculus has no side effects. (Let's revisit that assumption +at the end of term.) But as we'll see next week, it is *not* true that it's insensitive to the order of evaluation. So if that's what we mean by "pure", this lambda calculus isn't as pure as you might hope to get. Some *typed* lambda calculi will turn out to be more pure in that respect. > But this lambda calculus is at least "pure" in sense (2). At least, it -doesn't *explicitly talk about* any types. Some prefer to say that this -lambda calculus *does* have types implicitly, it's just that +doesn't *explicitly talk about* any types. Some prefer to say that the +Lambda Calculus *does* have types implicitly, it's just that there's only one type, so that every expression is a member of that one type. If you say that, you have to say that functions from this type to this type also belong to this type. Which is weird... In @@ -41,13 +36,15 @@ as you might hope to get. or "the untyped" Lambda Calculus, or even just "the" Lambda Calculus, this is the system that people will understand you to be referring to. +## Syntax ## + Here is its syntax:
-Variables: x, y, z... +Variables: x, y, z ...
-Each variable is an expression. For any expressions M and N and variable a, the following are also expressions: +Each variable is an expression. For any variable `a` and (possibly complex) expressions `M` and `N`, the following are also expressions: