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

    ブログ内検索

    最近の記事

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

    Blog Translation

    Powered By FC2ブログ

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


    FC2ブログ LOGIN

    with Ajax Amazon

    OpenIDによる個人情報の保護

    このエントリーを含むはてなブックマーク はてなブックマーク - OpenIDによる個人情報の保護 あとで読む
    ゆびとま(この指とまれ)という大手SNSのサービスが突然停止された。

    サービス停止のお知らせ - ゆびとま

    甚大なトラブルが発生したことにより、しばらくサービスを停止させて頂きます。



    <同窓会支援サイト>「ゆびとま」突然停止…会員350万人

    卒業後疎遠になった友達とインターネットを通じて再会しようという同窓会支援サイト「この指とまれ!」(通称・ゆびとま)が5月初めに突然停止された。
    会員数は約350万人に上り、小学校から大学まで約6万校の出身者が利用しているとされているだけに「お互いの連絡がとれなくなった」と混乱が起きている。
    また、登録に際して入力された膨大な個人情報の行方を危惧(きぐ)する声もあがっている。

    登録にあたっては、住所、氏名、生年月日、出身校名、メールアドレスなどを入力することになっているため、「個人情報の流出はないのか」といった不安の声も出ている。



    ●個人情報は金になる
    個人情報を販売すると、購入する人たちがいるので、金になる。
    昔から、名簿図書館のようなサービスがあった。

    三菱UFJ証券、社員が148万人分の顧客情報を不正持ち出し

    三菱UFJ証券は8日、元社員が個人顧客148万6651人分の情報を不正に持ち出し、そのうち4万9159人分を名簿業者に売却していた事実が判明したとして、事態を公表した。



    GIGAZINE曰く「楽天は個人情報を1件10円で販売している - スラッシュドット・ジャパン

    GIGAZINEの記事「楽天、利用者のメールアドレスを含む個人情報を「1件10円」でダウンロード販売していることが判明」によると、楽天が個人情報を流出ではなく「販売」していたそうです。
    すでに実名・住所などを利用したエロサイトの業者スパムが多数届いているとのこと。



    ●オプトアウト方式
    個人情報を購入した人たちは、どのように利用するのだろうか?
    その一つの方法が、ダイレクトメールの送付だ。

    オプトアウトとは 【opt-out】 - IT用語辞典

    ユーザの許諾無く、一方的に広告メールを送りつけること。
    また、それを拒否して広告を送付しないよう企業に依頼すること。
    ユーザの事前承諾なしに送られるダイレクトメールを「オプトアウトメール」と言う。

    オプトアウトとは逆に、ユーザが明示的に広告の受け取りを許諾することを「オプトイン」と言う。
    一般に、メールによる広告活動はオプトインによってなされるべきであり、オプトアウトなものは迷惑メールとして煙たがられる。



    ●オプトイン方式
    ダイレクトメールで宣伝を行う場合、宣伝内容とターゲットユーザーの関心分野とのマッチングが重要だ。
    メールフィルターを使っていれば、オプトアウトの宣伝メールはゴミ箱直行なので、意味がない。
    個人情報を買い取る人たちは、果たして十分な成果を上げられているのだろうか?

    その点、Googleのオプトイン方式は、非常にうまくやっている。
    Googleが個人情報を登録させる場合は、Googleが活用できるように規約を組み立てている。
    ターゲットユーザーのプロファイリングと、広告のマッチングを全自動で行ない、高いコンバージョン率を誇っている。

    ●他人の行動は制御不可能
    パーソナルコンピューターやインターネットが普及した現代においては、自分が登録してない情報、公開してない情報でも、流出してさらし者にされる時代だ。

    ケツ毛バーガー事件とはどんな事件だったのですか - Yahoo!知恵袋
    秋篠宮佳子さまプライベート写真 ネット流出で波紋 同級生男子が無断掲載

    ましていわんや、自分から提供した情報は、飛んで火に入る夏の虫~誰の手に渡るか分からないと思った方がいいだろう。
    自分の管理下にないものを、自分の思い通りに制御することは、ほとんど不可能であると言わざるを得ない。

    銀行口座、クレジットカード、携帯電話…多くの人は、自分が目に見えない鎖で首をつながれている奴隷になっており、自分の知らないところでさらし者になっていることが分かっていない。

    ●個人情報を登録しない
    個人情報を登録しないで、各種のWEBサービスを利用することはできるだろうか?
    完全ではないが、OpenIDという仕組みを使えば、登録の手間を省くことは可能になる。

    OpenID - Wikipedia

    OpenID(オープンアイディー)とはサイトを越えて使用できる「認証システム」と「そのシステムで利用できるID(identification)」を指す。
    個人が登録した情報を公開することで個人の同一性を保証する。
    複数のOpenIDシステム対応サイトを1つのOpenID(identification)で利用できる。
    情報提供は、OpenIDの所有者の同意に基づいて、いつ、どこで、だれに、何の目的で行われるかを管理できる。(ユーザーの同意に基づかない提供は無い。自分の知らせたい情報を書く)



    ●統合化されるインターネットサービス
    最近、P2P技術などを利用した大規模なクラスタリングよりも、クラウドコンピューティングの方が効率が良いと喧伝されているように思われる。
    「クラウド」は、「Web2.0」と同様に、単なるバズワードと見なすこともできるが、クラウド=リソースの仮想化、プラント化の方が、ユーザーにとって利便性が高くなるという予想は、あながち間違いではないと思う。

    クラウドコンピューティング - Wikipedia

    従来のコンピュータ利用は、ユーザー(企業、個人など)がコンピュータのハードウェア、ソフトウェア、データなどを、自分自身で保有・管理していたのに対し、クラウドコンピューティングでは「ユーザーはインターネットの向こう側からサービスを受け、サービス利用料金を払う」形になる。

    ユーザーが用意すべきものは最低限の接続環境(パーソナルコンピュータや携帯情報端末などのクライアント、その上で動くブラウザ、インターネット接続環境など)と、サービス利用料金となり、処理が実行されるコンピュータ本体や蓄積するデータなどの、購入や管理の大半が不要になる。

    クラウドコンピューティングは、従来から存在するネットワーク・コンピューティング、ユーティリティコンピューティング、SaaSなどを、ユーザーの視点で呼び直したもの、あるいはこれら要素を含み更に発展させたもの、などとされる。



    将来、量子コンピューターが実用化されて、超高速な並列処理が可能になった場合、クラスタリングではなくクラウドコンピューティングに近い形で利用しているのではないだろうか?
    (量子コンピューターが大量生産されて、1人が1台持てるようになれば、クラウドじゃなくてもいい。)

    コンピューターのリソースを外部のクラウドに一元化して使うスタイルと、個人情報をOpenIDに一元化して使うスタイルは、ハードとソフトのレイヤーにおいて相似形をなしていると思う。
    デメリットがあるとすれば、持てる者と持たざる者の二極化が進み、独占による不正が横行する可能性だろう。
    しかし、今も昔もそしてこれからも、人間が不正をしなくなるなんてことはまずないだろうから、状況は大差無しと。

    開発者や運営者の立場で見ると、面倒くさいユーザー管理、ユーザー認証をOpenIDに丸投げできるというメリットがある。
    マーケティングのために、オプトインで個人情報を収集したいなら、別の仕掛けを併設すればいい。

    本当に大事な情報は、コカコーラのレシピのように、外部には一切出さない。~自分の頭の中にだけ置いておけばOK。

    ●小額の決済サービス
    OpenIDの次は、小額決済サービスの普及だな。
    Amazon FPSみたいな仕組みを、日本の銀行や電話会社がどんどん提供すれば、通販市場がもっと活性化できる。

    正式サービスインの『Amazon FPS』 日本の課金システムをどう塗り替えるか?

    Amazon FPSは同社のクラウドサービス「Amazon Web Services (AWS)」のひとつとして2007年8月に限定ベータ提供が開始されたもので、2者間でのお金の転送や、クレジットカード/銀行口座からの電子送金などに対応した課金サービスとして利用できる。


    電話番号入力だけで送金 NTTドコモとみずほ銀提携

    決済の手数料がもっと安ければ、小額の取引が増えて、日本経済の活性化につながるのではないか?
    金の流れは、資本主義社会における血の巡りのようなもの。血行が悪くなると、弱ってくる。

    なんで政府・行政は、業界に提言・指導しないのだろうか?
    公務員ってやつは不況でも給料出るし、面倒くさい仕事は増やしたくない、自分に与えられた仕事をこなせばOK。
    民間で勝手にやってろと。
    まぁ、広く薄くピンハネできる仕組みだから、いづれ普及するだろうけど。


    夢ばかり見てた そして僕は喋りすぎた
    帽子の頭文字から 部屋番号を探しだした

    コーラの飲みすぎで筋肉障害の危険

    このエントリーを含むはてなブックマーク はてなブックマーク - コーラの飲みすぎで筋肉障害の危険 あとで読む
    炭酸飲料は、ゲップが出て飲みづらい。
    とても清涼感があるとは思えない。

    炭酸飲料に飽きたら、次はドラッグで清涼感を得るしかなくなるのだろうか?
    LSD・コーラ、メスカリン・コーラ、メタアンフェタミン・コーラなどがあったら、バカ売れするかもしれない。

    ●コーラの飲みすぎで筋肉障害の危険
    コーラを飲みすぎると筋肉障害になるというニュースがあった。

    コーラの飲みすぎで筋肉障害の危険、ギリシャの医師が警鐘

    【5月20日 AFP】(一部訂正)コーラなどの炭酸飲料を毎日数リットル飲むと、深刻な筋肉障害を発症する場合があると、ギリシャ・イオニア大学(University of Ioannina)などの研究チームが19日、警鐘を鳴らした。

    同大のモーゼス・エリサ(Moses Elisaf)医師を中心とする研究チームは、1日2-9リットルの炭酸飲料を飲んだ患者の症例を検証。
    その結果、加工糖やカフェインを多く含んだ清涼飲料水を大量に飲むと、血液中のカリウム濃度が急激に下がり、「低カリウム血症」と呼ばれる病気にかかる恐れがあることがわかったという。

    カリウム濃度が少しでも変わると、心臓血管系や筋神経系の機能に多大な影響を与える場合がある。
    低カリウム血症になると、筋力の低下、筋けいれん、動悸、吐き気などの症状が現れる。
    より深刻なケースでは、心臓病や重度のまひを引き起こすこともある。



    ●低カリウム血症
    低カリウム血症という病気があるそうだ。

    低カリウム血症 - Wikipedia
    低カリウム血症 - goo ヘルスケア
    メルクマニュアル家庭版, カリウム 155 章 ミネラルと電解質

    体のなかのカリウムのほとんど(98%)は細胞のなかにあり、残りのわずか(2%)が血液中など細胞の外に存在しています。
    しかし、血液中のカリウムは細胞のはたらきを調節するうえでとても重要で、この値が乱れると全身に重大な障害が生じます。
    通常、血液中のカリウム濃度は3・5~5・0mEq/lという狭い範囲内で維持されていますが、3・5mEq/l以下に低下した状態を低カリウム血症といいます。

    低カリウム血症が起こる原因は、
    (1) カリウムの摂取量が少ない、
    (2) 体外に出ていくカリウムの量が多い、
    (3) 血液中から細胞のなかにカリウムが取り込まれてしまう、
    の3つがあげられます。

    (3)はアルカローシスといって、何らかの原因で血液がアルカリ性に傾くことや、血糖を下げるインスリンというホルモンが血液中に増えることなどが原因になります。
    甲状腺機能亢進症(こうじょうせんきのうこうしんしょう)の場合にもしばしば起こります。



    糖分の多いコーラをガブ飲み

    血糖値を下げるためにインスリンの分泌

    低カリウム症

    というプロセスだろうか?

    ●ペットボトル症候群
    コーラの過剰摂取は低カリウム血症を引き起こす恐れあり - スラッシュドット・ジャパン

    ただのペットボトル症候群じゃないのか
    GIK療法というのがあってインスリンとブドウ糖を投与すると細胞内にブドウ糖が引き込まれるとともにカリウムも細胞内に入ります。
    その前にソフトドリンクケトーシス [dm-net.co.jp](ペットボトル症候群)という言葉を知らないのではないでしょうか。
    糖尿病がある一線を越えると、ケトン体が血中に多くなり、酸性に血が傾くケトアシドーシスになります。そこまで至れば細胞内からカリウムが出て高カリウム [u-toyama.ac.jp]になります。しかし、十分なインスリンが投与されると今度は細胞にカリウムが戻り低カリウムになります。自然経過を追ってしまい、教科書的な治療の手順を忘れてしまったのではなかろうかしらと、ちょっと首を傾げます。
    著しい高血糖では偽性低ナトリウムになりますが、恒常的に9Lの飲水が可能な状態なら呑みすぎによる低ナトリウムや低カリウムも危惧されます。マラソンでの低ナトリウム [nankodo.co.jp]が一例です。



    ペットボトル症候群 - Wikipedia

    ペットボトル症候群(ペットボトルしょうこうぐん、PET bottle syndrome)とは、 スポーツドリンク、清涼飲料水などを大量に飲み続けることによっておこる急性の糖尿病。

    市販飲料の多くには、100mlあたり10g(グラム)程度とかなり多く糖質が含まれている。
    スポーツドリンクにはたいてい100mlに6g程度の糖分が含まれている。
    ペットボトル飲料の普及とその手軽さから、知らず知らずのうちに過剰な糖分を摂取することになる。
    20代から30代の若者に多い。



    コーラの代わりにウーロン茶を飲んだほうがいいみたい。

    ●コーラを自分で作る
    ウーロン茶じゃ嫌だという人は、自分でコーラ風のドリンクを作って、糖分を少なめにしたらいいかもしれない。

    オープンコーラ - Wikipedia

    オープンコーラ(OpenCola)は、製法が自由に手に入り、その改変も自由という、ユニークなコーラ。
    以下に示すレシピは、2001年2月20日に公表された、バージョン1.1.3のものである。

    香料の製法
    * 10.0gの食用アラビアガム
    * 3.50mlのオレンジ油
    * 3.00mlの水
    * 2.75mlのライム油
    * 1.25mlの肉桂油
    * 1.00mlのレモン油
    * 1.00mlのナツメグ油
    * 0.25mlのコリアンダー油
    * 0.25mlのネロリ油
    * 0.25mlのラベンダー油

    濃縮液の製法
    * 2.36kgの白砂糖(プレーンなグラニュー糖)
    * 2.28lの水
    * 30.0mlのカラメル(着色料)
    * 小さじ3.50の75%リン酸またはクエン酸
    * 小さじ2.00の香料
    * 小さじ0.50のカフェイン(任意)

    飲料の製法
    濃縮液を5倍の濾過した水と混ぜ、飲料を炭酸化する。
    もしくは、蛇口で濃縮液と炭酸水を混ぜるソーダ水機を使う。



    ●コーラの安全性
    コーラを飲んでも死ななかった。
    1本飲んだくらいでは、どうってことない。
    1億本くらい飲んだら違いが分かるかな?

    コーラの安全性 - 教えて!goo

    私はコーラが好きでよく飲むのですが、おばあちゃんに「コーラを飲むと骨が溶けるから飲んじゃ駄目」と注意されます。
    そのような危険な商品を販売し続けられるわけはないと思うので、誤解を解きたいのですが、そのときに参考になりそうなサイト、本はないでしょうか?



    コーラが骨を溶かすというのは、本当なのですが、実際に骨を溶かしているのは、コーラ自体ではなく、コーラに含まれる炭酸によるものです。
    骨は、カルシウムでできていますが、カルシウムは、酸によって解けてしまいます。

    コーラが骨を溶かすという理由で、飲んではならないのであれば、サイダーも酢もレモンも全て食べたり飲んだりしてはならなくなってしまいます。
    クエン酸も取ることはできません。

    コーラを骨が解けるという理由で飲むのを避ける事は、全く見当違いですが、コーラ自体に体に良い成分は、全く含まれておりませんから、飲まない事による不利益はありませんし、糖分の取りすぎや、習慣性物質を取る事の不利益が有りますから、飲まないのであれば、それにコした事はありません。



    コーラのヤバさ → 低カリウム症、ペットボトル症候群>骨を溶かす

    制約なんて真っ平御免~コーラを飲み続けるという人は、自己責任で飲むしかない。
    中毒を克服する過程では、禁欲の苦しみを受け入れなければならない。
    そもそも中毒になっていなければ、禁欲の苦しみも生じなかったのだが、不満を言う人間は己の過ち、無智に気付いていない。
    酒、タバコ…世の中には中毒があふれかえっている。

    コーラ白書―世界のコーラ編コーラ白書―世界のコーラ編
    (2007/10)
    中本 晋輔中橋 一朗

    商品詳細を見る

    人種差別の言葉 ~ シンシャンション

    このエントリーを含むはてなブックマーク はてなブックマーク - 人種差別の言葉 ~ シンシャンション あとで読む
    人間のエゴ(自我意識)には様々な相があるが、エゴの最悪の状態が、
    自分さえ良ければ、他人はどうでもいい
    という状態である。

    あと49日:浜村拓夫の世界

    人間の意識は、「快楽を求め、苦しみを避ける」ようなバイアス、偏向がかかっています。
    人間のエゴ(自我意識)は、究極的には「自分さえ良ければ、他人はどうでも良い」という状態に至ります。
    綺麗事を抜きにすれば、人間は自分のことしか考えていないのです。
    この状態を経験すると、意識が解放的になり、非常にエネルギッシュかつ積極的になりますが、同時に、自他ともに傷付けてしまう行動をなす場合があります。



    この状態は、程度の差こそあれ全ての生物に備わっている特徴であり、具体的にはホメオスターシス(恒常性維持機能)として全ての生物に組み込まれている仕組みである。
    人間を含めた全ての生物の行動原理は、この特徴によって一切の例外なく理解・説明できる。
    エゴのメリットとデメリットの両面を理解した上で、次のステップとしてデメリットを解決していくことが必要になるだろう。

    【“人種差別の言葉 ~ シンシャンション”の続きを読む】

    Erlang(アーラン)まとめ記事

    このエントリーを含むはてなブックマーク はてなブックマーク - Erlang(アーラン)まとめ記事 あとで読む
    Erlangの入門に最適なまとめ記事があった。

    これから15分でErlangを始めるための資料

    Erlangを学習するときの資料
    並列プログラマに 10 の質問 - Joe Armstrong さんの場合
    -Erlangの父



    Erlangを勉強するときは、目を通しておきたい。

    プログラミングErlangプログラミングErlang
    (2008/02/23)
    Joe Armstrong

    商品詳細を見る

    プロプライエタリ proprietary

    このエントリーを含むはてなブックマーク はてなブックマーク - プロプライエタリ proprietary あとで読む
    よく言い間違える言葉がある。

    誤) プロプエタリー、プロプタエリー

    正) プロプライエタリー

    プロプライエタリとは - はてなキーワード

    プロプライエタリ (proprietary) とは独占的な、専属的なという意味で、特にコンピュータ産業におけるアルゴリズム、手法、ソースコード等の再利用不可能性を指す。



    プロプライエタリ - @IT情報マネジメント用語事典

    プロプライエタリ proprietary

    開発者・開発企業などが製品やシステムの仕様や規格、構造、技術を独占的に保持し、情報を公開していないこと
    その情報独占者でなければ、開発・修正・改編・管理ができない状態となる。

    プロプライエタリ(proprietary)は「専用の」「独自の」「独占的な」「所有権・占有権のある」「非公開の」の意味で、コンピュータ関連用語としてはオープン(open)の対義語となる。



    オープンの反対=クローズド、プロプライエタリと。

    問題は、プロプライエタリを間違えないで言えるか?だ。
    試しに3音節に区切って覚えてみる。

    プロ・プライ・エタリ
    pro・pri・etary
    …なんか英語の発音として変なかんじがする。

    proprietary の意味とは - 英和辞典 Weblio辞書

    pro・pri・e・tar・y
    [PROPERTY の形容詞形]



    発音記号は、5音節に区切ってあった。

    プロ・プライ・エ・タ・リ

    まあ、覚えやすいなら、後3つはくっ付けて、

    プロ・プライ・エタリ

    でもいいか。

    プロ・プライ・エタリ
    プロ・プライ・エタリ
    プロ・プライ・エタリ
    プロ・プライ・エタリ
    プロ・プライ・エタリ

    プロパティー(名詞)の形容詞がプロプライエタリーなんだな。
    あんまり似てない。

    ソフトウェアライセンスの基礎知識ソフトウェアライセンスの基礎知識
    (2008/09/25)
    可知 豊

    商品詳細を見る

    Clojure - Javaで動くLisp

    このエントリーを含むはてなブックマーク はてなブックマーク - Clojure - Javaで動くLisp あとで読む
    Clojure(クロージャー)というプログラム言語があった。

    ●Javaで動く
    Clojureは、Java仮想マシン(JVM)上で動くLispのような言語ということらしい。
    JVMを利用しているという点で、以前取り上げたScalaと似ている。

    ●新しい言語
    まだ登場して間もない、ホットな言語とのこと。

    Clojure の検索結果 約 213,000 件

    Clojure (本家)
    http://clojure.org/

    紹介サイト
    プログラミング言語Clojureとは
    Clojure ‎(紫藤のWiki)‎
    JVM上新Lisp Clojureのこと, Scalaも

    ●Java vs .NET
    Java仮想マシン上で動く言語が、いろいろ作られている。

    Javaと似たような仕組みは、マイクロソフトも作った。
    .NETフレームワーク上で動くC#だ。

    .NETを利用できるプログラム言語は、C#以外にも、VB.NETやIronPythonなどもある。
    JVMを利用できるプログラム言語として、Java以外に、ScalaやClojureなどがある。

    Lispを勉強→Clojureで実装~Javaを動かせる環境があるなら、開発言語は他のものを選んでもOKと。

    ●ロゴがカッコイイ
    Clojureのロゴマークはセンスが良いと思う。

    Clojure

    ラムダ(λ)とタイチー(陰陽の二元を表わす太極図)を組合わせたアイコンになっている。

    太極

    なんかサーファーっぽいと思った。

    Programming ClojureProgramming Clojure
    (2009/06/05)
    S Holloway

    商品詳細を見る

    concrete5というCMS

    このエントリーを含むはてなブックマーク はてなブックマーク - concrete5というCMS あとで読む
    concrete5というCMSがあった。

    concrete5日本語公式サイト
    http://concrete5-japan.org/
    concrete5本家サイト(英語)
    http://www.concrete5.org/

    OpenPNEをCodeIgniterで再構築しているMyNETSのサイトを見ていたら、concrete5というCMSが紹介されていたと。

    PukiWiki以外で、サクサクとページを作れるCMSがあればと思い、concrete5をテストしてみる。

    将来的には、LMSに使えるCMSを自作することになると思う。

    CMS構築 成功の法則CMS構築 成功の法則
    (2007/03)
    生田 昌弘門別 諭

    商品詳細を見る


    【“concrete5というCMS”の続きを読む】

    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)
    五十嵐 淳

    商品詳細を見る

    OCamlで作られたhaXeというプログラム言語

    このエントリーを含むはてなブックマーク はてなブックマーク - OCamlで作られたhaXeというプログラム言語 あとで読む
    OCamlの本は、関数型言語の入門書として読んだら終わりだと思っていた。
    その後、LispやJavaScriptの本に戻る予定だったけど、意外な用途が見えてきた。
    もしかしたら、OCamlも出番があるかもしれない!?

    ●OCamlで作られたhaXeというプログラム言語
    haXeというプログラム言語があるらしい。

    はてなキーワード > haXe

    haXeへっくす(コンピュータ)
    ActionScript風の文法を持つプログラミング言語。単一の言語で、サーバーサイド(NekoVM、PHP)とクライアントサイド(JavaScript、Flash)のコードを生成できる。

    マルチパラダイムプログラミング言語で、強い静的型付け、型推論、クラス型、列挙型、多相型、クロージャーなどを持つ。

    処理系はOCamlで書かれ、GPL(ライブラリは2条項BSD)で公開されている。MTASCの後継に位置付けられており、Adobe製品以外で唯一、ActionScript3のバイトコードを生成できる。



    WEBアプリを作るとき、これ一つでサーバーサイドとクライアントサイドのプログラムが書けるらしい。

    ●haXe関連の日本語ページ
    haXeの読み方は「ヘックス」とか、「エックス」(フランス語風の読み)とからしい。

    日本の haXe ユーザのためのハブサイト
    http://haxe-users.jp/
    haXe 言語レファレンス
    http://haxe.org/ref?lang=jp
    八角研究所:haXe
    http://www.hakkaku.net/tag/haxe

    haXe 2.03 リリース - スラッシュドット・ジャパン

    haXeはActionScript風の文法を持つプログラミング言語で、SWF(Adobe Flash)形式、JavaScript形式、PHP形式などにコンパイルでき、ウェブアプリケーションのクライアントサイド・サーバサイド両方が作れるという特徴を持ちます。



    見た目がJavaScriptやActionScriptに似てるからといって惑わされてはいけません。かなり進化してると思います。

    - Javaでいうジェネリクスのようにクラスに型パラメータを付けられるので、安全な構造を作れるし、キャストが要らない。
    - クラス同士に構造的な部分型があって、暗黙的に扱ってくれる。(ダックタイピング的な事が安全にできる。)
    - enumの個々の要素にパラメーターを付けることが出来て、実質的にバリアントとして使える。
    - 動的にクラス名とかメソッド名とか持ってるので、リフレクションも可能。

    ちなみに、haXe自体はOCamlで作られているらしい。



    餅は餅屋に~WEBアプリを作るなら、PHP・JavaScript・ActionScriptを使い分ければ済む話だけど、haXeはそれらを統合したところに意味があるんだろうな。

    OCamlには、こんな使い方もあったということで。

    詳説 ActionScript 3.0詳説 ActionScript 3.0
    (2008/11/22)
    Colin Moock

    商品詳細を見る

    UbuntuにOCamlをインストール

    このエントリーを含むはてなブックマーク はてなブックマーク - UbuntuにOCamlをインストール あとで読む
    Ubuntu 8.04に、関数型プログラミング言語「OCaml」をインストールして使ってみる。

    ●OCamlのインストール方法
    インストール方法 - OCaml.jp

    Debian系(Debian,Ubuntuなど)のOSでは、aptitudeによってインストールが可能です。
     $ su
     # aptitude install ocaml



    GNOME端末を立ち上げて、
    sudo aptitude install ocaml
    とコマンドを入力してみた。
    (suの代わりにsudoでやってみた。)

    あっという間にインストール完了。とても簡単だった。

    ●インストールされたパッケージ
    「プログラミング in OCaml」の356ページには、この本の内容をテストするだけなら、
    ocaml
    tcl8.4-dev
    tk-8.4-dev
    ocaml-mode
    の4つのパッケージがインストールされていればOKとあった。

    見たところ、
    ocaml
    tcl8.4
    tk-8.4
    は含まれていたが、
    ocaml-mode
    はデフォルトの詰合せセットには含まれていないようだった。
    まあ、EmacsでOCamlを操作するわけじゃなければ、ocaml-modeはなくてもOK。

    Ubuntuで用意されているOCamlパッケージの案内ページ
    http://packages.ubuntu.com/search?keywords=ocaml
    Ubuntu 8.04(コードネーム hardy)のOCamlはこれかな?
    Ubuntu -- hardy の ocaml パッケージに関する詳細

    ●Ocaml Browserの起動
    GNOME端末で、
    「ocamlbrowser」
    と入力すると、OCaml Browserが起動した。

    OCamlBrowserは、LablTkライブラリを使ってOCamlで書かれた、ライブラリ関数ブラウザ兼エディタ兼コンパイラシェルです。
    Tcl/Tkがインストールされていれば、Linuxであればocamlbrowserというコマンドで起動できます。



    OCamlBrowser

    「File」→「Shell」からOCamlのシェル(対話式コンパイラ画面)が開く。
    ここにOCamlのプログラムを書けば、動作をテストできる。
    試しに1 + 1 = 2の計算をやってみる。

    # 1 + 1;;
    - : int = 2



    おお!ちゃんと動いた!!!(笑)
    この感動を忘れちゃいけない。

    これで一応、OCamlのテスト環境が用意できた。
    UbuntuにOCamlをインストールするのは、とても簡単だった。

    ●MacOSXにOCamlをインストールする方法
    「プログラミング in OCaml」には、WindowsとLinuxにOCamlをインストールする方法が紹介されていたが、Macはハブられていた。

    OCamlをMacOSXにインストールする方法が紹介されていた。
    OCamlなど - yaakaito::Blog

    $ sudo port install ocaml
    MacPortsで入れました。


    MacPortsで、簡単にOCamlをインストールできるようだ。

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

    商品詳細を見る

    FC2Ad