[[!toc]]
+#Recursion: fixed points in the lambda calculus##
+
+Sometimes when you type in a web search, Google will suggest
+alternatives. For instance, if you type in "Lingusitics", it will ask
+you "Did you mean Linguistics?". But the engineers at Google have
+added some playfulness to the system. For instance, if you search for
+"anagram", Google asks you "Did you mean: nag a ram?" And if you
+search for "recursion", Google asks: "Did you mean: recursion?"
+
##What is the "rec" part of "letrec" doing?##
How could we compute the length of a list? Without worrying yet about what lambda-calculus implementation we're using for the list, the basic idea would be to define this recursively:
In OCaml, you'd define that like this:
- let rec get_length = fun lst ->
- if lst == [] then 0 else 1 + get_length (tail lst)
- in ... (* here you go on to use the function "get_length" *)
+ let rec length = fun lst ->
+ if lst == [] then 0 else 1 + length (tail lst)
+ in ... (* here you go on to use the function "length" *)
In Scheme you'd define it like this:
- (letrec [(get_length
- (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
- ... ; here you go on to use the function "get_length"
+ (letrec [(length
+ (lambda (lst) (if (null? lst) 0 [+ 1 (length (cdr lst))] )) )]
+ ... ; here you go on to use the function "length"
)
Some comments on this:
2. `cdr` is function that gets the tail of a Scheme list. (By definition, it's the function for getting the second member of an ordered pair. It just turns out to return the tail of a list because of the particular way Scheme implements lists.)
-3. I use `get_length` instead of the convention we've been following so far of hyphenated names, as in `make-list`, because we're discussing OCaml code here, too, and OCaml doesn't permit the hyphenated variable names. OCaml requires variables to always start with a lower-case letter (or `_`), and then continue with only letters, numbers, `_` or `'`. Most other programming languages are similar. Scheme is very relaxed, and permits you to use `-`, `?`, `/`, and all sorts of other crazy characters in your variable names.
+3. I use `length` instead of the convention we've been following so far of hyphenated names, as in `make-list`, because we're discussing OCaml code here, too, and OCaml doesn't permit the hyphenated variable names. OCaml requires variables to always start with a lower-case letter (or `_`), and then continue with only letters, numbers, `_` or `'`. Most other programming languages are similar. Scheme is very relaxed, and permits you to use `-`, `?`, `/`, and all sorts of other crazy characters in your variable names.
4. I alternate between `[ ]`s and `( )`s in the Scheme code just to make it more readable. These have no syntactic difference.
The main question for us to dwell on here is: What are the `let rec` in the OCaml code and the `letrec` in the Scheme code?
-Answer: These work like the `let` expressions we've already seen, except that they let you use the variable `get_length` *inside* the body of the function being bound to it---with the understanding that it will there refer to the same function that you're then in the process of binding to `get_length`. So our recursively-defined function works the way we'd expect it to. In OCaml:
+Answer: These work like the `let` expressions we've already seen, except that they let you use the variable `length` *inside* the body of the function being bound to it---with the understanding that it will there refer to the same function that you're then in the process of binding to `length`. So our recursively-defined function works the way we'd expect it to. In OCaml:
- let rec get_length = fun lst ->
- if lst == [] then 0 else 1 + get_length (tail lst)
- in get_length [20; 30]
+ let rec length = fun lst ->
+ if lst == [] then 0 else 1 + length (tail lst)
+ in length [20; 30]
(* this evaluates to 2 *)
In Scheme:
- (letrec [(get_length
- (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
- (get_length (list 20 30)))
+ (letrec [(length
+ (lambda (lst) (if (null? lst) 0 [+ 1 (length (cdr lst))] )) )]
+ (length (list 20 30)))
; this evaluates to 2
If you instead use an ordinary `let` (or `let*`), here's what would happen, in OCaml:
- let get_length = fun lst ->
- if lst == [] then 0 else 1 + get_length (tail lst)
- in get_length [20; 30]
+ let length = fun lst ->
+ if lst == [] then 0 else 1 + length (tail lst)
+ in length [20; 30]
(* fails with error "Unbound value length" *)
Here's Scheme:
- (let* [(get_length
- (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
- (get_length (list 20 30)))
- ; fails with error "reference to undefined identifier: get_length"
+ (let* [(length
+ (lambda (lst) (if (null? lst) 0 [+ 1 (length (cdr lst))] )) )]
+ (length (list 20 30)))
+ ; fails with error "reference to undefined identifier: length"
Why? Because we said that constructions of this form:
- let get_length = A
+ let length = A
in B
really were just another way of saying:
- (\get_length. B) A
+ (\length. B) A
-and so the occurrences of `get_length` in A *aren't bound by the `\get_length` that wraps B*. Those occurrences are free.
+and so the occurrences of `length` in A *aren't bound by the `\length` that wraps B*. Those occurrences are free.
-We can verify this by wrapping the whole expression in a more outer binding of `get_length` to some other function, say the constant function from any list to the integer 99:
+We can verify this by wrapping the whole expression in a more outer binding of `length` to some other function, say the constant function from any list to the integer 99:
- let get_length = fun lst -> 99
- in let get_length = fun lst ->
- if lst == [] then 0 else 1 + get_length (tail lst)
- in get_length [20; 30]
+ let length = fun lst -> 99
+ in let length = fun lst ->
+ if lst == [] then 0 else 1 + length (tail lst)
+ in length [20; 30]
(* evaluates to 1 + 99 *)
-Here the use of `get_length` in `1 + get_length (tail lst)` can clearly be seen to be bound by the outermost `let`.
+Here the use of `length` in `1 + length (tail lst)` can clearly be seen to be bound by the outermost `let`.
-And indeed, if you tried to define `get_length` in the lambda calculus, how would you do it?
+And indeed, if you tried to define `length` in the lambda calculus, how would you do it?
- \lst. (isempty lst) zero (add one (get_length (extract-tail lst)))
+ \lst. (isempty lst) zero (add one (length (extract-tail lst)))
-We've defined all of `isempty`, `zero`, `add`, `one`, and `extract-tail` in earlier discussion. But what about `get_length`? That's not yet defined! In fact, that's the very formula we're trying here to specify.
+We've defined all of `isempty`, `zero`, `add`, `one`, and `extract-tail` in earlier discussion. But what about `length`? That's not yet defined! In fact, that's the very formula we're trying here to specify.
What we really want to do is something like this:
2. If you tried this in Scheme:
- (define get_length
- (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )
+ (define length
+ (lambda (lst) (if (null? lst) 0 [+ 1 (length (cdr lst))] )) )
- (get_length (list 20 30))
+ (length (list 20 30))
You'd find that it works! This is because `define` in Scheme is really shorthand for `letrec`, not for plain `let` or `let*`. So we should regard this as cheating, too.
-3. In fact, it *is* possible to define the `get_length` function in the lambda calculus despite these obstacles. This depends on using the "version 3" implementation of lists, and exploiting its internal structure: that it takes a function and a base value and returns the result of folding that function over the list, with that base value. So we could use this as a definition of `get_length`:
+3. In fact, it *is* possible to define the `length` function in the lambda calculus despite these obstacles. This depends on using the "version 3" implementation of lists, and exploiting its internal structure: that it takes a function and a base value and returns the result of folding that function over the list, with that base value. So we could use this as a definition of `length`:
\lst. lst (\x sofar. successor sofar) zero
fold-based implementation of lists, and Church's implementations of
numbers, have a internal structure that *mirrors* the common recursive
operations we'd use lists and numbers for. In a sense, the recursive
-structure of the `get_length` operation is built into the data
+structure of the `length` operation is built into the data
structure we are using to represent the list. The non-recursive
-version of get_length exploits this embedding of the recursion into
+version of length exploits this embedding of the recursion into
the data type.
This is one of the themes of the course: using data structures to
###How fixed points help definie recursive functions###
-Recall our initial, abortive attempt above to define the `get_length` function in the lambda calculus. We said "What we really want to do is something like this:
+Recall our initial, abortive attempt above to define the `length` function in the lambda calculus. We said "What we really want to do is something like this:
\list. if empty list then zero else add one (... (tail lst))