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))] )) )
-
- (get_length (list 20 30))
+ (define length
+ (lambda (lst) (if (null? lst) 0 [+ 1 (length (cdr lst))] )) )
+
+ (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
isn't well-defined. The point of interest here is that its definition
requires recursion in the function definition.)
-Neither do the resources we've so far developed suffice to define the
+Neither do the resources we've so far developed suffice to define the
[[!wikipedia Ackermann function]]:
A(m,n) =
###Fixed points###
In general, we call a **fixed point** of a function f any value *x*
-such that f <em>x</em> is equivalent to *x*. For example,
+such that f <em>x</em> is equivalent to *x*. For example,
consider the squaring function `sqare` that maps natural numbers to their squares.
`square 2 = 4`, so `2` is not a fixed point. But `square 1 = 1`, so `1` is a
-fixed point of the squaring function.
+fixed point of the squaring function.
There are many beautiful theorems guaranteeing the existence of a
fixed point for various classes of interesting functions. For
You should be able to immediately provide a fixed point of the
identity combinator I. In fact, you should be able to provide a whole
-bunch of distinct fixed points.
+bunch of distinct fixed points.
With a little thought, you should be able to provide a fixed point of
the false combinator, KI. Here's how to find it: recall that KI
###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))
At this point, we have a definition of the length function, though
it's not complete, since we don't know what value to use for the
symbol `length`. Technically, it has the status of an unbound
-variable.
+variable.
Imagine now binding the mysterious variable:
the argument we supply is already the length function we are trying to
define. (Dehydrated water: to reconstitute, just add water!)
-But this is just another way of saying that we are looking for a fixed point.
+But this is just another way of saying that we are looking for a fixed point.
Assume that `h` has a fixed point, call it `LEN`. To say that `LEN`
is a fixed point means that
h LEN <~~> LEN
-But this means that
+But this means that
(\list . if empty list then zero else add one (LEN (tail list))) <~~> LEN
The strategy we will present will turn out to be a general way of
finding a fixed point for any lambda term.
-##Deriving Y, a fixed point combinator##
+##Deriving Y, a fixed point combinator##
How shall we begin? Well, we need to find an argument to supply to
`h`. The argument has to be a function that computes the length of a
length of a list. Let's try applying `h` to itself. It won't quite
work, but examining the way in which it fails will lead to a solution.
- h h <~~> \list . if empty list then zero else 1 + h (tail list)
+ h h <~~> \list . if empty list then zero else 1 + h (tail list)
There's a problem. The diagnosis is that in the subexpression `h
(tail list)`, we've applied `h` to a list, but `h` expects as its
-first argument the length function.
+first argument the length function.
So let's adjust h, calling the adjusted function H:
H H <~~> (\h \list . if empty list then zero else 1 + ((h h) (tail list))) H
<~~> \list . if empty list then zero else 1 + ((H H) (tail list))
== \list . if empty list then zero else 1 + ((\list . if empty list then zero else 1 + ((H H) (tail list))) (tail list))
- <~~> \list . if empty list then zero
+ <~~> \list . if empty list then zero
else 1 + (if empty (tail list) then zero else 1 + ((H H) (tail (tail list))))
-
+
We're in business!
-How does the recursion work?
+How does the recursion work?
We've defined `H` in such a way that `H H` turns out to be the length function.
In order to evaluate `H H`, we substitute `H` into the body of the
lambda term. Inside the lambda term, once the substitution has
Works!
-##What is a fixed point for the successor function?##
+##What is a fixed point for the successor function?##
Well, you might think, only some of the formulas that we might give to the `successor` as arguments would really represent numbers. If we said something like:
sink true true false ~~> I
sink true true true false ~~> I
-So we make `sink = Y (\f b. b f I)`:
+So we make `sink = Y (\f b. b f I)`:
- 1. sink false
+ 1. sink false
2. Y (\fb.bfI) false
3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) false
4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) false
Now we try the next most complex example:
- 1. sink true false
+ 1. sink true false
2. Y (\fb.bfI) true false
3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) true false
4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) true false
You should be able to see that `sink` will consume as many `true`s as
we throw at it, then turn into the identity function after it
-encounters the first `false`.
+encounters the first `false`.
The key to the recursion is that, thanks to Y, the definition of
`sink` contains within it the ability to fully regenerate itself as
Without pretending to give a serious analysis of the paradox, let's
assume that sentences can have for their meaning boolean functions
like the ones we have been working with here. Then the sentence *John
-is John* might denote the function `\x y. x`, our `true`.
+is John* might denote the function `\x y. x`, our `true`.
Then (1) denotes a function from whatever the referent of *this
sentence* is to a boolean. So (1) denotes `\f. f true false`, where
Y C
(\f. (\h. f (h h)) (\h. f (h h))) I
- (\h. C (h h)) (\h. C (h h)))
+ (\h. C (h h)) (\h. C (h h)))
C ((\h. C (h h)) (\h. C (h h)))
C (C ((\h. C (h h))(\h. C (h h))))
C (C (C ((\h. C (h h))(\h. C (h h)))))
One obstacle to thinking this through is the fact that a sentence
normally has only two truth values. We might consider instead a noun
-phrase such as
+phrase such as
(3) the entity that this noun phrase refers to
The chameleon nature of (3), by the way (a description that is equally
good at describing any object), makes it particularly well suited as a
-gloss on pronouns such as *it*. In the system of
+gloss on pronouns such as *it*. In the system of
[Jacobson 1999](http://www.springerlink.com/content/j706674r4w217jj5/),
pronouns denote (you guessed it!) identity functions...