FM Thesis

Well, it's been a couple of days, but there's not an awful lot to say, so this will be short. It's also late, so I don't feel like going into great detail.

On Tuesday, I read chapter 10 of Using Z. That was the chapter on free types. Basically, it introduced how to define an arbitrary type, such as enumerated types. It also showed how to use free types to model a binary tree, which was kind of interesting.

Basically, there are a couple of ways to define a free type. One is by explicitly enumerating the possible values, like this:
Colors::= red|gree|blue
Another is with a constructor function. The general case of the constructor looks like this:
FreeType::= constant|constructor <<source>>
This is convenient for recursive definitions, as you can have a constant as your base case and reference the free type in the constructor. The simplest example was defining the natural numbers as follows:
nat::= zero | succ <<nat>>
Another interesting example was the following definition of a binary tree:
Tree::= leaf <<N>> | branch <<Tree x Tree>>
This defines a tree as either a numbered leaf node or an ordered pair of trees.

In addition to the expected sections on induction and primitive recursion that this chapter included, there was also a breif section on consistency. Free types makes it possible to introduce contradictions into our math. The example given was the definition:
T::= d <<&weierp; T>>
The problem here is that power sets are not finitary, whatever that means. The text leaves the term undefined, except to say that we basically need to stick to finite constructs to maintain consistency. Apparently the idea is that non-finitary (or is it infinitary?) constructs generate too many values, so we would end up with a set T that must be bigger than itself.

Anyway, yesterday and today I spent in reviewing the past five chapters of Using Z. Basically just looking over the key points and taking some notes. The symbols were all starting to run together, so I figured it would help make them stick in my memory if I wrote them down.