昨日のエントリでカリーハワード同型対応について触れました。
関数を扱えることはどのようにプログラミング言語の能力をあげるか - きしだのはてな
ついでに、このエントリを書くのに調べたカリーハワード同型対応の資料をまとめておきます。
この記事では、カリーハワード同型対応で、どのような型がどのような論理命題に対応するかを解説してあります。
数理科学的バグ撲滅方法論のすすめ - 第14回 型＝命題，プログラム＝証明：ITpro
こちらのほうが、ちょっとくだけてるかな？
Curry-Howard Isomorphism - d.y.d.
カリーハワード同型対応での山場は、排中律がSchemeのcall/ccに対応するというところで、gotoなどもだいたいこれにあてはまるようです。
排中律、つまり「a または not a」という命題です。これは証明としてはアヤシイので、古典論理からはずしましょうとなって、直観主義論理というのができました。
これが、gotoはアヤシイのでプログラミング言語からはずしましょうという話に対応するわけです。ここがおもしろい。
このあたりは、こちらのエントリが詳しいですが、かなり形式的な説明なので読むのは大変。
call/ccと古典論理のカリー・ハワード対応 - 再帰の反復
書籍としては昨日もあげた「論理の哲学」がとてもいいです。
- 作者: 飯田隆
- 出版社/メーカー: 講談社
- 発売日: 2005/09/10
- メディア: 単行本（ソフトカバー）
- 購入: 1人 クリック: 25回
- この商品を含むブログ (43件) を見る
形式的な説明はこちらに載ってます。
- 作者: 萩谷昌己,西崎真也
- 出版社/メーカー: 岩波書店
- 発売日: 2007/06/27
- メディア: 単行本
- 購入: 14人 クリック: 442回
- この商品を含むブログ (36件) を見る
あとは、未読なんですが、この本も評判がよいようで上記「論理の哲学」でも取り上げられています。
- 作者: 小野寛晰
- 出版社/メーカー: 日本評論社
- 発売日: 1994/04/01
- メディア: 単行本
- 購入: 10人 クリック: 206回
- この商品を含むブログ (32件) を見る
