Martin-Lofの 理論とそのパラドックス - あいまいな本日の私 blog
Martin-Lofの1971年の論文では、循環性がその中核を占めています。彼は、この条件があるので、彼の理論は圏論と非常に相性が良い（ご存知のように、圏論では、圏全体は圏をなし、その意味で強い循環性を持ちます）と主張しています。しかし、翌年に、Girardがこの中核部分の（もしくは現代の書き方では Type: type）からパラドックス（ブラリ-フォルティのパラドックスの一般化）が導けることを証明し、彼の夢は消えました。現在では、循環的部分を削除した、厳格な可述性に基づく依存型理論（おそらく整合的だろうと思われるもの）が、Martin-Lofの体系ということになっています。 さて、Girardのパラドックスですが、文献は Girardの論文は仏文？だったはずなので、Thierry Coquandの An Analysis of Girard's Paradox (LICS 1986)をど
The Never Ending Programming Language - Hello, world! - s21g
身の回りに溢れているほとんど全てのプログラムは、 静止状態の表現としてソースコードを持ち、 計算機上で実行され、そして終了します。 少なくとも、終了しようと思えばできるように作られています。 しかしながら、近年では、Webサーバやネットワークプログラムのように、 継続的に動作することが当たり前で、停止状態に移行する事自体が 例外とされるようなプログラムが珍しくなくなってきています。 RubyやPerl, Pythonなどの動的言語と呼ばれる言語が普及し、 プログラム言語の価値は、実行速度から開発速度で測られる 比率が高くなりました。 そんな中、去年ぐらいから、静的言語でも動的言語でもない、 新しいプログラミング言語のパラダイムの可能性について考えています。 走り続けるプログラム はてしない物語。終了状態の無いプログラム。 停止することなく、動き続けることが想定されるService型プログラ
Matzにっき(2007-04-14)-Notes on Haskell: Fight the next battle
<< 2007/04/ 1 1. エープリルフール 2. [Ruby] オブジェクト指向機能を取り除いた Ruby-- が登場!? 2 1. [教会] セミナリー１日目 2. LMLML 3. [Ruby] 最速配信研究会 - なんだかいろいろ申し訳ない気分になった話 4. [Ruby] Headius: ActiveRecord 100%, Performance Doubling, Java Support Improving 3 1. [Ruby] Bitwise Magazine:: What's Right With Ruby? 2. [OSS] オープンソースソフトウエアがビジネスの成長を加速 3. Passion For The Future: なぜ株式投資はもうからないのか 4 1. [Ruby] Rails 1.2と1.1、速いのはどっち? - Railsbenchによる
ホワット・ア・ワンダフル・ワールド SQL とか全然知らないんですが
一応ルール型言語の研究者のはしくれとして違和感を感じたので． SQLに対する接し方 SQLは言語としては構造化以前のBASICレベルなので、複雑な事をさせたくない。1つのクエリが数十行あると、読みたくない。といって関数分けもできない。 ということで、複雑な処理は高機能な汎用言語上でやる。 SQL ってよー知らんのだけど，あれってまんま Prolog とちゃうん ? クエリの最適化かとも，Prolog プログラマならば誰でも無意識のうちにやってることだと思うしなぁ．なるべくバックトラックを減らすために，一気に探索範囲が絞られる順番にアトム (クエリ) を並べるとか． 逆に言うと，そういう下部の制御 (How) を意識しないといけないってのが，Prolog の (宣言型 (What) 言語としての) 致命的な欠点なんだけど．Java なんかに比べたら，はるかに高級な言語のような気が． まぁ，文
Matzにっき(2006-10-04) - 『現代という時代は、どのようなプログラミングを求めているのか？
<< 2006/10/ 1 1. [教会] お休み 2. 実家 2 1. U-20プロコン表彰式 2. インタビュー 3. Job Trends: ruby programmer 3 1. インタビュー 2. [OSS] OSS コンサル会社が設立 3. [Ruby] Rubyの生産性の高さはどこまで本当か? 4. [Ruby] block parameter to be local variables 5. ジョブズ氏のいないアップルが来る日--IT企業が直面する「後継者選び」 4 1. 即興トーク 2. [OSS] ソフトエイジェンシー、MySQL 開発者が直接サポートするサービスを開始 3. [OSS] Seasarは鶏か卵か? - ひが氏、キャズム越え柔道ストラテジ語る 4. 『現代という時代は、どのようなプログラミングを求めているのか？ 5 1. [Ruby] Ruby on R
極小プログラミング言語とホーア論理 - 檜山正幸のキマイラ飼育記 (はてなBlog)
一昨日定義した極小プログラミング言語を、TTPL（Tiny Toy Programming Language）というツマンネー名前で呼ぶことにします。 んでまー、TTPLをああいう仕様にしたのは、ホーア論理を直接的に使いたい、という理由があります。つうわけで、ホーア論理をTTPLを使って説明します。ただし、最初に言っておきますが、僕は（ホーア論理のような）プログラム証明を推奨する気はありません（どっちかいうと反対派）。それでも、理屈は知っておかないと、それから先に進めないってことはあります。 内容： ホーア式 ホーア式の正しさ プログラムの証明 こんなにめんどくさい なにが重要か ●ホーア式 ホーア論理の式（ホーア式とか、ホーア・トリプルと呼ばれる）は、プログラムの文と仕様記述を一緒にしたようなものです。p, qが論理式（条件）でSが文だとして、p{S}q という形で書きます。中括弧の使い
プログラミング言語や数式はバイダイレクショナルなのだ - 檜山正幸のキマイラ飼育記 (はてなBlog)
もうモナドの話題じゃないです。けど、少し引きずってますね； モナド関連で、「左から右」と「右から左」に触れたんですけど、そのことについてです。 ヘブライ語やアラビア語の書字方向（scriptingのdirection）は、右から左に向かう横書きということです。でも、"2006"という年号や"Isac Newton"なんて人名（外国人名になります）は左から右となるので、一行のなかに「右から左」と「左から右」が混じることになります。こんな書き方をバイダイレクショナル（bidirectional）、略してバイダイと形容します。 ヘブライ／アラビア語はたいへんだなー、と思うのだけど、プログラミング言語や数式も実はバイダイなんですよね。例えば、foo(a, b); bar(x);を考えてみると： 呼び出しの時間順は、foo(a, b);→bar(x); だから「左から右」でいいですね。しかし、引数を
OBB vs AABB - Radium Software Development
iPhoneの一般修理店は予約なしでも来店できる？ 基本的には飛び込みで修理に行ってもOK iPhoneを置いていたソファにうっかりと腰かけてしまい、パネルを割ってしまった、こんな時はスマホの一般修理店へ行きましょう。画面割れは、スマホやタブレットの故障原因として非常に多いものです。予約なしで突然お店に行っても平気かしらと、不安に思う方々もいらっしゃるかもしれません。結論としては特に問題はなく、予約なしで訪問しても画面割れの修理はお願いできます。 ただし他のサービス業のお店同様、予約なしの場合、お店が混雑していると順番待ちをしなければいけないです。特に繁盛しているスマホ修理のお店だと、行列が店内で出来ており、予約なしだと、自分の順番が巡ってくるまで長時間待たされる可能性があります。平日の朝、昼なら利用客が少ない場合が多く、飛び込みでも比較スムーズに修理が頼めます。 予約は入れた方が時短に、
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
