1 Rules
Bool-True
Int A;n−→n
Bool-False A; false −→ false
A;e1 −→ v1
A; let x = e1 in e2 −→ v2
Discussion 6 Worksheet
Spring 2019
A(x) = v Id A;x−→v
A; true −→ true
Let
A,x : v1;e2 −→ v2
Add
A;e1−→v1 A;e2−→v2 v3isv1+v2 A; e1 + e2 −→ v3
A;e1−→v1 A;e2−→v2 v3isv1∗v2 A; e1 ∗ e2 −→ v3
If-True
A;e1 −→ true A;e2 −→ v2 A; if e1 then e2 else e3 −→ v2
A; e1 −→ true Not-True A; not e1 −→ false
Mul
If-False
A;e1 −→ false A;e3 −→ v3 A; if e1 then e2 else e3 −→ v3
A; e1 −→ false Not-False A; not e1 −→ true
1
2 Derivations
Given the rules above, prove the following.
•; 1 + 2 ∗ 3 −→ 7
y:3; letx=1inx+y−→4
•; letx=trueinifnotxthen4else6−→6
2
3 Solutions
• ; 2 −→ 2
• ; 3 −→ 3 • ; 2 ∗ 3 −→ 6
•; 1 + 2 ∗ 3 −→ 7
6 is 2 * 3
• ; 1 −→ 1
7 is 1 + 6
A(x) = 1
y : 3, x : 1; x −→ 1
A(y) = 3
y : 3, x : 1; y −→ 3
4 is 1 + 3
y : 3; 1 −→ 1
y : 3, x : 1; x + y −→ 4 y:3; letx=1inx+y−→4
A(x) = true
x : true; x −→ true
•; true −→ true
x : true; not x −→ false x : true; 6 −→ 6 x : true; if not x then 4 else 6 −→ 6
•; letx=trueinifnotxthen4else6−→6
3