《程序设计语言的形式语义》课程教学资源（文献资料）Lecture Notes on the Lambda Calculus

Lecture Notes on the Lambda Calculus Peter Selinger DDaihouremde Abstract Topics de the lambda caleulutheCurry-Howrd isomorism. Contents 1 Introduction 4 1.1 Extensional vs.intensional view of functions 1.2 The lambda calculus 6 1.3 Untyped vs.typed lambda-calculi 7 1.4 Lambda calculus and computability............. 1.5 Connections to computer science..................9 1.6 Connections to logic 9 1.7 Connections to mathematics....................10 2 The untyped lambda calculus 2.1 Syntax

Lecture Notes on the Lambda Calculus Peter Selinger Department of Mathematics and Statistics Dalhousie University, Halifax, Canada Abstract This is a set of lecture notes that developed out of courses on the lambda calculus that I taught at the University of Ottawa in 2001 and at Dalhousie University in 2007. Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, combinatory algebras, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normal￾ization, type inference, denotational semantics, complete partial orders, and the language PCF. Contents 1 Introduction 4 1.1 Extensional vs. intensional view of functions . . . . . . . . . . . 4 1.2 The lambda calculus . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Untyped vs. typed lambda-calculi . . . . . . . . . . . . . . . . . 7 1.4 Lambda calculus and computability . . . . . . . . . . . . . . . . 8 1.5 Connections to computer science . . . . . . . . . . . . . . . . . . 9 1.6 Connections to logic . . . . . . . . . . . . . . . . . . . . . . . . 9 1.7 Connections to mathematics . . . . . . . . . . . . . . . . . . . . 10 2 The untyped lambda calculus 10 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1

2.2 Free and bound variables,a-equivalence.............. 12 2.3 Substitution. 14 2.4 Introduction to B-reduction. 16 2.5 Formal definitions of B-reduction and B-equivalence.......17 3 Programming in the untyped lambda calculus 18 3.1 Booleans 18 3.2 Natural numbers......,.,.,.,............., 19 3.3 Fixpoints and recursive functions 3.4 Other datatypes:pairs,tuples,lists,trees,etc. 23 4 The Church-Rosser Theorem 25 4.1 Extensionality,equivalence,and nreduction 25 4.2 Statement of the Church-Rosser Theorem,and some consequences 27 4.3 Preliminary remarks on the proof of the Church-Rosser Theorem.29 4.4 Proof of the Church-Rosser Theorem 31 4.5 Exercises 36 5 Combinatory algebras 37 5.1 Applicative structures. 38 5.2 Combinatory completeness 39 5.3 Combinatory algebras. 1 5.4 The failure of soundness for combinatory algebras 42 55 Lambda algebras..... 5.6 Extensional combinatory algebras 48 6 Simply-typed lambda calculus,propositional logic,and the Curry- Howard isomorphism 50 6.1 Simple types and simply-typed terms ..50 6.Connections to propositional logi 53 6.3 Propositional intuitionistic logic 55

2.2 Free and bound variables, α-equivalence . . . . . . . . . . . . . . 12 2.3 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.4 Introduction to β-reduction . . . . . . . . . . . . . . . . . . . . . 16 2.5 Formal definitions of β-reduction and β-equivalence . . . . . . . 17 3 Programming in the untyped lambda calculus 18 3.1 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.2 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.3 Fixpoints and recursive functions . . . . . . . . . . . . . . . . . . 21 3.4 Other datatypes: pairs, tuples, lists, trees, etc. . . . . . . . . . . . 23 4 The Church-Rosser Theorem 25 4.1 Extensionality, η-equivalence, and η-reduction . . . . . . . . . . . 25 4.2 Statement of the Church-Rosser Theorem, and some consequences 27 4.3 Preliminary remarks on the proof of the Church-Rosser Theorem . 29 4.4 Proof of the Church-Rosser Theorem . . . . . . . . . . . . . . . . 31 4.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 5 Combinatory algebras 37 5.1 Applicative structures . . . . . . . . . . . . . . . . . . . . . . . . 38 5.2 Combinatory completeness . . . . . . . . . . . . . . . . . . . . . 39 5.3 Combinatory algebras . . . . . . . . . . . . . . . . . . . . . . . . 41 5.4 The failure of soundness for combinatory algebras . . . . . . . . . 42 5.5 Lambda algebras . . . . . . . . . . . . . . . . . . . . . . . . . . 44 5.6 Extensional combinatory algebras . . . . . . . . . . . . . . . . . 48 6 Simply-typed lambda calculus, propositional logic, and the Curry￾Howard isomorphism 50 6.1 Simple types and simply-typed terms . . . . . . . . . . . . . . . . 50 6.2 Connections to propositional logic . . . . . . . . . . . . . . . . . 53 6.3 Propositional intuitionistic logic . . . . . . . . . . . . . . . . . . 55 2

6.4 An altemative presentation of natural deduction 57 6.5 The Curry-Howard Isomorphism.... 5 6.Reductions in the simply-typed lambda calculus 6.7 A word on Church-Rosser .................... 62 68 Reduction as proof simplification 6 Getting mileage out of the Curry-Howard isomorphism 6.10 Disjunction and sum types.. 65 6.11 Classical logic vs.intuitionistic logic......... 6.12 Classical logic and the Curry-Howard isomorphism........ 69 7 Polymorphism 70 8 Weak and strong normalization 8.1 Definitions 70 8 Weak and strong normalization in typed lambdacalculus 71 9 Type inference 72 9.1 Principal types 73 92 Type templates and type substitutions 74 9.3 Unifiers 75 9.4 The unification algorithm. 76 9.5 The type inference algorithm 78 10 Denotational semantics 9 10.1 Set-theoretic interpretation 102 Soundness 82 10.3 Completeness 84 11 The language PCF 85 11.1 Syntax and typing rules 85 11.2 Axiomatic equivalence 86

6.4 An alternative presentation of natural deduction . . . . . . . . . . 57 6.5 The Curry-Howard Isomorphism . . . . . . . . . . . . . . . . . . 59 6.6 Reductions in the simply-typed lambda calculus . . . . . . . . . . 61 6.7 A word on Church-Rosser . . . . . . . . . . . . . . . . . . . . . 62 6.8 Reduction as proof simplification . . . . . . . . . . . . . . . . . . 63 6.9 Getting mileage out of the Curry-Howard isomorphism . . . . . . 64 6.10 Disjunction and sum types . . . . . . . . . . . . . . . . . . . . . 65 6.11 Classical logic vs. intuitionistic logic . . . . . . . . . . . . . . . . 67 6.12 Classical logic and the Curry-Howard isomorphism . . . . . . . . 69 7 Polymorphism 70 8 Weak and strong normalization 70 8.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 8.2 Weak and strong normalization in typed lambda calculus . . . . . 71 9 Type inference 72 9.1 Principal types . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 9.2 Type templates and type substitutions . . . . . . . . . . . . . . . 74 9.3 Unifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 9.4 The unification algorithm . . . . . . . . . . . . . . . . . . . . . . 76 9.5 The type inference algorithm . . . . . . . . . . . . . . . . . . . . 78 10 Denotational semantics 79 10.1 Set-theoretic interpretation . . . . . . . . . . . . . . . . . . . . . 80 10.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 10.3 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 11 The language PCF 85 11.1 Syntax and typing rules . . . . . . . . . . . . . . . . . . . . . . . 85 11.2 Axiomatic equivalence . . . . . . . . . . . . . . . . . . . . . . . 86 3

11.3 Operational semantics 。。。 11.4 Big-step semantics 90 11.5 Operational equivalence. 91 11.6 Operational approximation 2 11.7 Discussion of operational equivalence 11.8 Operational equivalence and parallel or 93 12 Complete partialorders 95 12.1 Why are sets not enough.in general? 95 12.2 Complete partial orders....................... 96 12.3 Properties of limits. 9 12.4 Continuous functions 12.5 Pointed cpo's and strict functions 98 126 Productsand function spaces 98 12.7The of the simply-typed lambda caculus in com- plete partia rder 12.8 Cpo's and fixpoints 101 12.9 Example:Streams 102 13 Denotational semantics of PCF 102 13.1 Soundness and adequacy 102 13.2 Full abstraction 104 14 Bibliography 气 1 Introduction 1.1 Extensional vs.intensional view of functions What is a function?In modern mathematics the prevalent notion is that of"func tions as graphs":each function f has a fixed domain X and codomain Y,and a

11.3 Operational semantics . . . . . . . . . . . . . . . . . . . . . . . . 87 11.4 Big-step semantics . . . . . . . . . . . . . . . . . . . . . . . . . 90 11.5 Operational equivalence . . . . . . . . . . . . . . . . . . . . . . . 91 11.6 Operational approximation . . . . . . . . . . . . . . . . . . . . . 92 11.7 Discussion of operational equivalence . . . . . . . . . . . . . . . 92 11.8 Operational equivalence and parallel or . . . . . . . . . . . . . . 93 12 Complete partial orders 95 12.1 Why are sets not enough, in general? . . . . . . . . . . . . . . . . 95 12.2 Complete partial orders . . . . . . . . . . . . . . . . . . . . . . . 96 12.3 Properties of limits . . . . . . . . . . . . . . . . . . . . . . . . . 97 12.4 Continuous functions . . . . . . . . . . . . . . . . . . . . . . . . 98 12.5 Pointed cpo’s and strict functions . . . . . . . . . . . . . . . . . . 98 12.6 Products and function spaces . . . . . . . . . . . . . . . . . . . . 98 12.7 The interpretation of the simply-typed lambda calculus in com￾plete partial orders . . . . . . . . . . . . . . . . . . . . . . . . . 100 12.8 Cpo’s and fixpoints . . . . . . . . . . . . . . . . . . . . . . . . . 101 12.9 Example: Streams . . . . . . . . . . . . . . . . . . . . . . . . . . 102 13 Denotational semantics of PCF 102 13.1 Soundness and adequacy . . . . . . . . . . . . . . . . . . . . . . 102 13.2 Full abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 14 Bibliography 106 1 Introduction 1.1 Extensional vs. intensional view of functions What is a function? In modern mathematics, the prevalent notion is that of “func￾tions as graphs”: each function f has a fixed domain X and codomain Y , and a 4

functionf:Y isaset of pairsf considered equal if they vield the same output on each input.i(=)for allX.This is called the extensional view of functions,because it specifies that the only thing observable about a function is how it maps inputs to outputs. However.before the 20th century.functions were rarely looked at in this wav An older notion of functions as that of"functions as rules" In this view,to give on means to give a ru for how the function s t .O 2 o(=sin(e)from calculus.As before.two functions are extensionally equal if they have the same input-output behavior,but now we can also speak of another notion of equality:two functions are intensionally equal if they are given by (essentially)the same formula When we think of functions as given by formulas,it is not always necessary to fof course.the identity function.We may regard it as a function ider for instance the function In most of mathematics,the"fu nctions as graphs"parad digm is the most s that a Thus.when we prove a mathematical statement such as"any differentiable func tion is continuou s",we really mean this is true all functions(in the mathematical sense).not just those functions for which a rule can be given On the other hand,in computer science,the "functions as rules"paradigm is often more appropriate.Think of a computer program as defining a function that maps progra rs (and puts).but also about the output is calculated:How much time does it take? How much memory and disk space is used in the process?How much communi cation bandwidth usd？ se are in nal questions having to do with the Note that this word is intentionally spelled Tntensionally

function f : X → Y is a set of pairs f ⊆ X × Y such that for each x ∈ X, there exists exactly one y ∈ Y such that (x, y) ∈ f. Two functions f, g : X → Y are considered equal if they yield the same output on each input, i.e., f(x) = g(x) for all x ∈ X. This is called the extensional view of functions, because it specifies that the only thing observable about a function is how it maps inputs to outputs. However, before the 20th century, functions were rarely looked at in this way. An older notion of functions as that of “functions as rules”. In this view, to give a function means to give a rule for how the function is to be calculated. Often, such a rule can be given by a formula, for instance, the familiar f(x) = x 2 or g(x) = sin(e x ) from calculus. As before, two functions are extensionally equal if they have the same input-output behavior; but now we can also speak of another notion of equality: two functions are intensionally1 equal if they are given by (essentially) the same formula. When we think of functions as given by formulas, it is not always necessary to know the domain and codomain of a function. Consider for instance the function f(x) = x. This is, of course, the identity function. We may regard it as a function f : X → X for any set X. In most of mathematics, the “functions as graphs” paradigm is the most elegant and appropriate way of dealing with functions. Graphs define a more general class of functions, because it includes functions that are not necessarily given by a rule. Thus, when we prove a mathematical statement such as “any differentiable func￾tion is continuous”, we really mean this is true all functions (in the mathematical sense), not just those functions for which a rule can be given. On the other hand, in computer science, the “functions as rules” paradigm is often more appropriate. Think of a computer program as defining a function that maps input to output. Most computer programmers (and users) do not only care about the extensional behavior of a program (which inputs are mapped to which out￾puts), but also about how the output is calculated: How much time does it take? How much memory and disk space is used in the process? How much communi￾cation bandwidth is used? These are intensional questions having to do with the particular way in which a function was defined. 1Note that this word is intentionally spelled “intensionally”. 5

1.2 The lambda calculus The lambda calculus is a theory of functions as formulas.It is a system for ma nipulating functions as expressions well-know l oressions are made up from variables num bers(L,2,3,.,and operators(“+",“-”,“x”etc.An expression such as+y add,or the that somet results explicitly.So for instance.we write A=(+)×2 and not let w=x+y,then let u=22,then let A=wx u The latter notation would be tiring and cumbersome to manipulate. Let f be the function2.Then consider A=f(5) in the lambda calculus we just write A-(x.x2)5 The expression r.stands for the function that mans r to r2 (as on osed to the group terms. It is understood that the called a bound variable. One advantage of the lambda notation is that it allows us to easily talk about higher-order functions ie functions whose inputs and or outputs are themselves xr.f(f()). 6

1.2 The lambda calculus The lambda calculus is a theory of functions as formulas. It is a system for ma￾nipulating functions as expressions. Let us begin by looking at another well-known language of expressions, namely arithmetic. Arithmetic expressions are made up from variables (x, y, z . . .), num￾bers (1, 2, 3, . . .), and operators (“+”, “−”, “×” etc.). An expression such as x+y stands for the result of an addition (as opposed to an instruction to add, or the statement that something is being added). The great advantage of this language is that expressions can be nested without any need to mention the intermediate results explicitly. So for instance, we write A = (x + y) × z 2 , and not let w = x + y, then let u = z 2 , then let A = w × u. The latter notation would be tiring and cumbersome to manipulate. The lambda calculus extends the idea of an expression language to include func￾tions. Where we normally write Let f be the function x 7→ x 2 . Then consider A = f(5), in the lambda calculus we just write A = (λx.x2 )(5). The expression λx.x2 stands for the function that maps x to x 2 (as opposed to the statement that x is being mapped to x 2 ). As in arithmetic, we use parentheses to group terms. It is understood that the variable x is a local variable in the term λx.x2 . Thus, it does not make any difference if we write λy.y2 instead. A local variable is also called a bound variable. One advantage of the lambda notation is that it allows us to easily talk about higher-order functions, i.e., functions whose inputs and/or outputs are themselves functions. An example is the operation f 7→ f ◦ f in mathematics, which takes a function f and maps it to f ◦ f, the composition of f with itself. In the lambda calculus, f ◦ f is written as λx.f(f(x)), 6

and the operation that mapsftoffis writtenas Xf.Xr.f(f(z)). The evaluation of highe -order functions can get somewhat complex;as an exam ple,consider the following expression: ((Xf.xr.f(f(z)))(Ay.y2))(5) Convince yourself that this evaluates to 625.Another example is given in the following exercise: Exercise 1.Evaluate the lambda-expression （(af.z.fff))(Ag.Awg(g())(Az.z+1)）O) We will soon introduce some conventions for reducing the number of parentheses in such expressions. 1.3 Untyped vs.typed lambda-calculi We have already mentioned that when considerir ns as rules”,isno always necessary to know the domain and codomain of a function ahead of time The simplest example is the identity functionf which can have any set ain and c main are that we encountered above.One can check that o maps any function f:X to a function(f):.In this case,we say that the type of g is (X→X)→(X一X). By being fle mains and codoma s,we are able to manipulate func po d e we can take r=f,and we get f(f)=(Ar.)(f)=f. As another example,letw=Ar.r()

and the operation that maps f to f ◦ f is written as λf.λx.f(f(x)). The evaluation of higher-order functions can get somewhat complex; as an exam￾ple, consider the following expression: ￾ (λf.λx.f(f(x)))(λy.y2 )
(5) Convince yourself that this evaluates to 625. Another example is given in the following exercise: Exercise 1. Evaluate the lambda-expression ￾ (λf.λx.f(f(f(x)))) (λg.λy.g(g(y)))
(λz.z + 1) (0). We will soon introduce some conventions for reducing the number of parentheses in such expressions. 1.3 Untyped vs. typed lambda-calculi We have already mentioned that, when considering “functions as rules”, is not always necessary to know the domain and codomain of a function ahead of time. The simplest example is the identity function f = λx.x, which can have any set X as its domain and codomain, as long as domain and codomain are equal. We say that f has the type X → X. Another example is the function g = λf.λx.f(f(x)) that we encountered above. One can check that g maps any function f : X → X to a function g(f) : X → X. In this case, we say that the type of g is (X → X) → (X → X). By being flexible about domains and codomains, we are able to manipulate func￾tions in ways that would not be possible in ordinary mathematics. For instance, if f = λx.x is the identity function, then we have f(x) = x for any x. In particular, we can take x = f, and we get f(f) = (λx.x)(f) = f. Note that the equation f(f) = f never makes sense in ordinary mathematics, since it is not possible (for set-theoretic reasons) for a function to be included in its own domain. As another example, let ω = λx.x(x). 7

Exercise 2.What is w(w)? We have several options regarding types in the lambda calculus .Untyped lambda calculus.In the untyped lambda calculus,we never specify his gives us maxim argument that it does not understand app Simply-tvped lambda calculus.In the simply-typed lambda calculus.we always completely specify the type of every expression.This is very simila to the situation in set theory.We e never allow the pplication of a runctio s the identity function .Polymorphically typed lambda calculus.This is an intermediate situation ance,that a term has a type of the form As we will see.each of these alternatives has dramatically different properties from the others. 1.4 Lambda calculus and computability In the 1930's,several people were interested in the question:what does it mean for a functionf:NNto be compuable?An informal definition of computability s that the should be a pencil-and-paper me thod allowing a trained erson t Tne concept or a penc the following definitions of computability: ers attempt ed pap 1.Turing defined an idealized computer we now call a Tiring machine,and

Exercise 2. What is ω(ω)? We have several options regarding types in the lambda calculus. • Untyped lambda calculus. In the untyped lambda calculus, we neverspecify the type of any expression. Thus we never specify the domain or codomain of any function. This gives us maximal flexibility. It is also very unsafe, because we might run into situations where we try to apply a function to an argument that it does not understand. • Simply-typed lambda calculus. In the simply-typed lambda calculus, we always completely specify the type of every expression. This is very similar to the situation in set theory. We never allow the application of a function to an argument unless the type of the argument is the same as the domain of the function. Thus, terms such as f(f) are ruled out, even if f is the identity function. • Polymorphically typed lambda calculus. This is an intermediate situation, where we may specify, for instance, that a term has a type of the form X → X for all X, without actually specifying X. As we will see, each of these alternatives has dramatically different properties from the others. 1.4 Lambda calculus and computability In the 1930’s, several people were interested in the question: what does it mean for a function f : N → N to be computable? An informal definition of computability is that there should be a pencil-and-paper method allowing a trained person to calculate f(n), for any given n. The concept of a pencil-and-paper method is not so easy to formalize. Three different researchers attempted to do so, resulting in the following definitions of computability: 1. Turing defined an idealized computer we now call a Turing machine, and postulated that a function is computable (in the intuitive sense) if and only if it can be computed by such a machine. 2. Godel ¨ defined the class of general recursive functions as the smallest set of functions containing all the constant functions, the successor function, and 8

closed und is general recursive. 3.Church defined an idealized programming language called the lambda cal an be written as a lar a term It was proved by Church,Kleene.Rosser,and Turing that all three computational of computable fun ns Whe mode notioof comutability isaquestion tht ao benseredbecause thereisn 1.5 Connections to computer science The lambda calculus is a very idealized programming language:arguably.it is the Because or Its simpl hining and proving properties of program Many real-world programming languages can be regarded as extensions of the input/output,side effects da calculus provide a a le for stu h extensions,in isolation and jointly,to see how the a well-formed rogram will n CPeiesofpoeramaminglanguae(SLc The lambda calculus is also a tool used in compiler construction,see e.g.[8.9]. 1.6 Connections to logic In the 19th and early 20th centuries,there was a philosophical dispute among t what a proof is.The 0-9 ists such as that it is sufficient to derive a contradiction from the assumption that it doesn't exist

closed under certain operations (such as compositions and recursion). He postulated that a function is computable (in the intuitive sense) if and only if it is general recursive. 3. Church defined an idealized programming language called the lambda cal￾culus, and postulated that a function is computable (in the intuitive sense) if and only if it can be written as a lambda term. It was proved by Church, Kleene, Rosser, and Turing that all three computational models were equivalent to each other, i.e., each model defines the same class of computable functions. Whether or not they are equivalent to the “intuitive” notion of computability is a question that cannot be answered, because there is no formal definition of “intuitive computability”. The assertion that they are in fact equivalent to intuitive computability is known as the Church-Turing thesis. 1.5 Connections to computer science The lambda calculus is a very idealized programming language; arguably, it is the simplest possible programming language that is Turing complete. Because of its simplicity, it is a useful tool for defining and proving properties of programs. Many real-world programming languages can be regarded as extensions of the lambda calculus. This is true for all functional programming languages, a class that includes Lisp, Scheme, Haskell, and ML. Such languages combine the lambda calculus with additional features, such as data types, input/output, side effects, udpateable memory, object orientated features, etc. The lambda calculus provides a vehicle for studying such extensions, in isolation and jointly, to see how they will affect each other, and to prove properties of programming language (such as: a well-formed program will not crash). The lambda calculus is also a tool used in compiler construction, see e.g. [8, 9]. 1.6 Connections to logic In the 19th and early 20th centuries, there was a philosophical dispute among mathematicians about what a proof is. The so-called constructivists, such as Brower and Heyting, believed that to prove that a mathematical object exists, one must be able to construct it explicitly. Classical logicians, such as Hilbert, held that it is sufficient to derive a contradiction from the assumption that it doesn’t exist. 9

Ironically,one of the better-known examples of a proof that isn't constructive is Brower's proof of his rem,wh h states that every continuou give anyinformation on the ocaion of the on and does n The connection between lambda calculu us and constructive logics is via the"proof must be a"construction ie.a program.The lambda calculus is a notation for such programs.and it can also be used as a notion for(constuctive)proofs. For the most part.constructivism has not prevailed as a philosophy in main mathematics.However.there has been renewed interest in constructivism in the second half of the 20th century.The reason is that constructive proofs give more information thanc lassical on s,and in articular,they allow one o compute so math for in ion) computer algebra systems 1.7 Connections to mathematics e given meaning such models are constructed u sing methods from algebra.partially ordered sets.topology,category theory.and other areas of mathematics 2 The untyped lambda calculus 2.1 Syntax The lambda calculus is a formal language.The expressions of the language are called fambda termts,and we will give rules for manipulating them iables d noted by.et Lambda terms:M.N::=(MN)|(Ar.M) The above Backus-Naur Form (BNF)is a convenient abbreviation for the follow ing equivalent,more traditionally mathematical definition:

Ironically, one of the better-known examples of a proof that isn’t constructive is Brower’s proof of his own fixpoint theorem, which states that every continuous function on the unit disc has a fixpoint. The proof is by contradiction and does not give any information on the location of the fixpoint. The connection between lambda calculus and constructive logicsis via the “proofs￾as-programs” paradigm. To a constructivist, a proof (of an existence statement) must be a “construction”, i.e., a program. The lambda calculus is a notation for such programs, and it can also be used as a notion for (constuctive) proofs. For the most part, constructivism has not prevailed as a philosophy in mainstream mathematics. However, there has been renewed interest in constructivism in the second half of the 20th century. The reason is that constructive proofs give more information than classical ones, and in particular, they allow one to compute solu￾tions to problems (as opposed to merely knowing the existence of a solution). The resulting algorithms can be useful in computational mathematics, for instance in computer algebra systems. 1.7 Connections to mathematics One way to study the lambda calculus is to give mathematical models of it, i.e., to provide spaces in which lambda terms can be given meaning. Such models are constructed using methods from algebra, partially ordered sets, topology, category theory, and other areas of mathematics. 2 The untyped lambda calculus 2.1 Syntax The lambda calculus is a formal language. The expressions of the language are called lambda terms, and we will give rules for manipulating them. Definition. Assume given an infinite set V of variables, denoted by x, y, z etc. The set of lambda terms is given by the following Backus-Naur Form: Lambda terms: M, N ::= x (MN) (λx.M) The above Backus-Naur Form (BNF) is a convenient abbreviation for the follow￾ing equivalent, more traditionally mathematical definition: 10