Z notation specification to modify content of a set

Question

Let's say I have a set:

S: Id X Counter

Id: \nat

Counter: \nat

Need help to define an operation filter which takes in two parameters, x:\nat and y:\nat which I can apply to S. This function will match on the first parameter with \exists a \in S @ first(a) = x and then reduce second(a) with y. If the value is less than or equal to zero, a should be removed from the set S, otherwise (first(a), second(a) - y) should replace a.

If the above is indecipherable, just please give me any example definition that operates over a set and modifies it.

Thanks.

Answer 1

Your set of pairs S of natural numbers is a Z relation between natural numbers. Let's give the set of all such relations a name:

natrel == ℕ ↔ ℕ

Since the filter function will only modify some part of S, it is convenient to describe that separately.

The modify operation produces for a given pair (x, y) of arguments and a relation S the set of maplets a ↦ b − y satisfying your description:

• The maplet a ↦ b with a = x is in S and
• the new value b − y is greater than zero.

As a Z "axiomatic description" it is:

│   
│   modify : (ℕ × ℕ) → (natrel → natrel)
│   
├───
│   
│   ∀ x, y : ℕ; S : natrel ⦁ 
│     modify (x, y) S =
│       { a, b : ℕ | a ↦ b ∈ S ∧ a = x ∧ b > y ⦁ a ↦ b − y }
│   

Note that modify (x, y) S may well be empty if there are no such maplets in S.

Deletion of a maplet a ↦ b ∈ S where b is too small is modeled simply by excluding it in the set comprehension.

Now the filter operation is easy to define:

│   
│   filter : (ℕ × ℕ) → (natrel → natrel)
│   
├───
│   
│   ∀ x, y : ℕ; S : natrel ⦁ 
│     (filter (x, y) S) = ({x} ⩤ S) ∪ (modify (x, y) S)
│   

So the result of filter (x, y) S is a set union of the unchanged part of S on the left hand side with the maplets given by modify (x, y) S on the right hand side:

• Pairs in S where the first element is not x are left unchanged and
• pairs in S where the first element is x are modified (replaced or deleted).