Haskell CS 421 LogoCS 421 — Programming Languages

Big Step Semantics Editor

Big Step Semantics

Write a proof tree for the following judgement:

<if x>y then m:=xx else m:=yy fi,{x:=10,y:=20}>{x:=10,y:=20,m:=400}\lt \mathtt{if}\ x \gt y\ \mathtt{then}\ m:=x * x\ \mathtt{else}\ m := y * y\ \mathtt{fi}, \{ x:=10, y:=20 \} \gt \Downarrow \{ x:=10, y:=20, m:=400 \}

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: 29.56%
<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}}