Haskell CS 421 LogoCS 421 — Programming Languages

Big Step Semantics Editor

Here is a proof tree editor.

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

<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}}