Yコンビネータとゲーデルの不完全性定理 - (iwi)の日記
大学 | 00:36大学で論理学のテストがありました。そこで、ゲーデルの不完全性定理を勉強したのですが、ゲーデル文 A[y] = ∃w (Substx[y, y, w] ∧ (∃ p. Proof[w, p, 0]))として、A[x] の符号を z として G = A[num(z)]とYコンビネータ Y = λf·(λx·f (x x)) (λx·f (x x))って似てるなーって思いました。どこが似てるかっていうと、「そいつに自身を適用」みたいなことがどっちも2回出てくるところ。ゲーデル文は外側で「A[num(z)]」ってやって1回目で、その中でさらに 「Substx[y, y, w]」 ってやって2回目。Yコンビネータは外側で 「(λx·f (x x)) (λx·f (x x))」 ってやって1回目で、内側で「x x」ってやって2回目。自分の名前を使わずに自分を得たいという目的からして
Project LambdaCan---Lambda Calculus in a Can
You can get soup in a can. You can get bread in a can (*). Now the long wait is over! You can finally get Lambda Calculus in a can. Project LambdaCan is an amusing exercise in absurdity. It implements a reducer (interpreter) for the Lambda Calculus, a formal system (programming language) developed by Alonzo Church in the 1930's to attack the deepest mathematical problem of the day. This was the En
π計算を復習 - ラシウラ
昨日のゼミで紹介してもらったけど、bisimulationで逆にわからなくなってしまったので自習。 http://en.wikipedia.org/wiki/Pi-calculus まず、構文 小文字: チャネル、変数(プロセスもあり) 大文字: メタ変数(プロセス式だが、実際の式表現中には出ない) 0: nilプロセス(以降、何も影響しない) P | Q: プロセスを並行動作させるプロセス c(x).P: チャネルcに受信待ち、メッセージはxとしてbind、その後P実行するプロセス c.P: チャネルcにxを送信、その後Pを実行するプロセス (new x)P: チャネルxを作成し、bindしたプロセス !P: Pを無限に複製し並行実行させるプロセス たとえば、キューに、無限にイベントを発行したり、受け付けたりとか 例題: (new x)(x.0 | x(y).y.x(y).0) | z(
3分で解るHaskellのArrowの基本メモ - よくわかりません
日本語でArrowの説明があまり見付からなかったので、Haskell/Understanding arrows - Wikibooks, open books for an open worldを読んで理解したつもりのメモ。オリジナルの図を見ながらだと分かりやすいかも。誤り・間違いなど、乞うご指摘。 b->cな関数をArrowなるからくり箱に入れると、 (Arrow a) => a b c こんな型になる。型パラメタが、引数のbと返値のcのふたつ。 Monadは、値をからくり箱に入れたもの。からくり箱は基本的に(ヘンな)値。 Arrowは、関数をからくり箱に入れたもの。からくり箱は基本的に(ヘンな)関数。 arr :: (b -> c) -> a b c Monadでは、値をからくり箱に入れる関数returnがある。 Arrowでは、関数をからくり箱に入れる関数arrがある。 (>>>)
新言語考えた - まめめも
テーマは befunge + π計算。 ちなみにπ計算の知識は sumii 様のπ-calculus 超入門を読んだだけしかない。 以下、befunge はみな知っているものとしています。 基本部分 実行モデルは基本的には befunge で、2 次元上のコードをカーソルが走って fetch しながら実行が進む。初期状態では左上の原点から右方向に向かって走るプロセスが 1 本だけ。各プロセスは数値またはチャンネルからなるスタック (っぽいもの) を持っている。 '|' は fork 。進行方向に対して左右に分かれて走り出す。 v > AAA > | > BBB上のコードでは、 AAA と BBB を並列実行する。fork したらスタックは全部コピーされる (fork した後でスタックをいじっても、相方のスタックは変化しない) 。 '&' はチャンネルを生成してスタックに乗せる。'!' は送
To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction
To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction David C Keenan, 27-Aug-1996 last updated 10-May-2001 116 Bowman Parade, Bardon QLD 4065, Australia http://users.bigpond.net.au/d.keenan Abstract The lambda calculus, and the closely related theory of combinators, are important in the foundations of mathematics, logic and computer science. This
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Yahoo! Groups
http://www.city5.org/AlligatorEggs.html