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

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

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

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

**名無しさん＠お腹いっぱい。** · 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
がどうしても理解できません。これを使ってもうまく計算できません。誰か助けてください。。。