Homework VI

1. [20 points]

Consider the binary relation ∆ on natural numbers, Nat = {0, 1, 2, … }, defined by m ∆ n if the set of decimal digits appearing in m is the same as the set appearing in n (e.g., 26 ∆ 622 and 1003 ∆ 301).

(a) Show that ∆ is an equivalence relation,

(b) Describe the equivalence classes of Nat under ∆,

(c) Determine whether or not ∆ is a congruence for addition (i.e., if m ∆ n and j ∆ k, must it always be the case that m+j ∆ n+k?), and justify your answer.

2. [20 points]

An ADT describing natural numbers has been realized as a Miranda algebraic data type in our class directory /group/class/22c181/nat.m. It can be seen from experiments with evaluations in this ADT, that Miranda realizes the initial algebra semantics for this ADT. The isomorphism of classes of terms to the usual natural numbers is apparent, and is one of the functions defined in the script.

For this problem, add axioms to this specification of Nat for operations 'mul' (for multiplication) and 'mod3' (for remainder modulo 3) that characterize these familiar operations (i.e., imply the expected behavior). You should use Miranda to prototype your specification, and provide sufficient testing to illustrate the correctness of your axioms for all possible cases of arguments. In addition to submitting a printed script showing tests of your solution, you should submit your Miranda code (only) electronically to our class submit directory Hwk6.

3. [30 points]

For this problem you should add to the pushdown stack ADT example of Figure 1, equations to specify an additional operation BOT:Stack -> Nat whose informal description is that it returns the bottom item of a Stack object. Justify your specification with either (your choice) analysis arguing that the desired behavior is implied, or a Miranda animation that illustrates correct behavior (see stack.m in class directory); if you choose the latter option, you should turn in a printed script of tests, and submit your Miranda code (only) electronically to our class submit directory Hwk6.

NEW: ® Stack

PUSH: Stack ´ Integer ® Stack

POP: Stack ® Stack

TOP: Stack ® Nat

ISEMPTY: Stack -> Boolean

Nat and Boolean are pre-defined as the familiar types

===================================

for each sÎStack and nÎNat

POP(PUSH(s,n)) = s

TOP(PUSH(s,n)) = n

ISEMPTY(NEW) = True

ISEMPTY(Push(s,n)) = False

Figure 1: Pushdown Stack ADT