Modelling of Computer Systems
Table of Content
Chapter 8 Recursion and Inductive Definitions
8.1 InductivelyDefined Sets
8.2 InductivelyDefined Syntactic Sets
8.3 BackusNaur Form
8.4 InductivelyDefined Data Types
8.5 InductivelyDefined Functions
8.6 Recursive Functions
8.7 Recursive Procedures
Chapter 9 Mathematical Induction
9.1 Inconclusive Evidence
9.2 Induction Argument
9.4 Strong induction
9.5 Induction proof by induction definition
Chapter 10 Games and Strategy
10.1 Strategies for GamesofNoChange
10.2 NIM
10.3 Chomp
10.4 Hex
10.5 BridgIt
Chapter 11 Modelling Processes
11.1 Labelled Transition System
11.2 Processes
Chapter 12 Bisimulation Game
12.1 Bisimulation Game
12.2 Properties of Game Equivalence
13 Logical Properties of Processes
13.1 Mays and musts of processes
13.2 Modal Logic
1
,Modelling of Computer Systems
Chapter 8 Recursion and Inductive Definitions
8.1 InductivelyDefined Sets
Definition 8.1
An inductive definition of a set includes three components
1. The basis clause, which establishes that certain objects are in the set
2. The inductive clause, which defines the ways in which elements of a set can be used to
produce further elements which are also in the set
3. The extremal clause, where the set defined is the smallest set which satisfies the first two
clauses
Example 1
We can represent precisely the set ℕ of natural numbers by
1. 0 ϵ ℕ (basis clause)
2. (n+1) ϵ ℕ whenever n ϵ ℕ, in other words,
n ϵ ℕ ⇒ (n+1) ϵ ℕ (inductive clause)
3. Nothing else is in ℕ except those constructed from the first two clauses. In other words, ℕ
is the smallest set satisfying the first two clauses
Example 2
1. 1 ϵ ODD (basis clause)
2. if n ϵ ODD then (n+2) ϵ ODD (inductive clause)
3. The set ℕ also satisfies clauses 1 and 2 but is not the smallest set satisfying this, i.e. ODD
⊆ℕ
8.2 InductivelyDefined Syntactic Sets
Definition 8.2
The set A* of words over alphabet A is the smallest set satisfying
1. ε ϵ A*
2. if w ϵ A* and a ϵ A then aw ϵ A*
The set A+ of nonempty words over alphabet A is the smallest set satisfying
3. ε ϵ A+
4. if w ϵ A+ and a ϵ A then aw ϵ A+
“not” (¬), “or” (∨), and (∧), “implies” (⇒), “equivalent” (⇔)⊆
Exercise
Question: Define the set of positive decimal numbers PosDecNum. Such numbers should not
have leading zeros.
Answer: We define the set of PosDecNum as the smallest set satisfying
1. {1,2,3,4,5,6,7,8,9} ⊆ PosDecNum
2
, Modelling of Computer Systems
2. if m ϵ PosDecNum and n ϵ {0,1,2,3,4,5,6,7,8,9}
then mn ϵ PosDecNum
8.3 BackusNaur Form
Example
p ::= x:=e 1. The assignment statement “x:=e” assigns e to a variable x
| p1 ; p2 2. The sequential composition “p1 ; p2” of two smaller
| if b then p1 else p2 programs, where p2 executes when p1 terminates
| while b do p
8.4 InductivelyDefined Data Types
Definition 8.3
A list of natural numbers is defined by the BNF equation L ::= [ ] | n : L, where
n : natural number
[ ] : empty set
L : list
Example 1
[8,9,6,4]
= 8 : [9,6,4]
= 8 : (9 : [6,4])
= 8: (9 : (6 : [4]))
= 8 : (9 : (6 : (4 : [])))
Example 2
Binary trees are inductively defined by the BNF equation t ::= # | N(t1,t2) is represented by the
following picture:
3
