/home/pochi/ChangeLog / 2013-09-07

■ 証明するということ [数学][言語]

http://labs.timedia.co.jp/2013/08/post-22.html

ゲーデルの証明を一つずつプログラム言語で記述してしまえばいい！
そういうことならHaskellでしょう。だってHaskellのプログラムってそのまま数学の証明みたいだもんね！
まあそんな野望を抱いて最初の1章を読み終え、さてそろそろプログラムを書くか...
とHaskellに詳しい同僚に相談してみました

「無理っすよ、Haskellは述語論理（∀とか∃とか）を表現できないですから！
Haskellに述語論理をのっけたAgdaってのがあります」

これか↓

Wikipedia - Agda

The Agda Wiki
http://wiki.portal.chalmers.se/agda/pmwiki.php

チュートリアルは、PDFで論文ちっくに書かれてある。
ざっと見た感じ、わけわからん。


定理を証明するだけなら、そういう言語がいろいろあったよな、、、、

Wikipedia - 自動定理証明

これとか。
あと、証明プログラミングっていうのも面白いネタよね。
Coqなんかはちゃんと使えると楽しいのかなあ。

それはともかく、KOMMYとは同じ会社で背中合わせの席だったことがある。
どんな言語も3日あれば使いこなせるよ、と豪語しつつ、
実際に使いこなしていた。

すげぇと感心しつつ、Haskellさえちゃんとやったことのない身としては恐怖を覚えたのでした。

嘘は良くないなあ。
Haskellいじりもしてたような記憶があるんだがw

■ 中国人の大いなる「日本のアダルトビデオ」への関心 [ネタ]

http://business.nikkeibp.co.jp/article/opinion/20130826/252589/

中国ではアダルトビデオは違法コンテンツのはずなんだけど、
ものすごく愛されてるんだよね。

たとえばこんなのとか。

蒼井そらが日中関係を変えるほど中国で愛されている件
http://matome.naver.jp/odai/2133583533965309301

「日本人の女性は（AVで見るように）あんなに優しくて、男性に何でもしてくれるのか？」
「日本の女性は昼間は清楚に見えるけれど、夜になるとAV女優みたいに変身するって本当か？」
「日本女性はあんなに性に奔放なのか？」

こう聞かれたら、「そういう人もいるよ〜」、
と答えておけば夢を壊さずに済むのかしらねえ。
そういう人が皆無な国もあるのかもだし。

■ 中国のGreat Firewallの裏側のDNSの挙動とかを調べてきた話 [DNS][インターネット]

Mazのビアトークネタ。

中国でGreatだよ
http://www.attn.jp/maz/p/t/pdf/iij-2013-china-gf.pdf

面白かった。
面白い挙動するんだねえ。

- 誰に聞いても何か答えてくれる。
- 何を聞いてもA RRが返ってくる
- IPv6 だと普通に応答が返る
- TCP/53 だとフィルタリングされない
- ウェブアクセスは、ホスト名のパターンマッチでコンテンツフィルタしてる

技術的にはとっても面白いんだけど、こんなことをして楽しいのかねえ？＞中国政府
ただ、馬鹿だなあ、っては言えない気はする。
中国の支配者層って、ほんとに頭が良いのよね。
こうでもしないと、彼らが大切なものを守れない、と判断せざる得なかったのだろうなあ。
なにかを守るって大変だ。
とりあえずフリーキックの時には股間を手で押さえよう。


そういえば、JANOG16のときに、中国でエロコンテンツが見れるか確認してきて!、
と無茶振りをしたことがあったような。。。。
当時は大変失礼いたしました。

■ 2013年東京都内コワーキングスペースランキングベスト70！人気の秘密は？人気一覧シート付き [仕事]

http://keiei.freee.co.jp/2013/08/26/coworking/

東京の西側には結構あるのよねえ。
いいなあ。
東京の東側にはいまいち素敵なコワーキングスペースがないのよね。

なので、何か書き物とかあるときは、ルノアールばかりになってしまってるんだけど、
さすがに他の選択肢も欲しいんだよね。
素敵な場所はないかしら。
長居ができて、椅子が良くて、遅くまで開いてるとこが良いなあ。

関連)
ノマドならルノアールがはかどるよねぇ〜っていう10個の理由 --> [2012-08-21-5]