[B! ラムダ計算] ohnishiakiraのブックマーク

計算モデルと論理とゲーデルの不完全性定理 - Gemmaの日記

ゲーデルの不完全性定理は、数学を扱う数学、つまりメタ数学を考えるが、それだと理解が難しい。しかし、証明(数学)＝プログラムという悟りを開くと、プログラムを扱うプログラム、つまりメタプログラムを考えればよくなり、それならコンパイラ等でなじみがあるので理解が優しくなる。話の流れは以下。 1. プログラムとは何か 2. 証明とは何か 3. 証明＝プログラム , （　　 {、　{　　ヽ.ｰ､､＼､__ぃ._ゝ⌒ヾ iヾ）}､_ ﾝ_ｰ-_二ｰ-, 〉 {厶 _､ヽ　　　　　　　　　　　 _ ヽ._＞'´ ／ /,ィ／　/　ハYﾍい　　　　　　 ,.　-- 〃⌒ r−-､　　　　　　ィ´　〃 ,ｲ/7'　 ,ｲイ/　小ヽ丶、　,. ‐ '´ﾊ i 　 ″｀ヽ、、ヽ、　　　　　／幺ィ　 {从{小込v' jｩ仏厶川ﾘ}　 YV,　　小 Vj.　|丶　ヽ｀ｰ-ミー--'_,辷三彡

ohnishiakira 2010/02/20

リンク

ラムダ計算 λ...

► 2022 (2) ► 10月 (1) ► 2月 (1) ► 2021 (51) ► 11月 (2) ► 10月 (2) ► 9月 (4) ► 8月 (4) ► 7月 (4) ► 6月 (4) ► 5月 (3) ► 4月 (10) ► 3月 (7) ► 2月 (4) ► 1月 (7) ► 2020 (155) ► 12月 (7) ► 11月 (10) ► 10月 (8) ► 9月 (8) ► 8月 (11) ► 7月 (21) ► 6月 (19) ► 5月 (14) ► 4月 (20) ► 3月 (13) ► 2月 (10) ► 1月 (14) ► 2019 (293) ► 12月 (11) ► 11月 (12) ► 10月 (24) ► 9月 (29) ► 8月 (27) ► 7月 (36) ► 6月 (40) ► 5月 (24) ► 4月 (35) ► 3月 (42) ► 2月 (6

ohnishiakira 2010/02/17

リンク

ラムダ計算基礎文法最速マスター - 貳佰伍拾陸夜日記

ラムダ計算は, 多くのプログラミング言語, とくに関数型言語の原形になっています. ラムダ計算について理解しておくことは, 多くのプログラミング言語の習得に役立つでしょう. ラムダ計算はチューリング完全で, 計算能力としてはふつうのプログラミング言語と同じです. ラムダ計算で計算を書く訓練をしておくことは, 任意の計算を関数のみを使って(他の制御構文を用いずに)書くときに役立ちます. ふつうに書いたら煩雑な処理を, 関数型言語のやり方で書くとすっきりすることが多々あり, コードを自由自在に書くためには必須の考え方と言えるでしょう. 項ラムダ計算の式を項(term)と言います. 項は変数, 抽象, 適用のいずれかです. 変数変数(variable)はふつう1文字で書きます. 変数には関数内の束縛変数(bound variable)か自由変数(free variable)かという区別があり

ohnishiakira 2010/02/08

ラムダ計算

リンク

ラムダ計算とチューリングマシンの違い 2009-04-13 - きしだのはてな

ぼくもYコンビネータがわかるようになるまではそうだったのだけど、Yコンビネータを使うとどのような処理ができるのかがよくわからなくて悩んでいる人が多いように思う。他の人のブログを見ても、名前をつけずに再帰ができるのがすばらしいとか書いてあったりするのだけど、それによってどういう処理ができるのかわからずにいた。結論をいえばYコンビネータには、なにかの処理を便利にする能力はない。関数であらゆる計算ができるということが示せれば、あとは用なしだ。理論の礎としてうまってしまえばいい。結局、Yコンビネータによってどのような処理ができるかというのは、ラムダ計算の要素のメリットをチューリングマシンの中に見出そうとしてるといえる。ラムダ計算とチューリングマシンは、どちらも計算モデルという点では一致しているけど、全く違う。無限であるか有限かの違いといってもいい。チューリングマシンでは、データの量と処理

ohnishiakira 2009/04/14

リンク

紙芝居：ラムダ抽象 - 檜山正幸のキマイラ飼育記 (はてなBlog)

石井君*1が、2月19日セミナーのツイン・ホワイトボードを撮影してくれていたので、ハイライト(?)部分を紙芝居にしました。紙と鉛筆の準備はいいかな -- では、はじまりはじまり。 g = <a, b, x| a*x + b> という関数があるとき、これを2回“ラムダ抽象”してみます。ラムダ抽象とは、右肩ハット（^）または大文字ラムダ（Λ）で表されるオペレータです。ラムダ抽象とカリー化は同義語です*2。ラムダ抽象すると、n引数関数は(n-1)引数関数に変化し、その代わり戻り値が関数型になります。ただし、ここで言う「関数型」は数学的な関数の型ではなくて、とある実行エンジンEで実行する関数コードのデータ型のことです。 gの2回ラムダ抽象g^^を絵に描くとこうです。 gの1回ラムダ抽象 g^ = Λg と、gの2回ラムダ抽象 g^^ = Λ(Λg) を計算してみます。Λの計算規則*3を使えば、こ