Description
Exercise 1 Consider the following programming language, called miniML, that features (recursive) procedures and explicit references.
Syntax The syntax is defined as follows:
| P | → | E |
| E | → | n |
| | | x | |
| | | E + E | E − E | E ∗ E | E/E | |
| | | E − E | |
| | | iszero E | |
| | | if E then E else E | |
| | | let x = E in E | |
| | | letrec f(x) = E in E | |
| | | proc x E | |
| | | E E | |
| | | ref E | |
| | | ! E | |
| | | E := E | |
| | | E;E | |
| | | begin E end |
Semantics The semantics is defined with the following domain:
| Val | = | Z + Bool + Procedure + RecProcedure + Loc |
| Procedure | = | Var × E × Env |
| RecProcedure | = | Var × Var × E × Env |
| ρ ∈ Env | = | Var → Val |
| σ ∈ Mem | = | Loc → Val |
1
and evaluation rules:
ρ,σ0 0,σ1 ρ,σ0
ρ,σ0 ` iszero E ⇒ true,σ1 ρ,σ0 ` iszero
ρ,σ0 ` E1 ⇒ true,σ1 ρ,σ1 ` E2 ⇒ v,σ2
ρ,σ0 ` if E1 then E2 else E3 ⇒ v,σ2
ρ,σ0 ` E1 ⇒ false,σ1 ρ,σ1 ` E3 ⇒ v,σ2
ρ,σ0 ` if E1 then E2 else E3 ⇒ v,σ2
ρ,σ0 ` E1 ⇒ v1,σ1 [x 7→ v1]ρ,σ1 ` E2 ⇒ v,σ2
ρ,σ0 ` let x = E1 in E2 ⇒ v,σ2
[f 7→ (f,x,E1,ρ)]ρ,σ0 ` E2 ⇒ v,σ1
ρ,σ ` letrec f(x) = E in E ⇒ v,σ ρ,σ ` proc x E ⇒ (x,E,ρ),σ
Dom(σ1)
ρ,σ0 ` E ⇒ v,σ1
ρ,σ0 ` begin E end ⇒ v,σ1
Implement an interpreter of miniML. Raise an exception UndefinedSemantics whenever the semantics is undefined. Skeleton code will be provided (before you start, see README.md).
2
