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

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

どなたかβ変換の基本について教えてください．
(λ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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

はい．

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

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

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

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

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

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

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

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

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

あります

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

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

>>21
もちろん

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

なにか間違ってないか。

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

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

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

>>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))
だと思います．

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

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

>>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)
という解が求まった。という手順。

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

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

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

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

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

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

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

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

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

女に質問なんかできるか

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

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

>>34
実行ってなに？ww

CPS変換とかモナドとか?

>>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 変換って，λ計算の枠組みの中に含まれてるんでしょうか?

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

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

e1;e2 ≡ (λd.e2) e1

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

>>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)を手計算で示せたりはしたのかな。
自力で計算できそうになければ、時間のあるときに計算して書き込むけれど。

長文ごめんね。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

フェルマー乙

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

>>57
正確じゃない

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

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

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

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

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

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

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

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

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

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

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

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

>> 63
>> π計算だぜ

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

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

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

になるのですが。

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

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

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

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

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

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

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

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

ちっ
良スレかよ。

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

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

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

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

ぷ

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

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

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

ぷ

>>63
おじちゃん乙

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

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

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

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

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

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

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

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

　　　　　　　　　　　　過去スレ・コピペスレ

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

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

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

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

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

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

低学歴乙

> 現代の論理学

妄想乙

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

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

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

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

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

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

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


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

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

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

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

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

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

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

なにそれ

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

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

>>113
整数のリストとか

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

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

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

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

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

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

PCF で実数って、計算可能解析の話？

>>119
別にその話に限定するつもりはなかった。
俺は詳細を知らないが、PCFで実数というとcomputable analysisの話になりがちなの？

いや、詳しいことはぜんぜん知らないけどなんとなくそうかなって思っただけ

Yf=f(Yf)を満たす
不動点オペレータYの
導出の仕方がわかりません

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

>>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 が出てくるのかというとまあいろいろややこしいのだが。

ここにあった
ttp://d.hatena.ne.jp/sumii/20051203

保守

>>113
単純に自然数でいいのでは。
ASCIIなりUTF-8なりお好みのencodingでの文字列のメモリ上のイメージを
そのまま符号無し整数で解釈すれば1対1対応すると思う。たぶん。

>>124
sumii

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

このスレのほとんどのことはスマリヤンの "To Mock a Mockingbird" に書いてあります。Ｙについては "Little Schemer" を読んだら簡単に導出できます。

C++のテンプレートみたいに、コンパイル時に型や値について任意の計算を許すような体系はありますか？
例えば、パラメータ多相だけじゃなくて、「型引数がintならこの実装、それ以外ならこの実装」のような分岐を行ないたいです。

haskell

圏論でＣＣＣについて詳しく載っている参考書等を
教えていただけませんか
英語でも構いません

>>131
Lambek and Scott

>>132
ありがとうございました
Introduction to Higher-Order Categorical Logicですね
今度、探してみます

schemaを十二分に使うのに
λ計算って数学的にどこまで知っていればいいの？

Scheme のことだと思うが...。
名無しの関数を作るための特殊形式だと思っておけば、
ぶっちゃけ数学どうでもいい。基本的には。

ラムダ計算は，どこで役に立っているのでしょう？

Haskellとか

Haskellいいですね、余分なこと書かないでいいから、そこがいい。

iPhoneでhugsが走る時代だからなぁ

power = λm.λn m n
がどうしても理解できません。これを使ってもうまく計算できません。誰か助けてください。。。

それだけではこたえようがない

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を書き込んでから、今日一日考えてここまでは出せました。

λ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回適用する関数になるはず。

>>143
wにzを9回適用する関数になりました。ありがとうございますm(_ _)m
んー自分はまだまだ見方が甘いというか、本質を捉えきれてないみたいです。

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)はぱっと見、単純な相関はないように見えます
等価変換に毛が生えた程度だと思っていたので
よくわからなくなりました

アクセス規制中なんで詳しく書けないけど、
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))
だよ。

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

ありがとう。ちゃんと書いてなくて悪かったのですが一応その定義式は知っていて、
他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変換式を得た、のようには
いかないのでしょうか
これと上の長ったらしい式を比べるとかなり印象が違うので

>>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)は等価になるよ。

>>148
ああ、確かに！
自分で定義式を知ってると言っておきながら
>>145では再帰的には適用してませんね
もう一度計算しなおしてみます。ありがとうございました！

λ-calculusにおいてnormal order reduction(leftmost-outermost reduction)が
正規化戦略(normalizing reduction strategy)であることの証明を知りたいんですが
Webで見つかる資料で、証明が載ってるものってありますかね
一般のTRSでは(Orthogonal TRSですら)normal orderは正規化戦略ではないそうなので
その違いがどこから来るのかが知りたいのですが

>>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
それが普通だと思います

>>152
それは、お前さんの出た学科のカリキュラムが弱かったと言わざるを得ない。
関数型言語を扱う講義か何かでラムダ計算の基礎は教えて欲しいところ。
大体講義2回分もあれば十分だし。

ラムダ計算で
(λxy.(y(xxy)))(λxy.(y(xxy)))
以外の不動点演算子ってありますか？色々考えたけど思いつきません。

不動点演算子は無限にあるよ

英語版の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))

ありがとう

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

pedia

>>156
それ有名なやつだな。宿題か何かで出たが、初めて見たときに驚いた。

rの順番も修正した版もどっかでみたよ

流れを変えて済まないと思うのですが、λ計算における実数の取り扱いについて一つ思ったことを。

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

すいません、アレフを書きこんだら?に変換されちゃいました。
一個目の?はアレフ0、二個目はアレフ、三個目もアレフと解釈してください

>>161
結局何がしたいのかよくわからないなあ。λ計算で表現したいというけど

> z = λx.z

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

>>163
ご意見ありがとうございます。
z = λx.zはzを簡約化したらλx.zになるということを示したかったのですが、確かによく考えたらλ計算から逸脱していますね。
僕の思い違いでした。
やりたいのはλ計算で実数を表したかっただけなのですが、もしかして不可能なんでしょうか？
（つまりλ式全ての集合の要素数は可算無限個しかない？）

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

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.

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

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

>>165
無理数を扱う時にTMが停止しないことに言及した方がいいけど、
まあいいんじゃないの。

165です

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

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

>>165
正直なところ、それで何かを証明したようには見えないな。

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

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

情報板には滅多に来ないんだが久々に見たらこんなスレが立ってたんだ。

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

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

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

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

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

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

165です。

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

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

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

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

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

170です

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

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

>>169
まさかそんな細かいことを延々と突っ込んでくるとは。
「任意の無理数」と書けば良かったか？
大体おまいの言うように自明なことなんだから、そのくらい補完してくれよ。

de Bruijn indexって普通に良く知られていますか？
私数学屋で計算機科学の教育を受けていないのですが、学生時代にブルバキの集合論を読んだとき束縛変数のあまりにグラフィカルな消し方に「もっと一次元的に符号化できるのでは」と感じていた違和感を解消できました。

計算機科学でも学部出ただけなら普通は知らない、ってぐらい。
計算理論専攻でないと知らないと思う。

そうですか。
どうもありがとうございます。

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

いや、学部レベルでもラムダ計算を教えるようなまともな大学なら
こういう記法がありますよ、という程度かもしれんが、講義で言及する。

あー、最近はそうかも。

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

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

なるほど。
ラムダ項を知っているなら聞いたことぐらいはあるという感じですね。
どうもありがとう。

SとKはコンビネータ X = λx.xKSKで表現可能

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

>>109
　 ∧,,∧
　( `･ω･)　ｳｰﾑ…ここは？
　/　∽ |
　しー-Ｊ

unlambda大好き

はじめまして，いろいろなモデリング,モデルタイプとユニ-クなヘマスタイルがあリます，
元日と成人の日を祝い ，贈り物を贈りますよ！
かわいい人がたくさん，方法がかんだんですよ~！
ようこそwww.fhaircut.com へ
どうぞよろしくお願いします.

文法が変だと思ってたらやっぱり逆引き不可だったか。

無料
http://jbbs.livedoor.jp/otaku/12393/

はじめまして

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というように出来そうな気はするのですが
具体的にどういった式変形などをすれば良いのかがわかりません。

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