Today I read the sequences chapter of *Using Z*. I'd not been exposed to sequences before, so this was relatively new to me. Intuitively, a sequence is an ordered series of items that allows repetition, such as <a, b, b, c, a>. It turns out that sequences can also be viewed as functions from the natural numbers to some set of objects. Needless to say, this simplifies things from a conceptual standpoint, as it allows the reuse of a lot of mathematical language.

The chapter covered basics such as the definition of a sequence, operations such as concatenation and filtering, as well as functions for the head and tail of the sequence, reversing, etc.

This chapter also went into structural induction to prove properties of sequences. This was initially confusing to me, as they didn't give the usual symbolic statement of the proof rule for structural induction. They also define axioms for the equivalence of the predicate to be proved and construct the proof using those. It took me a couple of proofs to realize that the defined axiom was how they were getting form "*P s*" to some complex predicate.

Lastly, they introduced the idea of bags, which are basically sequences without order. Bags can be represented as a function from a set of objects to the natural number, where the number in the range represents the number of times the item is in the bag. This section also introduced bag-equivalents of set membership and subset, as well bag union and difference operators. The latter simply involve adding or subtracting the number of elements for each bag involved to get the resulting bag. The only odd thing I found was that the difference operator is a union cup with a minus sign in it, whereas I'd have thought an intersection cap would have been more appropriate. Oh well....

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.