Minutes and Next Week's Reading

[Joe Razavi]

Hi,

For next week's group, I think it would be best to finish off
discussing the untyped lambda calculus, and not progress any further
through the notes. That will let everybody get comfortable before we
move on (and give me a chance to think a bit harder about the next
reading, which requires some thought!).

Perhaps some exercises would be a good idea: I'll do 1.7.4, 1.7.18,
1.7.19, and 1.7.20.

Since quite a few people didn't make it to the last meeting, I have
some very terse minutes -- perhaps we can flesh out these concepts on
Monday?

> We examined this notion of "smallest" again. (i.e. "the smallest relation satisfying ...") the intended meaning is that the things related by the relation are only those compelled to be so by the conditions, and no others.
Of course, the cardinality of this relation (thought of as a set) may
be equal to the cardinality of various other plausible candidates;
what then did we mean by "smallest"?
The idea is that we can think of the subset relation as an order
relation -- then our required set is the minimum, under this order, of
all possible candidates allowed by the condition.

For a careful study of this idea, you could read Enderton's "Elements
of Set Theory" chapter 4, in which he defines the natural numbers
using this trick, and then *derives* that we get principles of
induction and recursion.


> To examine the concept of "primitive recursion" mentioned in the reading, we raised the inevitable spectre of the Ackermann function, which is recursive but grows more quickly than any primitive recursive function.


> To examine the concept of recursiveness, we examined the non-recursive example from the reading, pointing out that it is our old friend the diagonal argument dressed up as a function. After the discussion, I realized that I don't see where the special properties of the example are used -- in other words, why doesn't it prove that all sets are not recursive!?

See you on Monday,

Joe

[Giles Reger]

Hi all,

I think it's a good idea to make sure we're comfortable with the untyped lambda calculus - if not for any other reason than the fact that it's exciting.

I've done some of the exercises and am going to type them up. I haven't done any more work on the proof as I got side tracked by something - when looking at Exercise 1.1.17 I wanted to show that the given term was a fixed point combinator by running it. So, I've implemented the untyped lambda calculus in Scala to play with things like that - this also helps in defining datatypes and operations on them (Exercises 1.1.18-23).

I'm sharing the drop box folder I'll be putting all this stuff in so that other people can look at it if they want (you should all receive an email shortly). The started proof is in there too (may be wrong). I'm keen for people to share things and especially keen for people to tell me what I've got wrong and when I say stupid things - it's a very useful part of learning.

If you want to run the Scala stuff (Scala is a really cool cross between a functional and object-orientated language which compiles down to Java bytecode) you can either get the Eclipse plugin (www.scala-ide.org/) or download the compiler (www.scala-lang.org/downloads) and run it with Java. If you want to see a better implementation of the untyped lambda calculus and other similar things (and know OCaml) see Benjamin C.Pierce's website (http://www.cis.upenn.edu/~bcpierce/tapl/index.html) - his book is a very good practical introduction to type theory.

An additional exercise - write the lambda term to compute the nth Fibonacci number. 

See you all tomorrow,

Giles