曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾弐「集合族のデカルト積(途中から)」「定義による同等性」「デカルト積の応用(途中まで)」(復習編)

 こちらの復習編。他の回はこちらから。

名前(name)

 前回もそうだったが、プログラムの「名前(name)」というのがなんなのかよくわからない。計算機科学ではよくある言い回しなのだろうか。

 名前はわかっているけど実際の計算はよくわからないようなプログラムは名前だけ付けられるということか。型がわかっていれば実行の結果はそのカノニカルな要素になるというところまでわかる。

\Pi 等号について

 この規則の正当化がいろいろ書いてある。一瞬派生規則なのかと思ったが、計算という概念が付け加えられている。

\equiv の decidable とは?

 まず \equiv というのはメタ記号である。つまり、ITTのシステムの言語ではない。なので、例えば a \equiv b は、a = b のようなシステムの中の命題(本当は型がいると思うけど)と違ってシステムの外で勝手に決定できるということかと。

何故 suppressing するのか?

 これはよくわからないのだけれど、自然演繹が得られるということを示しておきたいのかも。ちゃんと論理の導出システムが作れますよ、と