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

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

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

**名無しさん＠お腹いっぱい。** · 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)を手計算で示せたりはしたのかな。
自力で計算できそうになければ、時間のあるときに計算して書き込むけれど。

長文ごめんね。

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

モナドとラムダというと computational lambda-calculus というのがありますね
聞いたことがあるだけでろくに読んでいませんが
http://www.disi.unige.it/person/MoggiE/ftp/lics89.pdf

**名無しさん＠お腹いっぱい。** · 2006/12/19(火) 16:46:45

領域理論て何のためにあるんですか？

31 · 2006/12/19(火) 23:22:17

プログラム意味論（横内）を読むのもいいかも。

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

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

**名無しさん＠お腹いっぱい。** · 2006/12/21(木) 00:53:51

>>43
輪講はやっぱりシェーンフィールドでしたか？

４２ · 2006/12/21(木) 09:22:47

質問しても誰も答えられないんだな

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

>>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)
の形になるのかもわかりません．．．

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

**名無しさん＠お腹いっぱい。** · 2006/12/23(土) 22:13:37

YF = F(YF) なんだよね。なら
Y (λgx.Sgx) = (λgx.Sgx) (Y (λgx.Sgx)) だよね。

**名無しさん＠お腹いっぱい。** · 2006/12/23(土) 22:19:07

>>46
> (\x.(\gx.(\xyz.xz(yz))gx)(xx))(\x.(\gx.(\xyz.xz(yz))gx)(xx))
変数の間は空白で区切らないといけないんでは？

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

大学の授業でやって単位も取ったけどなーんも覚えてないや。

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

>>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)
が明快な形で出てくることもない，と理解しています．

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

そんなに難しい話でもないのでは。
まず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の等式の証明は、λ項の正規形を求めることとは違うから。

**名無しさん＠お腹いっぱい。** · 2006/12/29(金) 00:55:30

実際に書いてみると、Yが不動点演算子であることの証明そのまんまだなあ。。
高橋正子が読めないのは置いておいて、米崎渡辺には不動点演算子なんかは
書いてたかどうかはっきり覚えてないんだよね。
不動点演算子Yを理解するための道筋を、今は上手く提示できない。
なにかいい方法ないかなー。

**名無しさん＠お腹いっぱい。** · 2007/01/13(土) 02:46:55

高橋（別姓を名乗ってた）も米崎も渡辺も、講義を生で聞いてた俺は勝ち組！
でも当時全く理解できなかった。
特に米崎は下手くそな英語で講義するな！

**名無しさん＠お腹いっぱい。** · 2007/01/31(水) 21:03:41

λ計算と圏論との技術的な違いは？
なんてこと聞いていいですか？

**名無しさん＠お腹いっぱい。** · 2007/02/01(木) 00:38:54

>>54
技術的な違いは知らないが、理論的な違いを説明するにはこの余白は狭すぎる

**名無しさん＠お腹いっぱい。** · 2007/02/01(木) 00:48:55

フェルマー乙

**名無しさん＠お腹いっぱい。** · 2007/02/01(木) 21:43:15

>>55
一般ユーザは理論なんかじゃなく道具がほしいわけですが。
技術的には、圏論＝λ計算＋有向グラフ　だくらいに
言えないものですか？

**名無しさん＠お腹いっぱい。** · 2007/02/01(木) 22:26:22

>>57
正確じゃない

**名無しさん＠お腹いっぱい。** · 2007/02/01(木) 23:12:57

>>58
道具として使えればよいので、正確じゃないくらいなら
気にしない。道具の見地からは、圏論＝what ?
教えてほしい。

**名無しさん＠お腹いっぱい。** · 2007/02/02(金) 10:14:46

λ計算:
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本足の恒温動物だ、というぐらいに不正確なものだけど。

**名無しさん＠お腹いっぱい。** · 2007/02/02(金) 19:52:46

>>60
早速愚問に答えてくれてありがとう。
でもそれくらいは知っているつもり。
圏論が商品だとすると、オッ使えそうだという使用説明を
聞いたことがない。ほんとに使っている人いるの？
木下さんの｢定義の正当化｣はよかったが、それでも
道具としてのよい解説はほんとにないね。

**名無しさん＠お腹いっぱい。** · 2007/02/02(金) 20:44:43

圏論は数学では有力な道具だよ。
でも圏論が有力なのは圏同値が言える場合が殆どだから
圏同値成立する2つの圏を見つけてこない限りは
情報の世界で有用だとは思えない。
俺は情報学を良く知らないから俺の認識不足かもしれないけどね

**名無しさん＠お腹いっぱい。** · 2007/02/02(金) 22:56:38

お前らまだλ計算とか圏論とか言ってるのかよ
遅れてるなー

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

**名無しさん＠お腹いっぱい。** · 2007/02/03(土) 01:49:52

>>59
ここはラムダのスレなので、ラムダの話に限れば圏論は意味論を与えるための
道具として使われてるよ、というのはどうだろう。
いくらなんでも「λ計算+有向グラフ」はありえない。
>>60も書いてるが、Haskell関係での貢献も大きいね。

**名無しさん＠お腹いっぱい。** · 2007/02/03(土) 22:03:39

>>64　レスポンスありがとう。
でも道具としても思想としてもやはりよくわからんね。
｢意味論を与えるため｣というのも本意でもなさそうだし。
わたしの場合は道具としてどう使えるかというのが
唯一の関心だが、だれかスパッと解説できないのかな？
ふつうこういう商品は売れないよ。
もともとそんなものかもしれないが。
スペンサーの形式法則みたいじゃつまらんね

**名無しさん＠お腹いっぱい。** · 2007/02/04(日) 00:17:26

>>65
道具としてという点で一つだけ挙げると、モナド関連の話がある。
Haskellなんかがそうだが、圏論のモナドを用いることによって、
副作用のあるプログラムを純粋な関数型言語で記述できるように
なった。影響の大きい仕事としては、E. MoggiのComputational
Lambdaが筆頭。
副作用を純粋な関数型言語で扱えるメリットはわかってもらえる
と思うが、こんなところでどうだろう？

**名無しさん＠お腹いっぱい。** · 2007/02/04(日) 01:10:23

>>66
モナドは不可逆という一点しか利用しておらず、圏論などと言うことはおこがましい

**名無しさん＠お腹いっぱい。** · 2007/02/04(日) 01:44:49

>> 67
(*ﾟーﾟ)/ｾﾝｾｰ
Grothendieck constructionとか、Sheafificationはどうでしょう？

**名無しさん＠お腹いっぱい。** · 2007/02/04(日) 01:46:54

>> 67
あと、Effective Toposとか。。。
ヽ( ´ ▽ ` )ノ

**名無しさん＠お腹いっぱい。** · 2007/02/04(日) 01:53:38

>> 63
>> π計算だぜ

polymorphic type system を与えて、SNになるようだったら、
π計算も大好きになれるんですけど。
deadlock freedomの十分条件を与える程度のtype systemしか
ないので、
（´・ω・`）ｼｮﾎﾞｰﾝ
です。

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

(`･ω･´) ｼｬｷｰﾝ

になるのですが。

**名無しさん＠お腹いっぱい。** · 2007/02/04(日) 04:13:58

>>67
そうですか。申し分けない。

**名無しさん＠お腹いっぱい。** · 2007/02/05(月) 12:21:40

書き込んでいる連中の研究室がなんとなくわかってきたりして。

**名無しさん＠お腹いっぱい。** · 2007/02/05(月) 12:54:02

>>72
受験生ですが、晒してくださいおねがいします＞＜

**名無しさん＠お腹いっぱい。** · 2007/02/07(水) 21:02:30

>>70
πでも型でSNはできなくもない。
ftp://ftp.dcs.qmw.ac.uk/lfp/kohei/pi-sn-journal.ps.gz
とか。かなり無理矢理だけど。

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

**名無しさん＠お腹いっぱい。** · 2007/02/09(金) 01:15:12

ラムダ計算のいいSolved Problem付き教科書ってない？
英語の奴でいいからさ。
型付まで網羅されてるとうれすぃ。

**名無しさん＠お腹いっぱい。** · 2007/02/09(金) 17:14:36

>>72
声が大きい人がいるような気がする。

**名無しさん＠お腹いっぱい。** · 2007/02/09(金) 17:23:42

気のせいだよ。
この分野やってる人は思ったより少なくないからね。

**名無しさん＠お腹いっぱい。** · 2007/02/10(土) 15:02:45

ちっ
良スレかよ。

**名無しさん＠お腹いっぱい。** · 2007/02/11(日) 20:37:05

>>77
ラムダ計算の研究やってる人は少いだろうね。

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

**名無しさん＠お腹いっぱい。** · 2007/03/14(水) 19:07:26

>>6
>>11
お前、本当に愛い奴だ。
そうやって、何年も前に２chで教えてもらった参考書を
一体何年間ネタとして使いまわしてるんだよｗ

**名無しさん＠お腹いっぱい。** · 2007/03/14(水) 19:08:17

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

ぷ

**名無しさん＠お腹いっぱい。** · 2007/03/14(水) 19:10:16

>31
ほほう。大きく出たな。
高橋研に問い合わせてみようかｗ

**名無しさん＠お腹いっぱい。** · 2007/03/14(水) 19:11:34

>>43
おやおや、amazonのレビューを「狂ってる」と言われた後で
またまた・・・

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

ぷ

**名無しさん＠お腹いっぱい。** · 2007/03/14(水) 19:12:24

>>63
おじちゃん乙

**名無しさん＠お腹いっぱい。** · 2007/03/14(水) 19:12:57

>>72
お前のｼﾞｻｸｼﾞｴﾝはいつも判りやすいなぁ

ぷ · 2007/03/14(水) 19:26:16

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

**名無しさん＠お腹いっぱい。** · 2007/03/14(水) 19:29:24

なんてったっけ？
哲学板やν速で暴れてたｸｿｽﾚ立て
あいつだな。

**名無しさん＠お腹いっぱい。** · 2007/03/15(木) 01:10:45

すみませんすぐ片付けますんで。
.　　　　　　　∧＿∧　
　　　　　　　（；´Д｀）　
　　-=≡ 　/　　　ヽ　　　　　　,.-'''"-─ `ー,--─'''''''''''i-､,,
.　　　　　 /|　|　　 |. |　　　　,.-,/　　　　　　 /::::::::::::::::::::::!,,　　＼
　-=≡　/.　＼ヽ／＼＼_　（　 ,'　　　　　 i:::::::::::::::::::::;ﾉ　ヽ-､,,/''ー'''"7
　　　　/　　　ヽ⌒)==ヽ_）=`''|　　　　　 |:::::::::::::::::::::}　　　　　｀`ー''"
-= 　 /　/⌒＼.＼　||　　|| 　 !　　　　　　　'､:::::::::::::::::::i >>ID:ds7xgK/t0
　　／／　　　 >　） || 　 || 　 '､　`-=''''フ'ー''ヽ、::::::::::/ヽ､-─-､,,-'''ヽ
　/　/ 　　　　/ ／＿||＿ ||　＿.＼＿／　　　　ヽ--く　　 _,,,..--┴-､ヽ
　し'　　　　　（＿つ￣(_））￣ (.)）￣￣￣￣￣￣￣￣ (_））￣(.)）　　＼>

**名無しさん＠お腹いっぱい。** · 2007/03/15(木) 01:51:30

過去の類似スレの総集編みたいなスレだな。

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

**名無しさん＠お腹いっぱい。** · 2007/03/15(木) 01:56:58

ロケットガールでλ計算を熱く語るおっさんが出てきたがこれって燃える物なの？

**名無しさん＠お腹いっぱい。** · 2007/03/15(木) 02:23:29

>>89
2chで何言ってんだｗ

**名無しさん＠お腹いっぱい。** · 2007/03/15(木) 07:26:39

　　　　　　　　　　　　過去スレ・コピペスレ

**名無しさん＠お腹いっぱい。** · 2007/03/17(土) 11:54:15

ラムダ計算はどういう応用や研究に役立ちそうでしょうか？
関数型言語の基礎になっているようですが，その他の可能性はありますか？

**名無しさん＠お腹いっぱい。** · 2007/03/17(土) 12:58:31

フーリエ積分だって十分条件しか与えられてないだろ

**名無しさん＠お腹いっぱい。** · 2007/03/17(土) 20:26:24

>>93
機械語をラムダ計算に翻訳して分析したりとかいう研究の話を聞いたことがある

**名無しさん＠お腹いっぱい。** · 2007/03/21(水) 15:42:28

応用は自分で考えてくれい
そこまで聞くようじゃ意味なかろう。

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

**名無しさん＠お腹いっぱい。** · 2007/03/21(水) 19:28:58

ある意味、現代の論理学はほぼすべてλ計算。
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
まあ「ほぼすべて」は言い過ぎかもしれんが。

**名無しさん＠お腹いっぱい。** · 2007/03/21(水) 20:03:06

低学歴乙

**名無しさん＠お腹いっぱい。** · 2007/03/21(水) 20:04:28

> 現代の論理学

妄想乙

**名無しさん＠お腹いっぱい。** · 2007/03/26(月) 15:04:04

あるいみ来るべき論理学はすべてλ計算

**名無しさん＠お腹いっぱい。** · 2007/03/26(月) 21:08:37

ほう、だったら「私は菊の花を生ける」をラムダ式で書いてみてください

**名無しさん＠お腹いっぱい。** · 2007/03/27(火) 12:40:41

> あるいみ来るべき論理学はすべてλ計算

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

**名無しさん＠お腹いっぱい。** · 2007/03/28(水) 00:57:57

素人の素朴な疑問。
　　　0 = λfx.x
　　　1 = λfx.fx
　　　2 = λfx.f(fx)
　　　3 = λfx.f(f(fx))
という話はよく見るんだけど、負の数とか小数とかはどうやってあらわすの？

**名無しさん＠お腹いっぱい。** · 2007/03/28(水) 00:59:21

素人の素朴な疑問。
　　　0 = λfx.x
　　　1 = λfx.fx
　　　2 = λfx.f(fx)
　　　3 = λfx.f(f(fx))
という話はよく見るんだけど、負の数とか小数とかはどうやってあらわすの？

**名無しさん＠お腹いっぱい。** · 2007/03/28(水) 01:08:12

負の数は(符号(真理値で実装), 絶対値)の組で、
小数は(整数部, 小数部)の組で、
それぞれ表せる。

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

**名無しさん＠お腹いっぱい。** · 2007/03/28(水) 20:53:07

整数は自然数のペアにするほうが普通かな。
まあどっちでも大して変わんないと思う。

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

**名無しさん＠お腹いっぱい。** · 2007/04/01(日) 21:48:05

でも、いまだに理論計算機科学の共通言語はλ計算なんだろ？

**名無しさん＠お腹いっぱい。** · 2007/04/01(日) 23:26:52

どうでもいいが、スレタイがラムダ項になってることに今気付いた。

**名無しさん＠お腹いっぱい。** · 2007/04/02(月) 22:51:34

>>101
普通にFωあたりで
「_は_を生ける」をP : * -> * -> *
「_は_の花」をQ : * -> * -> *として
(P 私 a) × (Q a 菊)じゃ駄目？
∃a.とかつけてもいいけど。
命題だからλ式（証明）じゃなくて型なわけだが。
なんか論理学的に深い問題がある話だったりする？

**名無しさん＠お腹いっぱい。** · 2007/05/06(日) 05:52:39

量子λ計算について教えてください。

**名無しさん＠お腹いっぱい。** · 2007/05/08(火) 07:32:48

なにそれ

**名無しさん＠お腹いっぱい。** · 2007/05/17(木) 10:31:00

直訳してググれ
http://www.google.com/search?q=quantum+lambda-calculus

**名無しさん＠お腹いっぱい。** · 2007/08/11(土) 16:58:21

λ式で文字列型ってどうやって表現するんですか？

**名無しさん＠お腹いっぱい。** · 2007/08/11(土) 23:47:18

>>113
整数のリストとか

**名無しさん＠お腹いっぱい。** · 2007/08/12(日) 06:09:15

├ e : N^* （Nは自然数の集合）って感じですか？

**名無しさん＠お腹いっぱい。** · 2007/08/12(日) 20:11:05

それって ├ e : string と書くのと変わらん気がする

**名無しさん＠お腹いっぱい。** · 2007/08/13(月) 00:02:47

>>106
小数っていうのは、表記の差異に過ぎないかもしれないね。
実数まで範囲を広げて考えてみると、いろいろ深い内容が見えてくるようなのだが、
残念ながら俺はまだ十分に理解できていない。
PCFで実数を扱う話題だとか、いろいろあるみたいだが。

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

**名無しさん＠お腹いっぱい。** · 2007/08/13(月) 01:06:42

実数は非可算無限個あるから、本質的に表現不可能だと思う
ただ実数の中でも、代数的数だけなら可算無限個しかないから、
λ計算で表現できそう

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