Relay-Version: version B 2.10.2 9/18/84 +2.11; site uk.ac.ox.prgv Posting-Version: version B 2.10.3 uknet 86/05/14; site uk.ac.oxford.prg Path: prgv!geraint From: Ruaridh Macdonald (on UK.MOD.RSRE) Newsgroups: zforum Subject: Z Forum Issue 2.4 Message-ID: <19 Date: 19 Nov 87 15:22:57 GMT Date-Received: 19 Nov 87 15:24:13 GMT Lines: 162 19th November 1987 Z FORUM Volume 2 Issue 4 ------------------ ------- ---------------- Today's Topics -------------- Bags, Extensionality and Disjointness Z Users Meeting --------------------------------------------------------------------- Date: Wed, 18 Nov 87 11:55:17 GMT From: mike@uk.ac.oxford.prg Subject: Bags, Extensionality and Disjointness BAGS, EXTENSIONALITY and DISJOINTNESS by Mike Spivey Here are a few observations about some details of the Z library; first, a discussion about the precise definition of (bag X), then an observation about (disjoint _). BAGS. It is tempting to say that a bag of elements of X is the same as a function which assigns a natural number to each element of X: bag X == X --> Nat. (Wrong) This leads to a problem with extensionality, by which I mean the property that two bags are equal if the same elements appear in them the same number of times. For example, the empty bag of natural numbers would be lambda n: Nat . 0, and the empty bag of primes would be lambda n: Prime . 0, and these are different -- in particular, they have different domains. The solution I have adopted is to define a bag as a partial function into the strictly positive integers Nat1: bag X == X -+> Nat1. Now the domain is just the set of elements which appear in the bag at least once, and we can define the bag membership relation (_ inbag _) [which is printed as "in", but I'm using that for set membership here] by x inbag B <==> x in (dom B). The function count: bag X --> (X --> Nat) gives the number of times any element occurs in a bag: count B = (lambda x: X . 0) oplus B. `oplus' is functional overriding. These bags are potentially infinite: although each element appears a finite number of times, it is possible to have an infinite number of different elements. Finite bags belong to the set fbag X == { B: bag X | dom B in F X }. `F X' is the collection of finite subsets of X. Two other functions defined in the Reference manual are bag union -- written as a union sign with a plus sign inside it, and items, which gives the bag of elements of a sequence. Bags can be written explicitly using fat square brackets. DISJOINTNESS: It doesn't make much sense to talk about a set of disjoint sets; its much better to talk about an indexed family of disjoint sets. The reason for this is simple: if we say disjoint { S, T } (Wrong) then this is bound to mean that EITHER S cap T = {} OR S = T. If S = T, then { S, T } = { S }, and any singleton set of sets is bound to be disjoint. To avoid this problem, I describe disjointness in terms of indexed families of sets, i.e. in terms of functions I -+> P X, where I is an indexing set. Here is the definition: == [I,X] ======================= | disjoint _: P(I -+> P X) ---------------- | forall S: I -+> P X . | disjoint S <==> | (forall i, j: dom S . i /= j ==> S(i) cap S(j) = {}) -------------------------------- The most common kind of indexed family of sets is a sequence of sets; just take the indexing set I to be Nat. So we can write disjoint < S, T > as a fancy way of saying S cap T = {}. But other indexing sets are also useful: if property: Ratepayer --> P House, (remember the Z course?) we can say that no house is owned by more than one person, forall p, q: Ratepayer . p /= q ==> property(p) cap property(q) = {}, by the simple predicate disjoint property. --------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Thu, 19 Nov 87 14:44 Subject: Z Users Meeting Z TUTORIAL AND Z USERS MEETING Dates: 7th and 8th December 1987 Venue: Department of External Studies, 1 Wellington Square, Oxford. TUTORIAL: A one day tutorial will be held on 7th December, given by members of the Programming Research Group. USERS MEETING: A users meeting will be held on 8th December. The topics to be presented will be: Recent developments in Z notation and development methods. Z standards and tools. Plans for Z education. Methods of refinement. Reports from users of Z. In addition, special project meetings will be held on 9th December. If you would like any further information about any of the above, please contact: Miss Emma Sowton, Programming Research Group, Computing Laboratory, 8-11 Keble Road, OXFORD OX1 3QD Tel.: (0865) 273849 ************************* END OF Z FORUM 2.4 ************************