CSc 520
Principles of Programming Languages
:

Christian Collberg

Department of Computer Science

University of Arizona

1 Pure vs. Impure Lambda Calculus

• The version of lambda calculus we have looked at so far has been impure -- it has contained constants such as 1#1 and add, sqr, etc.
• Church's Thesis says that lambda calculus can define every computable function.
• If we're going to believe Church's Thesis we are going to have to define the natural numbers, arithmetic operations, booleans, pairs, conditional expressions and recursion, directly in the calculus.
• A lambda calculus so defined contains no constants, and is said to be pure.

2 Church's Numerals

• We can encode a natural number as the number of times a function parameter is applied:
  2#2
  
• We can now define arithmetic operations:
  3#3
  

3 Church's Numerals -- succ

• succ's first argument is 4#4, the number to be incremented. succ just adds one more application of the 5#5 function (its second argument). The third argument (6#6) is the ``base case'', that is, zero.
  7#7
  

4 Church's Numerals -- succ...

8#8

5 Church's Numerals -- add

• add takes two numbers 4#4 and 9#9 as arguments.
• 10#10 simply plugs in 5#5 as the function used to represent numbers in the expression for 9#9, 11#11 does the same for the second number.
• 12#12 (representing 13#13) constructs a new function 14#14 (representing 5).

15#15

6 Church's Numerals -- add...

16#16

7 Church's Numerals -- mult

• Multiplying 17#17 is like adding 9#9 copies of 4#4 together:

18#18

8 Pairs

• Just like in Scheme, we can define pairs -- these allow us to construct data structures such as lists and trees.
• The definition of 19#19 below is similar to a dotted pair notation (or cons) in Scheme.
• 20#20 and 21#21 correspond to car and cdr, 22#22 is a special constant.

23#23

9 Pairs...

• We can construct a pair 24#24 (or 25#25 in Scheme notation) like this:

26#26

10 Pairs...

• We can construct the list 27#27 like this:

28#28

• We can go even further and substitute in the definition of 2.

11 Pairs...

• We can construct the list 29#29 like this:

30#30

12 Pairs...

• We can verify that Head works as specified:

31#31

13 Church's Booleans

• We define two constants for true and false, and a function if for selection:

32#32

• We can now write programs with control flow!

14 Church's Booleans...

• We can verify that if works as expected:

33#33

15 Church's Booleans...

• and can be defined like this:

34#34

16 Church's Booleans...

• iszero can be defined like this:

35#35

Recursion

17 Recursive Functions

• If lambda calculus is going to allow us to compute any function, we need for it to handle recursion.
• Example:
  
  36#36
  
  

• Unfortunately, the name 37#37 appears in the expression itself. Remember that we defined 38#38-operator as macro-expansion, and recursive macros make no sense.
• Recursion is defined in normal programming languages, but not in lambda calculus.

18 Fixed Points

• A fixed point is a value 6#6 in the domain of a function that is the same in the range 39#39.
• In other words, a fixed point of a function is a value left fixed by that function; for example, 0 and 1 are fixed points of the squaring function.
• Formally, a value 6#6 is a fixed point of a function 5#5 if
  
  40#40
  
  

19 Fixed Points -- Examples

• Every value in the domain of the identity function is a fixed point: 41#41
• 42#42
• 43#43
• 44#44
• 45#45
• 46#46
• 47#47

20 Fixed Points -- Examples...

5#5	fixed point
48#48	6
49#49	3
50#50	2,-2
51#51	every value
52#52	no value

• I.e., a fixed point is where you get back whatever you put in!

21 Fixed Point Combinators

• A combinator is a lambda-expression with no free variables.
• A fixed point combinator is a function 53#53 which, given another function 5#5, computes a fixed point of 5#5, so that
  
  54#54
  
  
  for all functions 5#5.
• Let's look at the fact function again:
  
  55#55
  
  

22 Fixed Point Combinators...

• Let's turn
  
  36#36
  
  
  into a higher-order function, by replacing the call to fact with a function 5#5
  
  56#56
  
  

• Now, pass fact to ffact as a parameter, and do a :
  
  57#57
  
  

23 Fixed Point Combinators...

• But, the right-hand side of
  
  57#57
  
  
  is just the body of fact
  
  36#36
  
  
  so we can write the identity:
  
  58#58
  
  

• Thus, fact is a fixed point for ffact.

24 Fixed Point Combinators...

• In lambda calculus, the fixed point combinator 59#59 is defined as
  
  60#60
  
  

• Let's see what happens when we apply that to an expression 61#61:
  62#62
  

25 Fixed Point Combinators...

• So, we saw that
  
  63#63
  
  

• In other words,
  
  64#64
  
  
  or for any expression 61#61, 65#65 is a fixed point for 61#61.

26 Fixed Point Combinators -- Example

• Let's get back to our definition of fact:
  
  36#36
  
  
  and the beta abstracted version ffact (we'll call it 66#66 for brevity)
  
  67#67
  
  

• And, so we can define
  
  68#68
  
  

• Let's try to evaluate
  
  69#69
  
  

27 Fixed Point Combinators -- Example...

70#70

• Where we've used the abbreviation
  
  71#71
  
  

28 Fixed Point Combinators -- Example...

72#72

29 Fixed Point Combinators -- Example...

73#73

30 Fixed Point Combinators -- Example...

74#74

31 Fixed Point Functions in Haskell

75#75

32 Fixed Point Functions in Haskell...

76#76

33 Readings and References

• Read pp. 156-157, in Syntax and Semantics of Programming Languages, by Ken Slonneger and Barry Kurtz, http://www.cs.uiowa.edu/~slonnegr/plf/Book.
• Read pp. 618-621, in Scott.

34 Acknowledgments

• Much of the material in this lecture on Lambda Calculus is taken from the book Syntax and Semantics of Programming Languages, by Ken Slonneger and Barry Kurtz, http://www.cs.uiowa.edu/~slonnegr/plf/Book.