我々の TDPE: 例
= reify(?f. ?n. f @? (n +? (1 +? 2)))= ?x. reify((?f. ?n. f @? (n +? (1 +? 2))) @ x)= ?x. reify(?n. x @? (n +? (1 +? 2)))= ?x. ?y. reify((?n. x @? (n +? (1 +? 2))) @ y)= ?x. ?y. reify(x @? (y +? (1 +? 2)))= ?x. ?y. reify(x @? (y +? 3))
(整数に対する +? の定義)
Previous slide
Next slide
Back to first slide
View graphic version