A Hierarchy of Data Types: From Trees to Sets

Abstract

In Section 4.4.1 we have introduced equational attributes as a means of declaring some equational properties of binary operators that allow Maude to use these properties efficiently in a built-in way in parsing and in matching modulo such equational axioms. We recall that Maude supports the following equational attributes:

• assoc (associativity),

• comm (commutativity),

• id:$\langle Term\rangle$ (identity, with the corresponding term for the identity element), with variations for left identity and right identity, and

• idem (idempotency).

An important restriction to bear in mind is that the assoc and idem attributes cannot be used together in any combination.

In this chapter we will show that equational attributes correspond to structural axioms of well-known data types built with a binary constructor operator. In this way we obtain a hierarchy of data types:

• non-empty binary trees, with elements only in their leaves, built with a free binary constructor, that is, a constructor with no equational axioms;

• non-empty lists, built with an associative constructor;

• lists, built with an associative constructor and an identity;

• multisets (or bags), built with an associative and commutative constructor and an identity; and

• sets, built with an associative, commutative, and idempotent constructor and an identity.

All these data types are generic, so that they can be constructed on top of any given data type of basic elements; for example, we can have lists of natural numbers, lists of Booleans, lists of sets of integers, etc. This genericity corresponds to making use of parameterized modules in Maude, which will be introduced later in Section 8.3. Therefore, in this chapter we only consider constructions over natural numbers. In Section 9.12 we will describe the predefined parameterized versions of lists and sets provided in the Maude prelude, and in Chapter 10 we will describe many other parameterized data types, like stacks, queues, sorted lists, multisets, and different versions of trees.