#副作用という言葉は注意が必要。主作用vs副作用という構図を考えると、main-effect vs side-effect ということかな。それじゃ main-effect と side-effect の違いは？
#副作用と聞くと、まず最初に連想するのは、クスリですね
#クスリとも笑えない（と連想する）
#主作用とか副作用とか、そういうところで分離する認識はよくない。全部 Arrow で書けばいいんじゃね？（極論）
#作用の上に作用を作らず、作用の下に作用を作らず - 福沢諭吉
#main-effect は意図した効果、side-effect はプログラマが意図しない効果。
#一般に意図した効果は善で、意図しない効果は悪。
#Haskell というか、型付けの強い関数型言語では、型でプログラマの意図や意思を書くんですよ、それは同意しますよね
#だから、型で書いてるんだから、意図しないとか出てこないんです。そんなものは書けない。Haskell ではね。
#一方、World はある個人の意図なんて知ったこっちゃない、なにもかもが縁でつながっていて、山火事のようにすばやく動き、山のように静かにたたずんでいる。
#Haskell は Real World に寄り添いたい、と思っているのであって、Real World と同じ力を持ちたいとは思っていないはずです。
#ここまではimperativeプログラマともコンセンサスがとれる？
#unsafeX とかそういう邪悪なものまで入れるのは、Haskell が頑張りすぎてますが、まあいいです
#imperative とか関係ないです。この世界をどう認識しているかによると思います
#哲学の議論にすりかえているわけではないです
#だって、プログラムは、コンピュータと接続されている小さな世界にしか影響できないから。
#その小さな世界の認識論は、すなわち、プログラマの認識論です
#imperativeプログラマ曰く、入出力するなら副作用がある、Haskellは入出力する、だからHaskellには副作用がある。
#そう言いたい。言いたい人をぼくは許容します。そう言うのはおかしい。そう言う人も僕は許容します。どちらも、同じことです。
#人というのは、矛盾を言っても大丈夫なように作られていますし、矛盾を言われても大丈夫なように作られています
#一方、type system はそうはいかない
#副作用と Haskell というテーマを語るなら、まず SF をわかりましょう、というのが僕の提案です
#SF は Science Fiction であり、Signal Function in reactive functional programming であり、Stupid Functional です！
#Science Fiction ?
##同様に、とても曖昧な「副作用」
#副作用のあるなしのどちらの立場をとるにせよ、世界をどのように、あるいは世界との関係をどのように認識するかの違いでしかない。ではそれはどのように違っているのかを同時に説明しないことが問題？
#禅問答をわかってない人は、同時に説明されたら「どっちやねん！」と脊髄反射すると思います。思い切りどついたれ
#あ、いけがみは極論しか言わないうえに、禅で物事を言うので、傍から見るとあたまおかしいですが、実際あたまおかしいですが、やさしさは保っています
#まさに「どっちやねん」と言われているところです :)
#「万物一切無」（すべてのものはない）とでも教えてあげると、そのひとは一つ馬鹿になるので、よい行いです
#頭で考えるのは、設計とか実装
#理念とか、言葉の意味とかは頭で考えちゃダメ、ゼッタイ。
#ところで、「純粋な」(曖昧につかってます)λ計算で、church numeral の比較というのはできるのでしょうか。そもそも意味がないのでしょうか。
#意味があって意味がない
#同型。でも違うように見える。
#両方の目を開けていなければダメです
#で、目を閉じて、心の中にひとつになって見えてなければダメです
#禅は、「よし」ということはめったにないので、ダメばっかりで、本当にすみません。まあお茶でも飲んだらいいんじゃない
#今日はあいにくの雨だから、傘も持たずに外を歩いて、冬とはこんなに暖かいものなのかと、体のなかからぽかぽかしてきたよ、とそういうことしたいな(体力ないので無理なのが本当に残念だ
#まあ、ぶぶでもすすることにしまひょ。
#子供のときには、何も考えずにそういうことができた。親は風邪ひくでしょって止めたけど。どちらの気持ちもよくわかる。
#定数(=データ構成子)のない世界で同値ということは意味がない？そもそも値とはなにのこと？
#自分で定義すれば
#と、突き放すのも禅なんです。その愛情をわかってほしい
#どんな人も、人であって知りたいと思う人は、知ります
#自分の中に答えは最初から入っているのを気がつかない、そういう人が、知りたいと思うんです。なんかもやもやしているのを、自分の中に感じ取っているから。
#体に矢がささっているとき、どこからその矢が飛んできたのかを探すのは滑稽です、すぐに医者に行って、抜いてもらいましょう
#根は同じなんだけど、なぜ？というより、どう説明すると納得できるかが重要だと感じています。でもせっかちなので、他人の説明を聞きたいというわけです。他力も本願 :)
#それを言われると弱いんだよねー。禅は３つのことしかやらない「自分で考えろ馬鹿」「休憩して自然を見ろ」「座禅を組んで心を空にしろ」
#ことば、はいちばん禅が苦手とするところだ。だからださくて誰も見向きもしない
#こういう話になるからHaskellは難しいと言われる:)
#well-educated な人か、あるいは何も知らないが元気の良い子供相手にしか向いてないからね、Haskell は
#むしろ、圏をもちださなかっただけ、偉いとほめてほしいところだ
#数学や教養まで身につくなんて、これほど素晴らしいプログラミング言語はみたことがない
#で、馬鹿だからもうわすれちゃったんだけど、nobsun の知りたいことはなんだっけ
#Haskellは、λ計算を計算の基礎におく
#現代のフォンノイマン計算機は、チューリング機械に計算の基礎をおく
#λ計算とチューリング機械は同等
#Haskellは現代のフォンノイマン計算機上のプログラミング言語と同等の計算記述力がある
#むちゃくちゃ大雑把にこんな議論があるとおもうんだけど。
#Haskellを型付定数付のλ計算に還元できるという主張にはなんとなくそうだろうなぁと思えるのだけど。
#じゃあ型付定数付きのλ計算を純粋なλ計算に還元できるという感覚がつかめていない。
#どうするんだろう。というのが直近の疑問。
#自然な疑問だと思います
#しかも、中間言語は strict なんだよね
#non-strict で書いていたと思っていたら、いつのまにか strict になっていた、何を言ってるんだとわからないかもしれないが(略
#non-strictとstrictとの違いにしても、なぜそれが問題になるかというと、簡約を直列にやるという暗黙の前提があるわけですよね。
#暗黙というか、Haskell 処理系の実装の一手法ですよね
#実装が意味に暗黙に含まれる？
#難しいのは命令男が命令男の言葉でHaskellを説明しろというからです。Haskellは、あるがままをうけいれればいいだけののに。(極論)
#nobsun が質問してる、還元の話と簡約の話は、Haskell 処理系の実装のこととしか、僕には見えないのです
#> cut-sea
#ああなんかちゃんと理解していないので、うまく表現できなくてもどかしい。
#ああ、わかりました
#ぼく、研究所やめるので、タイムインターメディアにいれてください。給料は格安でいいです
#それだったら、なんでもわかることになるんじゃないかな
#？？
#具体的な会社名を出すのはまずかったか。言いたかったことは、nobsun と cut-sea さんが議論している場所は、きっと職場だと思ったので、
#その職場に僕も入れてよ、ってことだけです
#人事権ないのかもしれないけど
#ああ。cut-seaはタイムインターメディアいまはタイムインターメディアには行ってないんですほとんど
#勘違いでしたか、大変すみません
#cut-seaはタイムインターメディアにいますが、私は今はほとんど行っていないんです。
#ここで喋ると、もれなく twitter がついてくるので、そこらへんはくれぐれも慎重にね
#そうでしたね。
#どんどん先にながしてしまおう。ネット上の発言はけっしてとりけせないので。。。orz
#いや、そっちに振ったのは私です。申し訳のないことをしました
#twitter ボットには、削除 API をつけてもらいたいな
#フォンノイマンの計算機はチューリング機械でシミュレートできそうですが、型付定数付λ計算はどのように純粋λ計算でシミュレートできのか想像できないということです。
#おおたしかに。
#> 削除API
##削除 API は、文頭で del last n とかがいいんじゃないかなあ
#で、この文が消えますが、本当によろしいですか、といったん聞いて
#こまけぇことはいいんだよ、ぽち。と押すと消える
##うーん、でもChatonそのものもログ残りますよ >all
#まあChatonの場合、データは私のサーバにあるので手動で消せないことはないですが。
#いや、そこまでは要求しないのですが
#Twitter には RT というおかしな習慣が根付いてしまったので…
#まあ、ここでも、人の噂は千里を走るといいますから、おなじことですが、そのスピードが違うだけです
# ／）
／／／）
／,.=ﾞ''"／
／ i f ,.r='"-‐'つ＿＿＿_ こまけぇこたぁいいんだよ！！
/ / _,.-‐'~／⌒ ⌒＼
／ ,i ,二ﾆ⊃（ ●）. （●）＼
/ ﾉ ilﾞフ::::::⌒（__人__）⌒::::: ＼
,ｲ｢ﾄ､ ,!,!| |r┬-| |
/ iﾄヾヽ_/ｨ"＼ `ー'´ ／
#わかりました、すみません、ほんとうにすみません、わたしのようなものが、こんなことをいって、ほんとうにすみません(サッ
#kazuさん訳のプログラミングHaskell読み終わったんだけど、確かに簡単に思えてくるから不思議だ。
#@cut-sea なにが簡単に思えましたか。いままで難しいとおもったことですか。きょうみつんつん。
#粘着ぎみに、むしかえしですが、純粋λ計算ではゼロはλf.λx.x １はλf.λx.f xとかやるんですよね。True は λx.λy.x False は λx.λy.y だと。そこまではいいんですが、TrueとかFalseを返すような述語の自明ではない具体例ってなにかあるんでしょうか？
#いや、そもそもあの範囲で難しいと思ったところがなかったということなのよ。
#それどういうこと？ってのは記憶にないの。
#確か唯一13章の論証のところで1パラグラフほど何回か読みなおしたけど、その程度で、いずれにせよHaskellは難しいという印象はなかったのね。
#ちょっとした工夫として、こう読みますと言ってるところが出てきますよね。
#正確なところを忘れたので書かないけど<-はこう読むとか>>=はこう読むとか。
#「そして」とかだったかな > (>>=)
#それがこの本の範囲では少なくとも違和感なくて、すっきりイメージできる
#どこに出てきてもその読み方（とらえ方）が通用するのが良い。
#継続のときもそうだったんだけど、よく難しいと言うんだけど、実は難しいのではなくて単に自分の理解しているほかの概念とのすり合わせとかができてないだけってのはあると思うんですよ。
#分かってみると、あーなんだ、こういうことだったのか。で、何を難しいと思ってたんだっけ？みたいなのって実はそういうものなのかなって少し思ったりした。
#つまり継続も今にして思えばそれ自体は難しい概念ではなくて、自分の脳内にある他の概念の何とどう結び付くか距離とか位置がまるで把握できなかったから脳内で宙ぶらりんだっただけなのかなってね。
#typeclassopediaではあまり特定のメタファに頼らない方がよいみたいな話があって、ファンクタはいずれファンクタとして分かるようになるみたいなことが書いてあったけど
#でもね、とっかかりとしてのメタファってのは、やっぱり私みたいな人間には重要。
#数学とかだとAはBのこと
#とか不明な言葉だけからでも関係を理解できる人間はいいんだろうけど
#私には「そして」と読むと理解できるよみたいな既知の概念とのマッピングは非常に分かった気になれる
#それがtypeclassopediaに書いてあるように不正確だったとしても、とっかかりになるのよ
#みんなモナドという円を完全な円として説明しようとするけど、それによって私はいつまでたっても理解のとっかかりができないでいるとして
#あるとき、正六角形を示されて、こんな形だととりあえず思えば？みたいに教えてもらったらすんなり受け入れられるとか。
#それが不正確でも正六角形というベースがあれば、そこからじょじょに修正を加えていっていずれ円に到達するんじゃんと思ってるからね、私は。
#ひとことだけ、でも直線 (Id モナド) を見せても「はぁ？」って思うでしょ
#だから、中間がどこらへんなのかなーというのは、人それぞれ違って、「ここからスタートすればわかる」ってのは背景知識によるんですよ
#そのとおり。
#だからAさんがピンとくるメタファとBさんがピンとくるメタファは違いますね
#で、私がダメなのは、正確さゆえなのですけど数学書によくある"メタファに一切頼らない説明"なのですよ
#ところで
#同じってどういうこと？って聞かれたらなんと説明しますか？>all
#僕ならすぐ言えるけど、またこいつかよ空気読めねえやつだなって言われそうだ
#どゆこと？
#いや、今日はここで、さんざん喋ったからさ
#すぐに言ってもいいのかなあ
#いや、しゃべる人と聞く人は持ちつ持たれつってことで
#ちがうか
#ひとさし指一本で足りる
#それでもいい？
#それが同じってどういうこと？についての説明？それとも今から説明が始まる？
#そう、もうはじまっている
#今からなのね。頼みます。
#キーボードから手を離して、人差し指を鼻の前、つまり顔の中心にもってきてください
#はい
#自分を指してます
#ああだめです、立てて
#立てるのかー立てました
#顔の中心においたまま適度に近づけるか遠ざけると、一本が二本に見える場所があります
#ひとさし指を見るのではなく、遠くを見よう
#ほー
#わかった？
#二本になりました
#でも、一本のひとさし指ですよね、同じってのはそういうことです。以上、お付き合いくださり、たいへんありがとう。僕も伝えることができて嬉しい。
#ふむ。面白い説明でした。
#今この話で思った点があります。
#このikegamiさんの説明はx==xは常にTrueだという法則を表現している。
#あ、それはちがう！！！！！！！！
#ちがう？
#cut-sea さんは二つの目を持っていて、適度な視力があったからこそ、二本に見えたんです
#目玉一個もらおうか
#あるいは二個もらってもいい
#常に true だなんて、とんでもない
#確かに片目つぶると1本のままだ
#じゃあ同じってのは単なる錯覚のことだ
#それも違いますよー
#:)
#そして、あってます。
#スルーするところだったけど聞き捨てならん＞常にTrueではない
#同じ、が、あたりまえ、あるいは物理的(経験的)なものについてなら、錯覚と呼んでもいいよ
#いやだから、両目をもらうって言ったんだ：常に
#手も足も出なくなったら、まだまだだ
#「それでも納得がいかん」と、こうこなくてはならない
#1本の指が2本に見えたけど、それはalias像であって元は1本のものだった
#同じとはaliasがあるから派生する概念なのかな
#cut-seaは伊東勝利とは別の像のように思ってたけど実は1人だった＞同じじゃん
#もしaliasがなければ同じという概念は生まれない？
#あるいは名前を付けることがなければ生まれない？
#xとかyとか名前を付けるから錯覚が生まれる？
#nobsun にも言ったけど、ちょっとは SF を読んだほうが人生楽しい
#パラレルワールドでは、なにもかもが、ちがう
#星新一はほぼすべて読んだ
#高校生のころ
#「どこで」同じといいたいのか、それも肝心なところだ
#そう
#でもさ
#「どこで」とか「何をもって」とかってのは
#明確にしなくても話しができるレイヤってありますよね
#ふふふ
#だからこそ話がずいぶん進んでから
#トイレに行く
#｢お前のいってる同じってどういう意味で言ってる？」となる
#私ももう少ししたら泳ぎに行かねば・・・
#「そんなもん食っちゃえば同じじゃねーか」と親父が口をすべらせる
#子供が「同じってどーゆーこと？」と聞きました
#用をすませた
#みなさんどうやって説明して納得してもらってんだろう
#私はどうやって同じの概念を獲得したのだろう？
#さて、おたちあい、トイレに行った僕、そして帰ってきた僕、このふたつの僕は同じでしょうか、それとも違うでしょうか
#名前はおなじっぽい
#この場では同じとみなす
#でもさっきから用をすませたぶんだけ体重がへってるし
#でも、用がすんだから、慌ててないよ、文 章 も ゆ っ く り タ イ プ し て い る
#常に代謝が進んでいるからなー
#あ、そろそろ移動
#同じってのはそういうもんですよ、見る角度によっては同じだったり、違ったりする（角度でも場所でもなんでもいい、そこには視点が入る）
#およいだらすっきりするでしょう、いってらっしゃい
#すんません。後で！
#いやいや、いい対話ができて、まだ生きていて良かった
#ああ、移動してたのではなしに乱入しそびれたか。
#違うものがあるから同じものがある。区別できるものがあるから、区別できないものがある。混沌だけなら違うも同じもない。
#数学を背景とするなら、合同関係なり同値類で割ってとか、関係代数にまで持ってけるんですけど、平易に説明ということで、こういうふうに言った
#関係を arrow とする圏にまで話をするのは、さかいさんとかとする
#でも、僕は、教えたくない人には金輪際、ひとつも教えたくないので教育免許は取りませんでした
#変化しないものがあると信じるから、変化する状態というものを考える。世界は状態をもつか？今の世界が3分まえに居た世界と同じだが景色は違うと思うから状態などというものを考えるのだ。1ナノ秒前の世界はそのときの世界であり、今とはべつものだと思えば世界に状態などなく、刹那があるだけなんだよ。
#「今」しかないです。過去や未来は、人間が名前をつけた「今」のことだと、僕らは解釈している
#さっきの「今」は通り過ぎていった、さようなら、また会おう
#とうぜん先刻のnobsunなる人物と今のnobsunなる人物は別人だ。
#この世界、割り切れるような頭の持ち主でさえ割り切ることはできないのだから、割ろうとせず、割ってくださいとも言わず、ただそれを見ればいい。見たくなかったら寝てください
#目をつぶって、象を撫でまわしたい年頃なので飽きるまでくりかえすとしよう。 :)
#nobsun は個人的に知ってるかもしれないけど、僕は本当に死にかけたし、実際なんども死ぬところをギリギリで止めた、だから、まだ生きているようだ
#あまりにも痛く、苦しかったので(24時間)、数学とか哲学は助けてくれなかった。神仏に祈っても治らなかった
#日ごろの信心が悪いのかと、あらゆる宗教書を読んだ。なにも変わらずくるしい、くるしい、そのとき
#学部のときに「漢文の素読」のつもりで買っていた本のなかに禅の本があった。これは、誰に感謝していいのかわからないが、とにかくこれ以上ないくらい感謝している
#そして僕は、まだ服薬しなきゃいけないけど、まあなんとか生きている。先生には、驚異的な回復力だと驚かれた
#まあ、お世辞なのかもしれないけど
#違うものがあるから同じものがある。区別できるものがあるから、区別できないものがある。
#その説明は==が実装できれば/=は*自動的に*実装できるということにあたると思える。
#つまり同じの説明を言い替えただけなので、今度は違うってどういうこと？となる
#同じという概念を一体どのくらいの年頃に獲得したのか忘れたけど
#x==xはtrueとか x==yがtrueならy==xもtrueでx==yがfalseならy==xもfalseとか
#そういう法則は全く意識してなかったのに話が通じるところまで同じの概念を抽象的に理解できる
#どうやって獲得したのかも思い出したいのだけど、なぜ理解できるのかも謎だ。
#==と/=との関係と
#区別できると区別できないとの関係はレイヤが違う気がする。
#ああなるほど。クラスが違うっていうことかな？
#そう。
#同じってどういうこと？と自分に問うた時、同じってのは同じってことだよなーとつぶやいた。
#説明になってないのだけど、他に説明を思いつかない。
#モナドを理解するとやはりモナドはモナドだよなーって説明に困るようなものなのでしょうかね
#赤って何？って言われたら
#色の一種なんだけど....
#そっからは説明難しい。
#血の色だよとか
##0xff0000
#なるほど。それもそうだ>0xff0000
#私は0x00ff00が赤に、0xff0000が緑に見えている。
#それはめずらしい
#いや
#それはどうみえているのか知らないけど、
#単に言葉を間違えているだけでは:-)
#色覚は人によって違います
#その「緑」は0xいくつ？(w > nobsun
#それはともかく、色とかをかんがえると
#google: 色覚バリアフリー
#結局私達は経験からなんとなく
#cut-seaが赤と感じているものを0x00ff00を見たときに感じる。
#これを確認する方法は？
#間違ったり正解を出している内に
#それは*感じる*なので分らないのでは？
#人差し指一本でたりる
#^^)/
#^^)/
#人差し指1本の話はなるほど面白いと思った。
# (^^)/
#cut-seaが赤と言った紙の色と同じ色の別の紙をnobsunが指示してその色のRGB値を調べる。
#のように、色のついたカードを用意して聞く：「あなたにとって赤はどれですか、人差し指で」
#同じ紙も調べないといけないか。
#いや、単に赤をどの色として学んだかだけではない？
#どう見えてようと
#その色をcut-seaとnobusnが同じ文化の中で赤と学んだなら
#それぞれ違う色に見えてるかもしれないけど、
#同じ色のものを赤だと指すことでしょう
#違う色を指す可能性は例えば赤緑色盲とかで
#赤ちゃんはまあだいたい誰でも赤ちゃんだよね
#区別がつかない場合とか
#あーどこまで赤に見えるかってことですか？
#赤ちゃんはどのくらいまで赤ちゃんと見做すか？って話？
#だとすれば極論すれば色盲と同じかなぁと思う
#キョクロニストにちかづく若者がまた一人
#若者ではないですけどねー。:-)
#人指し指を2本
#これらは違う指だけど、
#どっちも人指し指だよねーと
#つまりこれはどっちも人指し指という点では同じだと
#predicateが定義できるってのが区別できるクラスってことかな
#ある集合の要素なら何かのpredicateを通過している
#そう？
#考えるから悩むのであって、一度落ち着いて、考えるのがいいよ
#違うかな
#赤子のように手をひねって、ぐるりと世界観がかわり、わかる
#整数から整数への関数の集合があるとして、その元をどうやって区別する？
#整数から整数への関数をその集合に含まれない何かとは区別できるけど、元同士は区別できない。
#あーpredicateが定義できるなら云々ってのはちょっと対象が違うのか
##研究してらっさる方が
##ぬぬ。抽象概念は経験から具体例を通して学んでいるのだと思いはじめてたけど
#ああでもすべての入力に対して出力を比較すれば区別できるか。整数なら。
#まぁ数学者はそうなんだろうなぁ。
#あれれれ、先刻考えてたλの話なんか構文と意味がごちゃごちゃになってる気がしてきた。あらららら、足元崩壊。。。。。
#関数の区別の話はプログラミングHaskellにもちょこっと書いてあったかも
#入力と出力の組が完全に合致すれば良いはずだけど
#実際問題しらべつくせない。
#無限にあるから一般的には出来ないとか書いてなかったっけ
#そゆこと
#でもさ
#ふむ
#想像するんだけど、色んな簡約(最適化も簡約の一種と考えて)
#をしまくって同じ形になるとか、そういう可能性ってないものかな
#同じことを計算する2種類のやり方を記述したものが
#バリバリと簡約された結果同じ形になりましたーハイ！みたいなのって
#原理的にありえないのかしら
#\ x -> x + x と \ x -> x * 2 を区別する？
#そうそう
#そういうのを
#ホゲホゲ簡約とかフガフガ簡約とか駆使したら最終的に同じ形になるとかね
#上の二つは正規形だけど区別できる？
#区別できる？とは？
#そうそれがちゃんと規定されてない。
#？
#私が言ってるのは上の二つを最終的に同じ形に出来るような簡約ってないか？という話なんだけど
#上の二つを正規形と見做しているのは今がそうだってだけですよね？
#どういうこと？
#正規形=ここまでで簡約おしまい
#だという意味だと思ったんだけど違う？
#2つをさらに簡約するようなほげ簡約を考えるということ？
#そう
#ううん。直感的にはむりじゃね。
#+と
#あ、しまった
#+と
#くぅ
#+と*の間の変換というか関係があれば出来るはずだけど、
#そうすると
#あーいや、そうではないか
#それが唯一の形になるのか？という点？
#なんていうんだっけ数学的に
#ちゃろ。
#チャーチ・ロッサー性
#のこと？
#今Wikipediaみた。
#まぁそんなやつ。
#でも思ってた言葉はちょっと違ったと思う。
#*とか+とか2とかは定数だよね。
#うむ。
#いや
#*とか+って何かで定義されない？
#無理なんだっけ
#2+2は4に簡約できるよね
#うん
#でもその簡約はβ簡約じゃないよね。
#β簡約って何だっけ？
#適用？
#そう。
#(λx.e) a
#えぇ？じゃあβ簡約では？
#(((+) 2) 2)
#eのなかの束縛変数を実引数で置き換える。
#((+) 2 2)を簡約してみ
#そらしど。
#あー2+2のままなの？
#2+2を4にしているのはまた別で+の機能なのね
#δ簡約
#パターンマッチしている
#うーん。よくわからない。
#でも、今の例だけに関して言えばx * y = x + x * (y-1)としてどんどん展開していけば x * 2 => x + xにできそうに思えない？
#パターンマッチってのは 2 + 2 = 4という定義があるってこと？
#あるようなものってこと？
#そう。
#ちょい風呂。風呂PCが欲しいなぁ。
#ググったら日下部さんのブログがヒットした
#ういっす
#風呂あがり。
#はやい
#区別できるかどうかは、パターンマッチができるかどうかということになる？
#意識が飛びそう
#パターンマッチって
#あ、すまん。気にしないで。
#パターンマッチできる=δ簡約できる
#という話かな
#データ構成子がある = 区別できる
#うん。それは分るような気がする
#ただしマッチさせてるのは構成子までですよね。
#そう。
#おーけー
#でね。純粋なλ計算にはデータ構成子がないわけさ。
#純粋なというと？
#あー、λ*計算*ね
#おーけー単なる誤読です。続けてください。
#e ::= x -- 変数
| λx.e -- λ抽象
| e e' -- 適用
#つまりパターンマッチはないのさね。
#確かにλ計算のトピックにはδ簡約は出てこなかった
#いや、λβδ計算(うろおぼえ)というのがあって、これに登場する
#α変換とη簡約はでてた
#ごめんη変換だ
##δ簡約はそもそもググってもまとまった情報は上位にでてこないので分りませんが
#萩谷先生の関数プログラミングにちゃんと説明がある
#おお
#あ、萩谷せんせいの方ね
#でパターンマッチなしで、なにかの判定をする述語がつくれるんだろうか。
#p32参照中。。。
#今初めてこの本を読むという失礼。。。
#nobsunは作れないんじゃないか？と考えているのね？
#私は考えたことすらないので分りませんが、そうだとするとどうなる？？
#いや逆でなにかできるんじゃないかと思ってるんだけど、全くそうぞうがつかない。
#あら、そうなんだ
#ああ、「区別できるかどうかは、パターンマッチができるかどうかということになる？」に繋るのね
#できないとすると、あらゆる計算はλ計算で表現できる、λ計算で表現できるものが計算可能なものだ。というチャーチの主張はどうなる？
#あれ？
#パターンマッチ=δ簡約ですよね？
#λ計算にはδ簡約は含まれないでおーけー？
#データ構成子ないしね。
#ちょっと違う。δredexであることはパターンマッチでしか表現できない
#表現というか判定か。
#δ簡約は便法でチャーチ数の上で足し算定義できるよね。
#あーそこにくるのか。
#そう。
#計算可能性の話って実は勉強してすぐ挫折したので
#つか挫折してない学問あんのか？
#いや、ともかく計算可能なもの云々の主張が正しいとすると
#使わずに述語がでけるー
#あるいは
#δ簡約は計算ではない
#かの
#どっちかじゃないでしょうか
#2+2=4が計算ではないなんてことはないか
#じゃあ主張が間違っている
#もしくは
#それはないでしょ。
#使わずに述語が書ける
#のどっちか
#書けるはず。そうとうするものが。
#でもどう書くとこれは1つの述語だよね。といえるのか想像できん。
#もしかしてλx.λy. xをTrueとして云々の話をしてたのはこのこと？
#そう。
#trivialじゃない例は？ってやつ
#はっはぁ
#そう。
#KがTrueでしたね
#flipすれば良いからCKがFalse？
#KI
#どっちでもいいけど。KI=falseでもいいということ
#あれ？λx.λy.yがFalseですよね？
#const id y = yにならないよね
#KIxy = Iy = y
#const id x y = y
#おお
#なんか騙されてる気がする
#それだとidもFalseって言えない？
#あーちがうか
#ダメだ。
#x y二つとる必要があるのか
#すまない。進めてください。
#ああできた。Cがnotだね。
#flip=not？
#flip x y z = x z y
#true = const
#false = const id
#not = flip
#flip const y z = const z y = z
#そそ
#偶数かどうかを判定できるね。
#flip constは確かにconstを否定してるな
#チャーチ数が偶数かどうかを判定できる。
#うん。
#あ、なんかものまね鳥にあったような気もするぞ
#これがトリビアルじゃない例だね
#そうなんだ。よみこんでないので覚えてない。
#私も途中でゲーデルの問題になって足が止まった
#そこまではきっちり解いてたんだけど、解答の解説が分らないのよ。
#で、そゆところは原書読めって言われて、それもそうかと思って買ったのがある。
#さっき萩谷せんせいの本をものまね鳥の下からひっこぬいた:-)
#トリビアルじゃない例がわかったところで。明日はやいのでもうねますです。おやすみ。
#はい。
#23.論理鳥
#t=K,f=KIとして
#否定鳥N=Vft
#論理積鳥c=Rf
#論理和鳥d=Tt
#Vxyz=zxy
#Rxyz=yzx
#Txy=yx
#あと
#もし-その時鳥i=Rt
#その場合に限り鳥e=CSN
#もちろんSxyz=xz(yx)
#また読みたくなってきた
haskell-ja > Archives > 2009/12/03