メールフォーム
rpfの日々の気づき 2006年08月
プロフィール

r.p.f

Author:r.p.f
もの作り、電子工作、コンピュータ一般のページ

何かを作る事が好きなコンピュータおたくです。

もの作りやコンピュータなどで日々の気づきを書いて行こうと思っています。

NeXTSTEP派からMacOSX派へ改宗

最近の記事
最近のコメント
最近のトラックバック
月別アーカイブ
カテゴリー
カレンダー
07 | 2006/08 | 09
- - 1 2 3 4 5
6 7 8 9 10 11 12
13 14 15 16 17 18 19
20 21 22 23 24 25 26
27 28 29 30 31 - -
ブロとも申請フォーム

この人とブロともになる


スポンサーサイト

...--/--/-- --:--...

上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。



スポンサー広告 | TRACKBACK(-) | COMMENT(-) |



Locally Cartesian Closed Category

...2006/08/23 23:14...

Structual Proof Thery と Martin-Lof Type Theory は 密接に結びつく。このことが、Natural Deduction の正規化の過程と Typed Lambda Calculus における beta reduction との Structual なアナロジーとなるのか。Typed Lambda Calculus は、Cartesian Closed Category でモデル化できる。ならば、Martin-Lof Type Theory も Cartesian Closed Category でモデル化できのかなと思った。そこでちょっと Wikipedia を調べてみた。どうも Seely が locally cartesian closed category という概念を導入して Martin-Lof type theory をモデル化しているそう。Seely は、*autonomous category を使って Linear Logic のモデル化もしている。凄い人なんだなあ。

スポンサーサイト




Martin Lof Type Theory

...2006/08/22 23:55...

ML などと戯れていると必ず Martin-Lof の Type Theory というのが出てくる。こう言われると、それ以外の Type Theory ってあるのとか、そもそも Martin-Lof の Type Theory ってどういうものという疑問が素朴に湧いてくる。(B.Russel が所謂ラッセルのパラドックスの解決のために Type Theory を使ったと聞いたことはあるけど厳密なものはみたことがないし知らない。)たまたま良い本を見つけた。

Programming in Martin-Lof Type Theory
Cambiridge University Press

という本。Constructive Mathematics で何かの分類に(なんの分類かはよくわからないが)Type Theory が使われていたそう。当然のことながら集合の言葉で書かれている。これを Curry-Howard 対応で Proposition を Type と考え、Type が Set であるから Set を Poroposition と見なして logic の言葉で構築し直したのが Martin-Lof の仕事。最終的に Dependent Type を伴って1階の命題論理で体系化している。(途中いろいろある。)Polymorpic Set というのがあってこれが Polymorphic Type になるようだ。論理で体系化されたのでコンピュータの上に載せて計算できるようになるから使えるようになった素晴らしいということになるわけか。Unification を使えばよいのかなと思っていると実際には Well-ordering の概念を使って term rewrite よろしく計算する(所謂 Milner の W algorism)。論理をちゃんと勉強する意欲が湧く。





WWDC2006

...2006/08/08 22:02...

昨晩、みることができなかったので今見ながら記載。
昼間、ニュースをみていて Leopard についてはほとんど情報が開示されていないのでがっかり。
しかし、Xeon の搭載を今見てびっくり。128bit Vector Engine を積んでいるとある。
SPECfp で 1.6 倍と言っている。確か G5 Quad で 70Gflops に達するのではなかったのか?
これが Vector Engine を使った結果なのかどうなのかは不明。
事前に情報が流れていた DVD スロットが2つというのはあっていた。
私はこの Vector Engine に興味津々。










CALENDER
07 ⇔ 2006/08 ⇔ 09
Sun Mon Tue Wed Thu Fri Sat
- - 1 2 3 4 5
6 7 8 9 10 11 12
13 14 15 16 17 18 19
20 21 22 23 24 25 26
27 28 29 30 31 - -
ブログ内検索
RSSフィード
リンク
このブログをリンクに追加する
メールフォーム

名前:
メール:
件名:
本文:





MonotaRO (モノタロウ)【法人向けストア】







上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。