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 <<℘ 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.

You can reply to this entry by leaving a comment below. You can send TrackBack pings to this URL. This entry accepts Pingbacks from other blogs. You can follow comments on this entry by subscribing to the RSS feed.

## Add your comments #

A comment body is required. No HTML code allowed. URLs starting with http:// or ftp:// will be automatically converted to hyperlinks.