Operational Semantics

Hongfei Fu

John Hopcroft Center for Computer Science

Shanghai Jiao Tong University

Mar. 19th, 2020

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 1 / 59
Previous Lecture

an introduction to operational semantics

rules and derivation trees

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 2 / 59
Today’s Topic

equivalence of commands through derivations

one-step operational semantics
mathematical induction over derivations

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 3 / 59
 Equivalence of Commands

textbook, Page 19 – 24

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 4 / 59
Equivalence of Commands

Definition
definition: ⟨c, σ⟩ → σ ′ iff there is a derivation tree with conclusion
⟨c, σ⟩ → σ ′ .
equivalence: c ∼ c′ iff ∀σ, σ ′ . (⟨c, σ⟩ → σ ′ ⇔ ⟨c′ , σ⟩ → σ ′ )

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 5 / 59
Equivalence of Commands

w = while b do c;
w ∼ if b then c; w else skip

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 6 / 59
Equivalence of Commands

w = while b do c;
for all states σ, σ ′ ,
⟨w, σ⟩ → σ ′ iff ⟨if b then c; w else skip, σ⟩ → σ ′ .

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 7 / 59
Equivalence of Commands

Proof
⟨w, σ⟩ → σ ′ implies ⟨if b then c; w else skip, σ⟩ → σ ′ .

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 8 / 59
Equivalence of Commands

⟨w, σ⟩ → σ ′ implies ⟨if b then c; w else skip, σ⟩ → σ ′ .

Case 1: ⟨b, σ⟩ → false

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 9 / 59
Equivalence of Commands

⟨w, σ⟩ → σ ′ implies ⟨if b then c; w else skip, σ⟩ → σ ′ .

Case 1: ⟨b, σ⟩ → false
from the rule for while-loop:
..
.
⟨b, σ⟩ → false
(σ ′ = σ)
⟨w, σ⟩ → σ

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 9 / 59
Equivalence of Commands

⟨w, σ⟩ → σ ′ implies ⟨if b then c; w else skip, σ⟩ → σ ′ .

Case 1: ⟨b, σ⟩ → false
from the rule for while-loop:
..
.
⟨b, σ⟩ → false
(σ ′ = σ)
⟨w, σ⟩ → σ

thus:
..
.
⟨b, σ⟩ → false ⟨skip, σ⟩ → σ
⟨if b then c; w else skip, σ⟩ → σ
. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 9 / 59
Equivalence of Commands

⟨w, σ⟩ → σ ′ implies ⟨if b then c; w else skip, σ⟩ → σ ′ .

Case 2: ⟨b, σ⟩ → true

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 10 / 59
Equivalence of Commands

⟨w, σ⟩ → σ ′ implies ⟨if b then c; w else skip, σ⟩ → σ ′ .

Case 2: ⟨b, σ⟩ → true
from the rule for while-loop:
.. .. ..
. . .
⟨b, σ⟩ → true ⟨c, σ⟩ → σ ⟨w, σ ⟩ → σ ′
′′ ′′

⟨w, σ⟩ → σ ′

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 10 / 59
Equivalence of Commands

⟨w, σ⟩ → σ ′ implies ⟨if b then c; w else skip, σ⟩ → σ ′ .

Case 2: ⟨b, σ⟩ → true
from the rule for while-loop:
.. .. ..
. . .
⟨b, σ⟩ → true ⟨c, σ⟩ → σ ⟨w, σ ⟩ → σ ′
′′ ′′

⟨w, σ⟩ → σ ′

it follows that:
.. ..
. .
⟨c, σ⟩ → σ ⟨w, σ ⟩ → σ ′
′′ ′′

⟨c; w, σ⟩ → σ ′
. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 10 / 59
Equivalence of Commands

⟨w, σ⟩ → σ ′ implies ⟨if b then c; w else skip, σ⟩ → σ ′ .

Case 2: ⟨b, σ⟩ → true
it follows that:
.. ..
. .
⟨c, σ⟩ → σ ′′ ⟨w, σ ′′ ⟩ → σ ′
⟨c; w, σ⟩ → σ ′

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 11 / 59
Equivalence of Commands

⟨w, σ⟩ → σ ′ implies ⟨if b then c; w else skip, σ⟩ → σ ′ .

Case 2: ⟨b, σ⟩ → true
it follows that:
.. ..
. .
⟨c, σ⟩ → σ ′′ ⟨w, σ ′′ ⟩ → σ ′
⟨c; w, σ⟩ → σ ′

hence:
.. ..
. .
..
. ⟨c, σ⟩ → σ ⟨w, σ ⟩ → σ ′
′′ ′′

⟨b, σ⟩ → true ⟨c; w, σ⟩ → σ ′

⟨if b then c; w else skip, σ⟩ → σ ′

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 11 / 59
Equivalence of Commands

⟨if b then c; w else skip, σ⟩ → σ ′ implies ⟨w, σ⟩ → σ ′ .

Case 1:
..
.
⟨b, σ⟩ → false ⟨skip, σ⟩ → σ
⟨if b then c; w else skip, σ⟩ → σ
Case 2:
.. ..
. .
⟨b, σ⟩ → true ⟨c; w, σ⟩ → σ ′
⟨if b then c; w else skip, σ⟩ → σ ′

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 12 / 59
Equivalence of Commands

⟨if b then c; w else skip, σ⟩ → σ ′ implies ⟨w, σ⟩ → σ ′ .

Case 1:
..
.
⟨b, σ⟩ → false ⟨skip, σ⟩ → σ
⟨if b then c; w else skip, σ⟩ → σ
..
.
⟨b, σ⟩ → false
⟨w, σ⟩ → σ

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 13 / 59
Equivalence of Commands

⟨if b then c; w else skip, σ⟩ → σ ′ implies ⟨w, σ⟩ → σ ′ .

Case 2:
.. ..
. .
..
. ⟨c, σ⟩ → σ ⟨w, σ ⟩ → σ ′
′′ ′′

⟨b, σ⟩ → true ⟨c; w, σ⟩ → σ ′

⟨if b then c; w else skip, σ⟩ → σ ′
.. .. ..
. . .
⟨b, σ⟩ → true ⟨c, σ⟩ → σ ⟨w, σ ⟩ → σ ′
′′ ′′

⟨while b do c, σ⟩ → σ ′

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 14 / 59
 Small-Step Operational Semantics

textbook, Page 24 – 26

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 15 / 59
One-Step Operational Semantics

Motivation
Full-step operational semantics ignores internal execution.
Single-step execution are important in parallel environments.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 16 / 59
One-Step Operational Semantics

Arithmetic Expressions
big-step semantics: ⟨a, σ⟩ → n
small-step semantics: ⟨a, σ⟩ →1 ⟨a′ , σ⟩

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 17 / 59
One-Step Operational Semantics

Arithmetic Expressions
⟨a0 , σ⟩ →1 ⟨a′0 , σ⟩
⟨a0 + a1 , σ⟩ →1 ⟨a′0 + a1 , σ⟩
⟨a1 , σ⟩ →1 ⟨a′1 , σ⟩
⟨n + a1 , σ⟩ →1 ⟨n + a′1 , σ⟩

(p = m + n)
⟨n + m, σ⟩ →1 ⟨p, σ⟩

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 18 / 59
One-Step Operational Semantics

Commands
big-step semantics: ⟨c, σ⟩ → σ ′
small-step semantics: ⟨c, σ⟩ →1 ⟨c′ , σ ′ ⟩

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 19 / 59
One-Step Operational Semantics

Commands
⟨a, σ⟩ →1 ⟨a′ , σ⟩
(a′ ̸∈ Z)
⟨X := a, σ⟩ →1 ⟨X := a′ , σ⟩
⟨a, σ⟩ →1 ⟨n, σ⟩
(n ∈ Z)
⟨X := a, σ⟩ →1 σ [n/X]

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 20 / 59
One-Step Operational Semantics

Commands
⟨c1 , σ⟩ →1 ⟨c′1 , σ ′ ⟩
⟨c1 ; c2 , σ⟩ →1 ⟨c′1 ; c2 , σ ′ ⟩
⟨c1 , σ⟩ →1 σ ′
⟨c1 ; c2 , σ⟩ →1 ⟨c2 , σ ′ ⟩

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 21 / 59
One-Step Operational Semantics

Question
What about if-branches and while-loops?

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 22 / 59
 Principles of Induction

textbook, Page 27 – 38

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 23 / 59
Principles of Induction

mathematical induction
structural induction
induction on derivation trees
well-founded induction

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 24 / 59
Mathematical Induction

Description
P: a property (or predicate, assertion, formula) over natural numbers

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 25 / 59
Mathematical Induction

Description
P: a property (or predicate, assertion, formula) over natural numbers
illustration: if P(0) and P(n) ⇒ P(n + 1) for all natural numbers n,
then it holds that P(n) for all natural numbers n.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 25 / 59
Mathematical Induction

Description
P: a property (or predicate, assertion, formula) over natural numbers
illustration: if P(0) and P(n) ⇒ P(n + 1) for all natural numbers n,
then it holds that P(n) for all natural numbers n.
formal statement:

[P(0) & ∀n ∈ N. (P(n) ⇒ P(n + 1))] ⇒ ∀n ∈ N.P(n)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 25 / 59
Mathematical Induction

Proof

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 26 / 59
Mathematical Induction

Proof
P = {n ∈ N | P(n)} ⊆ N;

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 26 / 59
Mathematical Induction

Proof
P = {n ∈ N | P(n)} ⊆ N;
P is an inductive set: 0 ∈ P and n ∈ P ⇒ n + 1 ∈ P;

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 26 / 59
Mathematical Induction

Proof
P = {n ∈ N | P(n)} ⊆ N;
P is an inductive set: 0 ∈ P and n ∈ P ⇒ n + 1 ∈ P;
N is the smallest inductive set: N ⊆ P;

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 26 / 59
Mathematical Induction

Proof
P = {n ∈ N | P(n)} ⊆ N;
P is an inductive set: 0 ∈ P and n ∈ P ⇒ n + 1 ∈ P;
N is the smallest inductive set: N ⊆ P;
P = N: i.e., ∀n ∈ N.P(n);

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 26 / 59
Mathematical Induction

Course-of-Values Induction

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 27 / 59
Mathematical Induction

Course-of-Values Induction
target: ∀n.P(n);

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 27 / 59
Mathematical Induction

Course-of-Values Induction
target: ∀n.P(n);
variant form: Q(n) := ∀k < n.P(k);

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 27 / 59
Mathematical Induction

Course-of-Values Induction
target: ∀n.P(n);
variant form: Q(n) := ∀k < n.P(k);
equivalence: ∀n.P(n) is equivalent to ∀n.Q(n);

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 27 / 59
Mathematical Induction

Course-of-Values Induction
target: ∀n.P(n);
variant form: Q(n) := ∀k < n.P(k);
equivalence: ∀n.P(n) is equivalent to ∀n.Q(n);
base step: Q(0) is vacuously true;

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 27 / 59
Mathematical Induction

Course-of-Values Induction
target: ∀n.P(n);
variant form: Q(n) := ∀k < n.P(k);
equivalence: ∀n.P(n) is equivalent to ∀n.Q(n);
base step: Q(0) is vacuously true;
the induction step: Q(n) ⇒ Q(n + 1) for all n;
the induction step: (∀k < n.P(k)) ⇒ P(n) for all n;

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 27 / 59
Mathematical Induction

Course-of-Values Induction
target: ∀n.P(n);
variant form: Q(n) := ∀k < n.P(k);
equivalence: ∀n.P(n) is equivalent to ∀n.Q(n);
base step: Q(0) is vacuously true;
the induction step: Q(n) ⇒ Q(n + 1) for all n;
the induction step: (∀k < n.P(k)) ⇒ P(n) for all n;

Question
Where do we require that P(0) holds?

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 27 / 59
Well-Founded Induction

Definition
A: a set
≺ ⊆ A × A: a binary relation on A
The relation ≺ is well-founded if:
there is no infinite descending sequence . . . ≺ an ≺ . . . ≺ a1 ≺ a0 in A;

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 28 / 59
Well-Founded Induction

Definition
A: a set
≺ ⊆ A × A: a binary relation on A
The relation ≺ is well-founded if:
there is no infinite descending sequence . . . ≺ an ≺ . . . ≺ a1 ≺ a0 in A;
well-foundedness implies irreflexibility: ∀a ∈ A.a ̸≺ a.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 28 / 59
Well-Founded Induction

Minimal Elements
A: a set
≺ ⊆ A × A: a binary relation on A
Q ⊆ A: a subset of A
u ∈ Q: an element of Q
The element u is a minimal element in Q if ∀v ∈ Q. (v ̸≺ u).

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 29 / 59
Well-Founded Induction

Minimal Elements
A: a set
≺ ⊆ A × A: a binary relation on A
Q ⊆ A: a subset of A
u ∈ Q: an element of Q
The element u is a minimal element in Q if ∀v ∈ Q. (v ̸≺ u).

Proposition
The relation ≺ is well-founded iff any nonempty subset Q ⊆ A has a
minimal element.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 29 / 59
Well-Founded Induction

Proposition
A: a set
≺: a binary relation on A
The relation ≺ is well-founded iff any nonempty subset Q ⊆ A has a
minimal element.

Proof for “⇐”(by contradiction)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 30 / 59
Well-Founded Induction

Proposition
A: a set
≺: a binary relation on A
The relation ≺ is well-founded iff any nonempty subset Q ⊆ A has a
minimal element.

Proof for “⇐”(by contradiction)

Suppose that ≺ is not well-founded.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 30 / 59
Well-Founded Induction

Proposition
A: a set
≺: a binary relation on A
The relation ≺ is well-founded iff any nonempty subset Q ⊆ A has a
minimal element.

Proof for “⇐”(by contradiction)

Suppose that ≺ is not well-founded.
There exists an infinite sequence . . . ≺ an ≺ . . . ≺ a1 ≺ a0 .

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 30 / 59
Well-Founded Induction

Proposition
A: a set
≺: a binary relation on A
The relation ≺ is well-founded iff any nonempty subset Q ⊆ A has a
minimal element.

Proof for “⇐”(by contradiction)

Suppose that ≺ is not well-founded.
There exists an infinite sequence . . . ≺ an ≺ . . . ≺ a1 ≺ a0 .
The set {a0 , a1 , . . . , an , . . . } does not have a minimal element.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 30 / 59
Well-Founded Induction

Proposition
A: a set
≺: a binary relation on A
The relation ≺ is well-founded iff any nonempty subset Q ⊆ A has a
minimal element.

Proof for “⇒” (by contradiction)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 31 / 59
Well-Founded Induction

Proposition
A: a set
≺: a binary relation on A
The relation ≺ is well-founded iff any nonempty subset Q ⊆ A has a
minimal element.

Proof for “⇒” (by contradiction)

Suppose that there exists a nonempty subset Q ⊆ A having no
minimal elements, i.e., ∀u ∈ Q.∃v ∈ Q.v ≺ u.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 31 / 59
Well-Founded Induction

Proposition
A: a set
≺: a binary relation on A
The relation ≺ is well-founded iff any nonempty subset Q ⊆ A has a
minimal element.

Proof for “⇒” (by contradiction)

Suppose that there exists a nonempty subset Q ⊆ A having no
minimal elements, i.e., ∀u ∈ Q.∃v ∈ Q.v ≺ u.
Then starting from any u0 , one can construct a sequence u0 , u1 , . . .
of infinite descending elements in A.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 31 / 59
Well-Founded Induction

Statement
≺: a well-founded binary relation on a set A
P: a property on elements of A (a subset of A)
the principle:

∀a ∈ A.P(a) iff ∀a ∈ A. [(∀b ≺ a.P(b)) ⇒ P(a)]

Proof for “⇒”

Straightforward.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 32 / 59
Well-Founded Induction

Statement
≺: a well-founded binary relation on a set A
P: a property on elements of A (a subset of A)
the principle:

∀a ∈ A.P(a) iff ∀a ∈ A. [(∀b ≺ a.P(b)) ⇒ P(a)]

Proof for “⇐” (by contradiction)

Suppose that ∃a.¬P(a) and define Q := {a ∈ A | ¬P(a)}.
Q is nonempty and hence has a minimal element a∗ .
(∀b ≺ a∗ .b ̸∈ Q), and hence (∀b ≺ a∗ .P(b)).
From (∀b ≺ a∗ .P(b)) ⇒ P(a∗ ), we have P(a∗ ).

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 33 / 59
Well-Founded Induction

Example
A = N, ≺ = {(n, n + 1) | n ∈ N}: mathematical induction
A = N, ≺ = {(m, n) ∈ N × N | m < n}: course-of-value induction

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 34 / 59
Structural Induction

Motivation
mathematical induction: inductive proofs on natural numbers
structural induction: inductive proofs on syntactic structures

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 35 / 59
Structural Induction

Arithmetic Expressions

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 36 / 59
Structural Induction

Arithmetic Expressions
Aexp: the set of all arithmetic expressions

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 36 / 59
Structural Induction

Arithmetic Expressions
Aexp: the set of all arithmetic expressions
≺: a0 ≺ a1 iff a0 is an immediate syntactical child of a1

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 36 / 59
Structural Induction

Arithmetic Expressions
Aexp: the set of all arithmetic expressions
≺: a0 ≺ a1 iff a0 is an immediate syntactical child of a1
P: a property on arithmetic expressions

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 36 / 59
Structural Induction

Arithmetic Expressions
Aexp: the set of all arithmetic expressions
≺: a0 ≺ a1 iff a0 is an immediate syntactical child of a1
P: a property on arithmetic expressions
well-founded induction:

∀a ∈ Aexp. [(∀b ≺ a.P(b)) ⇒ P(a)] implies ∀a ∈ Aexp.P(a)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 36 / 59
Structural Induction

Arithmetic Expressions

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 37 / 59
Structural Induction

Arithmetic Expressions
bases step: P holds at atomic arithmetic expressions n, X.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 37 / 59
Structural Induction

Arithmetic Expressions
bases step: P holds at atomic arithmetic expressions n, X.
inductive step: if P holds at arithmetic expressions a0 , a1 , then P also
holds at a0 + a1 , a0 − a1 , a0 × a1 .

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 37 / 59
Structural Induction

Arithmetic Expressions
bases step: P holds at atomic arithmetic expressions n, X.
inductive step: if P holds at arithmetic expressions a0 , a1 , then P also
holds at a0 + a1 , a0 − a1 , a0 × a1 .
consequence: P holds at all arithmetic expressions.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 37 / 59
Structural Induction

Example
For all arithmetic expressions a, states σ and integers m, m′ ,

⟨a, σ⟩ → m ∧ ⟨a, σ⟩ → m′ ⇒ m = m′ .

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 38 / 59
Structural Induction

The Inductive Proof

base step: ⟨n, σ⟩ → n, ⟨X, σ⟩ → σ(X)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 39 / 59
Structural Induction

The Inductive Proof

base step: ⟨n, σ⟩ → n, ⟨X, σ⟩ → σ(X)
inductive step:
⟨a0 , σ⟩ → n0 , ⟨a1 , σ⟩ → n1
⟨a0 + a1 , σ⟩ → n0 + n1

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 39 / 59
Structural Induction

Boolean Expressions
∀b, σ, t, t′ . [(⟨b, σ⟩ → t & ⟨b, σ⟩ → t′ ) ⇒ t = t′ ] .

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 40 / 59
Structural Induction

Proposition
∀c, σ, σ ′ , σ ′′ . [(⟨c, σ⟩ → σ ′ & ⟨c, σ⟩ → σ ′′ ) ⇒ σ ′ = σ ′′ ] .

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 41 / 59
Structural Induction

Proposition
∀c, σ, σ ′ , σ ′′ . [(⟨c, σ⟩ → σ ′ & ⟨c, σ⟩ → σ ′′ ) ⇒ σ ′ = σ ′′ ] .

Question
Can we prove this proposition through structural induction?

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 41 / 59
Question

Proposition
∀c, σ, σ ′ , σ ′′ . [(⟨c, σ⟩ → σ ′ & ⟨c, σ⟩ → σ ′′ ) ⇒ σ ′ = σ ′′ ] .

Rules for While Loops

⟨b, σ⟩ → false
⟨while b do c, σ⟩ → σ

⟨b, σ⟩ → true, ⟨c, σ⟩ → σ ′′ , ⟨while b do c, σ ′′ ⟩ → σ ′

⟨while b do c, σ⟩ → σ ′

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 42 / 59
Induction on Derivation Trees

A: the set of all derivation trees (or derivations)

≺: r0 ≺ r1 iff r0 is a proper sub-derivation tree of r1
well-founded induction:
[( ) ]
∀r ∈ A. ∀r′ ≺ r.P(r′ ) ⇒ P(r) implies ∀r ∈ A.P(r)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 43 / 59
Induction on Derivation Trees

Rule Instance (X/y)

X: premise (a finite set of elements)
y: conclusion (a single element)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 44 / 59
Induction on Derivation Trees

Axiom Instances: ∅/y

Other Rule Instances: {x1 , . . . , xn }/y

x1 , . . . , xn
y

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 45 / 59
Induction on Derivation Trees

Derivation Trees
R: a set of rule instances
y: an element
An R-derivation of y is
either a rule instance (∅/y)
or ({d1 , . . . , dn }/y) such that
({x1 , . . . , xn }/y) is a rule instance
each di is a (smaller) R-derivation of xi

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 46 / 59
Induction on Derivation Trees

Notations
R: a set of rule instances
d: an R-derivation
y: an element
Then we write
d ⊩R y: d is an R-derivation of y.
⊩R y: d ⊩R y for some derivation d.
d ⊩ y, ⊩ y: omission of R

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 47 / 59
Induction on Derivation Trees

Notations
R: a set of rule instances
d: an R-derivation
y: an element
Then we have
(∅/y) ⊩R y if (∅/y) ∈ R
({d1 , . . . , dn }/y) ⊩R y if ({x1 , . . . , xn }/y) ∈ R and
d1 ⊩R x1 , . . . , dn ⊩R xn

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 48 / 59
Induction on Derivation Trees

The Well-Founded Relation on Derivation Trees

d, d′ : derivations
d′ ≺ d if d′ is a proper sub-derivation of d.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 49 / 59
Induction on Derivation Trees

Proposition
∀c, σ, σ ′ , σ ′′ . [(⟨c, σ⟩ → σ ′ & ⟨c, σ⟩ → σ ′′ ) ⇒ σ ′ = σ ′′ ] .

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 50 / 59
Induction on Derivation Trees

Proposition
∀c, σ, σ ′ , σ ′′ . [(⟨c, σ⟩ → σ ′ & ⟨c, σ⟩ → σ ′′ ) ⇒ σ ′ = σ ′′ ] .
P(d) := ∀c, σ, σ ′ , σ ′′ . [(d ⊩ ⟨c, σ⟩ → σ ′ ∧ ⟨c, σ⟩ → σ ′′ ) ⇒ σ ′ = σ ′′ ]

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 50 / 59
Induction on Derivation Trees

Proposition
∀c, σ, σ ′ , σ ′′ . [(⟨c, σ⟩ → σ ′ & ⟨c, σ⟩ → σ ′′ ) ⇒ σ ′ = σ ′′ ] .
P(d) := ∀c, σ, σ ′ , σ ′′ . [(d ⊩ ⟨c, σ⟩ → σ ′ ∧ ⟨c, σ⟩ → σ ′′ ) ⇒ σ ′ = σ ′′ ]
the goal: ∀d′ ≺ d.P(d′ ) implies P(d)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 50 / 59
Induction on Derivation Trees

∀c, σ, σ ′ , σ ′′ . [(⟨c, σ⟩ → σ ′ & ⟨c, σ⟩ → σ ′′ ) ⇒ σ ′ = σ ′′ ] .

base step:
..
.
⟨a, σ⟩ → m
⟨skip, σ⟩ → σ ⟨X := a, σ⟩ → σ [m/X]

inductive step:
.. .. ..
. . .
⟨b, σ⟩ → true ⟨c, σ⟩ → σ ′′ ⟨while b do c, σ ′′ ⟩ → σ ′
⟨while b do c, σ⟩ → σ ′

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 51 / 59
Program Termination

A Variant of Euclidean’s Algorithm

w h i l e ¬(M = N) do
if M ≤ N
then N := N − M
e l s e M := M − N

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 52 / 59
Program Termination

A Variant of Euclidean’s Algorithm

Euclid =
w h i l e ¬(M = N) do
if M ≤ N
then N := N − M
e l s e M := M − N

Termination Property
∀σ. [(σ(M) ≥ 1 ∧ σ(N) ≥ 1) ⇒ (∃σ ′ .⟨Euclid, σ⟩ → σ ′ )]

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 53 / 59
Program Termination

Termination Property
∀σ. [(σ(M) ≥ 1 ∧ σ(N) ≥ 1) ⇒ (∃σ ′ .⟨Euclid, σ⟩ → σ ′ )]

Proof

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 54 / 59
Program Termination

Termination Property
∀σ. [(σ(M) ≥ 1 ∧ σ(N) ≥ 1) ⇒ (∃σ ′ .⟨Euclid, σ⟩ → σ ′ )]

Proof
A := {σ ∈ Σ | σ(M) ≥ 1 ∧ σ(N) ≥ 1}.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 54 / 59
Program Termination

Termination Property
∀σ. [(σ(M) ≥ 1 ∧ σ(N) ≥ 1) ⇒ (∃σ ′ .⟨Euclid, σ⟩ → σ ′ )]

Proof
A := {σ ∈ Σ | σ(M) ≥ 1 ∧ σ(N) ≥ 1}.
σ ≺ σ ′ iff the followings hold:
1 σ(M) ≤ σ ′ (M) and σ(N) ≤ σ ′ (N);
2 σ ̸= σ ′ ;

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 54 / 59
Program Termination

Termination Property
∀σ. [(σ(M) ≥ 1 ∧ σ(N) ≥ 1) ⇒ (∃σ ′ .⟨Euclid, σ⟩ → σ ′ )]

Proof
A := {σ ∈ Σ | σ(M) ≥ 1 ∧ σ(N) ≥ 1}.
σ ≺ σ ′ iff the followings hold:
1 σ(M) ≤ σ ′ (M) and σ(N) ≤ σ ′ (N);
2 σ ̸= σ ′ ;
P(σ) := ∃σ ′ .⟨Euclid, σ⟩ → σ ′ .

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 54 / 59
Program Termination

Termination Property
∀σ. [(σ(M) ≥ 1 ∧ σ(N) ≥ 1) ⇒ (∃σ ′ .⟨Euclid, σ⟩ → σ ′ )]

Proof
A := {σ ∈ Σ | σ(M) ≥ 1 ∧ σ(N) ≥ 1}.
σ ≺ σ ′ iff the followings hold:
1 σ(M) ≤ σ ′ (M) and σ(N) ≤ σ ′ (N);
2 σ ̸= σ ′ ;
P(σ) := ∃σ ′ .⟨Euclid, σ⟩ → σ ′ .
our goal: prove ∀σ ∈ A.P(σ) by
[( ) ]
∀σ ∈ A. ∀σ ′ ≺ σ.P(σ ′ ) ⇒ P(σ)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 54 / 59
Well-founded Induction

Proof
P(σ) := ∃σ ′ .⟨Euclid, σ⟩ → σ ′ .
our goal: prove ∀σ ∈ A.P(σ) by
[( ) ]
∀σ ∈ A. ∀σ ′ ≺ σ.P(σ ′ ) ⇒ P(σ)

Suppose that ∀σ ′ ≺ σ.P(σ ′ ).

Case σ(M) = σ(N):
..
.
⟨¬M = N, σ⟩ → false
⟨Euclid, σ⟩ → σ

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 55 / 59
Well-founded Induction

Proof
P(σ) := ∃σ ′ .⟨Euclid, σ⟩ → σ ′ .
our goal: prove ∀σ ∈ A.P(σ) by
[( ) ]
∀σ ∈ A. ∀σ ′ ≺ σ.P(σ ′ ) ⇒ P(σ)

Suppose that ∀σ ′ ≺ σ.P(σ ′ ).

Case σ(M) ̸= σ(N):

⟨if M ≤ N then N := N − M else M := M − N, σ⟩ → σ ′′

where {
σ [σ(N) − σ(M)/N] if σ(N) ≥ σ(M)
′′
σ =
σ [σ(M) − σ(N)/M] otherwise
and σ ′′ ≺ σ;
. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 56 / 59
Well-founded Induction

Proof
P(σ) := ∃σ ′ .⟨Euclid, σ⟩ → σ ′ .
Prove ∀σ ∈ A. [(∀σ ′ ≺ σ.P(σ ′ )) ⇒ P(σ)].
Suppose that ∀σ ′ ≺ σ.P(σ ′ ).
Case σ(M) ̸= σ(N):
⟨¬(M = N), σ⟩ → true;
⟨if M < N then N := N − M else M := M − N, σ⟩ → σ ′′ and σ ′′ ≺ σ;
⟨Euclid, σ ′′ ⟩ → σ ′ for some σ ′ ;
Conclusion: ⟨Euclid, σ⟩ → σ ′

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 57 / 59
Summary

equivalence reasoning using rules

small-step semantics
principles of induction
mathematical induction
induction on derivation trees
well-founded induction
proving program property through induction
proving program termination through induction

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 58 / 59
Homework

Problem
Consider the command

c = while X ≤ 100 do X := X + 2

where X is a location (program variable). For each initial state σ,

determine the state σ ′ such that ⟨c, σ⟩ → σ ′ and verify your answer.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .
Hongfei Fu (SJTU JHC) Operational Semantics Mar. 19th, 2020 59 / 59