Естественная семантика языка 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