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

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

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

**名無しさん＠お腹いっぱい。** · 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"を表現できるんじゃないかな

**名無しさん＠お腹いっぱい。** · 2007/08/13(月) 21:23:59

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

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

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

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

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

**名無しさん＠お腹いっぱい。** · 2007/09/28(金) 04:04:06

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

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

**名無しさん＠お腹いっぱい。** · 2007/09/28(金) 11:25:18

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

**名無しさん＠お腹いっぱい。** · 2007/09/28(金) 11:43:39

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

**名無しさん＠お腹いっぱい。** · 2008/01/09(水) 12:26:03

保守

**名無しさん＠お腹いっぱい。** · 2008/01/09(水) 20:55:15

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

**名無しさん＠お腹いっぱい。** · 2008/01/11(金) 21:49:33

>>124
sumii

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

**名無しさん＠お腹いっぱい。** · 2008/01/18(金) 20:49:28

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

**名無しさん＠お腹いっぱい。** · 2008/01/19(土) 17:10:15

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

**名無しさん＠お腹いっぱい。** · 2008/03/26(水) 19:48:57

haskell

**名無しさん＠お腹いっぱい。** · 2008/04/22(火) 06:56:52

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

**名無しさん＠お腹いっぱい。** · 2008/04/22(火) 10:52:23

>>131
Lambek and Scott

**名無しさん＠お腹いっぱい。** · 2008/04/23(水) 07:17:07

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

**名無しさん＠お腹いっぱい。** · 2008/10/28(火) 07:06:23

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

**名無しさん＠お腹いっぱい。** · 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が停止しないことに言及した方がいいけど、
まあいいんじゃないの。