>>769
そうですね
多分対応自体はわかると思います
しかし実際カリーハワード対応で基礎論の世界に持って行くことの効用がよくわかりません
基礎論の世界に持っていって基礎論でよく知られたなんかの定理が使えるとかいうわけでもなさそうですし
最初はcall by needの実装の話、すなわちcall by needでは展開された評価式に同じexpressionが出たとき、その内容を保持して同じ評価を何度も繰り返すのを防ぐらしいですが、もちろんどんな評価でも何でもかんでもメモするわけではないようなので、結局自分で手前でメモ化する必要がでたりします
どういう時はcall by needのメモ化が効いてどういう場合は効かないのかよくわからないので現状は“やってみる”しかないし、やってみて上手くいかなくても、なんか上手い書き方すればやってくれるのか、はなからだめなのか、その判別もつきません