1 of 90

1

Programming Languages and Compilers (CS 421)

Talia Ringer (they/them)

4218 SC, UIUC

https://courses.grainger.illinois.edu/cs421/fa2023/

Based heavily on slides by Elsa Gunter, which were based in part on slides by Mattox Beckman, as updated by Vikram Adve and Gul Agha

2 of 90

Operational Semantics

What it is:

Describe how to execute (implement) programs of language on a virtual machine, by describing how to execute each program statement (i.e., following the structure of the program)
Meaning of program is how its execution changes the state of the machine

Tradeoffs:

Easy to implement
Hard to reason about abstractly (without thinking about implementation details)

*

2

3 of 90

Operational Semantics

What it is:

Describe how to execute (implement) programs of language on a virtual machine, by describing how to execute each program statement (i.e., following the structure of the program)
Meaning of program is how its execution changes the state of the machine

Tradeoffs:

Easy to implement
Hard to reason about abstractly (without thinking about implementation details)

*

3

4 of 90

Operational Semantics

Can be small step or big step

Small step: define meaning of one step of execution of a program statement at a time
Big step: define meaning in terms of value of execution of whole program statement

Common to have both and relate them

*

4

5 of 90

Operational Semantics

Can be small step or big step

Small step: define meaning of one step of execution of a program statement at a time
Big step: define meaning in terms of value of execution of whole program statement

Common to have both and relate them

*

5

6 of 90

6

Questions before we start?

7 of 90

7

Transition (Small Step) Semantics

8 of 90

Transition Semantics

Also known as small-step operational semantics
Describes how each program construct transforms machine state by transitions
Rules look like

(C, m) --> (C’, m’) or (C, m) --> m’

C, C’ is code remaining to be executed
m, m’ represent the state/memory/environment
Sometimes m (or C) not needed

Indicates exactly one step of computation

8

Transition Semantics

9 of 90

Transition Semantics

Also known as small-step operational semantics
Describes how each program construct transforms machine state by transitions
Rules look like

(C, m) → (C’, m’) or (C, m) → m’

C, C’ is code remaining to be executed
m, m’ represent the state/memory/environment
Sometimes m (or C) not needed

Indicates exactly one step of computation

9

Transition Semantics

10 of 90

Evaluation Semantics

Transitions successfully stop when E/C is a value/memory
Evaluation fails if no transition possible, but not at value/memory
Value/memory is the final meaning of original expression/command (in the given state)

Coarse semantics: final value/memory
More fine grained: whole transition sequence

10

Transition Semantics

11 of 90

Evaluation Semantics

Transitions successfully stop when E/C is a value/memory
Evaluation fails if no transition possible, but not at value/memory
Value/memory is the final meaning of original expression/command (in the given state)

Coarse semantics: final value/memory
More fine grained: whole transition sequence

11

Transition Semantics

12 of 90

Evaluation Semantics

Transitions successfully stop when E/C is a value/memory
Evaluation fails if no transition possible, but not at value/memory
Value/memory is the final meaning of original expression/command (in the given state)

Coarse semantics: final value/memory
More fine grained: whole transition sequence

12

Transition Semantics

13 of 90

Simple Imperative Language Syntax

I ∈ Identifiers

N ∈ Numerals

B ::= true | false | B & B | B or B | � not B | E < E | E = E

E ::= N | I | E + E | E * E | E - E | - E | (E)

C ::= skip | C; C | I := E |� if B then C else C fi | while B do C od

13

Transition Semantics

14 of 90

Simple Imperative Language Syntax

I ∈ Identifiers

N ∈ Numerals

B ::= true | false | B & B | B or B | � not B | E < E | E = E

E ::= N | I | E + E | E * E | E - E | - E | (E)

C ::= skip | C; C | I := E |� if B then C else C fi | while B do C od

14

Transition Semantics

15 of 90

Simple Imperative Language Syntax

I ∈ Identifiers

N ∈ Numerals

B ::= true | false | B & B | B or B | � not B | E < E | E = E

E ::= N | I | E + E | E * E | E - E | - E | (E)

C ::= skip | C; C | I := E |� if B then C else C fi | while B do C od

15

Transition Semantics

16 of 90

Simple Imperative Language Syntax

I ∈ Identifiers

N ∈ Numerals

B ::= true | false | B & B | B or B | � not B | E < E | E = E

E ::= N | I | E + E | E * E | E - E | - E | (E)

C ::= skip | C; C | I := E |� if B then C else C fi | while B do C od

16

Transition Semantics

17 of 90

Simple Imperative Language Semantics

Values V:

Numerals N
Boolean atoms {true, false}

(I, m) → (m(I), m)

17

Transition Semantics

(E, m) → (V, m’)

Id

18 of 90

Simple Imperative Language Semantics

Values V:

Numerals N
Boolean atoms {true, false}

(I, m) → (m(I), m)

18

Transition Semantics

(E, m) → (V, m’)

Id

Look up identifiers

19 of 90

Simple Imperative Language Semantics

(false & B, m) → (false, m)

(true & B, m) → (B, m)

(B, m) → (B”, m)

(B & B’, m) → (B” & B’, m)

19

Transition Semantics

(B, m) → (B’, m’)

Short-circuit

And-F

And-T

And

20 of 90

Simple Imperative Language Semantics

(false & B, m) → (false, m)

(true & B, m) → (B, m)

(B, m) → (B”, m)

(B & B’, m) → (B” & B’, m)

20

Transition Semantics

(B, m) → (B’, m’)

Short-circuit

And-F

And-T

And

21 of 90

Simple Imperative Language Semantics

(false & B, m) → (false, m)

(true & B, m) → (B, m)

(B, m) → (B”, m)

(B & B’, m) → (B” & B’, m)

21

Transition Semantics

(B, m) → (B’, m’)

Short-circuit

And-F

And-T

And

22 of 90

Simple Imperative Language Semantics

(false & B, m) → (false, m)

(true & B, m) → (B, m)

(B, m) → (B”, m)

(B & B’, m) → (B” & B’, m)

22

Transition Semantics

(B, m) → (B’, m’)

Evaluate first clause one step

And-F

And-T

And

23 of 90

Simple Imperative Language Semantics

(false & B, m) → (false, m)

(true & B, m) → (B, m)

(B, m) → (B”, m)

(B & B’, m) → (B” & B’, m)

23

Transition Semantics

(B, m) → (B’, m’)

Evaluate first clause one step

And-F

And-T

And

24 of 90

Simple Imperative Language Semantics

(false & B, m) → (false, m)

(true & B, m) → (B, m)

(B, m) → (B”, m)

(B & B’, m) → (B” & B’, m)

24

Transition Semantics

(B, m) → (B’, m’)

Evaluate first clause one step

And-F

And-T

And

25 of 90

Simple Imperative Language Semantics

(true or B, m) → (true, m)

(false or B, m) → (B, m)

(B, m) → (B”, m)

(B or B’, m) → (B” or B’, m)

25

Transition Semantics

(B, m) → (B’, m’)

Or is similar

Or-T

Or-F

Or

26 of 90

Simple Imperative Language Semantics

(not true, m) → (false, m)

(not false, m) → (true, m)

(B, m) → (B’, m)

(not B, m) → (not B’, m)

26

Transition Semantics

(B, m) → (B’, m’)

Not-T

Not-F

Not

Not is not too different

27 of 90

27

Questions so far?

Transition Semantics

28 of 90

Simple Imperative Language Semantics

(E, m) → (E’’, m)

(E ~ E’, m) → (E’’ ~ E’, m)

(E, m) → (E’, m)

(V ~ E, m) → (V ~ E’, m)

(U ~ V, m) → (true, m) or (false, m) depending on whether U ~ V holds or not

28

Transition Semantics

(E, m) → (E’, m’)

Evaluate LHS first …

Rel-E

Rel-V

29 of 90

Simple Imperative Language Semantics

(E, m) → (E’’, m)

(E ~ E’, m) → (E’’ ~ E’, m)

(E, m) → (E’, m)

(V ~ E, m) → (V ~ E’, m)

(U ~ V, m) → (true, m) or (false, m) depending on whether U ~ V holds or not

29

Transition Semantics

(E, m) → (E’, m’)

Evaluate LHS first …

Rel-E

Rel-V

30 of 90

Simple Imperative Language Semantics

(E, m) → (E’’, m)

(E ~ E’, m) → (E’’ ~ E’, m)

(E, m) → (E’, m)

(V ~ E, m) → (V ~ E’, m)

(U ~ V, m) → (true, m) or (false, m) depending on whether U ~ V holds or not

30

Transition Semantics

(E, m) → (E’, m’)

Evaluate LHS first …

… until you get a value

Rel-E

Rel-V

31 of 90

Simple Imperative Language Semantics

(E, m) → (E’’, m)

(E ~ E’, m) → (E’’ ~ E’, m)

(E, m) → (E’, m)

(V ~ E, m) → (V ~ E’, m)

(U ~ V, m) → (true, m) or (false, m) depending on whether U ~ V holds or not

31

Transition Semantics

(E, m) → (E’, m’)

Evaluate LHS first …

… until you get a value

Rel-E

Rel-V

32 of 90

Simple Imperative Language Semantics

(E, m) → (E’’, m)

(E ~ E’, m) → (E’’ ~ E’, m)

(E, m) → (E’, m)

(V ~ E, m) → (V ~ E’, m)

(U ~ V, m) → (true, m) or (false, m) depending on whether U ~ V holds or not

32

Transition Semantics

(E, m) → (E’, m’)

Evaluate LHS first …

… until you get a value

Rel-E

Rel-V

33 of 90

Simple Imperative Language Semantics

(E, m) → (E’’, m)

(E op E’, m) → (E’’ op E’, m)

(E, m) → (E’, m)

(V op E, m) → (V op E’, m)

(U op V, m) → (N, m) � where N is the specified value for U op V

33

(E, m) → (E’, m’)

Transition Semantics

Evaluate LHS first …

… until you get a value

Arith-E

Arith-V

34 of 90

34

Questions so far?

Transition Semantics

35 of 90

Simple Imperative Language Semantics

(skip, m) → m

(E, m) → (E’, m)

(I ::= E, m) → (I ::= E’, m)

(I ::= V, m) → m[I ← V ]

35

(C, m) → m’

Transition Semantics

Skip

Assign-E

Assign-V

(C, m) →(C’, m’)

36 of 90

Simple Imperative Language Semantics

(skip, m) → m

(E, m) → (E’, m)

(I ::= E, m) → (I ::= E’, m)

(I ::= V, m) → m[I ← V ]

36

(C, m) → m’

Transition Semantics

Skip

Assign-E

Assign-V

Skip means done evaluating

(C, m) →(C’, m’)

37 of 90

Simple Imperative Language Semantics

(skip, m) → m

(E, m) → (E’, m)

(I ::= E, m) → (I ::= E’, m)

(I ::= V, m) → m[I ← V ]

37

(C, m) → m’

Transition Semantics

Skip

Assign-E

Assign-V

Skip means done evaluating

(C, m) →(C’, m’)

38 of 90

Simple Imperative Language Semantics

(skip, m) → m

(E, m) → (E’, m)

(I ::= E, m) → (I ::= E’, m)

(I ::= V, m) → m[I ← V ]

38

(C, m) → m’

Transition Semantics

Skip

Assign-E

Assign-V

Evaluate RHS of assignment …

(C, m) →(C’, m’)

39 of 90

Simple Imperative Language Semantics

(skip, m) → m

(E, m) → (E’, m)

(I ::= E, m) → (I ::= E’, m)

(I ::= V, m) → m[I ← V ]

39

(C, m) → m’

Transition Semantics

Skip

Assign-E

Assign-V

Evaluate RHS of assignment …

(C, m) →(C’, m’)

40 of 90

Simple Imperative Language Semantics

(skip, m) → m

(E, m) → (E’, m)

(I ::= E, m) → (I ::= E’, m)

(I ::= V, m) → m[I ← V ]

40

(C, m) → m’

Transition Semantics

Skip

Assign-E

Assign-V

Evaluate RHS of assignment …

… until you get a value

(C, m) →(C’, m’)

41 of 90

Simple Imperative Language Semantics

(skip, m) → m

(E, m) → (E’, m)

(I ::= E, m) → (I ::= E’, m)

(I ::= V, m) → m[I ← V ]

41

(C, m) → m’

Transition Semantics

Skip

Assign-E

Assign-V

Evaluate RHS of assignment …

… until you get a value

(C, m) →(C’, m’)

42 of 90

Simple Imperative Language Semantics

(C, m) → (C”, m’ )

(C; C’, m) → (C”; C’, m’)

(C, m) → m’

(C; C’, m) → (C’, m’ )

42

(C, m) → m’

Transition Semantics

Evaluate first command of sequence first …

Seq-L

Seq-R

(C, m) →(C’, m’)

43 of 90

Simple Imperative Language Semantics

(C, m) → (C”, m’ )

(C; C’, m) → (C”; C’, m’)

(C, m) → m’

(C; C’, m) → (C’, m’ )

43

(C, m) → m’

Transition Semantics

Evaluate first command of sequence first …

Seq-L

Seq-R

(C, m) →(C’, m’)

44 of 90

Simple Imperative Language Semantics

(C, m) → (C”, m’ )

(C; C’, m) → (C”; C’, m’)

(C, m) → m’

(C; C’, m) → (C’, m’ )

44

(C, m) → m’

Transition Semantics

Evaluate first command of sequence first …

Seq-L

Seq-R

… until it gives back a memory

(C, m) →(C’, m’)

45 of 90

Simple Imperative Language Semantics

(C, m) → (C”, m’ )

(C; C’, m) → (C”; C’, m’)

(C, m) → m’

(C; C’, m) → (C’, m’ )

45

(C, m) → m’

Transition Semantics

Evaluate first command of sequence first …

Seq-L

Seq-R

… until it gives back a memory

(C, m) →(C’, m’)

46 of 90

Simple Imperative Language Semantics

(if true then C else C’ fi, m) → (C, m)

(if false then C else C’ fi, m) → (C’, m)

(B, m) → (B’, m)

(if B then C else C’ fi, m) → (if B’ then C else C’ fi, m)

46

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

If-T

If-F

If

47 of 90

Simple Imperative Language Semantics

(if true then C else C’ fi, m) → (C, m)

(if false then C else C’ fi, m) → (C’, m)

(B, m) → (B’, m)

(if B then C else C’ fi, m) → (if B’ then C else C’ fi, m)

47

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

If-T

If-F

If

If guard is true, evaluate first branch

48 of 90

Simple Imperative Language Semantics

(if true then C else C’ fi, m) → (C, m)

(if false then C else C’ fi, m) → (C’, m)

(B, m) → (B’, m)

(if B then C else C’ fi, m) → (if B’ then C else C’ fi, m)

48

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

If-T

If-F

If

If guard is false, evaluate second branch

49 of 90

Simple Imperative Language Semantics

(if true then C else C’ fi, m) → (C, m)

(if false then C else C’ fi, m) → (C’, m)

(B, m) → (B’, m)

(if B then C else C’ fi, m) → (if B’ then C else C’ fi, m)

49

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

If-T

If-F

If

Evaluate guard until it’s a value, so one of the above applies

50 of 90

50

Questions so far?

Transition Semantics

51 of 90

Simple Imperative Language Semantics

(B, m) 🡪 (B’, m)

??

(while B do C od, m) → ??(while B’ do C od, m)

51

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

Question: What should while do?

52 of 90

Simple Imperative Language Semantics

(B, m) 🡪 (B’, m)

(B, m) → (B’, m)

(while B do C od, m) → (while B’ do C od, m)

(while B’ do C od, m)

52

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

This is tempting, but it is wrong!

53 of 90

Simple Imperative Language Semantics

(B, m) 🡪 (B’, m)

(while B do C od, m) →� (if B then C; while B do C od else skip fi, m)

(while B’ do C od, m)

53

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

Rather, we unroll the loop once

54 of 90

Simple Imperative Language Semantics

(B, m) 🡪 (B’, m)

(while B do C od, m) →� (if B then C; while B do C od else skip fi, m)

(while B’ do C od, m)

54

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

Rather, we unroll the loop once …

55 of 90

Simple Imperative Language Semantics

(B, m) 🡪 (B’, m)

(while B do C od, m) →� (if B then C; while B do C od else skip fi, m)

(while B’ do C od, m)

55

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

… continue while guard is true …

56 of 90

Simple Imperative Language Semantics

(B, m) 🡪 (B’, m)

(while B do C od, m) →� (if B then C; while B do C od else skip fi, m)

(while B’ do C od, m)

56

(C, m) → m’

(C, m) →(C’, m’)

Transition Semantics

… and stop when guard is false.

57 of 90

57

Questions so far?

58 of 90

58

Example

59 of 90

Example Evaluation

First step:

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → ??

59

Transition Semantics Example

60 of 90

Example Evaluation

First step:

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →� ??

60

Transition Semantics Example

If

Evaluate guard until it’s a value

61 of 90

Example Evaluation

First step:

(x > 5, {x -> 7}) → ??

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →� ??

61

Transition Semantics Example

If

Evaluate guard until it’s a value

62 of 90

Example Evaluation

First step:

(x > 5, {x -> 7}) → ??

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →� ??

62

Transition Semantics Example

If

How to evaluate guard?

63 of 90

Example Evaluation

First step:

??

(x > 5, {x -> 7}) → ??

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →� ??

63

Transition Semantics Example

If

The guard is a relation

Rel-E

64 of 90

Example Evaluation

First step:

(x, {x -> 7}) → ??

(x > 5, {x -> 7}) → ??

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →� ??

64

Transition Semantics Example

If

And x is not yet a value, so we evaluate LHS first

Rel-E

65 of 90

Example Evaluation

First step:

(x, {x -> 7}) → ??

(x > 5, {x -> 7}) → ??

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →� ??

65

Transition Semantics Example

If

x is an identifier …

Rel-E

Id

66 of 90

Example Evaluation

First step:

(x, {x -> 7}) → (7, {x -> 7})

(x > 5, {x -> 7}) → ??

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →� ??

66

Transition Semantics Example

If

x is an identifier so we look it up

Id

Rel-E

67 of 90

Example Evaluation

First step:

(x, {x -> 7}) → (7, {x -> 7})

(x > 5, {x -> 7}) → (7 > 5, {x -> 7})

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →� ??

67

Transition Semantics Example

If

Propagate downward

Id

Rel-E

68 of 90

Example Evaluation

First step:

(x, {x -> 7}) → (7, {x -> 7})

(x > 5, {x -> 7}) → (7 > 5, {x -> 7})

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → �(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7})

68

Transition Semantics Example

If

Propagate downward

Id

Rel-E

69 of 90

69

Questions so far?

Transition Semantics Example

70 of 90

Example Evaluation

First step:

(x, {x -> 7}) → (7, {x -> 7})

(x > 5, {x -> 7}) → (7 > 5, {x -> 7})

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → �(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7})

70

Transition Semantics Example

If

Id

Rel-E

71 of 90

Example Evaluation

Second step:

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → � ??

71

Transition Semantics Example

72 of 90

Example Evaluation

Second step:

(7 > 5, {x -> 7}) → ??

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → � ??

72

Transition Semantics Example

Evaluate guard until it’s a value (still not a value)

If

73 of 90

Example Evaluation

Second step:

(7 > 5, {x -> 7}) → (true, {x -> 7})

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → � ??

73

Transition Semantics Example

By semantics of >

If

Evaluate guard until it’s a value (still not a value)

74 of 90

Example Evaluation

Second step:

(7 > 5, {x -> 7}) → (true, {x -> 7})

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → �(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7})

74

Transition Semantics Example

By semantics of >

If

Evaluate guard until it’s a value (still not a value)

75 of 90

Example Evaluation

Second step:

(7 > 5, {x -> 7}) → (true, {x -> 7})

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → �(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7})

75

Transition Semantics Example

By semantics of >

If

Evaluate guard until it’s a value (now it’s a value!)

76 of 90

Example Evaluation

Second step:

(7 > 5, {x -> 7}) → (true, {x -> 7})

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → �(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7})

Third step:

(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → � ??

76

Transition Semantics Example

If

If-T

77 of 90

Example Evaluation

Second step:

(7 > 5, {x -> 7}) → (true, {x -> 7})

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → �(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7})

Third step:

(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) → � (y := 2 + 3, {x -> 7})

77

Transition Semantics Example

If

If-T

Step to then case

78 of 90

Example Evaluation

Fourth Step:

(2 + 3, {x -> 7}) → (5, {x -> 7})

(y := 2 + 3, {x -> 7}) → (y := 5, {x -> 7})

78

Transition Semantics Example

Assign-E

79 of 90

Example Evaluation

Fourth Step:

(2 + 3, {x -> 7}) → (5, {x -> 7})

(y := 2 + 3, {x -> 7}) → (y := 5, {x -> 7})

Fifth Step:

(y := 5, {x -> 7}) → {y -> 5, x -> 7}

79

Transition Semantics Example

Assign-E

Assign-V

80 of 90

Example Evaluation

Bottom line:

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(y := 2 + 3, {x -> 7}) →

(y := 5, {x -> 7}) →

{y -> 5, x -> 7}

80

Transition Semantics Example

81 of 90

Example Evaluation

Bottom line:

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(y := 2 + 3, {x -> 7}) →

(y := 5, {x -> 7}) →

{y -> 5, x -> 7}

81

Transition Semantics Example

82 of 90

Example Evaluation

Bottom line:

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(y := 2 + 3, {x -> 7}) →

(y := 5, {x -> 7}) →

{y -> 5, x -> 7}

82

Transition Semantics Example

83 of 90

Example Evaluation

Bottom line:

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(y := 2 + 3, {x -> 7}) →

(y := 5, {x -> 7}) →

{y -> 5, x -> 7}

83

Transition Semantics Example

84 of 90

Example Evaluation

Bottom line:

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(y := 2 + 3, {x -> 7}) →

(y := 5, {x -> 7}) →

{y -> 5, x -> 7}

84

Transition Semantics Example

85 of 90

Example Evaluation

Bottom line:

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if 7 > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(if true then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →

(y := 2 + 3, {x -> 7}) →

(y := 5, {x -> 7}) →

{y -> 5, x -> 7}

(if x > 5 then y := 2 + 3 else y := 3 + 4 fi, {x -> 7}) →* {y -> 5, x -> 7}

85

Transition Semantics Example

86 of 90

Transition Semantics Evaluation

A sequence of steps with trees of justification for each step:

(C₁, m₁)→(C₂, m₂) → (C₃, m₃) → … → m

Let →* be the transitive closure of →
i.e., the smallest transitive relation containing →

86

Transition Semantics Example

87 of 90

87

Questions?

88 of 90

88

Next Class: Lambda Calculus

89 of 90

Next Class

89

Operational

Semantics

Lambda Calculus

Axiomatic Semantics

III : Language Semantics

Lamda Calculus

90 of 90

Just started grading EC2
WA9 is due this Thursday
MP10 is not, in fact, for credit (it is for Q5)
Q5 is immediately upon returning from break
May be in touch about extra makeup opportunities
All deadlines can be found on course website
Use office hours and class forums for help

Next Class

90