计算の概念
0 likes419 views
数学において「计算」という概念はどのように定式化されるかについての绍介です．题材としてラムダ计算を取り上げています．
![自己紹介
计算の概念
関連分野
まとめ
计算とは？
ラムダ計算
他のモデル
計算可能性に関する結果
ラムダ計算
定義 (β 簡約)
2 つのラムダ項の間の関係 →β を次で定める
(λx.M)N →β M[x := N]
※ M 中の x を N で置き換える
齊藤 信臣 计算とは](https://image.slidesharecdn.com/conceptofcomp-181029225948/85/-9-320.jpg)
![自己紹介
计算の概念
関連分野
まとめ
计算とは？
ラムダ計算
他のモデル
計算可能性に関する結果
ラムダ計算
定義 (β 簡約)
2 つのラムダ項の間の関係 →β を次で定める
(λx.M)N →β M[x := N]
※ M 中の x を N で置き換える
β 簡約は，ラムダ計算における「計算」操作
齊藤 信臣 计算とは](https://image.slidesharecdn.com/conceptofcomp-181029225948/85/-10-320.jpg)
![自己紹介
计算の概念
関連分野
まとめ
计算とは？
ラムダ計算
他のモデル
計算可能性に関する結果
ラムダ計算
定義 (β 簡約)
2 つのラムダ項の間の関係 →β を次で定める
(λx.M)N →β M[x := N]
※ M 中の x を N で置き換える
β 簡約は，ラムダ計算における「計算」操作
e.g.,
(λx.x)y →β y
齊藤 信臣 计算とは](https://image.slidesharecdn.com/conceptofcomp-181029225948/85/-11-320.jpg)
![自己紹介
计算の概念
関連分野
まとめ
计算とは？
ラムダ計算
他のモデル
計算可能性に関する結果
ラムダ計算
定義 (β 簡約)
2 つのラムダ項の間の関係 →β を次で定める
(λx.M)N →β M[x := N]
※ M 中の x を N で置き換える
β 簡約は，ラムダ計算における「計算」操作
e.g.,
(λx.x)y →β y
(λy.yz)(λy.yz) →β (λy.yz)z →β zz
齊藤 信臣 计算とは](https://image.slidesharecdn.com/conceptofcomp-181029225948/85/-12-320.jpg)
![自己紹介
计算の概念
関連分野
まとめ
计算とは？
ラムダ計算
他のモデル
計算可能性に関する結果
ラムダ計算
定義 (β 簡約)
2 つのラムダ項の間の関係 →β を次で定める
(λx.M)N →β M[x := N]
※ M 中の x を N で置き換える
β 簡約は，ラムダ計算における「計算」操作
e.g.,
(λx.x)y →β y
(λy.yz)(λy.yz) →β (λy.yz)z →β zz
(λx.xx)(λx.xx) →β (λx.xx)(λx.xx) →β ...
齊藤 信臣 计算とは](https://image.slidesharecdn.com/conceptofcomp-181029225948/85/-13-320.jpg)
![自己紹介
计算の概念
関連分野
まとめ
计算とは？
ラムダ計算
他のモデル
計算可能性に関する結果
ラムダ計算
定義 (β 簡約)
2 つのラムダ項の間の関係 →β を次で定める
(λx.M)N →β M[x := N]
※ M 中の x を N で置き換える
β 簡約は，ラムダ計算における「計算」操作
e.g.,
(λx.x)y →β y
(λy.yz)(λy.yz) →β (λy.yz)z →β zz
(λx.xx)(λx.xx) →β (λx.xx)(λx.xx) →β ...
λx.M は「関数」を表している: λx.M ≈ f(x) = M[x]
齊藤 信臣 计算とは](https://image.slidesharecdn.com/conceptofcomp-181029225948/85/-14-320.jpg)
![自己紹介
计算の概念
関連分野
まとめ
まとめ
まとめ
「計算」の数学的モデル
機械的な有限の手続き
計算で解ける問題/解けない問題がある
プログラムの停止性判定
ヒルベルトの第 10 問題
ラムダ計算
関数概念を抽象化したような，記号列の書き換え体系
β 簡約が計算操作: (λx.M)N →β M[x := N]
Turing 機械，帰納的関数といったモデルも存在する
→ これらが表現する関数クラスは一致
齊藤 信臣 计算とは](https://image.slidesharecdn.com/conceptofcomp-181029225948/85/-31-320.jpg)
计算の概念
- 1. 自己紹介 计算の概念 関連分野 まとめ 计算とは 齊藤 信臣 情報理工学研究科 数理?計算科学専攻 鹿島研究室 2014/07/02 (水) 齊藤 信臣 计算とは
- 2. 自己紹介 计算の概念 関連分野 まとめ 自己紹介 自己紹介 齊藤 信臣 (さいとう のぶたか) 修士 2 年 情報科学科 → 数理?計算科学専攻 鹿島研究室 専門は数理論理学 齊藤 信臣 计算とは
- 3. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 今日の話 1 自己紹介 自己紹介 2 计算の概念 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 3 関連分野 計算にまつわる分野 4 まとめ まとめ 「計算」とは何かについて，理学部らしく数学的に捉えてみま しょう！ 齊藤 信臣 计算とは
- 5. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 计算とは？ なんとなく「計算」のイメージはある ものを数える，四則演算など 紙とペンで式を変形していく コンピュータでプログラムを動かす 実は厳密な 数学的モデル が存在する 20 世紀初頭くらいから研究され始めた 機械的に実行可能な有限の手続き 「計算」によって 解ける問題/解けない問題 の区別 齊藤 信臣 计算とは
- 6. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 ラムダ计算とは？ 計算のモデルの 1 つ 定義はすごくシンプル！ 記号列とその書き換え 関数の概念を抽象化した体系 ※「ラムダ」はギリシャ文字の λ 齊藤 信臣 计算とは
- 7. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 まずラムダ計算の基本， ラムダ項 と β 簡約 を定義する 定義 (ラムダ項) 1 変数 x, y, z, ... はラムダ項 2 M と N がラムダ項のとき，(MN) はラムダ項 3 x が変数，M がラムダ項のとき，(λx.M) はラムダ項 ※こういう定義を「帰納的定義」という 齊藤 信臣 计算とは
- 8. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 まずラムダ計算の基本， ラムダ項 と β 簡約 を定義する 定義 (ラムダ項) 1 変数 x, y, z, ... はラムダ項 2 M と N がラムダ項のとき，(MN) はラムダ項 3 x が変数，M がラムダ項のとき，(λx.M) はラムダ項 ※こういう定義を「帰納的定義」という e.g., xy λx.x (λx.x)y ((λx.x)y)(λz.(xy)z) 齊藤 信臣 计算とは
- 9. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 定義 (β 簡約) 2 つのラムダ項の間の関係 →β を次で定める (λx.M)N →β M[x := N] ※ M 中の x を N で置き換える 齊藤 信臣 计算とは
- 10. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 定義 (β 簡約) 2 つのラムダ項の間の関係 →β を次で定める (λx.M)N →β M[x := N] ※ M 中の x を N で置き換える β 簡約は，ラムダ計算における「計算」操作 齊藤 信臣 计算とは
- 11. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 定義 (β 簡約) 2 つのラムダ項の間の関係 →β を次で定める (λx.M)N →β M[x := N] ※ M 中の x を N で置き換える β 簡約は，ラムダ計算における「計算」操作 e.g., (λx.x)y →β y 齊藤 信臣 计算とは
- 12. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 定義 (β 簡約) 2 つのラムダ項の間の関係 →β を次で定める (λx.M)N →β M[x := N] ※ M 中の x を N で置き換える β 簡約は，ラムダ計算における「計算」操作 e.g., (λx.x)y →β y (λy.yz)(λy.yz) →β (λy.yz)z →β zz 齊藤 信臣 计算とは
- 13. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 定義 (β 簡約) 2 つのラムダ項の間の関係 →β を次で定める (λx.M)N →β M[x := N] ※ M 中の x を N で置き換える β 簡約は，ラムダ計算における「計算」操作 e.g., (λx.x)y →β y (λy.yz)(λy.yz) →β (λy.yz)z →β zz (λx.xx)(λx.xx) →β (λx.xx)(λx.xx) →β ... 齊藤 信臣 计算とは
- 14. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 定義 (β 簡約) 2 つのラムダ項の間の関係 →β を次で定める (λx.M)N →β M[x := N] ※ M 中の x を N で置き換える β 簡約は，ラムダ計算における「計算」操作 e.g., (λx.x)y →β y (λy.yz)(λy.yz) →β (λy.yz)z →β zz (λx.xx)(λx.xx) →β (λx.xx)(λx.xx) →β ... λx.M は「関数」を表している: λx.M ≈ f(x) = M[x] 齊藤 信臣 计算とは
- 16. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 ラムダ計算で自然数と，自然数上の演算を表現する 定義 (自然数を表すラムダ項) 自然数 n を表すラムダ項 Cn を次で定める Cn Def. = λfx. n times f(f(...(f x)...)) 齊藤 信臣 计算とは
- 17. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 ラムダ計算で自然数と，自然数上の演算を表現する 定義 (自然数を表すラムダ項) 自然数 n を表すラムダ項 Cn を次で定める Cn Def. = λfx. n times f(f(...(f x)...)) 0 ≈ λfx.x 1 ≈ λfx.fx 2 ≈ λfx.f(fx) 3 ≈ λfx.f(f(fx)) ... 齊藤 信臣 计算とは
- 18. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 定義 (自然数の足し算を表すラムダ項) 足し算を表すラムダ項 Add を次で定める Add Def. = λxyuv.xu(yuv) 齊藤 信臣 计算とは
- 19. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 ラムダ計算 定義 (自然数の足し算を表すラムダ項) 足し算を表すラムダ項 Add を次で定める Add Def. = λxyuv.xu(yuv) *注意* λ のついた変数名を書き換えただけのラムダ項同士は同一 視する: (λx.x) と (λy.y)，(λfx.fx) と (λuv.uv) など 齊藤 信臣 计算とは
- 20. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 例えばラムダ計算での 1 + 2 は: 齊藤 信臣 计算とは
- 21. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 例えばラムダ計算での 1 + 2 は: AddC1C2 = (λxyuv.xu(yuv))C1C2 齊藤 信臣 计算とは
- 22. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 例えばラムダ計算での 1 + 2 は: AddC1C2 = (λxyuv.xu(yuv))C1C2 →β λuv.C1u(C2uv) = λuv.C1u((λfx.f(fx))uv) 齊藤 信臣 计算とは
- 23. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 例えばラムダ計算での 1 + 2 は: AddC1C2 = (λxyuv.xu(yuv))C1C2 →β λuv.C1u(C2uv) = λuv.C1u((λfx.f(fx))uv) →β λuv.C1u(u(uv)) = λuv.(λfx.fx)u(u(uv)) 齊藤 信臣 计算とは
- 24. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 例えばラムダ計算での 1 + 2 は: AddC1C2 = (λxyuv.xu(yuv))C1C2 →β λuv.C1u(C2uv) = λuv.C1u((λfx.f(fx))uv) →β λuv.C1u(u(uv)) = λuv.(λfx.fx)u(u(uv)) →β λuv.u(u(uv)) = C3 齊藤 信臣 计算とは
- 25. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 例えばラムダ計算での 1 + 2 は: AddC1C2 = (λxyuv.xu(yuv))C1C2 →β λuv.C1u(C2uv) = λuv.C1u((λfx.f(fx))uv) →β λuv.C1u(u(uv)) = λuv.(λfx.fx)u(u(uv)) →β λuv.u(u(uv)) = C3 AddC1C2 =β C3， すなわち 1 + 2 = 3 が得られる！ (一般の場合も簡単に示せる) 齊藤 信臣 计算とは
- 27. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 他の計算モデルとの関係 ラムダ計算以外のモデル Turing 機械 テープに書かれた文字を書き換えていく，ハード ウェア的モデル． 帰納的関数 足し算?掛け算など基本的な演算と，関数の合成な どで構成される自然数上の関数． 齊藤 信臣 计算とは
- 28. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 他の計算モデルとの関係 ラムダ計算以外のモデル Turing 機械 テープに書かれた文字を書き換えていく，ハード ウェア的モデル． 帰納的関数 足し算?掛け算など基本的な演算と，関数の合成な どで構成される自然数上の関数． ラムダ計算，Turing 機械，帰納的関数で表現可能な関数は一致 する これらで表現できるものを「計算」と見なす (Church-Turing の提唱) コンピュータの原理も理論的には Turing 機械と同等 齊藤 信臣 计算とは
- 29. 自己紹介 计算の概念 関連分野 まとめ 计算とは？ ラムダ計算 他のモデル 計算可能性に関する結果 有名な結果 次の事実が知られている 任意に与えられた Turing 機械が有限時間で停止するかどう かを判定する Turing 機械は存在しない 任意に与えられたディオファントス方程式が整数解を持つか 否かを判定する Turing 機械は存在しない ※ 1900 年の国際数学者会議@パリで提示された問題 ※「ヒルベルトの第 10 問題」と呼ばれる 齊藤 信臣 计算とは
- 31. 自己紹介 计算の概念 関連分野 まとめ まとめ まとめ 「計算」の数学的モデル 機械的な有限の手続き 計算で解ける問題/解けない問題がある プログラムの停止性判定 ヒルベルトの第 10 問題 ラムダ計算 関数概念を抽象化したような，記号列の書き換え体系 β 簡約が計算操作: (λx.M)N →β M[x := N] Turing 機械，帰納的関数といったモデルも存在する → これらが表現する関数クラスは一致 齊藤 信臣 计算とは
- 32. 自己紹介 计算の概念 関連分野 まとめ まとめ おまけ このスライドも LATEX で作っています (Beamer というクラス) 齊藤 信臣 计算とは