CSCI2408 DSD – Theory of Stacks

Type Stack

The stack is one of the simplest linear data structures whose access protocol is described as last-in-first-out (or, equivalently as first-in-last-out) Stacks are used extensively in many computer programs and typical applications include expression evaluation, parsing, and parameter passing.

Algebraic Specification

Type:

STACK

Sets:

STACK, Object, Boolean

Syntax:

nilStack	:	STACK
push	:	Object × STACK → STACK
pop	:	STACK → STACK
top	:	STACK → Object
isEmpty	:	STACK → Boolean

Axioms:

∀ x Î (Object - {error}); s ∈ (STACK - {error})

the following expressions yield true

1. isEmpty (nilStack)
2. ¬ isEmpty (push(x,s))
3. top (push(x,s)) = x
4. pop (push(x,s)) = s
5. top (nilStack) = error
6. pop (nilStack) = error
7. the functions push, pop, top and isEmpty are strict

We will refer to a particular stack axiom by prefixing its number with the letter S. Axiom S4 describes the characteristic behaviour of a stack. The functions which return stacks are constructor functions. The functions which return true or false are predicates. A function is strict if it returns error whenever any of its arguments is error.

Valid Stacks

If we assume that integers are contained in the type Object then the following expressions represent valid stacks.

1. nilStack
2. push (1, nilStack)
3. push (2, push (1, nilStack))
4. pop (push (2, push (1, nilStack)))
5. push (3, pop (push (2, push (1, nilStack))))
6. push (top (push (2, push (1, nilStack))), pop (push (1, nilStack)))

It is possible to simplify the last three examples by applying the stack axioms to reduce the stack expressions. We show the steps involved for each case below.

pop (push (2, push (1, nilStack)))

	pop (push (2, push (1, nilStack)))
≡	push (1, nilStack)	axiom S4

push (3, pop (push (2, push (1, nilStack))))

	push (3, pop (push (2, push (1, nilStack))))
≡	push (3, push (1, nilStack))	axiom S4

push (top (push (2, push (1, nilStack))), pop (push (1, nilStack)))

	push (top (push (2, push (1, nilStack))), pop (push (1, nilStack)))
≡	push (top (push (2, push (1, nilStack))), nilStack)	axiom S4
≡	push (2, nilStack)	axiom S3

Invalid Stacks

The following expressions do not represent valid stacks:

1. pop (nilStack)
2. push (2, pop (nilStack))
3. push (top (nilStack), nilStack)
4. push (2, pop (pop (push (1, nilStack))))

We will demonstrate that they are invalid by showing that each one reduces to error.

pop (nilStack)

	pop (nilStack)
≡	error	axiom S6

push (2, pop (nilStack))

	push (2, pop (nilStack))
≡	push (2, error)	axiom S6
≡	error	axiom S7

push (top (nilStack), nilStack)

	push (top (nilStack), nilStack)
≡	push (error, nilStack)	axiom S5
≡	error	axiom S7

push (2, pop (pop (push (1, nilStack))))

	push (2, pop (pop (push (1, nilStack))))
≡	push (2, pop (nilStack))	axiom S4
≡	push (2, error)	axiom S5
≡	error	axiom S7

Reduced Stack Expressions

The examples in the previous section indicate that every valid stack may be reduced to a normal form. The stack axioms provide the rules by which stack expressions can be reduced.

Definition – Reduced Stack Expression

A stack expression is in reduced form (i.e. it is a reduced stack expression) if it is either nilStack or an expression of the form push (x, s) where x denotes some valid object, and s is a reduced stack expression.

By using the axioms, all stack expressions can either be reduced or have the value error.

Exercises
Reduce each of the following stack expressions. You should indicate which axiom you are using at each stage of the reduction.

1. pop (push (2, nilStack))
2. push (3, pop (push (2, nilStack)))
3. pop (push (3, pop (push (2, nilStack))))
4. pop (pop (push (3, push (2, nilStack))))
5. pop (pop (pop (push (3, push (2, push (1, nilStack))))))
6. push (3, push (2, push (1, pop (pop (pop (nilStack))))))
7. push (top (push (2, nilStack)), nilStack)
8. pop (push (top (push (4, nilStack)), nilStack))
9. pop (push (top (pop (nilStack)), nilStack))
10. push (top (pop (push (2, push (3, nilStack)))), nilStack)