ようこそ!浜村拓夫の世界へ

    ブログ内検索

    最近の記事

    ブックマーク数の多い記事

    Blog Translation

    Powered By FC2ブログ

    Powered By FC2ブログ
    ブログやるならFC2ブログ


    FC2ブログ LOGIN

    with Ajax Amazon

    OCamlのまなびかた~型付きラムダ計算って何だ?

    このエントリーを含むはてなブックマーク はてなブックマーク - OCamlのまなびかた~型付きラムダ計算って何だ? あとで読む
    OCamlの勉強方法についてアドバイスがあった。

    OCamlのまなびかた - まあ、そんなもんでしょう。

    OCamlには日本語の本が3冊あります。じっくり勉強したい人には本という媒体が適していると思います。「プログラミングの基礎」はプログラミングそのものも一緒に学びたい人向け。OCaml自体を勉強したいなら「プログラミング in OCaml」。手っ取り早く応用してみたい人は「入門OCaml」。

    英語ですがマニュアルを読むと全体像が分かって来て安心できます。OCamlに関する丁寧で完全な一次元情報はこれしかないといってもよく、隅から隅まで有用です。

    [追記]OCamlとかHaskellのようなML系の言語に初めて触れる人は、型付きλ計算について少し予備知識を持つと、理解が深まると思います。



    ・日本語の本を読む。
    ・英語のマニュアルには、詳しく解説してある。
    ・型付きλ計算について予備知識を持つとグッド。

    ●型付きλ計算
    型付きλ計算って何だろ?

    自然演繹による証明がλ式に対応する
    自然演繹の証明が、型付きのλ計算のなかで自然に表現できる



    第14回 型=命題,プログラム=証明 - 数理科学的バグ撲滅方法論のすすめ:ITPro

    MLの型と型推論
    MLやHaskellなど多くの静的型付き関数型言語には,「型推論」という機能がある。
    これは,プログラム中の変数や関数の型を省略しても,「もっとも一般的」な型を言語処理系が勝手に推論してくれる,という機能だ。

    型推論の「逆問題」
    型推論は「式を与えられたら,その型を求める」という問題だった。
    逆に,「型を与えられたら,その型を持つ式を求める」ことを考えてみよう。

    関数は「ならば」の証明,組は「かつ」の証明
    型は,ある種の論理式とみなすことができる。
    'aや'bのような型変数はAやBなどの命題変数に,-> は論理記号の⇒(ならば)に,*は∧(かつ)に対応する。

    型が論理式(命題)にあたるとすれば,その型を持つ式(プログラム)は何にあたるのだろうか?
    実は,「式」は「型」が表す命題の証明とみなすことができる。
    このような「型=命題,プログラム=証明」という対応のことを,カリー・ハワードの対応(Curry-Howard correspondence)という。

    これらの理論は一般に,型理論(type theory)と呼ばれ,数学の定理やプログラムの仕様などをコンピュータによって厳密に検証する定理証明器(theorem prover)の基礎として,盛んに研究されている。



    よく分からんが、型は命題(論理式)として扱われるらしい。

    ●カリー・ハワードの対応
    技術者/プログラマのためのラムダ計算、論理、圏 第3回に行ってきた

    第3回 自然演繹と型付きラムダ計算、カリー/ハワード対応
    論理を中心に話をすすめていき、論理でやっていることが最終的にラムダ計算に対応することを感覚的に理解することで、カリー・ハワード対応を感じるのが目的、という感じ。



    カリー/ハワード(Curry-Howard)の対応を知らない子ども達および大人達へ - 檜山正幸のキマイラ飼育記
    Kuwataさんによるまとめ

    「カリー・ハワードの対応」ってのがキーワードみたいだな。
    …これは多分、即席で理解できる話じゃなさそう。
    あとでじっくり読んでみよう。

    プログラミング in OCaml ~関数型プログラミングの基礎からGUI構築まで~プログラミング in OCaml ~関数型プログラミングの基礎からGUI構築まで~
    (2007/11/30)
    五十嵐 淳

    商品詳細を見る
    関連記事

    コメント

    コメントの投稿


    管理者にだけ表示を許可する

    トラックバック

    トラックバックURL:
    http://hamamuratakuo.blog61.fc2.com/tb.php/355-f0b99c06

    FC2Ad