カリー・ハワード対応 (3)

reducibilityに入る。定義だらけのところは終わり、がしがしと証明していく。一般論をやっているので、なかなか何のためにやっているのかをつかみにくい。どこにも何の説明もない記法が出てきて何のことやら。とって何だろう。Gallierの別の論文を見てみるか。*1

*1:前者がβ-reductionの推移閉包、後者が反射推移閉包でした。