Inference Rules and Axioms

An inference rule is a set of antecedents and a consequent. If the antecedents are true, the consequent follows. (If A and B then C)

\frac{A B}{C} = Inference Rule

Logic Rules:

\frac{A ⟹ B A}{A} = If A implies B and A then B

Notational conventions:

$v$ is a variable representing values
$t$ is a variable representing terms
$\pm$ is an operation in our concrete syntax while $+$ is an operation in Haskell
$t_{1} ⇓ t_{2}$ is an evaluation relation, it is read " $t_{1}$ evaluates to $t_{2}$ "

Rules

Values evaluate to themselves. (Note the underline)

eval (Num v) = v

\frac{}{\underset{―}{v} ⇓ v} = NumE

Subtraction in AE is subtraction in Haskell

Note

We add a second rule to make sure invalid cases evaluate as well.

eval (Sub (Num v1) (Num v2))

\frac{t_{1} ⇓ v_{1} t_{2} ⇓ v_{2} v_{1} \geq v_{2}}{t_{1} \underset{―}{-} t_{2} ⇓ v_{1} - v_{2}} = SubE+

\frac{t_{1} ⇓ v_{1} t_{2} ⇓ v_{2} v_{1} < v_{2}}{t_{1} \underset{―}{-} t_{2} ⇓ 0} = SubEZero