SDPE との関係:HOAS を用いた SDPE
R(?x. t) = ?y. R((?x. t) @ y)
R(t1 @ t2) = (?x. t) @ R(t2) (if R(t1) = ?x. t)
R(t1 @ t2) = R(t1) @ R(t2) (otherwise)
?
??(?x. t) = ?x. t
t1 @? t2 = (?x. t) @ t2 (if t1 = ?x. t)
t1 @? t2 = t1 @ t2 (otherwise)
? @? の定義と一致する!
Previous slide
Next slide
Back to first slide
View graphic version