Естественная семантика языка Exp4.

11) Естественная семантика языка Exp4.

Правило CR
_________
р |- n =>A n

Правило VarR
___________
р|- x =>A r(x)

Правило OpR
р|- e =>A v       р|- e’ =>A v’
р|- e op e’ =>A Ap(opNum, v, v’)

Правило LocR
р|- e =>A v    р[x/v]|- e’ =>A v’
р|- let x = e in e’ =>A v’

Правило IfR
р|- be =>B T         р|- e =>A v
р|- if be Then e Else e’ =>A v

р|- be =>B F         р|- e’ =>A v’
р|- if be Then e Else e’ =>A v’

Семантика отношения =>B

Правило CR
_________           _________
р|- T =>B T           р|- F =>B F

Правило VarR
_____________
р|- bx =>B r(bx)

Правило EqR
р|- e =>A v      р|- e’ =>A v
р|- Equal(e,e’) =>B T

р|- e =>A v    р|- e’ =>A v’
--------------------------------   [v =/= v’]
р|- Equal(e,e’) =>B F

Правило BOpR
р|- be =>B bv             р|- be’ =>B bv’
р|- be bop be’ =>B Ap(bop, bv, bv’)

Правило NotR
р|- be =>B T             р|- be =>B F
р|- Not be =>B F      р|- Not be =>B T