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

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

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

**名無しさん＠お腹いっぱい。** · 2008/10/28(火) 15:30:49

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

130.153.209.7 · 2009/01/23(金) 00:50:16

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

**名無しさん＠お腹いっぱい。** · 2009/01/25(日) 11:31:06

Haskellとか

**名無しさん＠お腹いっぱい。** · 2009/03/13(金) 11:30:45

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

**名無しさん＠お腹いっぱい。** · 2009/03/13(金) 11:59:30

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

**名無しさん＠お腹いっぱい。** · 2009/04/05(日) 00:16:44

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

**名無しさん＠お腹いっぱい。** · 2009/04/05(日) 13:30:26

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

**名無しさん＠お腹いっぱい。** · 2009/04/05(日) 21:25:06

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

**名無しさん＠お腹いっぱい。** · 2009/04/05(日) 21:49:52

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

**名無しさん＠お腹いっぱい。** · 2009/04/05(日) 22:24:38

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

**名無しさん＠お腹いっぱい。** · 2009/05/23(土) 16:40:59

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

**名無しさん＠お腹いっぱい。** · 2009/05/24(日) 14:18:37

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

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

**名無しさん＠お腹いっぱい。** · 2009/05/25(月) 20:22:46

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

**名無しさん＠お腹いっぱい。** · 2009/05/29(金) 20:27:59

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

**名無しさん＠お腹いっぱい。** · 2009/05/30(土) 19:21:39

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

**名無しさん＠お腹いっぱい。** · 2009/06/03(水) 13:03:48

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

**名無しさん＠お腹いっぱい。** · 2009/06/05(金) 19:03:24

>>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を作用させても元の式には一致しません
具体的な計算例を他に知らないのですが
もし何かご存じでしたら教えて頂けないでしょうか

**名無しさん＠お腹いっぱい。** · 2009/07/16(木) 00:07:33

大学で情報工学を学んだけれど、ラムダ計算なんてしたことがない
これって、まずいですか？

**名無しさん＠お腹いっぱい。** · 2009/07/18(土) 16:47:32

>>152
それが普通だと思います

**名無しさん＠お腹いっぱい。** · 2009/07/18(土) 17:52:40

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

**名無しさん＠お腹いっぱい。** · 2009/07/26(日) 18:14:55

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

**名無しさん＠お腹いっぱい。** · 2009/07/26(日) 18:45:57

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

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

**名無しさん＠お腹いっぱい。** · 2009/07/26(日) 18:54:10

ありがとう

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

**名無しさん＠お腹いっぱい。** · 2009/07/26(日) 20:40:06

pedia

**名無しさん＠お腹いっぱい。** · 2009/07/27(月) 01:27:15

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

**名無しさん＠お腹いっぱい。** · 2009/07/27(月) 12:22:46

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

**名無しさん＠お腹いっぱい。** · 2009/08/03(月) 18:44:55

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

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

**名無しさん＠お腹いっぱい。** · 2009/08/03(月) 18:47:27

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

**名無しさん＠お腹いっぱい。** · 2009/08/03(月) 20:58:02

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

> z = λx.z

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

**名無しさん＠お腹いっぱい。** · 2009/08/03(月) 21:59:52

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

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

**名無しさん＠お腹いっぱい。** · 2009/08/04(火) 00:15:21

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.

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

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

**名無しさん＠お腹いっぱい。** · 2009/08/04(火) 00:42:10

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

**名無しさん＠お腹いっぱい。** · 2009/08/04(火) 11:01:16

165です

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

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

**名無しさん＠お腹いっぱい。** · 2009/08/04(火) 21:22:19

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

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

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

**名無しさん＠お腹いっぱい。** · 2009/08/05(水) 01:04:50

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

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

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

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

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

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

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

**名無しさん＠お腹いっぱい。** · 2009/08/05(水) 10:53:46

165です。

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

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

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

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

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

**名無しさん＠お腹いっぱい。** · 2009/08/05(水) 11:16:23

170です

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

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

**166** · 2009/08/05(水) 16:54:09

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

**名無しさん＠お腹いっぱい。** · 2009/09/21(月) 00:53:42

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

**名無しさん＠お腹いっぱい。** · 2009/09/21(月) 11:18:29

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

**名無しさん＠お腹いっぱい。** · 2009/09/21(月) 11:53:12

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

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

**名無しさん＠お腹いっぱい。** · 2009/09/21(月) 12:15:34

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

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

あー、最近はそうかも。

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

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

**名無しさん＠お腹いっぱい。** · 2009/09/21(月) 18:56:57

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

**名無しさん＠お腹いっぱい。** · 2009/12/10(木) 15:46:51

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

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

**名無しさん＠お腹いっぱい。** · 2009/12/28(月) 07:35:58

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

**名無しさん＠お腹いっぱい。** · 2009/12/30(水) 03:28:06

unlambda大好き

**fhaircut** · 2009/12/31(木) 15:49:38

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

**名無しさん＠お腹いっぱい。** · 2009/12/31(木) 17:39:30

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

**omanko** · 2010/01/13(水) 13:29:52

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

**名無しさん＠お腹いっぱい。** · 2010/07/08(木) 14:10:14

はじめまして

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

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