前の日 / 次の日 / 最新 / 2013-09

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

01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30

2013-09-07 Sat

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

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なんかはちゃんと使えると楽しいのかなあ。

Coqによる証明プログラミング from Yoshiki Nakamura



それはともかく、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]

2021 : 01 02 03 04 05 06 07 08 09 10 11 12
2020 : 01 02 03 04 05 06 07 08 09 10 11 12
2019 : 01 02 03 04 05 06 07 08 09 10 11 12
2018 : 01 02 03 04 05 06 07 08 09 10 11 12
2017 : 01 02 03 04 05 06 07 08 09 10 11 12
2016 : 01 02 03 04 05 06 07 08 09 10 11 12
2015 : 01 02 03 04 05 06 07 08 09 10 11 12
2014 : 01 02 03 04 05 06 07 08 09 10 11 12
2013 : 01 02 03 04 05 06 07 08 09 10 11 12
2012 : 01 02 03 04 05 06 07 08 09 10 11 12
2011 : 01 02 03 04 05 06 07 08 09 10 11 12
2010 : 01 02 03 04 05 06 07 08 09 10 11 12
2009 : 01 02 03 04 05 06 07 08 09 10 11 12
2008 : 01 02 03 04 05 06 07 08 09 10 11 12
2007 : 01 02 03 04 05 06 07 08 09 10 11 12
2006 : 01 02 03 04 05 06 07 08 09 10 11 12
2005 : 01 02 03 04 05 06 07 08 09 10 11 12
2004 : 01 02 03 04 05 06 07 08 09 10 11 12

最終更新時間: 2021-01-08 21:13