λ-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

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