檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2015-11-09 (月)

林晋さんのこと、根拠なきイチャモンのこと

| 08:55 | 林晋さんのこと、根拠なきイチャモンのことを含むブックマーク

先週のことでタイミングが遅れていますが、

相変わらず、何の根拠も示さずに知ったふうな事をのたまう。無根拠・非論理の芸風は死ぬまで治らない(治さない)のでしょう。

林晋さん*1へのたちの悪い言及を目にしてしまったので、一言いわずにはおれない気分です。


まず、林晋さんの著書について述べます。林さんの本は3冊持っていて、目次と索引しか見ない僕*2にしてはよく参照してます。

コロナ社の『数理論理学』*3は手が届く場所に置いてあります。

数理論理学 (コンピュータ数学シリーズ)

数理論理学 (コンピュータ数学シリーズ)

カリー/ハワード対応について説明している論理の本は少ないので、非常に助かります。かつてラムダセミナー/モニャドセミナーでカリー/ハワード対応を題材にしたときのネタ本はこれです。

この本『数理論理学』は、コンピューターサイエンス向けに論理をリフォームすることを目指して書かれたもので、自然演繹やシーケント計算のようなポピュラーな話題でも、伝統や標準的な解説法に拘らず、林さん独自の工夫が随所にあります。

それと、共立出版『プログラム検証論』と遊星社『構成的プログラミングの基礎』が、僕が持っている林さんの本です。

プログラム検証論 (情報数学講座 8)

プログラム検証論 (情報数学講座 8)

構成的プログラミングの基礎

構成的プログラミングの基礎

この2冊は、ちょっと今どこにあるやら? 去年(2014年)7月に本棚のスナップショットを撮った一覧から探してみると、確かに存在してますが、その後不要品は処分して、移動もしたので…

『プログラム検証論』にはホーア論理について詳しく書いてありました。日本語の本であんなに詳しいのは他にないんじゃないかな*4。『構成的プログラミングの基礎』のほう*5は、難しくてダメでした ^^;。

『プログラム検証論』は共立出版の情報数学講座シリーズの一冊ですが、このオレンジ本シリーズは良い本が多いですね。型付きラムダ計算や領域方程式の解き方なんかは、『プログラム意味論』と『プログラミング言語の基礎理論』の2冊から学べます。

プログラム意味論 (情報数学講座)

プログラム意味論 (情報数学講座)

プログラミング言語の基礎理論 (情報数学講座)

プログラミング言語の基礎理論 (情報数学講座)

僕は、林晋さんのお話を聞いたことが一度だけあります。むかーしですが、富山大学での学会講演です。そのときは、竹内外史さんが来日していて、「P≠NP予想」の講演があって、それを目当てに知人Kさんに誘われたのでした。竹内さんの話はまったく覚えてないです(理解できなかったからでしょう)が、林さんが再帰やフラクタルの話をしていたのは覚えています。プレゼンテーションで、スヌーピーが再帰する絵を使っていたのが印象に残っています(ウケてた)。


その林さんが最近公開した文書「あるソフトウェア工学者の失敗 日本のITは何故弱い」が注目を集めたのは11月3日(先週の火曜日)のことのようです*6

それを取り上げたid:JavaBlackさんの記事が:

他についてもソフトウエア工学に関して幾つか誤りが見られるし,


ソフトウエアに詳しい人なら「なにを今更」「間違いだらけ」だから.

id:JavaBlackさんがこのテの根拠のないイチャモンを付けるのはいつものことです。あまりにも類型的なパターンを使うので、「論理的であるかのごとくに装って、根拠のないイチャモンをつける 13+2 の方法」という解説記事の動機とメインサンプルになっているほどです。

今回も何の根拠もないイチャモンだろうと僕は思っていますが、林さんといえども間違えない保証はないわけで、「ソフトウエア工学に関して幾つか誤り」がないとは断言できません。id:JavaBlackさんにお願いしたいのは、「ソフトウエア工学に関して幾つか誤り」のなかの1つでいいので、どこがどのように誤りであるかをハッキリと指摘して欲しい、ということです。(お願いをきいてもらえる事は絶望的だろうが言っておく。)

インターネットのコミュニケーション形態が「あー、嫌だなぁ」と感じるのはこういう時です。林さんのような当代きってのエキスパートが、その経験と知見を真摯に綴った文書に対して、id:JavaBlackさんのような「根拠のないイチャモン」常習者がしたり顔で「他についてもソフトウエア工学に関して幾つか誤りが見られる」と言えてしまう。そして、一部の人はそのタワ言のほうを信じてしまうだろう、という構図。どうにも切なくなります。

*1:敬称が「さん」である理由は、「すごくえらい人には敬称が付けにくい」参照。

*2:要するにチャンと読まないので、書評記事は書けないです。が、1/2以上読めたりすると嬉しくて記事にします。例 →「渡辺竜・著『レスポンシブWebデザイン』はとても良い本だ

*3:同じコロナ社から同じタイトル(『数理論理学』)の本がもう一冊出ています。http://www.amazon.co.jp/dp/4339024899 ちょっと紛らわしい。

*4林さんの文書にも書いてありますが、証明の実行は労力がかかり過ぎ、現実的ではないですけどね。

*5:林さんが後で“捨てた”分野の教科書です。

*6:林さんの文書に対する感想は今回は述べませんが、わずかな希望を含みながらも全般に悲観的な内容です。

nagaenagae 2015/11/10 23:07 檜山さん、いつも参考になる記事を書いていただきましてありがとうございます。

誤りがあることは言うが、それがどこにあるか言わない人にはイライラします。
どこにあるのか質問したとき、そんなこともわからないのかとかバカにされるとさらにイライラします。

そういう人からは離れてしまうのが一番いいのかなと考えています。

m-hiyamam-hiyama 2015/11/11 11:14 nagaeさん、
「関わらないのが吉」なのは、おっしゃるとおりだと思います。
が、林さんに対して、あまりにも失礼な物言いです。

僕は、「アインシュタインは間違っている」という人が、アインシュタインに対して失礼だとは思いません。**自説**を述べて、**本気**でアインシュタインより自説が正しいと信じているわけですから。
しかし、**自説**も無いし、**本気**で間違いだとも思ってなく、エラソウにしたいがための誹謗。
関わってイライラするよりも、何も言わないフラストレーションのほうが大きかった、という事情でした。これ以上は関わりません。

KENZKENZ 2015/11/11 12:10 この記事をきっかけにしてこの論説を読むことができたので、僕は感謝しています。
業界の人がなんとなく思っていることと、それを実際に歩み、切り拓き、壁にぶつかって検証されて見出された結論との間には、天地の差があるように思います。
10年前にこの結論を根拠を持って断じていた訳でもないのであれば、結果は思ってた通りだった!って自称予言者の手口じゃないですか。

自分が巨人の肩に乗っかっていることは、わすれないようにしたいです。

m-hiyamam-hiyama 2015/11/11 13:40 KENZさん、お久しぶりです。
> 業界の人がなんとなく思っていることと、それを実際に歩み、切り拓き、壁にぶつかって検証されて見出された結論との間には、天地の差があるように思います。
言いたかったのは、まさにそこです。一言でいえば同じ結論でも、その結論に至るプロセスと知見の価値は全く違う、ということです。
林論説、読後感がよろしくないのは確かですが。

xx 2015/11/18 11:58 ここ数年、haskell方面等で再び、型推論から(カリー=ハワード同型を経て?)証明(=バグのないプログラム)といった理想が盛り上がっている印象がありませんか?

これは、林先生の経験と絶望を追体験するのかそれを乗り越える何かが起きるのか、浅学にして想像がつかないのですが(個人的には限定した領域での有効性の再発見、そのカバー領域に関する知見を得て終了かなとか)、桧山さんの感覚・推測があればお聞きしてみたいです。

m-hiyamam-hiyama 2015/11/18 18:19 xさん、
「バグのないプログラム」の話は、数十年のスパンで盛り上がったり盛り下がったりなので、今後どうなるかは、僕には分かりません。証明から生成したプログラムとか証明付きのプログラムという方向は望みが薄いのではないかと思います。
プログラミング言語より仕様記述言語のほうを何とかすべきだと思ってますが、これはこれで難しいし。
いずれにしても、既存の方法や習慣とギャップがあると受け入れてもらえないので、今のやり方のなかに少しずつ形式性や厳密性を注入していくしかないような気がしています。

xx 2015/11/19 01:30 なるほど、ありがとうございます。

oraemonoraemon 2016/10/01 04:13 amazonのレビューページに一応根拠を示して批判してる方を見つけました。
なお林さんご本人ご降臨。論破されブログに悪口を書き、コメントを削除した上逃亡したもよう。
https://www.amazon.co.jp/gp/customer-reviews/R2SIPCTY4CMCRC/ref=cm_cr_arp_d_viewpnt?ie=UTF8&ASIN=4003394410#R2SIPCTY4CMCRC

m-hiyamam-hiyama 2016/10/03 11:08 oraemonさん、
そういうことがあったのですね。
僕は当該の書籍を読んでないので何とも言えません。読んだところで、ドイツ語が云々のところはまったくドイツ語が分からないので判断不可能です。
書籍に誤訳、説明不足が実際にあったとしても、このエントリーに何か影響があるとも思いません。