2010年2月15日のブックマーク (8件)

  • [PDF]Proofs are Programs: 19th Century Logic and 21st Century Computing

  • WEBrickを使うためのメモ - 再帰の反復blog

    WEBrickは、HTTPサーバを簡単に作ることができるライブラリらしい。 しかし「じゃあ簡単に作ってみよう」と思ってRubyのマニュアルのWEBrickの部分を見ても、まったく要領を得ないので、使うためのメモを書いておく。 HTTPServer 簡単なHTTPサーバ サーバがおこなう仕事を設定する (+ FileHandlerの使用例) マウントで仕事を分ける (+ CGIHandlerの使用例) テスト用Webサーバとして使う 自前のサーブレット(ハンドラー)を定義する GenericServer HTTPProxyServer HTTPServer まず標準リファンレンスは次 Rubyリファレンスマニュアル library webrick/httpserver 簡単なHTTPサーバ とりあえずぜんぜん役に立たないHTTPサーバを作ってみる。 HTTPサーバの仕事は、クライアントからの

    WEBrickを使うためのメモ - 再帰の反復blog
  • call/ccと古典論理のカリー・ハワード対応 - 再帰の反復blog

    「直観主義論理のカリー・ハワード対応」の続き。 call/ccと継続 call/ccというのは、gotoを強力にしたものだと思っておけば良い。ただしScheme以外のプログラミング言語では、あまり見かけない機能。 例えばブロック構造から抜け出すための命令がある言語を考える。どのブロックから抜け出すかはラベルで指定する。またラベルはギリシャ文字で表すことにする。とりあえず次のような感じになるだろう。jumpの部分を実行するとブロックから抜け出す。 :α{ ... ... jump α; ... // ここは実行されない }でも、ブロック自体が値を持っている(値を返す)ようにした方が汎用的になる。例えば、次のプログラムはflagが真ならxに1が代入され、偽なら2が代入される。 x = :α{ ... ... if (flag) { jump α 1; } ... 2; }値を返すにしても返さな

  • Lambda-mu calculus - Wikipedia

    tanimina
    tanimina 2010/02/15
    λμ計算。古典論理に対応するラムダ計算
  • CiteSeerX

    About CiteSeerX is an evolving scientific literature digital library and search engine. @2007-2026 The Pennsylvania State University

    tanimina
    tanimina 2010/02/15
    ラムダ計算にcall/ccを追加すると古典論理に対応する
  • d.y.d. 文字コード&ベイズ推定

    12:21 06/05/28 うたひめ 先日の記事に書いたように KOKIA にハマりまして、 とりあえず片っ端から聴いてみることにしました。まずは 1st アルバムの 『songbird』 から … …4曲目の "白い雪" ヤバい。超ヤバい。なんだこれ。ツボすぎる。 ベスト盤を聴いたとき感じた揺らぎなく落ち着いた歌唱力的な曲を期待して聴きはじめたら、 予想外の声質の歌が飛び込んできてびっくりしました。もちろん抜群に巧いのに かわりはないんですが、ずっと儚げな、ガラス細工みたいなイメージの、ああ、その、 つまり白い雪みたいな雰囲気の綺麗な声で。その声と奇跡的にマッチしたメロディ。 すごいなあ。9曲目の "ありがとう…" もベスト盤でのリテイクと比べて同じ印象で、 Amazonのreview で TenderBerry さんという方が近いことを書いておられました。 しかし書いてて自分の語彙の

    tanimina
    tanimina 2010/02/15
    カリーハワード同型対応
  • 2008-04-17

    callcc と shift/reset についてわかるとこだけ書いてみます。 継続 callcc という操作は、現在から実行終了まで、継続をまるごと取り出します。例題。 p [1] + callcc {|k| [2] + k.call([3]) } #=> [1, 3] callcc では callcc がリターンしてから実行終了するまでの継続 k が取り出せます。k.call([3]) で継続が呼ばれると、いきなり「callcc が [3] を返した瞬間」に実行が飛びます。つまりこんな感じ。 p [1] + [3] あとは自明ですね。"[2] +" のあたりは無視されます。 部分継続 shift という操作は、現在から reset まで、継続の一部だけを取り出します。この継続の一部を部分継続といいます。例題。 p [1] + reset { [2] + shift {|k| [3] +

    2008-04-17
  • 部分継続について本気出して考えてみた - (new Hatena).blog()

    以前何度か部分継続について書いたことがあるんですが、当時は表面的な振る舞いを観察して何となく分かった気になった程度の拙い説明しか出来ませんでした。 その上、最近のプログラミングでもほとんど活用しておらず、改めて理解し直す必要を感じてきた次第です。 そこで今回は、部分継続の概念的な理解を目指し、基礎的な事柄を中心にまとめていきたいと思います。 基的に PLT Scheme (MzScheme) の評価モデルに即して書いていくため、Scheme 一般に当てはまる話になっていない部分もあるかも知れません。その点ご了承ください。 Redex と継続 Scheme の評価モデルにおいて、 (+ 1 (+ 2 0))という式を評価するとき、まず (+ 2 0)の部分が評価され、その結果の値に対して (+ 1 [])という残りの計算が行われます。 ここで角括弧で示した部分を reducible exp

    部分継続について本気出して考えてみた - (new Hatena).blog()