————– Not t ↦ Not t′
Exercises
1. Define the Idris constructors for the semantics of Not.
data (↦) : Term → Term → Type where NotFls : Not Fls ↦ Tru
NotTru : Not Tru ↦ Fls
NotInd: t↦t′ →
data (↦) : Term → Term → Type where IfTru : Cond Tru t1 t2 ↦ t1
IfFls : Cond Fls t1 t2 ↦ t2
IfInd :
t ↦ t’ —————————- Cond t t1 t2 ↦ Cond t’ t1 t2
Not Tru Fls Not Fls Tru
t t′ Nott Nott′
→
CS 582 • Operational Semantics
1
Exercises
2. Determine the semantics of the term Not (Not Tru) and find a derivation (= proof) for it.
nf : Not Fls ↦ Tru nf = NotFLs
nnt : Not (Not Tru) ↦ Not Fls nnt = NotInd NotTru
data (↦*) : Term → Term → Type where Idemp : t ↦* t
Trans : t1 ↦ t2 → t2 ↦* t3 → t1 ↦* t3
data (↦) : Term → Term → Type where NotFls : Not Fls ↦ Tru
NotTru : Not Tru ↦ Fls
NotInd : t ↦ t′ → Not t ↦ Not t′
…
nnts : Not (Not Tru) ↦* Tru
nnts = NotInd NotTru `Trans` NotFls `Trans` Idemp
CS 582 • Operational Semantics
Hint: Perform 3 steps:
(1) Not Fls ↦ …
(2) Not (Not Tru) ↦ … (3) Combine (1) and (2)
2
Exercises
data (↦*) : Term → Term → Type where Idemp : t ↦* t
Trans : t1 ↦ t2 → t2 ↦* t3 → t1 ↦* t3
↦⊆× ∗
4. Define the ↦* predicate using inference rules.
∗
1 2 2 ∗ 3
1 ∗ 3
CS 582 • Operational Semantics 3
∗ 5. Draw a derivation tree for
Not Tru Fls Not Fls Tru
t t′ Nott Nott′
Exercises
the statement
Not (Not Tru) ↦* Tru
Not TruFls
Not (Not Tru) Not Fls
CS 582 • Operational Semantics
1 2 2 ∗ 3 ∗
Not FlsTru Tru∗ Tru Not Fls ∗ Tru
13
Not (Not Tru) ∗ Tru
nnts : Not (Not Tru) ↦* Tru
nnts = NotInd NotTru `Trans` NotFls `Trans` Idemp
4
Exercises
data Update : (Var,Val) → State → State → Type where
Init : Update (x,v) [] [v]
Upd : Update (0,v) (u::s) (v::s)
Ctxt : Update (x,v) s s’ → Update (S x,v) (w::s) (w::s’)
7. Provide a derivation for the following state transition.
upd_y : Update (Y,4) MyState [2,4]
upd_y = Ctxt Upd
Y : Var Y=1
MyState : State
MyState = [2,3]
CS 582 • Operational Semantics
5
Exercises
data Lookup : Var → State → Val → Type where Found : Lookup 0 (v::s) v
Search : Lookup x s v → Lookup (S x) (w::s) v
data Eval : State → Exp → Val → Type where
E_N :Evals(Nn)n
E_Plus:Evalsen→Evalse’m →Evals(Plusee’)(n+m) E_V :Lookupxsn→Evals(Vx)n
8. Prove the following statements.
x_plus_4 : Eval MyState (V X `Plus` N 4) 6
x_plus_4 = E_Plus (E_V Found) E_N
MyState : State
MyState = [2,3]
CS 582 • Operational Semantics
6
x_plus_4_plus_y : Eval MyState ((V X `Plus` N 4) `Plus` V Y) 9
x_plus_4_plus_y = E_Plus x_plus_4 (E_V (Search Found))