名前(name)
前回もそうだったが、プログラムの「名前(name)」というのがなんなのかよくわからない。計算機科学ではよくある言い回しなのだろうか。
名前はわかっているけど実際の計算はよくわからないようなプログラムは名前だけ付けられるということか。型がわかっていれば実行の結果はそのカノニカルな要素になるというところまでわかる。
等号について
この規則の正当化がいろいろ書いてある。一瞬派生規則なのかと思ったが、計算という概念が付け加えられている。
の decidable とは?
まず というのはメタ記号である。つまり、ITTのシステムの言語ではない。なので、例えば は、 のようなシステムの中の命題(本当は型がいると思うけど)と違ってシステムの外で勝手に決定できるということかと。
何故 suppressing するのか?
これはよくわからないのだけれど、自然演繹が得られるということを示しておきたいのかも。ちゃんと論理の導出システムが作れますよ、と