5ちゃんねる ★スマホ版★ ■掲示板に戻る■ 全部 1- 最新50  

■ このスレッドは過去ログ倉庫に格納されています

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

1 :名無しさん@お腹いっぱい。:2006/12/08(金) 00:45:53 ID:fx6EeyNJ0
λ計算について議論しましょう.
とりあえず,λ計算の基本から,各種関数型言語との関係,さらには研究ネタ
まで,λ計算に関係の深い話題ならなんでも OK ということで.


2 :名無しさん@お腹いっぱい。:2006/12/08(金) 00:47:18 ID:fx6EeyNJ0
どなたかβ変換の基本について教えてください.
(λ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

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


3 :2:2006/12/08(金) 00:50:16 ID:fx6EeyNJ0
すいません,書き忘れました.

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

4 :名無しさん@お腹いっぱい。:2006/12/08(金) 01:11:53 ID:gqCTHlyc0
> (λx.x)((λx.x)x)
> ^^^^^^^
> ->((λx.x)x)((λx.x)x)
いくらなんでもこの簡約はありえないだろ常識的に考えて。。。

5 :名無しさん@お腹いっぱい。:2006/12/08(金) 01:30:41 ID:fx6EeyNJ0
>>4
ぐはぁ,ホントだ...
早速ありがとうございました.

6 :名無しさん@お腹いっぱい。:2006/12/08(金) 01:49:33 ID:fx6EeyNJ0
日本語英語を問わず,初学者向けに基礎から解説している文献があったら
教えていただけませんか? アマゾンの書評を見て,

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

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


7 :名無しさん@お腹いっぱい。:2006/12/08(金) 03:10:37 ID:dVua0loM0
>>6
コンピュータサイエンス入門の紫のやつ

8 :名無しさん@お腹いっぱい。:2006/12/08(金) 09:11:50 ID:fx6EeyNJ0
>>7
Scheme を題材にした SICP のことでしょうか?
(http://jargon.net/jargonfile/p/PurpleBook.html)
だとすると,Church number は扱っていますが, Church-Rosser
の定理などは扱っていないので,これだけではλ計算の勉強には
不十分に思えます.
それとも別の本のことですか?

9 :名無しさん@お腹いっぱい。:2006/12/08(金) 09:46:08 ID:gqCTHlyc0
>>6
高橋正子が無理なら渡辺米崎のがいいよ。
『計算論入門』渡辺治 米崎直樹 日本評論社 2100円

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

10 :名無しさん@お腹いっぱい。:2006/12/08(金) 11:36:11 ID:dVua0loM0
>>8
違う違う
http://www.amazon.co.jp/gp/product/4000050060

11 :6:2006/12/08(金) 15:42:05 ID:Fpcw2EMX0
>>9
ありがとうございます.
ググってみると他でも評判が良さそうなので,買ってみます.

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

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

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


12 :名無しさん@お腹いっぱい。:2006/12/08(金) 18:37:48 ID:ZwUUWqVu0
>>11
そのレビュワーおかしいな。
ラムダ計算に関して、そこに挙げられている3冊はいずれも
『コンピュータサイエンス入門』よりも難しいぜ。

13 :名無しさん@お腹いっぱい。:2006/12/08(金) 21:39:21 ID:ZvDwNqoe0
最初の入り口なら、googleで検索してどっかの大学の
講義資料のPDFを読んだほうがいいんじゃないか。
参考文献もそこに書いてあるでしょ。

14 :名無しさん@お腹いっぱい。:2006/12/08(金) 23:01:13 ID:CD77k6tS0
>>6
Henk Barendregt, “Lambda Calculi with Types”,
available from: ttp://www.cs.ru.nl/~henk/papers.html

ところで Hindley & Seldin の新版が出るという話があるけど、マダァ-? (・∀・ )っ/凵⌒☆チンチン

15 :名無しさん@お腹いっぱい。:2006/12/09(土) 00:16:33 ID:M4mrgYq60
>>11
とりあえず面白そうだというのが動機ということでいいかな。
ただ、λ計算の勉強がプログラミングの役に立つということには肯定的になれない。
λ計算が必要になる方向は山ほどあるが、例えば>>14のBarendregtのようなのは王道。

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

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

16 :6:2006/12/09(土) 13:01:14 ID:sjo5ErmH0
>>12
なるほど,そうですか.
アマゾンにはなさそうなので,探してみます.

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

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

はい.

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

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

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

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

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

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

17 :名無しさん@お腹いっぱい。:2006/12/09(土) 18:58:19 ID:+9XAEm1x0
>「コンピュータサイエンス入門―アルゴリズムとプログラミング言語」

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

18 :名無しさん@お腹いっぱい。:2006/12/09(土) 20:28:48 ID:Pfl1+DBh0
型付ラムダ計算と型付でないラムダ計算に本質的な違いってあるの?

19 :名無しさん@お腹いっぱい。:2006/12/09(土) 20:43:58 ID:o7ud+6Zb0
あります

20 :名無しさん@お腹いっぱい。:2006/12/09(土) 20:45:40 ID:o7ud+6Zb0
>>18
たとえば、型なしでラッセルのパラドックスをどう説明する?

21 :名無しさん@お腹いっぱい。:2006/12/09(土) 21:05:05 ID:Pfl1+DBh0
なるほどレスどうも。
ところで、型付でないラムダ計算の世界にも
カリー・ハワードの対応は存在しますか?

22 :名無しさん@お腹いっぱい。:2006/12/09(土) 21:06:58 ID:o7ud+6Zb0
>>21
もちろん

23 :名無しさん@お腹いっぱい。:2006/12/09(土) 21:19:58 ID:Pfl1+DBh0
型なしラムダ計算の型付けってどういうことなんですか。
もしそれができるなら、すべてのラムダ計算は型付である
と考えてしまっていいのでしょうか。

24 :名無しさん@お腹いっぱい。:2006/12/09(土) 22:15:24 ID:NzjU++XC0
なにか間違ってないか。

25 :名無しさん@お腹いっぱい。:2006/12/09(土) 22:29:17 ID:Pfl1+DBh0
どこかおかしいですか。当方初心者ゆえご教示ねがいます。

26 :名無しさん@お腹いっぱい。:2006/12/09(土) 22:58:50 ID:M4mrgYq60
>>16
まずは個人のことに関する質問に答えてくれてありがとう。
これで少しは質問にも答えやすくなると思う。

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


27 :6:2006/12/11(月) 11:28:27 ID:FDDBt+TK0
>>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))
だと思います.


28 :名無しさん@お腹いっぱい。:2006/12/11(月) 22:11:45 ID:RLHBhv8f0
Yが不動点演算子であることを考えると、(4)でGは(λgx.Sgx)の不動点になるように
定義してあるんだよね。
だから(3)のように(λgx.Sgx)をGに適用したら、Gが返ってくるようになってる。
もしかしたら不動点演算子が何をしているのかよくわかってないのかも。
定理2.12の意味がわかりにくいのかな。

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

29 :名無しさん@お腹いっぱい。:2006/12/12(火) 01:12:08 ID:CcSGY4sH0
>>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)
という解が求まった。という手順。

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

30 :6:2006/12/12(火) 20:40:46 ID:j/nvRo2a0
>>28
>もしかしたら不動点演算子が何をしているのかよくわかってないのかも。
>定理2.12の意味がわかりにくいのかな。

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

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

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

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

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

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


31 :名無しさん@お腹いっぱい。:2006/12/15(金) 18:19:27 ID:YruGzNNfO
自分は大昔、高橋正子研にいたことがある。
ラムダ計算で分かんないことがあったら教授してもいいよ。

32 :名無しさん@お腹いっぱい。:2006/12/16(土) 02:53:58 ID:J33ulpYB0
女に質問なんかできるか

33 :名無しさん@お腹いっぱい。:2006/12/16(土) 16:31:33 ID:wXiS3cZ70
>>32
腐ったエサに釣られおってからに。

34 :名無しさん@お腹いっぱい。:2006/12/18(月) 19:49:55 ID:/KHo9KCp0
>>31
おお,それは素晴らしい.
ではせっかくなので...
条件分岐や再帰(繰り返し)はλ計算で表現できそうだ,というのは
なんとなくわかるんですが,逐次実行というのはλ計算ではどうい
うものに相当するんでしょうか? 逐次実行なんていうのはλ計算に
は存在しない?

35 :名無しさん@お腹いっぱい。:2006/12/18(月) 19:54:31 ID:qp+mM75v0
>>34
実行ってなに?ww

36 :名無しさん@お腹いっぱい。:2006/12/18(月) 20:47:46 ID:2cGaSwLx0
CPS変換とかモナドとか?

37 :名無しさん@お腹いっぱい。:2006/12/18(月) 21:43:51 ID:/KHo9KCp0
>>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 変換って,λ計算の枠組みの中に含まれてるんでしょうか?

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

38 :名無しさん@お腹いっぱい。:2006/12/18(月) 22:01:24 ID:V7rk4+Pv0
値呼びλ計算だとよくこんな感じでやってるよね>逐次実行
(dはe2に自由な出現を持たない変数)

e1;e2 ≡ (λd.e2) e1



39 :名無しさん@お腹いっぱい。:2006/12/18(月) 22:10:11 ID:qp+mM75v0
>>37
基本的にラムダ計算には実行の概念はありません。
というのも、計算にI/Oなるものは存在しないからです。

40 :名無しさん@お腹いっぱい。:2006/12/19(火) 00:57:15 ID:+qnJ1mPk0
>>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)を手計算で示せたりはしたのかな。
自力で計算できそうになければ、時間のあるときに計算して書き込むけれど。

長文ごめんね。

41 :名無しさん@お腹いっぱい。:2006/12/19(火) 12:39:29 ID:2cG7e0aK0
モナドとラムダというと computational lambda-calculus というのがありますね
聞いたことがあるだけでろくに読んでいませんが
http://www.disi.unige.it/person/MoggiE/ftp/lics89.pdf

42 :名無しさん@お腹いっぱい。:2006/12/19(火) 16:46:45 ID:6z03Pwwj0
領域理論て何のためにあるんですか?

43 :31:2006/12/19(火) 23:22:17 ID:psf7CPmq0
プログラム意味論(横内)を読むのもいいかも。

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

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

44 :名無しさん@お腹いっぱい。:2006/12/21(木) 00:53:51 ID:0w/HJ1im0
>>43
輪講はやっぱりシェーンフィールドでしたか?

45 :42:2006/12/21(木) 09:22:47 ID:TNnO14/x0
質問しても誰も答えられないんだな

46 :名無しさん@お腹いっぱい。:2006/12/23(土) 17:12:53 ID:hnglVPuq0
>>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)
の形になるのかもわかりません...

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


47 :名無しさん@お腹いっぱい。:2006/12/23(土) 22:13:37 ID:443fv80m0
YF = F(YF) なんだよね。なら
Y (λgx.Sgx) = (λgx.Sgx) (Y (λgx.Sgx)) だよね。

48 :名無しさん@お腹いっぱい。:2006/12/23(土) 22:19:07 ID:443fv80m0
>>46
> (\x.(\gx.(\xyz.xz(yz))gx)(xx))(\x.(\gx.(\xyz.xz(yz))gx)(xx))
変数の間は空白で区切らないといけないんでは?

49 :名無しさん@お腹いっぱい。:2006/12/23(土) 23:58:05 ID:tGpE9bcF0
大学の授業でやって単位も取ったけどなーんも覚えてないや。

50 :名無しさん@お腹いっぱい。:2006/12/24(日) 12:09:47 ID:CQ9FSVwv0
>>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)
が明快な形で出てくることもない,と理解しています.


51 :名無しさん@お腹いっぱい。:2006/12/29(金) 00:32:18 ID:FQrEwVjt0
そんなに難しい話でもないのでは。
まず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の等式の証明は、λ項の正規形を求めることとは違うから。

52 :名無しさん@お腹いっぱい。:2006/12/29(金) 00:55:30 ID:FQrEwVjt0
実際に書いてみると、Yが不動点演算子であることの証明そのまんまだなあ。。
高橋正子が読めないのは置いておいて、米崎渡辺には不動点演算子なんかは
書いてたかどうかはっきり覚えてないんだよね。
不動点演算子Yを理解するための道筋を、今は上手く提示できない。
なにかいい方法ないかなー。

25 KB
■ このスレッドは過去ログ倉庫に格納されています

★スマホ版★ 掲示板に戻る 全部 前100 次100 最新50

read.cgi ver 05.04.00 2017/10/04 Walang Kapalit ★
FOX ★ DSO(Dynamic Shared Object)