Haskell CS 421 LogoCS 421 — Programming Languages

Big Step Semantics Editor

Big Step Semantics

Write a proof tree for the following judgement:

t:=a+b;a:=b;b:=t,{a:=10,b:=20}{t:=30,a:=20,b:=30}\langle t := a + b; a := b; b := t, \{ a:=10, b:=20 \} \rangle \Downarrow \{ t:=30, a:=20, b:=30 \}

Each line of your tree should have the following components:

  1. a number followed by a period to indicate its depth in the tree. 0 is the root.
  2. a configuration, in the form < stmtstmt, snn > (where nn is an integer) or as a set of variable assignments. For example, the notation s2 represents σ2\sigma_2.
  3. A downarrow operator as ||, ||e, or ||b, as appropriate.
  4. A value
  5. A rule name in parenthesis.

If you use s or s1, etc. in your proof tree, you must follow the tree with their expanded out definitions.

The starter code shows a valid tree for a proof of <m:=x+1,σ>σ2\lt m := x + 1, \sigma \gt \Downarrow \sigma_2.

Here are the big step rules.

Proof Tree Editor

Score: 25.00%
<x,σ>e3VAR<1,σ>e1CONST<x+1,σ>e10ARITH<m:=x+y,σ>σ2ASSIGN\frac{\frac{\frac{}{\displaystyle <x,\sigma_{}> \Downarrow_e 3} \textstyle \mathrm{V\small{AR}} \quad \frac{}{\displaystyle <1,\sigma_{}> \Downarrow_e 1} \textstyle \mathrm{C\small{ONST}}}{\displaystyle <x+1,\sigma_{}> \Downarrow_e 10}\textstyle \mathrm{A\small{RITH}}}{\displaystyle <m:=x+y,\sigma_{}> \Downarrow \sigma_{2}}\textstyle \mathrm{A\small{SSIGN}}