Attempt at a simplified big step notation

custom_big_step.md

AST

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Var(name: String)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec(name: String, value: Expr, body: Expr)
  case Function(param: String, body: Expr)
  case Apply(function: Expr, arg: Expr)
  case Cond(pred: Expr, thenBranch: Expr, elseBranch: Expr)

enum Value:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Function(param: String, body: Expr, env: Env)

Literals

Num

--------------------------------
E |- Num value ⇓ Value.Num value

Bool

----------------------------------
E |- Bool value ⇓ Value.Bool value

Simple functions

Add

E |- lhs ⇓ n1    E |- rhs ⇓ n2
--------------------------------------
E |- Add lhs rhs ⇓ Value.Num (n1 + n2)

Gt

E |- lhs ⇓ n1    E |- rhs ⇓ n2
--------------------------------------
E |- Gt lhs rhs ⇓ Value.Bool (n1 > n2)

Conditionals

E |- pred ⇓ true    E |- thenBranch ⇓ n
----------------------------------------
E |- Cond pred thenBranch elseBranch ⇓ n

E |- pred ⇓ false    E |- elseBranch ⇓ n
----------------------------------------
E |- Cond pred thenBranch elseBranch ⇓ n

Local bindings

Let

E |- value ⇓ n1    E[name <- n1] |- body ⇓ n2
---------------------------------------------
E |- Let name value body ⇓ n2

Var

-----------------------
E |- Var name ⇓ E(name)

Non-recursive functions

Function

------------------------------------------------------
E |- Function param body ⇓ Value.Function param body E

Apply

E |- function ⇓ Lambda param body E'    arg ⇓ n1   E'[param <- n1] |- body ⇓ n2
-------------------------------------------------------------------------------
E |- Apply function arg ⇓ n2

Recursive functions

E' = E[name <- null]; E' |- value ⇓ n1    update(E', name, n1); E' |- body ⇓ n2
--------------------------------------------------------------------------------
E |- LetRec name value body ⇓ n2