SDPE との関係:HOAS から FOAS への変換

F(?x. t) = ?y. F((?x. t) @ y) (where y is fresh)

F(t1 @ t2) = F(t1) @ F(t2)

F(y) = y

? reify の定義と一致する！

Previous slide

Next slide

Back to first slide

View graphic version