λ-calculus.λ計算.(lambda calculus)

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 00:45:53

λ計算について議論しましょう．
とりあえず，λ計算の基本から，各種関数型言語との関係，さらには研究ネタ
まで，λ計算に関係の深い話題ならなんでも OK ということで．

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 00:47:18

どなたかβ変換の基本について教えてください．
(λx.x)((λx.x)x) というλ式のβ変換には複数
の変換の仕方があると思うのですが，たとえば，

(λx.x)((λx.x)x)
　　　　^^^^^^^
->(λx.x)x
^^^^^^^
->x

の場合と，

(λx.x)((λx.x)x)
^^^^^^^
->((λx.x)x)((λx.x)x)
　^^^^^^^^^^
->x((λx.x)x)
　　^^^^^^^
->xx

とで結果が異なってしまいます．
どこで間違えているのでしょうか?

2 · 2006/12/08(金) 00:50:16

すいません，書き忘れました．

(λx.x)((λx.x)x)
　　　　^^^^^^^
の ^^^^ 部分は，注目しているβ基を表しています．

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 01:11:53

> (λx.x)((λx.x)x)
> ^^^^^^^
> ->((λx.x)x)((λx.x)x)
いくらなんでもこの簡約はありえないだろ常識的に考えて。。。

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 01:30:41

>>4
ぐはぁ，ホントだ．．．
早速ありがとうございました．

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 01:49:33

日本語英語を問わず，初学者向けに基礎から解説している文献があったら
教えていただけませんか? アマゾンの書評を見て，

高橋正子,『計算論：計算可能性とラムダ計算』, ISBN4-7649-0184-6, 1991

を買ってみたんですが，自分には難しすぎて独習は絶望的に思えます．

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 03:10:37

>>6
コンピュータサイエンス入門の紫のやつ

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 09:11:50

>>7
Scheme を題材にした SICP のことでしょうか?
(http://jargon.net/jargonfile/p/PurpleBook.html)
だとすると，Church number は扱っていますが, Church-Rosser
の定理などは扱っていないので，これだけではλ計算の勉強には
不十分に思えます．
それとも別の本のことですか?

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 09:46:08

>>6
高橋正子が無理なら渡辺米崎のがいいよ。
『計算論入門』渡辺治米崎直樹日本評論社 2100円

λの勉強してどういう方向に行きたいのかにもよるが。

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 11:36:11

>>8
違う違う
http://www.amazon.co.jp/gp/product/4000050060

6 · 2006/12/08(金) 15:42:05

>>9
ありがとうございます．
ググってみると他でも評判が良さそうなので，買ってみます．

> λの勉強してどういう方向に行きたいのかにもよるが。

とりあえずの動機は，プログラミングの役に立つかもしれないので，
関数型言語の理論的な背景を知っておきたい，という程度ですが，λ
計算を勉強しておくとどういう応用の可能性があるのか，興味があり
ます．λ計算の知識が必要になるような「方向」って，どんなものが
あるのでしょうか?

>>10
>http://www.amazon.co.jp/gp/product/4000050060
在庫切れ．．．orz
というのはさておき，レビューコメントに，
> 第II部「プログラミング言語」はラムダ計算をやったことがないと読むのは
> かなりつらいと思います。
> 横内寛文『プログラム意味論』、高橋正子『計算論』、大堀淳『プログラミ
> ング言語の基礎理論』とかで一度やってからトライした方がいいでしょう。
とあるので，高橋正子『計算論』のλ計算解説でわからない自分には
さらにちんぷんかんぷんなんじゃなかろうかと思うんですが．．．

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 18:37:48

>>11
そのレビュワーおかしいな。
ラムダ計算に関して、そこに挙げられている3冊はいずれも
『コンピュータサイエンス入門』よりも難しいぜ。

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 21:39:21

最初の入り口なら、googleで検索してどっかの大学の
講義資料のPDFを読んだほうがいいんじゃないか。
参考文献もそこに書いてあるでしょ。

**名無しさん＠お腹いっぱい。** · 2006/12/08(金) 23:01:13

>>6
Henk Barendregt, “Lambda Calculi with Types”,
available from: ttp://www.cs.ru.nl/~henk/papers.html

ところで Hindley & Seldin の新版が出るという話があるけど、ﾏﾀﾞｧ-? （･∀･）っ/凵⌒☆ﾁﾝﾁﾝ

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 00:16:33

>>11
とりあえず面白そうだというのが動機ということでいいかな。
ただ、λ計算の勉強がプログラミングの役に立つということには肯定的になれない。
λ計算が必要になる方向は山ほどあるが、例えば>>14のBarendregtのようなのは王道。

こっちからも質問させてもらうが、キミは学部にいるのかな？学科や学年など、
差し支えない範囲で知りたいのだけれど。高校生ならそれもまた良し。

>>12
Amazonのレビュワーなんか信用できないよね。
補うために横内みたいなのを薦めるあたり狂ってる。

6 · 2006/12/09(土) 13:01:14

>>12
なるほど，そうですか．
アマゾンにはなさそうなので，探してみます．

>>13
>>14
Web 上で公開されていた
Barendregt et al., `Introduction to Lambda Calculus', 2000
が良さそうかなぁ，と思って眺め始めたところです．
型付きλ計算は，型なしをかじってからにしようと思ってます．

>>15
>とりあえず面白そうだというのが動機ということでいいかな。

はい．

>λ計算が必要になる方向は山ほどあるが、例えば>>14のBarendregtのようなのは王道。

>>14 のタイトルを眺めると，数学の命題証明に使うんですかね?

>こっちからも質問させてもらうが、キミは学部にいるのかな？学科や学年など、
>差し支えない範囲で知りたいのだけれど。高校生ならそれもまた良し。

ソフトウェアの研究開発部門で働いている社会人です．
しかし大学では CS 関連教育を受けていたわけではないので，ある意
味高校生と同レベルです．初心に帰って勉強したいです．

>>>12
>Amazonのレビュワーなんか信用できないよね。
>補うために横内みたいなのを薦めるあたり狂ってる。

そうですか．
とりあえず >>9 は注文したので，届くまでは Web 上の文献と高橋
『計算論』を見比べてうんうん唸っておきます．

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 18:58:19

＞「コンピュータサイエンス入門―アルゴリズムとプログラミング言語」

版元では切れてるけど、まだ店頭にはある鴨よ。
ネットでチェックしたら池袋Ｊ堂に１冊在庫。欲しい人はキープしちゃったら。

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 20:28:48

型付ラムダ計算と型付でないラムダ計算に本質的な違いってあるの？

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 20:43:58

あります

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 20:45:40

>>18
たとえば、型なしでラッセルのパラドックスをどう説明する？

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 21:05:05

なるほどレスどうも。
ところで、型付でないラムダ計算の世界にも
カリー・ハワードの対応は存在しますか？

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 21:06:58

>>21
もちろん

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 21:19:58

型なしラムダ計算の型付けってどういうことなんですか。
もしそれができるなら、すべてのラムダ計算は型付である
と考えてしまっていいのでしょうか。

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 22:15:24

なにか間違ってないか。

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 22:29:17

どこかおかしいですか。当方初心者ゆえご教示ねがいます。

**名無しさん＠お腹いっぱい。** · 2006/12/09(土) 22:58:50

>>16
まずは個人のことに関する質問に答えてくれてありがとう。
これで少しは質問にも答えやすくなると思う。

横レスだけれど、`Introduction to Lambda Calculus', Barendregt et al.を
流し読みしてみた。演習問題も無理なものはなさそうだし、全部できなくても
いいから腰を据えて読めば、いい勉強になると思った。
一部で二階のラムダ計算が紹介されてたりして、論理がわかってないと理解に
困るとは思うけれど。

6 · 2006/12/11(月) 11:28:27

>>26
もろもろ，ありがとうございます．

早速その `Introduction to Lambda Calculus'
http://citeseer.ist.psu.edu/barendregt94introduction.html
なのですが，p.12 の 2.13 の例 (i) でいきなりつまずいています．
この例のココロもピンと来ないのですが，とくに以下の部分がわか
りません．

∃G∀X GX = SGX が成り立つことを，
∀X GX = SGX <= Gx = SGx　　　　　…(1)
　　　　　　 <= G = λx.SGx　　　 …(2)
　　　　　　 <= G = (λgx.Sgx)G　 …(3)
　　　　　　 <= G ≡ Y(λgx.Sgx)　…(4)

として示そうとしていますが，(3) と (4) の間の変換はなぜ
こうなるのでしょうか?
ここで X は任意のλ式で，
S ≡ λxyz.xz(yz)
Y ≡ λf.(λx.f(xx))(λx.f(xx))
だと思います．

**名無しさん＠お腹いっぱい。** · 2006/12/11(月) 22:11:45

Yが不動点演算子であることを考えると、(4)でGは(λgx.Sgx)の不動点になるように
定義してあるんだよね。
だから(3)のように(λgx.Sgx)をGに適用したら、Gが返ってくるようになってる。
もしかしたら不動点演算子が何をしているのかよくわかってないのかも。
定理2.12の意味がわかりにくいのかな。

上のようなことをあまり考えないで単純に簡約しても(4)から(3)は出てくるんだけれど、
手間がかかりすぎる上に不動点定理の意味が理解できないまま進んでしまうこともある。

**名無しさん＠お腹いっぱい。** · 2006/12/12(火) 01:12:08

>>27
任意のFに対して、Xについての方程式FX = Xには解がある、というのが2.12(i)の主張。
具体的に、その解の一つはYFである、というのが2.12(ii)の主張。

Xが両辺に現れる方程式があったとき、それをなんとかして
X = (なにか)X
の形に変形できれば、2.12(ii)を適用して
X ≡ Y(なにか)
というひとつの解を求めることができる。

2.13(i)はこの手法の実例で、まず∃G∀X GX = SGXを証明するために
∀X GX = SGX
が成り立つようなGを具体的に与えようとしている。そのためにこの式を変形し、
G = (λgx.Sgx)G
とする。この時点で2.12(ii)が適用できるので、
G ≡ Y(λgx.Sgx)
という解が求まった。という手順。

しかし、その本は全体的に不親切な気がする。入門書ってみんなこんなもの？

6 · 2006/12/12(火) 20:40:46

>>28
>もしかしたら不動点演算子が何をしているのかよくわかってないのかも。
>定理2.12の意味がわかりにくいのかな。

おっしゃるように，2.12 の fixedpoint theorem のところをちゃんと
理解していなかったようです．

> 上のようなことをあまり考えないで単純に簡約しても(4)から(3)は出てくるんだけれど、

うーむ．．．
(4) の右辺を単純に簡約していって，どの状態になったら G が出てく
るのでしょうか?

>>29
ありがとうございます．
とてもわかりやすい解説だと思いました．

> しかし、その本は全体的に不親切な気がする。入門書ってみんなこんなもの？

今のところ，まだ注文した >>9 も発送されていないので，もう少しこ
れで頑張ってみようと思っています．
英語でも構いませんので，わかりやすい入門書があれば引き続き情報
お待ちしてます．> 皆様．

**名無しさん＠お腹いっぱい。** · 2006/12/15(金) 18:19:27

自分は大昔、高橋正子研にいたことがある。
ラムダ計算で分かんないことがあったら教授してもいいよ。

**名無しさん＠お腹いっぱい。** · 2006/12/16(土) 02:53:58

女に質問なんかできるか

**名無しさん＠お腹いっぱい。** · 2006/12/16(土) 16:31:33

>>32
腐ったエサに釣られおってからに。

**名無しさん＠お腹いっぱい。** · 2006/12/18(月) 19:49:55

>>31
おお，それは素晴らしい．
ではせっかくなので．．．
条件分岐や再帰(繰り返し)はλ計算で表現できそうだ，というのは
なんとなくわかるんですが，逐次実行というのはλ計算ではどうい
うものに相当するんでしょうか? 逐次実行なんていうのはλ計算に
は存在しない?

**名無しさん＠お腹いっぱい。** · 2006/12/18(月) 19:54:31

>>34
実行ってなに？ww

**名無しさん＠お腹いっぱい。** · 2006/12/18(月) 20:47:46

CPS変換とかモナドとか?

**名無しさん＠お腹いっぱい。** · 2006/12/18(月) 21:43:51

>>35
実行とは言わないのかな．
逐次実行と書いたのは，構造化プログラミングの論理構造のうち，
「順次」のことだと思ってください．
ttp://ja.wikipedia.org/wiki/%E6%A7%8B%E9%80%A0%E5%8C%96%E3%83%97%E3%83%AD%E3%82%B0%E3%83%A9%E3%83%9F%E3%83%B3%E3%82%B0

>>36
なぜに CPS 変換が関係するんでしょうか?
で，CPS 変換って，λ計算の枠組みの中に含まれてるんでしょうか?

モナドって，圏論由来のモナドですよね?
圏論は，λ計算とはどういう関係になるんでしょうか?

**名無しさん＠お腹いっぱい。** · 2006/12/18(月) 22:01:24

値呼びλ計算だとよくこんな感じでやってるよね＞逐次実行
（dはe2に自由な出現を持たない変数）

e1;e2 ≡ (λd.e2) e1

**名無しさん＠お腹いっぱい。** · 2006/12/18(月) 22:10:11

>>37
基本的にラムダ計算には実行の概念はありません。
というのも、計算にI/Oなるものは存在しないからです。

**名無しさん＠お腹いっぱい。** · 2006/12/19(火) 00:57:15

>>37
ラムダでも実行という概念を考えられないわけではないと思うよ。
実行を計算の進行だと考えたりすれば、β簡約の1ステップを実行1ステップと言えない
わけでもない。勉強してれば色々出てくるけれど、簡約の順序を様々に定めてみたり、
自然意味論なんていう概念を持ちだしてみたり、バリエーションは豊かだなあ。
和書だと
プログラミング言語の基礎理論, 大堀淳, 共立出版
に書いてあるけれど、あせって理解しようとする必要もまだないと思う。
意味論っていうキーワードを知っておくのはいいかもしれない。

CPSは純粋なラムダ計算の枠外のものと思っていいんじゃないかな。
これもあわてて取り組むこともないだろうけれど、さっきこんなページみつけちゃった。
ttp://www.is.s.u-tokyo.ac.jp/vu/jugyo/processor/process/soft/compilerresume/coverq3/coverq3.html
処理系の方面に興味が移ったら、必須の知識だろうね。

モナドに関してはラムダ計算を拡張する手段と考えることもできて、それが一番わかり
やすい捉えかたかもしれない。Haskellのモナドなんかは、ラムダで副作用なしにI/Oを
実現できるようにした研究の実用例としての筆頭だな。ただ、Haskellのモナドだけで
しかモナドを考えられないようになったら、困ることが起こりうる。
圏論とラムダ計算の関係は他にもあって、計算現象が何を意味しているのかを捉える手
段であったりする。むしろこちらの方が一般性があって重要だけど。Haskellのモナド
は、計算現象のうちの一部である副作用を考える上で役割を果たした、と言えるよね。

ところで、Yコンビネータの件が解決したのか気になるんだけど、どうなの？
不動点定理を理解して、かつ>>28の(4)から(3)を手計算で示せたりはしたのかな。
自力で計算できそうになければ、時間のあるときに計算して書き込むけれど。

長文ごめんね。