5ちゃんねる ★スマホ版★ ■掲示板に戻る■ 全部 1- 最新50  

■ このスレッドは過去ログ倉庫に格納されています

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

1 :名無しさん@お腹いっぱい。:2006/12/08(金) 00:45:53 ID:fx6EeyNJ0
λ計算について議論しましょう.
とりあえず,λ計算の基本から,各種関数型言語との関係,さらには研究ネタ
まで,λ計算に関係の深い話題ならなんでも OK ということで.


2 :名無しさん@お腹いっぱい。:2006/12/08(金) 00:47:18 ID:fx6EeyNJ0
どなたかβ変換の基本について教えてください.
(λ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

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


3 :2:2006/12/08(金) 00:50:16 ID:fx6EeyNJ0
すいません,書き忘れました.

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

4 :名無しさん@お腹いっぱい。:2006/12/08(金) 01:11:53 ID:gqCTHlyc0
> (λx.x)((λx.x)x)
> ^^^^^^^
> ->((λx.x)x)((λx.x)x)
いくらなんでもこの簡約はありえないだろ常識的に考えて。。。

5 :名無しさん@お腹いっぱい。:2006/12/08(金) 01:30:41 ID:fx6EeyNJ0
>>4
ぐはぁ,ホントだ...
早速ありがとうございました.

6 :名無しさん@お腹いっぱい。:2006/12/08(金) 01:49:33 ID:fx6EeyNJ0
日本語英語を問わず,初学者向けに基礎から解説している文献があったら
教えていただけませんか? アマゾンの書評を見て,

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

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


7 :名無しさん@お腹いっぱい。:2006/12/08(金) 03:10:37 ID:dVua0loM0
>>6
コンピュータサイエンス入門の紫のやつ

8 :名無しさん@お腹いっぱい。:2006/12/08(金) 09:11:50 ID:fx6EeyNJ0
>>7
Scheme を題材にした SICP のことでしょうか?
(http://jargon.net/jargonfile/p/PurpleBook.html)
だとすると,Church number は扱っていますが, Church-Rosser
の定理などは扱っていないので,これだけではλ計算の勉強には
不十分に思えます.
それとも別の本のことですか?

9 :名無しさん@お腹いっぱい。:2006/12/08(金) 09:46:08 ID:gqCTHlyc0
>>6
高橋正子が無理なら渡辺米崎のがいいよ。
『計算論入門』渡辺治 米崎直樹 日本評論社 2100円

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

10 :名無しさん@お腹いっぱい。:2006/12/08(金) 11:36:11 ID:dVua0loM0
>>8
違う違う
http://www.amazon.co.jp/gp/product/4000050060

11 :6:2006/12/08(金) 15:42:05 ID:Fpcw2EMX0
>>9
ありがとうございます.
ググってみると他でも評判が良さそうなので,買ってみます.

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

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

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


12 :名無しさん@お腹いっぱい。:2006/12/08(金) 18:37:48 ID:ZwUUWqVu0
>>11
そのレビュワーおかしいな。
ラムダ計算に関して、そこに挙げられている3冊はいずれも
『コンピュータサイエンス入門』よりも難しいぜ。

13 :名無しさん@お腹いっぱい。:2006/12/08(金) 21:39:21 ID:ZvDwNqoe0
最初の入り口なら、googleで検索してどっかの大学の
講義資料のPDFを読んだほうがいいんじゃないか。
参考文献もそこに書いてあるでしょ。

14 :名無しさん@お腹いっぱい。:2006/12/08(金) 23:01:13 ID:CD77k6tS0
>>6
Henk Barendregt, “Lambda Calculi with Types”,
available from: ttp://www.cs.ru.nl/~henk/papers.html

ところで Hindley & Seldin の新版が出るという話があるけど、マダァ-? (・∀・ )っ/凵⌒☆チンチン

15 :名無しさん@お腹いっぱい。:2006/12/09(土) 00:16:33 ID:M4mrgYq60
>>11
とりあえず面白そうだというのが動機ということでいいかな。
ただ、λ計算の勉強がプログラミングの役に立つということには肯定的になれない。
λ計算が必要になる方向は山ほどあるが、例えば>>14のBarendregtのようなのは王道。

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

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

16 :6:2006/12/09(土) 13:01:14 ID:sjo5ErmH0
>>12
なるほど,そうですか.
アマゾンにはなさそうなので,探してみます.

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

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

はい.

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

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

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

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

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

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

17 :名無しさん@お腹いっぱい。:2006/12/09(土) 18:58:19 ID:+9XAEm1x0
>「コンピュータサイエンス入門―アルゴリズムとプログラミング言語」

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

18 :名無しさん@お腹いっぱい。:2006/12/09(土) 20:28:48 ID:Pfl1+DBh0
型付ラムダ計算と型付でないラムダ計算に本質的な違いってあるの?

19 :名無しさん@お腹いっぱい。:2006/12/09(土) 20:43:58 ID:o7ud+6Zb0
あります

20 :名無しさん@お腹いっぱい。:2006/12/09(土) 20:45:40 ID:o7ud+6Zb0
>>18
たとえば、型なしでラッセルのパラドックスをどう説明する?

21 :名無しさん@お腹いっぱい。:2006/12/09(土) 21:05:05 ID:Pfl1+DBh0
なるほどレスどうも。
ところで、型付でないラムダ計算の世界にも
カリー・ハワードの対応は存在しますか?

22 :名無しさん@お腹いっぱい。:2006/12/09(土) 21:06:58 ID:o7ud+6Zb0
>>21
もちろん

23 :名無しさん@お腹いっぱい。:2006/12/09(土) 21:19:58 ID:Pfl1+DBh0
型なしラムダ計算の型付けってどういうことなんですか。
もしそれができるなら、すべてのラムダ計算は型付である
と考えてしまっていいのでしょうか。

24 :名無しさん@お腹いっぱい。:2006/12/09(土) 22:15:24 ID:NzjU++XC0
なにか間違ってないか。

25 :名無しさん@お腹いっぱい。:2006/12/09(土) 22:29:17 ID:Pfl1+DBh0
どこかおかしいですか。当方初心者ゆえご教示ねがいます。

26 :名無しさん@お腹いっぱい。:2006/12/09(土) 22:58:50 ID:M4mrgYq60
>>16
まずは個人のことに関する質問に答えてくれてありがとう。
これで少しは質問にも答えやすくなると思う。

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


27 :6:2006/12/11(月) 11:28:27 ID:FDDBt+TK0
>>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))
だと思います.


28 :名無しさん@お腹いっぱい。:2006/12/11(月) 22:11:45 ID:RLHBhv8f0
Yが不動点演算子であることを考えると、(4)でGは(λgx.Sgx)の不動点になるように
定義してあるんだよね。
だから(3)のように(λgx.Sgx)をGに適用したら、Gが返ってくるようになってる。
もしかしたら不動点演算子が何をしているのかよくわかってないのかも。
定理2.12の意味がわかりにくいのかな。

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

29 :名無しさん@お腹いっぱい。:2006/12/12(火) 01:12:08 ID:CcSGY4sH0
>>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)
という解が求まった。という手順。

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

30 :6:2006/12/12(火) 20:40:46 ID:j/nvRo2a0
>>28
>もしかしたら不動点演算子が何をしているのかよくわかってないのかも。
>定理2.12の意味がわかりにくいのかな。

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

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

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

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

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

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


31 :名無しさん@お腹いっぱい。:2006/12/15(金) 18:19:27 ID:YruGzNNfO
自分は大昔、高橋正子研にいたことがある。
ラムダ計算で分かんないことがあったら教授してもいいよ。

32 :名無しさん@お腹いっぱい。:2006/12/16(土) 02:53:58 ID:J33ulpYB0
女に質問なんかできるか

33 :名無しさん@お腹いっぱい。:2006/12/16(土) 16:31:33 ID:wXiS3cZ70
>>32
腐ったエサに釣られおってからに。

34 :名無しさん@お腹いっぱい。:2006/12/18(月) 19:49:55 ID:/KHo9KCp0
>>31
おお,それは素晴らしい.
ではせっかくなので...
条件分岐や再帰(繰り返し)はλ計算で表現できそうだ,というのは
なんとなくわかるんですが,逐次実行というのはλ計算ではどうい
うものに相当するんでしょうか? 逐次実行なんていうのはλ計算に
は存在しない?

35 :名無しさん@お腹いっぱい。:2006/12/18(月) 19:54:31 ID:qp+mM75v0
>>34
実行ってなに?ww

36 :名無しさん@お腹いっぱい。:2006/12/18(月) 20:47:46 ID:2cGaSwLx0
CPS変換とかモナドとか?

37 :名無しさん@お腹いっぱい。:2006/12/18(月) 21:43:51 ID:/KHo9KCp0
>>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 変換って,λ計算の枠組みの中に含まれてるんでしょうか?

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

38 :名無しさん@お腹いっぱい。:2006/12/18(月) 22:01:24 ID:V7rk4+Pv0
値呼びλ計算だとよくこんな感じでやってるよね>逐次実行
(dはe2に自由な出現を持たない変数)

e1;e2 ≡ (λd.e2) e1



39 :名無しさん@お腹いっぱい。:2006/12/18(月) 22:10:11 ID:qp+mM75v0
>>37
基本的にラムダ計算には実行の概念はありません。
というのも、計算にI/Oなるものは存在しないからです。

40 :名無しさん@お腹いっぱい。:2006/12/19(火) 00:57:15 ID:+qnJ1mPk0
>>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)を手計算で示せたりはしたのかな。
自力で計算できそうになければ、時間のあるときに計算して書き込むけれど。

長文ごめんね。

41 :名無しさん@お腹いっぱい。:2006/12/19(火) 12:39:29 ID:2cG7e0aK0
モナドとラムダというと computational lambda-calculus というのがありますね
聞いたことがあるだけでろくに読んでいませんが
http://www.disi.unige.it/person/MoggiE/ftp/lics89.pdf

42 :名無しさん@お腹いっぱい。:2006/12/19(火) 16:46:45 ID:6z03Pwwj0
領域理論て何のためにあるんですか?

43 :31:2006/12/19(火) 23:22:17 ID:psf7CPmq0
プログラム意味論(横内)を読むのもいいかも。

意味論を勉強するなら、せっかくだからコンパイラの勉強も関連でやってみると面白い。

学生時代、ラムダ計算ばかりやってたわけじゃなく、論理学や竹内外史さんの本ばかり
読まされていたから、なんか頭がごちゃごちゃであんま思い出せないや。

44 :名無しさん@お腹いっぱい。:2006/12/21(木) 00:53:51 ID:0w/HJ1im0
>>43
輪講はやっぱりシェーンフィールドでしたか?

45 :42:2006/12/21(木) 09:22:47 ID:TNnO14/x0
質問しても誰も答えられないんだな

46 :名無しさん@お腹いっぱい。:2006/12/23(土) 17:12:53 ID:hnglVPuq0
>>40
もろもろご解説ありがとうございます.
計算にはトライしてみたんですが,理解できていません.

G ≡ Y(λgx.Sgx) …(4)
≡(λf.(λx.f(xx))(λx.f(xx)))(λgx.Sgx) :Y を置き換え
≡(λf.(λx.f(xx))(λx.f(xx)))(λgx.(λxyz.xz(yz))gx) :S を置き換え
≡(λx.(λgx.(λxyz.xz(yz))gx)(xx))(λx.(λgx.(λxyz.xz(yz))gx)(xx)) :f を置き換え
で,この先どうしていけば収集がつくのかわからず,
ttp://www.dina.kvl.dk/~sestoft/lamreduce/
ttp://ellemose.dina.kvl.dk/~sestoft/lamreduce/lamframes.html

(\x.(\gx.(\xyz.xz(yz))gx)(xx))(\x.(\gx.(\xyz.xz(yz))gx)(xx))
として trace / normal order で入れてみたところ,
Normal order:
(\x.(\gx.(\xyz.xz yz) gx) xx) (\x.(\gx.(\xyz.xz yz) gx) xx)
==> (\gx.(\xyz.xz yz) gx) (xx)
==> (\xyz.xz yz) (xx)
==> xz yz
Performed 3 beta-reductions

という結果になりました.
なぜこういう簡約になるのかわかりませんし,なぜ単純な簡約で
G = (λgx.Sgx)G  …(3)
の形になるのかもわかりません...

お手すきのときにでも,ご解説いただければ嬉しいです.


47 :名無しさん@お腹いっぱい。:2006/12/23(土) 22:13:37 ID:443fv80m0
YF = F(YF) なんだよね。なら
Y (λgx.Sgx) = (λgx.Sgx) (Y (λgx.Sgx)) だよね。

48 :名無しさん@お腹いっぱい。:2006/12/23(土) 22:19:07 ID:443fv80m0
>>46
> (\x.(\gx.(\xyz.xz(yz))gx)(xx))(\x.(\gx.(\xyz.xz(yz))gx)(xx))
変数の間は空白で区切らないといけないんでは?

49 :名無しさん@お腹いっぱい。:2006/12/23(土) 23:58:05 ID:tGpE9bcF0
大学の授業でやって単位も取ったけどなーんも覚えてないや。

50 :名無しさん@お腹いっぱい。:2006/12/24(日) 12:09:47 ID:CQ9FSVwv0
>>47
そうですね.
>>6 の本質的なところは >>28, >>29 で解説があったとおりだろうと思うのですが,
以下のような指摘があったので,単純に簡約して (4) から (3) が出てくるのかど
うか実際に試してみました.
>>28
>上のようなことをあまり考えないで単純に簡約しても(4)から(3)は出てくるんだけれど、
>手間がかかりすぎる上に不動点定理の意味が理解できないまま進んでしまうこともある。
>>40
>ところで、Yコンビネータの件が解決したのか気になるんだけど、どうなの?
>不動点定理を理解して、かつ>>28の(4)から(3)を手計算で示せたりはしたのかな。
>自力で計算できそうになければ、時間のあるときに計算して書き込むけれど。

>>46
ご指摘感謝です.
くっつけちゃうと 1 つの変数になっちゃうんですね.
ちゃんと説明に書いてありました.orz

(\x.(\g x.(\x y z.x z (y z)) g x) (x x))(\x.(\g x.(\x y z.x z (y z)) g x)(x x))
を入れてみると,λ式は長くなる一方で終了しませんでした.
Y や S は事前に定義されているようなので最初から,すなわち Y(\g x.S g x)
でも試してみましたが同様です.

とうわけで今のところ,>>27 の (4) を単純に簡約しても計算は止まらず (3)
が明快な形で出てくることもない,と理解しています.


51 :名無しさん@お腹いっぱい。:2006/12/29(金) 00:32:18 ID:FQrEwVjt0
そんなに難しい話でもないのでは。
まずYが不動点演算子なのは大丈夫だよね?
Y:=λf.(λx.f(xx))(λx.f(xx)) とおくと、任意のXに対してX(YX)=YXとなる。
つまり、YがXの不動点を作りだす項になってるわけ。これは>>27に証明があるはず。

不動点定理の例として、G:=Y(λgx.Sgx)という定義のもとでG=(λgx.Sgx)Gを示す。
>>27での"="がどういう定義なのか読んでないけれど、高橋正子の本のp.66
に定義がある(記号はβが添えてあるけれど)ので、その解釈でいいと思う。
気になるのが>>27での記号"<="なんだけど、これは"="を用いた等式を導く理論の
ことを意識できるならいいかもね。高橋本だとp.96以降になる。
(4)をもとにして(3)の左辺と右辺が"="の関係にあることを、高橋本でいう公理系β
で導けばいい。
簡単のためにA:=(λgx.Sgx)とおくと、
(左辺)=G=YA -> (λx.A(xx))(λx.A(xx)) -> A((λx.A(xx))(λx.A(xx)))
となる。一方、
(右辺)=AG=A(YA) -> A((λx.A(xx))(λx.A(xx)))
となって、(3)の等式が成り立つ。
これは高橋本の公理系βで導くことのできる等式なので、上のスケッチを参考に
して形式的に書き下してみるのは良い練習だと思うよ。

ところで、この問題を考えるのにあたって>>46のサイトで正規形を求めたのは間違い
なのは理解できてるのかな?
もともとの>>27の等式の証明は、λ項の正規形を求めることとは違うから。

52 :名無しさん@お腹いっぱい。:2006/12/29(金) 00:55:30 ID:FQrEwVjt0
実際に書いてみると、Yが不動点演算子であることの証明そのまんまだなあ。。
高橋正子が読めないのは置いておいて、米崎渡辺には不動点演算子なんかは
書いてたかどうかはっきり覚えてないんだよね。
不動点演算子Yを理解するための道筋を、今は上手く提示できない。
なにかいい方法ないかなー。

53 :名無しさん@お腹いっぱい。:2007/01/13(土) 02:46:55 ID:+Ig8F9i+O
高橋(別姓を名乗ってた)も米崎も渡辺も、講義を生で聞いてた俺は勝ち組!
でも当時全く理解できなかった。
特に米崎は下手くそな英語で講義するな!

54 :名無しさん@お腹いっぱい。:2007/01/31(水) 21:03:41 ID:6thJQwOu0
λ計算と圏論との技術的な違いは?
なんてこと聞いていいですか?

55 :名無しさん@お腹いっぱい。:2007/02/01(木) 00:38:54 ID:4QfEgNQD0
>>54
技術的な違いは知らないが、理論的な違いを説明するにはこの余白は狭すぎる

56 :名無しさん@お腹いっぱい。:2007/02/01(木) 00:48:55 ID:+34wy7Oj0
フェルマー乙

57 :名無しさん@お腹いっぱい。:2007/02/01(木) 21:43:15 ID:K+vNzHhD0
>>55
一般ユーザは理論なんかじゃなく道具がほしいわけですが。
技術的には、圏論=λ計算+有向グラフ だくらいに
言えないものですか?

58 :名無しさん@お腹いっぱい。:2007/02/01(木) 22:26:22 ID:kRNkT8qk0
>>57
正確じゃない

59 :名無しさん@お腹いっぱい。:2007/02/01(木) 23:12:57 ID:K+vNzHhD0
>>58
道具として使えればよいので、正確じゃないくらいなら
気にしない。道具の見地からは、圏論=what ?
教えてほしい。

60 :名無しさん@お腹いっぱい。:2007/02/02(金) 10:14:46 ID:RFLtQC8p0
λ計算:
data LambdaExpression = Variable String | Abstraction String LambdaExpression | Application LambdaExpression LambdaExpression

betaTransition :: LambdaExpression -> LambdaExpression
betaTransition e = ...

圏論:
class Cat o a where
idArrow : a o o
composeArrow : a o o -> a o o -> Maybe (a o o)
-- composeArrow must satisfy ...

-- Cat o aのサブクラスがいっぱい
-- TemplateHaskellを使って型から自動生成された関数がいっぱい

こんなイメージかね。哺乳類とは4本足の恒温動物だ、というぐらいに不正確なものだけど。


61 :名無しさん@お腹いっぱい。:2007/02/02(金) 19:52:46 ID:LF1iI1XI0
>>60
早速愚問に答えてくれてありがとう。
でもそれくらいは知っているつもり。
圏論が商品だとすると、オッ使えそうだという使用説明を
聞いたことがない。ほんとに使っている人いるの?
木下さんの「定義の正当化」はよかったが、それでも
道具としてのよい解説はほんとにないね。

62 :名無しさん@お腹いっぱい。:2007/02/02(金) 20:44:43 ID:zMkKAG570
圏論は数学では有力な道具だよ。
でも圏論が有力なのは圏同値が言える場合が殆どだから
圏同値成立する2つの圏を見つけてこない限りは
情報の世界で有用だとは思えない。
俺は情報学を良く知らないから俺の認識不足かもしれないけどね


63 :名無しさん@お腹いっぱい。:2007/02/02(金) 22:56:38 ID:KrEAD7TE0
お前らまだλ計算とか圏論とか言ってるのかよ
遅れてるなー

これからのトレンドはπ計算だぜ

64 :名無しさん@お腹いっぱい。:2007/02/03(土) 01:49:52 ID:70ceOPpy0
>>59
ここはラムダのスレなので、ラムダの話に限れば圏論は意味論を与えるための
道具として使われてるよ、というのはどうだろう。
いくらなんでも「λ計算+有向グラフ」はありえない。
>>60も書いてるが、Haskell関係での貢献も大きいね。

65 :名無しさん@お腹いっぱい。:2007/02/03(土) 22:03:39 ID:IahLCrBY0
>>64 レスポンスありがとう。
でも道具としても思想としてもやはりよくわからんね。
「意味論を与えるため」というのも本意でもなさそうだし。
わたしの場合は道具としてどう使えるかというのが
唯一の関心だが、だれかスパッと解説できないのかな?
ふつうこういう商品は売れないよ。
もともとそんなものかもしれないが。
スペンサーの形式法則みたいじゃつまらんね

66 :名無しさん@お腹いっぱい。:2007/02/04(日) 00:17:26 ID:WKIXrpRj0
>>65
道具としてという点で一つだけ挙げると、モナド関連の話がある。
Haskellなんかがそうだが、圏論のモナドを用いることによって、
副作用のあるプログラムを純粋な関数型言語で記述できるように
なった。影響の大きい仕事としては、E. MoggiのComputational
Lambdaが筆頭。
副作用を純粋な関数型言語で扱えるメリットはわかってもらえる
と思うが、こんなところでどうだろう?

67 :名無しさん@お腹いっぱい。:2007/02/04(日) 01:10:23 ID:6qLK1Z2H0
>>66
モナドは不可逆という一点しか利用しておらず、圏論などと言うことはおこがましい

68 :名無しさん@お腹いっぱい。:2007/02/04(日) 01:44:49 ID:zzUqFVaZ0
>> 67
(*゚ー゚)/センセー
Grothendieck constructionとか、Sheafificationはどうでしょう?


69 :名無しさん@お腹いっぱい。:2007/02/04(日) 01:46:54 ID:zzUqFVaZ0
>> 67
あと、Effective Toposとか。。。
ヽ( ´ ▽ ` )ノ

70 :名無しさん@お腹いっぱい。:2007/02/04(日) 01:53:38 ID:zzUqFVaZ0
>> 63
>> π計算だぜ

polymorphic type system を与えて、SNになるようだったら、
π計算も大好きになれるんですけど。
deadlock freedomの十分条件を与える程度のtype systemしか
ないので、
(´・ω・`)ショボーン
です。

deadlock freedomの必要十分条件を与えるtype systemがあれば
もう少しは

(`・ω・´) シャキーン

になるのですが。



71 :名無しさん@お腹いっぱい。:2007/02/04(日) 04:13:58 ID:WKIXrpRj0
>>67
そうですか。申し分けない。

72 :名無しさん@お腹いっぱい。:2007/02/05(月) 12:21:40 ID:odqa2CoY0
書き込んでいる連中の研究室がなんとなくわかってきたりして。

73 :名無しさん@お腹いっぱい。:2007/02/05(月) 12:54:02 ID:WosI6ZgP0
>>72
受験生ですが、晒してくださいおねがいします><

74 :名無しさん@お腹いっぱい。:2007/02/07(水) 21:02:30 ID:yTGJKQRq0
>>70
πでも型でSNはできなくもない。
ftp://ftp.dcs.qmw.ac.uk/lfp/kohei/pi-sn-journal.ps.gz
とか。かなり無理矢理だけど。

あと、λの型だって、SNやprogressの「必要十分条件」は与えてないだろう。
まあ、πがλほどきれいじゃないのは同意するが。


75 :名無しさん@お腹いっぱい。:2007/02/09(金) 01:15:12 ID:vrNq1duY0
ラムダ計算のいいSolved Problem付き教科書ってない?
英語の奴でいいからさ。
型付まで網羅されてるとうれすぃ。

76 :名無しさん@お腹いっぱい。:2007/02/09(金) 17:14:36 ID:vWS3ApOk0
>>72
声が大きい人がいるような気がする。

77 :名無しさん@お腹いっぱい。:2007/02/09(金) 17:23:42 ID:zpxlhCu80
気のせいだよ。
この分野やってる人は思ったより少なくないからね。

78 :名無しさん@お腹いっぱい。:2007/02/10(土) 15:02:45 ID:VDR57wCl0
ちっ
良スレかよ。

79 :名無しさん@お腹いっぱい。:2007/02/11(日) 20:37:05 ID:PgEe6Rsu0
>>77
ラムダ計算の研究やってる人は少いだろうね。

ラムダ計算使って研究してる人は少くないんで、油断できんよ。

80 :名無しさん@お腹いっぱい。:2007/03/14(水) 19:07:26 ID:ds7xgK/t0
>>6
>>11
お前、本当に愛い奴だ。
そうやって、何年も前に2chで教えてもらった参考書を
一体何年間ネタとして使いまわしてるんだよw

81 :名無しさん@お腹いっぱい。:2007/03/14(水) 19:08:17 ID:ds7xgK/t0
>16
> ソフトウェアの研究開発部門で働いている社会人です.
> しかし大学では CS 関連教育を受けていたわけではないので,ある意
> 味高校生と同レベルです.初心に帰って勉強したいです.



82 :名無しさん@お腹いっぱい。:2007/03/14(水) 19:10:16 ID:ds7xgK/t0
>31
ほほう。大きく出たな。
高橋研に問い合わせてみようかw

83 :名無しさん@お腹いっぱい。:2007/03/14(水) 19:11:34 ID:ds7xgK/t0
>>43
おやおや、amazonのレビューを「狂ってる」と言われた後で
またまた・・・

> 論理学や竹内外史さんの本ばかり
> 読まされていたから、なんか頭がごちゃごちゃであんま思い出せないや。



84 :名無しさん@お腹いっぱい。:2007/03/14(水) 19:12:24 ID:ds7xgK/t0
>>63
おじちゃん乙

85 :名無しさん@お腹いっぱい。:2007/03/14(水) 19:12:57 ID:ds7xgK/t0
>>72
お前のジサクジエンはいつも判りやすいなぁ

86 ::2007/03/14(水) 19:26:16 ID:ds7xgK/t0
ex-phenomenologistさんが書き込んだレビュー

・Set Theory: An Introduction to Independence Proofs :
 Studies in Logic and the Foundations of Mathematics Series
 (Studies in Logic and the Foundations of Mathematics) Kenneth Kunen著
・Logic and Structure (Universitext) Dirk Van Dalen著
・Elements of Set Theory Herbert B. Enderton著
・A Mathematical Introduction to Logic Herbert B. Enderton著
・ First-Order Modal Logic (Synthese Library) Melvin Fitting著

・Thinking About Mathematics: The Philosophy of Mathematics Stewart Shapiro著

・Godel's Proof Douglas R. Hofstadter著
・ゲーデルは何を証明したか―数学から超数学へ E. ナーゲル著

・コンピュータサイエンス入門―アルゴリズムとプログラミング言語 大堀 淳著
・Logic: A Very Short Introduction (Very Short Introductions) Graham Priest著
・論理学をつくる 戸田山 和久著
・集合とはなにか―はじめて学ぶ人のために 竹内 外史著
・なっとくする集合・位相 瀬山 士郎著
・ゼロから学ぶ線形代数 小島 寛之著

 線形代数の入門書として最適, 2003/6/23
 抽象的で何をやっているのかいまいちつかめない線形代数に対して、
 図形的なイメージを豊富に与えてくれる入門書。
 もちろんいろいろな限界はあるけども(例えば外積の説明は物足りない)、
 非常に分かりやすくて初学者にお勧め。この本でイメージを掴みつつ、
 さらに他の本にステップアップできる。
 練習問題は公式や定理を確認する手計算のものだけに配慮されている。


87 :名無しさん@お腹いっぱい。:2007/03/14(水) 19:29:24 ID:ds7xgK/t0
なんてったっけ?
哲学板やν速で暴れてたクソスレ立て
あいつだな。

88 :名無しさん@お腹いっぱい。:2007/03/15(木) 01:10:45 ID:qTQBnbGB0
すみませんすぐ片付けますんで。
.       ∧_∧ 
       (;´Д`) 
  -=≡  /    ヽ       ,.-'''"-─ `ー,--─'''''''''''i-、,,
.      /| |   |. |    ,.-,/        /::::::::::::::::::::::!,,  \
 -=≡ /. \ヽ/\\_ (  ,'          i:::::::::::::::::::::;ノ ヽ-、,,/''ー'''"7
    /    ヽ⌒)==ヽ_)=`''|          |:::::::::::::::::::::}     ``ー''"
-=   / /⌒\.\ ||  ||   !       '、:::::::::::::::::::i >>ID:ds7xgK/t0
  / /    > ) ||   ||   '、 `-=''''フ'ー''ヽ、::::::::::/ヽ、-─-、,,-'''ヽ
 / /     / /_||_ || _.\_/     ヽ--く   _,,,..--┴-、 ヽ
 し'     (_つ ̄(_)) ̄ (.)) ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄ (_)) ̄(.))   \>

89 :名無しさん@お腹いっぱい。:2007/03/15(木) 01:51:30 ID:01aqA7n6O
過去の類似スレの総集編みたいなスレだな。

なんで毎回同じ話をコピペするわけ?

90 :名無しさん@お腹いっぱい。:2007/03/15(木) 01:56:58 ID:/20QNIll0
ロケットガールでλ計算を熱く語るおっさんが出てきたがこれって燃える物なの?

91 :名無しさん@お腹いっぱい。:2007/03/15(木) 02:23:29 ID:G9NvniZw0
>>89
2chで何言ってんだw

92 :名無しさん@お腹いっぱい。:2007/03/15(木) 07:26:39 ID:03piNePF0







            過去スレ・コピペスレ







93 :名無しさん@お腹いっぱい。:2007/03/17(土) 11:54:15 ID:Gp6MxBj/0
ラムダ計算はどういう応用や研究に役立ちそうでしょうか?
関数型言語の基礎になっているようですが,その他の可能性はありますか?


94 :名無しさん@お腹いっぱい。:2007/03/17(土) 12:58:31 ID:e+/D4orH0
フーリエ積分だって十分条件しか与えられてないだろ

95 :名無しさん@お腹いっぱい。:2007/03/17(土) 20:26:24 ID:YOmlrM/Q0
>>93
機械語をラムダ計算に翻訳して分析したりとかいう研究の話を聞いたことがある

96 :名無しさん@お腹いっぱい。:2007/03/21(水) 15:42:28 ID:L3+1hhWQ0
応用は自分で考えてくれい
そこまで聞くようじゃ意味なかろう。

上の方に釣りっぽいおっさんが粘ってたけどさw

97 :名無しさん@お腹いっぱい。:2007/03/21(水) 19:28:58 ID:rx1TrOAK0
ある意味、現代の論理学はほぼすべてλ計算。
http://www.google.com/search?q=%E3%82%AB%E3%83%AA%E3%83%BC+%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89
まあ「ほぼすべて」は言い過ぎかもしれんが。


98 :名無しさん@お腹いっぱい。:2007/03/21(水) 20:03:06 ID:+fDuJToY0
低学歴乙

99 :名無しさん@お腹いっぱい。:2007/03/21(水) 20:04:28 ID:+fDuJToY0
> 現代の論理学

妄想乙

100 :名無しさん@お腹いっぱい。:2007/03/26(月) 15:04:04 ID:Yg450B7BO
あるいみ来るべき論理学はすべてλ計算

101 :名無しさん@お腹いっぱい。:2007/03/26(月) 21:08:37 ID:s9dS2YJO0
ほう、だったら「私は菊の花を生ける」をラムダ式で書いてみてください

102 :名無しさん@お腹いっぱい。:2007/03/27(火) 12:40:41 ID:Sxduj1iD0
> あるいみ来るべき論理学はすべてλ計算

糞スレ立てスパが妄想全開になっちゃってるな

103 :名無しさん@お腹いっぱい。:2007/03/28(水) 00:57:57 ID:13BXxGxF0
素人の素朴な疑問。
   0 = λfx.x
   1 = λfx.fx
   2 = λfx.f(fx)
   3 = λfx.f(f(fx))
という話はよく見るんだけど、負の数とか小数とかはどうやってあらわすの?

104 :名無しさん@お腹いっぱい。:2007/03/28(水) 00:59:21 ID:13BXxGxF0
素人の素朴な疑問。
   0 = λfx.x
   1 = λfx.fx
   2 = λfx.f(fx)
   3 = λfx.f(f(fx))
という話はよく見るんだけど、負の数とか小数とかはどうやってあらわすの?

105 :名無しさん@お腹いっぱい。:2007/03/28(水) 01:08:12 ID:RHA7BU4i0
負の数は(符号(真理値で実装), 絶対値)の組で、
小数は(整数部, 小数部)の組で、
それぞれ表せる。


…素人の素朴な考えだけど。

106 :名無しさん@お腹いっぱい。:2007/03/28(水) 20:53:07 ID:lfG0kx2b0
整数は自然数のペアにするほうが普通かな。
まあどっちでも大して変わんないと思う。

有理数なら整数のペアにするのがよくある手だけど、小数はあんまり見ないな。
浮動小数点とか、やればできるはずだけど使い道がないのかも。

107 :名無しさん@お腹いっぱい。:2007/04/01(日) 21:48:05 ID:uqJTKNGY0
でも、いまだに理論計算機科学の共通言語はλ計算なんだろ?

108 :名無しさん@お腹いっぱい。:2007/04/01(日) 23:26:52 ID:sJWe+qKl0
どうでもいいが、スレタイがラムダ項になってることに今気付いた。

109 :名無しさん@お腹いっぱい。:2007/04/02(月) 22:51:34 ID:QfWKFBp10
>>101
普通にFωあたりで
「_は_を生ける」をP : * -> * -> *
「_は_の花」をQ : * -> * -> *として
(P 私 a) × (Q a 菊)じゃ駄目?
∃a.とかつけてもいいけど。
命題だからλ式(証明)じゃなくて型なわけだが。
なんか論理学的に深い問題がある話だったりする?


110 :名無しさん@お腹いっぱい。:2007/05/06(日) 05:52:39 ID:+O439kON0
量子λ計算について教えてください。

111 :名無しさん@お腹いっぱい。:2007/05/08(火) 07:32:48 ID:tpSFEYo+O
なにそれ

112 :名無しさん@お腹いっぱい。:2007/05/17(木) 10:31:00 ID:CivwlhID0
直訳してググれ
http://www.google.com/search?q=quantum+lambda-calculus

113 :名無しさん@お腹いっぱい。:2007/08/11(土) 16:58:21 ID:rHg7wKqb0
λ式で文字列型ってどうやって表現するんですか?

114 :名無しさん@お腹いっぱい。:2007/08/11(土) 23:47:18 ID:UNwzvzRr0
>>113
整数のリストとか

115 :名無しさん@お腹いっぱい。:2007/08/12(日) 06:09:15 ID:iEvaVrJy0
├ e : N^* (Nは自然数の集合)って感じですか?

116 :名無しさん@お腹いっぱい。:2007/08/12(日) 20:11:05 ID:YoiYsya60
それって ├ e : string と書くのと変わらん気がする

117 :名無しさん@お腹いっぱい。:2007/08/13(月) 00:02:47 ID:vTa4QSRp0
>>106
小数っていうのは、表記の差異に過ぎないかもしれないね。
実数まで範囲を広げて考えてみると、いろいろ深い内容が見えてくるようなのだが、
残念ながら俺はまだ十分に理解できていない。
PCFで実数を扱う話題だとか、いろいろあるみたいだが。

>>116
そのstringという型を、標準的な算術の入った型体系だけで考えると、いろいろ面白いかも。


118 :名無しさん@お腹いっぱい。:2007/08/13(月) 01:06:42 ID:duuVQcq10
実数は非可算無限個あるから、本質的に表現不可能だと思う
ただ実数の中でも、代数的数だけなら可算無限個しかないから、
λ計算で表現できそう

あと比較的最近の論文で、http://homepages.cwi.nl/~tromp/cl/LC.ps
にリストを表現する方法として、任意のP, Q, Rに対して
<P, Q, ..., R> ≡ λz . z P Q ... R
なんていうのがあった
この場合は型無しの話になるけど、文字列"P Q ... R"を表現できるんじゃないかな

119 :名無しさん@お腹いっぱい。:2007/08/13(月) 21:23:59 ID:Kf4SK00H0
PCF で実数って、計算可能解析の話?

120 :名無しさん@お腹いっぱい。:2007/08/13(月) 21:47:40 ID:vTa4QSRp0
>>119
別にその話に限定するつもりはなかった。
俺は詳細を知らないが、PCFで実数というとcomputable analysisの話になりがちなの?

121 :名無しさん@お腹いっぱい。:2007/08/13(月) 22:08:03 ID:Kf4SK00H0
いや、詳しいことはぜんぜん知らないけどなんとなくそうかなって思っただけ

122 :名無しさん@お腹いっぱい。:2007/09/28(金) 04:04:06 ID:xu52pyjv0
Yf=f(Yf)を満たす
不動点オペレータYの
導出の仕方がわかりません

Y=λf.(λx.f(xx))(λx.f(xx))とすれば
Yf=f(Yf)となるのは確かめられるのですが・・・

123 :名無しさん@お腹いっぱい。:2007/09/28(金) 11:25:18 ID:yHi56D3f0
>>122
関数をもらって関数を返す関数 f が与えられたとき gx=f(xx) とすると
gg=f(gg) なので gg=fix.f となる。
g=λx.f(xx) から fix.f=(λx.f(xx))(λx.f(xx)) と書け、f を抽象すると Y が出る。

と、昔書いた自分用メモに書いてあった。
なんでこんな g が出てくるのかというとまあいろいろややこしいのだが。

124 :名無しさん@お腹いっぱい。:2007/09/28(金) 11:43:39 ID:yHi56D3f0
ここにあった
ttp://d.hatena.ne.jp/sumii/20051203

125 :名無しさん@お腹いっぱい。:2008/01/09(水) 12:26:03 ID:FpU+9RPo0
保守


126 :名無しさん@お腹いっぱい。:2008/01/09(水) 20:55:15 ID:5rdOQWTT0
>>113
単純に自然数でいいのでは。
ASCIIなりUTF-8なりお好みのencodingでの文字列のメモリ上のイメージを
そのまま符号無し整数で解釈すれば1対1対応すると思う。たぶん。

127 :名無しさん@お腹いっぱい。:2008/01/11(金) 21:49:33 ID:N5y4LcIa0
>>124
sumii

これだけで誰だかわかったww

128 :名無しさん@お腹いっぱい。:2008/01/18(金) 20:49:28 ID:c/ULHqOA0
このスレのほとんどのことはスマリヤンの "To Mock a Mockingbird" に書いてあります。Yについては "Little Schemer" を読んだら簡単に導出できます。

129 :名無しさん@お腹いっぱい。:2008/01/19(土) 17:10:15 ID:9Nk3Kf9T0
C++のテンプレートみたいに、コンパイル時に型や値について任意の計算を許すような体系はありますか?
例えば、パラメータ多相だけじゃなくて、「型引数がintならこの実装、それ以外ならこの実装」のような分岐を行ないたいです。

130 :名無しさん@お腹いっぱい。:2008/03/26(水) 19:48:57 ID:R1JkK1Rr0
haskell

131 :名無しさん@お腹いっぱい。:2008/04/22(火) 06:56:52 ID:vPfSVsQA0
圏論でCCCについて詳しく載っている参考書等を
教えていただけませんか
英語でも構いません

132 :名無しさん@お腹いっぱい。:2008/04/22(火) 10:52:23 ID:ymUV2OpA0
>>131
Lambek and Scott

133 :名無しさん@お腹いっぱい。:2008/04/23(水) 07:17:07 ID:GpN6by4A0
>>132
ありがとうございました
Introduction to Higher-Order Categorical Logicですね
今度、探してみます

134 :名無しさん@お腹いっぱい。:2008/10/28(火) 07:06:23 ID:SpD1aKye0
schemaを十二分に使うのに
λ計算って数学的にどこまで知っていればいいの?

135 :名無しさん@お腹いっぱい。:2008/10/28(火) 15:30:49 ID:4dogQ9xH0
Scheme のことだと思うが...。
名無しの関数を作るための特殊形式だと思っておけば、
ぶっちゃけ数学どうでもいい。基本的には。

136 :130.153.209.7 :2009/01/23(金) 00:50:16 ID:enbjnUxM0
ラムダ計算は,どこで役に立っているのでしょう?

137 :名無しさん@お腹いっぱい。:2009/01/25(日) 11:31:06 ID:mPO65Ll10
Haskellとか

138 :名無しさん@お腹いっぱい。:2009/03/13(金) 11:30:45 ID:9enCL1eY0
Haskellいいですね、余分なこと書かないでいいから、そこがいい。

139 :名無しさん@お腹いっぱい。:2009/03/13(金) 11:59:30 ID:9enCL1eY0
iPhoneでhugsが走る時代だからなぁ

140 :名無しさん@お腹いっぱい。:2009/04/05(日) 00:16:44 ID:mOa6uvRm0
power = λm.λn m n
がどうしても理解できません。これを使ってもうまく計算できません。誰か助けてください。。。

141 :名無しさん@お腹いっぱい。:2009/04/05(日) 13:30:26 ID:4mtktBWD0
それだけではこたえようがない

142 :名無しさん@お腹いっぱい。:2009/04/05(日) 21:25:06 ID:mOa6uvRm0
power c2 c3 →* c2 c3 = λs.λz.s(s z) c3 → λz.c3(c3 z)
までは出来るのですが、
λz.c3(c3 z) = λz.λs.λz.s(s(s z)) (c3 z) → λs.λz.s(s(s c3 z))
とすると、先に進めなくなってしまうような気がして困っています。。。
λz.c3(c3 z)のzをsに変えてλs.c3(c3 s)とすると、うまく計算できてc9が出るのですが、
そういうことをしていいのかよく分かりません。。。

>>140を書き込んでから、今日一日考えてここまでは出せました。

143 :名無しさん@お腹いっぱい。:2009/04/05(日) 21:49:52 ID:o0IgqX6G0
λz.c3(c3 z)
= λz. ((c3) (c3 z)) ← かっこ付けただけ。>>142だとここで間違って(λz. (c3)) (c3 z)になってる。
= λz. ((λs.λz.s(s(s z))) (c3 z)) ← 最初のc3を展開

ここで、sに(c3 z)を代入するんだけど、(c3 z)のzは外側のzだったのに、単純に代入するとλz. (λz.(c3 z)((c3 z)((c3 z) z)))になって内側のzになっちゃうので、先に内側のzをwに名前を変える(α変換)

= λz. ((λs.λw.s(s(s w))) (c3 z)) ← α変換
= λz. (λw.(c3 z)((c3 z)((c3 z) w))) ← sに(c3 z)を代入

あとはc3を展開してけば、wにzを9回適用する関数になるはず。



144 :名無しさん@お腹いっぱい。:2009/04/05(日) 22:24:38 ID:mOa6uvRm0
>>143
wにzを9回適用する関数になりました。ありがとうございますm(_ _)m
んー自分はまだまだ見方が甘いというか、本質を捉えきれてないみたいです。

145 :名無しさん@お腹いっぱい。:2009/05/23(土) 16:40:59 ID:TUjdIdIZ0
CPS変換がよくわかりません
何かいい参考文献ありますでしょうか

特に関数適用のCPS変換式(plotkin)はCPS(M N) = λk.M (λm.N (λn.(m n) k))
この時いくつかやってみると
M=λab.a,N=λa.aの時 CPS(MN)=λkbmn.mnk MN=λab.b
M=λab.a,N=λxy.yxの時 CPS(MN)=λkbmy.y (λn.m n k) MN=λabc.cb
M=λa.a a,N=λxyz,xz(yz)の時 CPS(MN)=λkyz.z (y z) k (k (y z)) MN=λabc.bc(abc)
となり、MNとCPS(MN)はぱっと見、単純な相関はないように見えます
等価変換に毛が生えた程度だと思っていたので
よくわからなくなりました


146 :名無しさん@お腹いっぱい。:2009/05/24(日) 14:18:37 ID:sgei56PuO
アクセス規制中なんで詳しく書けないけど、
CPS(x) = λk. k x
CPS(λx. M) = λk. k (λx. CPS(M))
CPS(M N) = λk. CPS(M) (λm. CPS(N) (λn. (m n) k))
だよ。

参考文献は他の人にまかせた。


147 :名無しさん@お腹いっぱい。:2009/05/25(月) 20:22:46 ID:POzhZa420
ありがとう。ちゃんと書いてなくて悪かったのですが一応その定義式は知っていて、
他2式に比べて関数適用のCPS変換だけ単純には見えないので取り上げました

(f g) xという式は
(λx1. (f (λx2. (g (λ x3. ((x2 x3) (λ x4. (x (λ x5. ((x4 x5) x1))))))))))
というように変換されるわけですが
f gを逆η変換してλa.f g a、これにxを与えれば
(λa.f g a) x(ただしaはf gのどちらからもfree)
これは元のf(g x)と等価だと思います
CPS変換なので他2式と同様にしてholeを入れて
λb.(b ((λa.f g a) x))とでもすればCPS変換式を得た、のようには
いかないのでしょうか
これと上の長ったらしい式を比べるとかなり印象が違うので

148 :名無しさん@お腹いっぱい。:2009/05/29(金) 20:27:59 ID:+z1JFlBwO
>>145
CPS(λx. M)はλk. k (λx. M)ではなく、λk. k (λx. CPS(M))。
(M N)も同じように再起的にN MをCPS変換する必要がある。
それをちゃんとやって、λ式の簡約を丁寧にやれば、>>145の例はM NとCPS(M N) (λx. x)は等価になるよ。


149 :名無しさん@お腹いっぱい。:2009/05/30(土) 19:21:39 ID:OrHYnlf90
>>148
ああ、確かに!
自分で定義式を知ってると言っておきながら
>>145では再帰的には適用してませんね
もう一度計算しなおしてみます。ありがとうございました!

150 :名無しさん@お腹いっぱい。:2009/06/03(水) 13:03:48 ID:OogE7GXX0
λ-calculusにおいてnormal order reduction(leftmost-outermost reduction)が
正規化戦略(normalizing reduction strategy)であることの証明を知りたいんですが
Webで見つかる資料で、証明が載ってるものってありますかね
一般のTRSでは(Orthogonal TRSですら)normal orderは正規化戦略ではないそうなので
その違いがどこから来るのかが知りたいのですが

151 :名無しさん@お腹いっぱい。:2009/06/05(金) 19:03:24 ID:91YJOkBH0
>>148
sabry and felleisen(p11)を参考にschemeでFischerのCPS変換を実装してみました
参考文献:変換式はほぼ146のものと同じです
ttp://www.ccs.neu.edu/scheme/pubs/lfp92-sf.ps.gz

12ページに簡約例が載っており
F[((lx.x) y)]=λk.((λk.(k λk.λx.((λk.kx) k)))
(λm.((λk.ky)
(λn.((m k) n)))))
自作コードの出力は
(λk .((λx1 .(x1 (λk x .((λx2 .(x2 x)) k))))
(λm .((λx3 .(x3 y))
(λn .((m k) n))))))
この場合はλx.xを作用させるとちゃんとyになります
しかし、>>145の例をCPS変換してβ簡約したものは以下のようになり
(λx1 .(x1 (λx2 x3 .(x2 (λx4 x5 .(x4 x5))))))
(λx1 .(x1 (λx2 x3 .(x2 (λx4 x5 .(x4 (λx6 x7 .((x7 x6) x5))))))))
(λx1 .(x1 (λx2 x3 .(x2 (λx4 x5 .((x3 (λx6 .(x4 (λx7 x8 .((x5 (λx9 .((x6 (λx10 .((x9 x7) x10))) x8))) x8)))))x5))))))
λx.xを作用させても元の式には一致しません
具体的な計算例を他に知らないのですが
もし何かご存じでしたら教えて頂けないでしょうか

152 :名無しさん@お腹いっぱい。:2009/07/16(木) 00:07:33 ID:Osr2so3B0
大学で情報工学を学んだけれど、ラムダ計算なんてしたことがない
これって、まずいですか?

153 :名無しさん@お腹いっぱい。:2009/07/18(土) 16:47:32 ID:ydVwiaP30
>>152
それが普通だと思います

154 :名無しさん@お腹いっぱい。:2009/07/18(土) 17:52:40 ID:3BC677EM0
>>152
それは、お前さんの出た学科のカリキュラムが弱かったと言わざるを得ない。
関数型言語を扱う講義か何かでラムダ計算の基礎は教えて欲しいところ。
大体講義2回分もあれば十分だし。

155 :名無しさん@お腹いっぱい。:2009/07/26(日) 18:14:55 ID:3COIhkEK0
ラムダ計算で
(λxy.(y(xxy)))(λxy.(y(xxy)))
以外の不動点演算子ってありますか?色々考えたけど思いつきません。

156 :名無しさん@お腹いっぱい。:2009/07/26(日) 18:45:57 ID:sxVpjgi00
不動点演算子は無限にあるよ

英語版のwikiにいくつかのってる。
Yk = (L L L L L L L L L L L L L L L L L L L L L L L L L L)
L = λabcdefghijklmnopqstuvwxyzr. (r (t h i s i s a f i x e d p o i n t c o m b i n a t o r))


157 :名無しさん@お腹いっぱい。:2009/07/26(日) 18:54:10 ID:3COIhkEK0
ありがとう

な、なんじゃこりゃあ・・・
もっと分かりやすい奴はないんでしょうか・・・?
英語版のwikiですか、見てみます。

158 :名無しさん@お腹いっぱい。:2009/07/26(日) 20:40:06 ID:/IvZO/fF0
pedia

159 :名無しさん@お腹いっぱい。:2009/07/27(月) 01:27:15 ID:RfPn8qbw0
>>156
それ有名なやつだな。宿題か何かで出たが、初めて見たときに驚いた。

160 :名無しさん@お腹いっぱい。:2009/07/27(月) 12:22:46 ID:fOo27lsc0
rの順番も修正した版もどっかでみたよ

161 :名無しさん@お腹いっぱい。:2009/08/03(月) 18:44:55 ID:vQYTOl1h0
流れを変えて済まないと思うのですが、λ計算における実数の取り扱いについて一つ思ったことを。

僕が見た資料では自然数nはzにsをn回作用させることで表現しています。
n = s(s(s(...s(z)...)))
これで表現できる自然数の数は?、つまり可算無限個なわけです。
すると、同じ可算無限個である整数や有理数はこれと似た手法で表現できることが予測されます。
が、実数の数は?、非可算無限個なわけで、同じ手法で表現できそうにはありません。
つまり何が言いたいかというと、実数をλ計算で表現するには全く別の方法が必要であるということです。
そこで提案なのですが、λ式の集合の数については言及されてないことから?以上の個数であると仮定し、実数zを次のように定義してはどうでしょうか?
z = λx.z
という再帰的な定義です。(再帰的な定義はいけないという文章を見かけたことはありますが、ここではよしとします)
例を挙げるならば
π = λx.π
などです。
さて、この再帰的な定義による実数で計算を行うことを考えます。
例として一番簡単な足し算はどうなるでしょうか?
pre+ = λy.(入力にyを足したλ式に変換するλ式)
+ = λx.(pre+ x)
pre+に入力できるλ式は非可算無限個ですから、pre+が出力できるλ式の数も非可算無限個
とすると+が出力できるλ式も非可算無限個になり、これで実数の足し算が可能になるわけです。
問題点はpre+は非可算無限個の入力に対して非可算無限回の比較を行わなくてはならない点でしょうか。
それができるならば完璧な定義だと思うのですが、皆さんどう思いますか?

162 :名無しさん@お腹いっぱい。:2009/08/03(月) 18:47:27 ID:vQYTOl1h0
すいません、アレフを書きこんだら?に変換されちゃいました。
一個目の?はアレフ0、二個目はアレフ、三個目もアレフと解釈してください

163 :名無しさん@お腹いっぱい。:2009/08/03(月) 20:58:02 ID:T3i/bak30
>>161
結局何がしたいのかよくわからないなあ。λ計算で表現したいというけど

> z = λx.z

この = がλ式として同じという意味なら、そんなのを許した時点で
普通のλ計算から逸脱してるよね。

164 :名無しさん@お腹いっぱい。:2009/08/03(月) 21:59:52 ID:vQYTOl1h0
>>163
ご意見ありがとうございます。
z = λx.zはzを簡約化したらλx.zになるということを示したかったのですが、確かによく考えたらλ計算から逸脱していますね。
僕の思い違いでした。
やりたいのはλ計算で実数を表したかっただけなのですが、もしかして不可能なんでしょうか?
(つまりλ式全ての集合の要素数は可算無限個しかない?)

λ計算で実数を表すことが不可能という定理が存在することをお知りになっている方がおられましたら教えていただけないでしょうか?
その逆、λ計算で実数を表すことが可能という定理が存在する場合にも同様に教えていただけないでしょうか?

165 :名無しさん@お腹いっぱい。:2009/08/04(火) 00:15:21 ID:ni/oiWa50
164です

>>164の疑問を考えていたのですが、一つの答えが出ました。
http://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97
によると、λ計算はチューリングマシンと等価な数理モデルです。
つまりチューリングマシンでできることはλ計算ででき、チューリングマシンでできないことはλ計算でできません。
完全チューリングマシンは実数を扱うことができません。
よってλ計算は実数を扱うことができません。
q.e.d.

この証明は合ってるでしょうか?

以下補足
公理的集合論では実数よりも多くの要素を扱えます。
しかしλ計算では実数以上の要素を扱えません。
よってλ計算を基礎として数学を作る事は不可能です。

166 :名無しさん@お腹いっぱい。:2009/08/04(火) 00:42:10 ID:m0rcM/ks0
>>165
無理数を扱う時にTMが停止しないことに言及した方がいいけど、
まあいいんじゃないの。

167 :名無しさん@お腹いっぱい。:2009/08/04(火) 11:01:16 ID:ni/oiWa50
165です

>>166
TMが停止しないということについては、非可算無限個の数字で表される無理数を可算無限個の数字で表すことができない為だ、と理解しています。(証明にはなってませんが)

λ計算の限界がちらりと見えたようなのでなんだかすっきりしました、ありがとうございます。
これで安心してλ計算の勉強を進めることができます。
λ計算の勉強が終わったら次はトポスあたりに手を出してみましょうか

168 :名無しさん@お腹いっぱい。:2009/08/04(火) 21:22:19 ID:n+aV3xNy0
>>165
正直なところ、それで何かを証明したようには見えないな。

> 完全チューリングマシンは実数を扱うことができません。

この主張の正確な意味は?

169 :名無しさん@お腹いっぱい。:2009/08/05(水) 01:04:50 ID:rpl+0u4T0
情報板には滅多に来ないんだが久々に見たらこんなスレが立ってたんだ。

>>167
165の「証明」を見るとλ計算の「能力」の意味がλ計算をどの立場で使うかによって違うという事を理解してないんじゃないの?
トポスとか先走るのもいいけどBarendregtでもじっくり読んでλ計算ちゃんと勉強したら?

ついでに言えば165の意味で「実数をλで扱えない」事なんて全く自明だよ。
可算個の記号から成る可算列全ての集合は可算集合に過ぎないので、
有限な長さのが、一方、実数全体は非可算集合だから
有限な長さのλ項全ての集合も可算集合(但し、変数の集合は当然ながら可算集合とする)。
一方、実数全体は非可算集合を成すので、個々の実数に対して1:1で表現するλ項の作り方は存在しない。
(ほとんどの実数…それらはRでルベーグ測度1の部分集合を成す…はλ項やTMのテープ上の記号列としては表現不可能)
任意の異なる2つの実数に対して異なるλ項を割り当てる方法が存在しない以上、
実数に関する等号演算をλ計算では定義しようがないので、λ計算では実数を完全な形では扱えない。
【証明終わり】

>>166
> >>165
> 無理数を扱う時にTMが停止しないことに言及した方がいいけど、

これは即断過ぎる。
単に165の証明での全く工夫のないナイーブな実数の表現方法(素直に2進展開をテープ上の記号列で表す方法)の場合だけに成り立つ話で一般性はない。

例えば2の平方根は無理数だが、これをTMがちゃんと停止する形で扱う事は可能。
(つまり2の平方根の代数的性質による記号操作で処理すれば良い)

だから原理的には全ての代数的数をTMで扱えるようにはできるだろうし、
超越数でもπとかeとかのような代数的性質で特徴づけ可能な「素直な超越数」ならば
各々の代数的性質に基づく操作に帰着して処理すれば良い。

170 :名無しさん@お腹いっぱい。:2009/08/05(水) 10:53:46 ID:AJcBtZQx0
165です。

>>169
エレガントで本質を突いた証明ありがとうございます。
全ての実数を扱うことはできないがπやeといった限定された無理数なら扱うことができるというあたり、λ計算を基にした関数型プログラミング言語でプログラミングを行う際に参考になりそうです。

>λ計算をどの立場で使うか
僕がλ計算を勉強した一番の理由は、人間社会のモデルを作りたかったからです。
人間社会のモデルを表現する言語を模索し、その候補の一つとしてλ計算を考えたのです。
なので僕の求めているλ計算の「能力」は「人間社会のモデルを記述することができる」というものです。
(理論社会学で社会のモデルは作られているのだが、自然言語で表現しているために曖昧で分かりづらく、物理学のように数学でモデルを定義した場合に比べ発展性に乏しい)
人間社会を記述するためには、まずその構成要素となる人間を記述できなくてはなりません。
古典物理学で考えると、社会を構成する人間は実数的な存在である原子から成り立っているので、人間社会のモデルを表現するための言語は実数を表現できなくてはいけないという理由から
λ計算で実数を扱うことが可能であるかという問題に突き当りました。
(つまり人間社会は本質的な部分に実数を含む)
(量子論で考えると不確定性原理から原子が離散的な存在である可能性がある。が、そこまで考えると泥沼になりそうなので考えないw)

>Barendregtでもじっくり読んでλ計算ちゃんと勉強したら?
参考資料の御教示ありがとうございます。
ネットで調べたところBarendregtさんはλ計算の専門家のようですね、論文も書いていらっしゃるし本も書いていらっしゃる。
そして無料で読める文章もネットにアップしてらっしゃる(僕のような金なし学生には嬉しい)w
関数型プログラミング言語をおいおいやろうと思っているので、その時に参考にさせていただきます。

今の目的は人間社会のモデルを作ることなので、λ計算をじっくり勉強するよりも、λ計算をさらりと勉強してトポスの方に先走ってみようと思います。

尚、僕の使っている参考書は
清水 義夫, "圏論による論理学―高階論理とトポス", 東京大学出版会, 2007
あとはネット上で見つけた日本語の大学の授業資料とか
僕自身は物理系の大学四年生です。

171 :名無しさん@お腹いっぱい。:2009/08/05(水) 11:16:23 ID:AJcBtZQx0
170です

読み返したら誤解を招きそうなところがあったので補足します。

>実数的な存在である原子
これは原子の位置を測定して得られる結果は、三個の実数である(位置を表す三次元ベクトル)という意味です

172 :166:2009/08/05(水) 16:54:09 ID:gtOdYbeV0
>>169
まさかそんな細かいことを延々と突っ込んでくるとは。
「任意の無理数」と書けば良かったか?
大体おまいの言うように自明なことなんだから、そのくらい補完してくれよ。

173 :名無しさん@お腹いっぱい。:2009/09/21(月) 00:53:42 ID:Tvr1+9fsI
de Bruijn indexって普通に良く知られていますか?
私数学屋で計算機科学の教育を受けていないのですが、学生時代にブルバキの集合論を読んだとき束縛変数のあまりにグラフィカルな消し方に「もっと一次元的に符号化できるのでは」と感じていた違和感を解消できました。

174 :名無しさん@お腹いっぱい。:2009/09/21(月) 11:18:29 ID:QoSnJrNd0
計算機科学でも学部出ただけなら普通は知らない、ってぐらい。
計算理論専攻でないと知らないと思う。

175 :名無しさん@お腹いっぱい。:2009/09/21(月) 11:53:12 ID:Tvr1+9fsI
そうですか。
どうもありがとうございます。

せっかくなのでさらに教えて頂きたいのですが、関数型言語の実装に関わるような方にもあまり知られていないのでしょうか?


176 :名無しさん@お腹いっぱい。:2009/09/21(月) 12:15:34 ID:2oWZB7Ka0
いや、学部レベルでもラムダ計算を教えるようなまともな大学なら
こういう記法がありますよ、という程度かもしれんが、講義で言及する。

177 :名無しさん@お腹いっぱい。:2009/09/21(月) 12:34:05 ID:QoSnJrNd0
あー、最近はそうかも。

> 関数型言語の実装に関わるような方にもあまり知られていないのでしょうか?

必ず知っている、ということはない、ぐらいかな。
SKIコンビネータのほうが多分知られている。

178 :名無しさん@お腹いっぱい。:2009/09/21(月) 18:56:57 ID:Tvr1+9fsI
なるほど。
ラムダ項を知っているなら聞いたことぐらいはあるという感じですね。
どうもありがとう。

179 :名無しさん@お腹いっぱい。:2009/12/10(木) 15:46:51 ID:6ofJayyd0
SとKはコンビネータ X = λx.xKSKで表現可能

ttp://lecture-wiki.ecc.u-tokyo.ac.jp/index.php?uonoue%2FIPL_PC06

180 :名無しさん@お腹いっぱい。:2009/12/28(月) 07:35:58 ID:Oj04Yr+dO
>>109
  ∧,,∧
 ( `・ω・) ウーム…ここは?
 / ∽ |
 しー-J


181 :名無しさん@お腹いっぱい。:2009/12/30(水) 03:28:06 ID:wiNBB2eB0
unlambda大好き

182 :fhaircut:2009/12/31(木) 15:49:38 ID:avh6s8XC0
はじめまして,いろいろなモデリング,モデルタイプとユニ-クなヘマスタイルがあリます,
元日と成人の日を祝い ,贈り物を贈りますよ!
かわいい人がたくさん,方法がかんだんですよ~!
ようこそwww.fhaircut.com へ
どうぞよろしくお願いします.

183 :名無しさん@お腹いっぱい。:2009/12/31(木) 17:39:30 ID:sV11Hmlj0
文法が変だと思ってたらやっぱり逆引き不可だったか。

184 :omanko:2010/01/13(水) 13:29:52 ID:njvgHgeO0
無料
http://jbbs.livedoor.jp/otaku/12393/

185 :名無しさん@お腹いっぱい。:2010/07/08(木) 14:10:14 ID:5syAtst50
はじめまして

church数において
plus:λa b. λf x. a f (b f x)
times:λa b. λf. a (b f)
exp:λa b. b a
となりますが、これらを導出するにはどのようにすれば良いのでしょうか?

0にbをa回plusすると、timesというように出来そうな気はするのですが
具体的にどういった式変形などをすれば良いのかがわかりません。

ヒントや概略でも良いので宜しければどなたか教えて頂けると助かります。

66 KB
■ このスレッドは過去ログ倉庫に格納されています

★スマホ版★ 掲示板に戻る 全部 前100 次100 最新50

read.cgi ver 05.04.00 2017/10/04 Walang Kapalit ★
FOX ★ DSO(Dynamic Shared Object)