それは障害児ときょうだい児の愛の物語…か?

ここ数日何度も何度も「アナと雪の女王」を頭の中で反芻している。

この物語が「同性愛を肯定している!」と言われているという話をどこかで読んだ。まぁ確かにそう読めなくもない。最後の方でエルサがアナに

「私のために犠牲になってくれたの?」

と質問するくだりがあるのだがこれへのアナの返答が

「…I love you.」

なのである。

英語圏のloveは、日本語として使われるときのニュアンスよりもずっと広い意味で使われるので、これを兄弟愛と解釈しても何の問題もないのだが、逆に言えば同性愛として解釈することもできることになる。

ちなみにこの部分、字幕では「だってあなたの妹だもの…」というような訳がついていたと思う。直訳すると日本人には同性愛的なニュアンスしか感じられないと翻訳者も思ったのだろう。

さて、そんな解釈もできる「アナと雪の女王」だが、別の見方もできるように思われる。

それは、エルサの能力を「障害」ととらえると見えてくる。

制御できない超能力を持つということは、普通の人の中で普通に生きていくことが難しいという意味で、これは正に健常者の中での障害者と同じポジションとなる。そういう見方をすると、この物語は「自分の障害とどう向き合っていくか」を表すと共に「子供や兄弟の障害とどう向き合っていくか」という非常に重いテーマを持った作品のように感じられるから面白い。

脚本家の意図は分からないが、障害児を持った親がどう振る舞うべきなのか、障害児の兄弟はどうなのか、この物語はこの物語なりの解答を出してくれているように思う。これ以上はないほどのきれいごとにしか感じられないかもしれないが。

見る人によって全然別の解釈ができる「アナと雪の女王」是非見てみてください。できれば吹き替えと字幕の両方がおすすめです。

大きなゆきだるま~

映画「アナと雪の女王」の吹き替えを娘と見てきて、ついでにサントラも入手してと、なんだかズッポリはまっている状況である。

で、英語の歌詞でサントラを聴いていると、ところどころひっかかるところがある。日本語の歌詞が英語の歌詞と全然違う部分があるのである。

「アナと雪の女王」の翻訳者はずいぶん苦労されたと思われるし、結果としていい仕事をしているとは思うのだが、それでも文字数の関係で吹き替えでは恐らくかなりの逡巡を経て今の歌詞があてられているのではなかろうか。

それでも、だいぶ意味が変わってしまっている、というか結構大事なところが削れてしまっていると思える部分がいくつかある。

たとえば、「雪だるま作ろう」で、幼少期のアナは鍵穴に口をあけて「大きな雪だるま~」と日本語で歌っているのだが、この部分の英語の歌詞は「It doesn’t have to be a snowman」である。直訳すれば「雪だるまにならなくてもいいからさぁ」という意味だ。

アナはなぜこんなことを言っているのだろう。

日本語でアナはエルサに「雪だるま作ろう」と言っっているが、これも元の詩の直訳は「Do you want to build a snowman?」(あなたは雪だるまを作りたいと思わないの?)である。「作ろう」と言っているのではないのだ。「作ってよ」と言っているのである。

アナがエルサに事情も知らず無邪気にお願いして断られるこの構図は、氷の宮殿でアナがエルサにアレンデールを救ってほしいと頼む状況と同じである。氷にの宮殿に向かうアナもその願いがかなえられるという根拠は何も持っていなかったし、心のなかで「やっぱ無理かも」という気持ちがあったはずである。何度もわざわざ「大丈夫よ」と繰り返す様子を見てもそのことが窺える。

この「氷の宮殿での説得失敗」を、この最初の段階でさりげなく歌の中に織り交ぜて示唆しているのがこの「It doesn’t have to be a snowman」という歌詞なのではないかと思うだ。

この映画では、「愛と怖れ」が大きなテーマとなっていて、その対象関係がいろいろなところに投射されている。「アナとエルサ」「オラフとマシュマーロウ」「アレンデール宮殿と氷の宮殿」といった具合である。

つまりこの物語で「雪だるま」はアナとエルサの間の愛の象徴として登場しており、ストーリーの全編を通して大きな意味を持たされているのだ。

アナがエルサに雪だるまを要求するというのは、宮殿でエルサに「一緒に暮らそうよ」と呼びかけるのと同じことなのである。

雪だるまと言えば、エルサが「Let it go」を歌いながら残った片方の手袋を高く投げあげ、自分の解放を宣言した直後に無意識に作ったものがこの雪だるまだったことも非常に意味が深い。怖れから解放された魂から最初に出てきたものが愛の象徴だったのだから。

このあたりの描写をあまり口説くならないようにサラッと見せているところは本当に上手いなぁと思わされる。何度も鑑賞に堪えるというか、見るたびに発見があって飽きさせないし、様々な解釈ができるのである。名作というのはこういうものなのだなぁとつくづく思う。

早く日本版ブルーレイでないかなぁと。

集団投射

先日、「題名のない音楽会」でノイズミュージックが取り上げられるという大事件があった。

http://news.biglobe.ne.jp/entertainment/0413/jc_140413_4804036021.html

ノイズミュージックの認知度を上げる千載一隅のチャンスとあってか、大友良英氏のテンションも上がりっぱなしである。

その中で、高柳昌行/阿部薫の「集団投射」が紹介されていた。

阿部薫は以前からちょっと真剣に聞いてみたかったので、これを機会に御茶ノ水「ジャニス」で借りてきた。

このジャニスのすごいところは、こういう超マイナーなCDが普通にレンタルされているところである。ただし値段は結構高い。でもAmazonで買うと2万円以上にもなっているCDなので、多少高くても「ありがたや、ありがたや」と財布を開いて借りてくるしかないのだ。

http://www.amazon.co.jp/%E9%9B%86%E5%9B%A3%E6%8A%95%E5%B0%84-Mass-Projection-%E9%AB%98%E6%9F%B3%E6%98%8C%E8%A1%8C/dp/B00005B1IN

で、SONYのUDA-1で再生が始まった瞬間、僕は反射的に頭を少し低くしてしまった。

身の危険を感じたのである。

ほぼ「音による爆撃」と言ってもいいかもしれない。

始まった瞬間から全力である。で、そのままおしまいまでずっとそのテンションが維持されている。こんな音楽を夜な夜なやっていたら、それこそ長生きできそうにない。

あまり日常生活に疑問や不満や理不尽を感じていない時には、この音楽はそれこそ雑音にしか感じられないかもしれないが、そういったものが自分に鬱積しているときに聴くと最高のBGMになるような気がする。

この音楽が生まれた時代もまた、そういう時代だったのだろう。

ブルーレイ

正直、いまだにレンタルやセルのビデオ屋さんで主力となっているのがDVDであることに違和感を感じている。

こんな僕もつい数か月前まではDVDで十分だと思っていたのである。しかし、実際に自分でブルーレイの動画を見てから完全に考えが変わってしまった。

「なぜDVDで十分だと思うのか」

SONYがオーディオ分野でハイレゾを押している。それの是非はともかくとして、ブルーレイによる動画は誰が見てもDVDとの違いが明らかにわかるレベルである。オーディオはダイナミックレンジの違いがわかるほど音量を上げられる機会はそうそうないが、ヴィジュアルの方は少し顔をモニタに近づけるだけですぐに画質の違いがわかる。

同じものがDVDとブルーレイの両方で売られているなら、DVDを購入する理由はほとんど感じられないほどの画質差である。

そもそもDVDはハイビジョンを意識した規格ではない。今当たり前になっている1920ピクセルのモニタにはスペックが完全に不足している。しかも4Kはともかくとして720ピクセルは、アナログフィルムの情報量を再現する使命を負うにはあまりに低スペックである。「サウンドオブミュージック」の時代のフィルムですら、DVDではフィルムの情報量をまったく伝えきれていない。

しつこいようだが「その差は、誰が見ても明らか」である。オーディオのハイレゾのように、「わかる人にはわかる」というレベルのものではないのである。

もう一つ理解できないのは、店頭でのPOP代わりの映像モニタが、フルハイビジョンでないことが非常に多いことである。いまだに4:3のモニタが使われていることすら珍しくない。こんなことでブルーレイのメディアが売れるわけがない。

ハイビジョンに移行してもう何年も経つのだから、いいかげんみんなブルーレイに移行しようよと。

何が困っているって、欲しいものがまだDVDでしか発売されてなかったりするのだ。でも今更DVDを購入するのも負けた気がしてね…

ブレスの位置

前回中島みゆきの話がブレスのネタだったので、その続きというか・・・

男女問わずボーカルがその音楽を演出する際に最も大事な要素に挙げるべきもののひとつは「ブレスの位置」なのではないかと思う。

自分で何かの曲を歌っていても、ブレスの位置がふらふらと動いているうちは「まだこの曲は歌いこめてないなぁ」という気がするし、逆にその曲についての自分なりの「演出」が決まってきたときは、自然にブレスの位置が固定されてくる。

ブレスの位置を語る上で一番わかりやすい例は、カーペンターズの「Goodbye to Love」ではないかと思う。

この演奏をブレスの位置に注目して聴くとわかると思うが、ブレスの位置が

(I’ll say goodbye to love)

(No one ever cared if I should live or die)

(Time and time again the chance for love has passed me by  And all I know of love is how to live without it)

(I just can’t seem to find it)

(So I’ve made my mind up I must live my life alone)

(And though it’s not the easy way  I guess I’ve always known  I’d say goodbye to love)

(There are no tomorrow for this heart of mine)

(Surely time will lose these bitter memories  And I’ll find that there is someone to believe in And to live for)

(something I could live for)

(All the years of useless search  Have finally reached an end)

(Loneliness and empty days will be my only friend )

(From this day love is forgotten)

(I’ll go on as best I can)

こんな感じで、単純に息が続くか続かないかや、文の区切りでブレスをしているわけではないことがわかる。ブレスは音楽的な演出のひとつで、「歌う」という行為の大事な要素なのである。

中にはちょっと聴いていて息苦しさを感じるほど長いフレーズもあったりして、このへんはカレン・カーペンターの息の長さに舌を巻くしかないのであるが、彼女自身(もしくは演出をしている兄)がその必然を感じなければこんな無理をする必要もないわけで、歌うという行為でブレスの位置は大事なのだなぁと思わされるのである。

 

中島みゆきの衝撃

僕は結構な「中島みゆき」世代で、オールナイトニッポンも聞いていたのだが、何故か「中島みゆきのオールナイトニッポン」だけは聞いた記憶が数えるほどしかない。今では伝説にもなっているそのラジオプログラムについては、改めてここで書く必要もないほど人口に膾炙しているといえるだろう。

そんな数回の「中島みゆきオールナイト」体験だが、今でもはっきりと覚えていて自分の中で反芻しそのたびに驚きを新たにしているものがある。

あるリスナーからの葉書での「『あの娘』という曲のサビで女の子の名前をたくさん並べているところがありますが、息継ぎの場所がなく一気に歌えなくて困っている。どうすればいいか」という相談であった。

普通のシンガーなら、ブレスが続くようになる練習とかコツとか、目立たないで息継ぎできる場所とかを語るところであるが、中島みゆきはこんなことを言ったのである。

『中盤を過ぎたあたりに「ひろこ」という名前があるので、その「ひ」を息を吸いながら歌えばいいんじゃないか。ガハハハ。』

本当なのである。しかも実演までしたのである。

言っておくがこの歌、「あの娘をたとえば殺しても/あなたは私を愛さない」という、ちょっと男ならぞっとするような歌なのである。とてもギャグにできるような内容ではないのだ。

それを自らギャグにし実演までしてぐひょぐひょと下品に笑ってみせる中島みゆきのオールナイトニッポンを聴いて、僕はそっとラジオを消したのである。

エアコンの設定温度

女房は寒がりで、何度言ってもいつの間にかエアコンの設定温度を24℃にしている。

僕などはこの時期外気との温度差を考えると18℃以下にしてしまうのだが、女房に譲るところがあったにせよ、20℃設定で寒いということはないんじゃないかと思うのだが。

エアコンのリモコンに「管理者モード」のようなものがあって、パスワードを入れないと24℃設定にできないとか、そういう機能があってもいいんじゃないかと思う。

スマート家電とか言ってるメーカーの人、そういう機能付きませんか。光熱費出してるの僕なんですよ。

プログラムに証明が付く日

この記事は「Theorem Prover Advent Calendar 2013」6日目の記事です。

http://qiita.com/advent-calendar/2013/theorem_prover

神田「野らぼー」にて、地下の薄暗い店内で…

「そう言えばこないだ隣で起こってたポインタオーバーラン、対応大変そうだったですけどちゃんと家に帰れてたんでしょうかね、新婚なのに…」

「ヌルポとかポインタオーバーランとか、どうして無くならないんだろうね。その時はみんな手を抜いてるつもりなんて毛頭なくて、一生懸命考えて大丈夫だと思ってるはずなんだけどね。レビューもして、それでも起こった後でみんなでソース見てみると、なんで気づかなかったんだよ!ってことになる。」

「人間って、そういうの苦手なんでしょうねきっと。ほら、『何かほかにありませんか』って聞かれても出てこないじゃないですか。静的な解析って、過去の経験を軸に見ていくことはできますけど、人を集めたところで結局集まった人の中では大丈夫だと思った、っていうレベルにしかならないんですよね。もちろんやらないよりずっといいんでしょうけど。」

「テストを書いて、テストを流して、静的解析を通して、レビューもして、でも絶対大丈夫って気になることってあまりないよね。なんかモヤッとしたものが残ることがあって。そうそう、僕はTさんのこういう直観を割と信用してて、あの人がテスト結果を見て何か不審な顔を見せた時は必ず何かそこに撃ち漏らしがあると思うことにしてる。」

「そういう人って頼りになりますよね。でもできればそういう人に頼らずに枕を高くして寝たいじゃないですか。」

「何かいい方法ないもんかねぇ・・・」

鶏のモモ肉をパリパリに焼いた『丸亀焼き』をスチールの皿の上で転がしながら先輩が考え込む。

ソフトウェアの形

「結局のところ、ソフトウェアの正しさを、納品前にどう示せるか、ってことですよね。図形でいうと、目指す形があって、その形になっていることをちゃんと確認する方法があるか、ということじゃないですか。」

「まぁ、そうかな」

後輩らしき方が、ちょっと考えた後でナプキンを出してペンで図を書き始めた。

「たとえば、まぁ目指すソフトウェアがこういう形だったとするじゃないですか。」

fig01

「丸だな」

「話をややこしくしたくないんで。このプログラムは、二つの入力をとってboolを返す関数だとしましょう。横軸は入力1で、縦軸が入力2です。白はtrue、黒はfalseを返す出力を表しています。こういう要件のプログラムだと思ってください。」

「ほう。」

「で、プログラムのテストを書くじゃないですか。これでできることって、この中の特定のケースに限って、特定の値が返ることを試してみることですよね。つまり、こんな特定の点ごとに、true、falseであることを確認するわけです」

fig02

「まぁ、そうだよな。」

「でも、考えてください。座標は無数にあって、とてもすべての点を試すことなんてできませんよね。これが2軸の整数ならまだ何とか総当たりもできなくないかもしれませんが、軸がもう一つ付くとアウトでしょうきっと。テストというのは、プログラムの形を確認する上でとても大切なものですが、結局のところ「点」でしか形を確認することができないんですよ。この点をどれだけ増やそうが、それをすり抜けている部分が無いことを示すことはできないんです。」

「まぁ、テストする方だってただ漫然とテストの点を選んでるわけじゃなくて、いろんなテスト技法を使って一つ一つの『点』の意義を上げていく努力はしているんだけどな。」

「そうなんですが、テストケースをすり抜けてしまう事象が後で見つかるという悲劇はこれを見ると避けられない気がしてきませんか?」

「静的な解析や、レビューなんかはどうなんだろう」

「これはあくまでイメージなのですが、静的解析やレビュー、それに最近の言語に取り入れられている『静的型』の効果というのは、こんな感じです。」

と言いながら彼はナプキンに線を引き始めた。

fig03

「こういったソースの論理を機械的に解析する作業は、こんな風に設計を『線』で追い込んでる感じなんですよ。単発のテストケースみたいにキワキワを目がけて攻めていけるわけじゃないけど、一定の条件の入力においては、要件を満たすことが連続的に示されるということです。うまくすれば、面で塗りつぶすこともできるかもしれません。」

「これだけ見てると、テストの方がよりプログラムの形に迫りやすいように見えるけど、どうなんだろう」

「これが難しいところで、テストだけでは対応できないものもあるかもしれないんですよ。こんなケースとかだと、テストはすり抜けてしまって、静的な解析でないと捕まえられないケースもあるかもしれません。」

fig04

「あくまで概念的なものですが。ただ、単体テストも進化してきて、テストケースをある程度境界線を意識しながら自動的に無数に作成してテストしてくれるツールもあって、そういうものを使うとテストをすり抜けることもグッと少なくなると思います。ただし、こういうものにはある程度限界があると思うんですよ。」

テストの行き着く先

「限界というと?」

「例えば、上のプログラムなら、境界線付近のどの入力がtrueでどの入力がfalseか、人間があらかじめ計算して確かめておく必要がありますよね。」

「そうしないとテストをしても正しいかどうか分からないね」

「そうやってテストケースを追加していく訳ですが、テストケースが増えれば増えるほど、テストケースを作る人間の側がミスをする可能性も増えていくわけですよ。」

「まぁ、実際にテストケースを流してから、エラーになったものだけ、プログラムとテストケースの両方を確認して、間違っているのがどっちなのか確認してるね。」

「そうなんですよ。人間が人手でテストケースの入力に対応する『正しい』出力を予想しようとすると、必ず一定の割合でミスは起こるんです。もっと悪いのは、テストケースを自動的に生成してくれるのはいいんですが、結果の確認は後で人間にさせる、というツールです。」

「そういうのあったあった。ソースを解析して網羅率の高いテストケースを自動生成して流してくれるんだけど、結果は出力を見て一つ一つ人間が確認するようになってるやつ。」

「人間って、そういうの無理なんですよ。入力を見せられて『この出力結果を予想して』って言われるとちゃんとできる人でも、結果を見せられて『これは正しいですか?』って確認を求められると、あまり考えずに『うん』って言ってしまいがちなんです。一つや二つならともかく、自動生成ツールはテストケースを作るのが仕事ですから、何百というテストケースを作って流し、表の形で見せて一つ一つ確認してチェックボックスをONにしろっていうわけです。相当な精神力がないと正しい判断はできなくなりますよ。」

「となると、テストケースと結果予想は先に作っておかないとダメということだよね。」

「そうなんですが、そうやってテストケースとその実行結果予想を沢山作っているうちに、ふと一つの考えが頭に浮かんでくるわけですよ。『これ、入力を決めたら、実行予想結果を計算するマクロをExcelで書けばいんじゃね?』って。」

「まぁプログラマならそう思うのも無理はないだろうな。」

「そして、嬉々としてExcelのVBA画面を起動し、マクロを書き出してふと思うわけですよ。『入力から出力を計算するプログラムって、テスト対象のプログラムそのものじゃん』って。同じプログラム二度書いてどうすんだよと。」

「確かにそうだね。」

「でもですよ、この話は決してバカな話でもないんですよ。最初に手作業でやっていたテストケース作成作業だって同じことなんです。このテストケースの数を増やしていくという行為は、同じプログラムを二度書くのと、意味合いでは等価な行為に収束するんですよ。」

「...」

「何が言いたいかというと、同じプログラムを二つ書いて、両者に同じ入力をしたら同じ出力が出るということを無数に確認するということは、テストケースを無数に書くというのと究極的には同じことで、これは決して無意味なことではないんです。」

「...そうかもしれない」

「ただ、同じ人が同じ詳細設計書を見て同じ言語で書くと本当に同じプログラムが出来てしまうので、機能設計レベルから二つのチームに分かれて、なるべくパラダイムの違う別のプログラミング言語で同じプログラムを作るのが一番いいということなんです。で、完成した二つのプログラムの結果をつき合わせて、違いがあればどちらが間違っているか確認して、時間の許す限り気の済むまでテストをして、気が済んだらどちらか実行が速いとか使用メモリが少ないとか、都合のいい方のプログラムを採用すれば済むことなんです。さらに言えば、両者に仕様の誤解があったなら、それは仕様書にあいまいさが残っていることも示唆してくれるんです。」

「こ・・コストは倍になるけどな」

「実際にはテストの自動化が出来ることを考えると1.5倍ぐらいで済むんじゃないかと思うんですよ。実はもう一つあって、両者のプログラムの作り方はできれば逆向きであることが理想なんです。」

「逆向き?」

「例えば、一方は『trueとなる条件を一つ一つ組み立てていくように』してもう一方は『falseとなる条件を積み重ねていくように』作るといった具合です。この図で言うと、trueチームは白い部分の外側から内側に包み込んでいくように、falseチームは黒い円の内側から外側に成長するようにプログラムを定義するということです。」

fig05

「そして境界線あたりでせめぎ合うということか」

「そうです。両者正しく出来れていれば境界線で交わることはないはずですし、どちらにも属さない領域もできないはずです。これをモンテカルロ的に確認できれば、プログラムは高い確率で矛盾なくできていると思えるんじゃないかと。」

「しかしそれは両チームストレスだろうな~きっと。」

「もちろんこれは理想的には、という話なのですが。」

二つのプログラムが同じであることの証明

山盛りだった煮干しバラシ天がすっかりなくってしまった。

「理想的には、という流れのついでに、もう一つお話ししましょうか」

「何だまだあるのか。何か頼んでからにしようぜ」

揚げうどんと新しい酒が来るのを待ってから話を続けた。

「さっきの『二つプログラムを作る』という案なんですが、実はまだ弱点があるんですよ。分かりますか?」

「コストとかモチベーションとかかなぁ・・・どっちかテストケースにされると分かってると元気でないかもしれない」

「それもあるかもしれませんが、そういうことじゃなくて、この二つのプログラムのつき合わせも結局のところ『時間の限り』でしかないところなんですよ。有限の時間で、無限に近い入力のある実際のプログラムの入力を全パターン試すことなど結局できないんです。もちろんテストケースを手書きするよりもずっと良好な結果が得られるとは思いますが。」

「そんなのしょうがないんじゃないか。そんなもんだろ」

「それが、そうでもないような仕組みも無くはないんですよ。ただしかなり険しい道のりですが」

「ほう。まだ終電まで時間があるし聞かせてもらおうじゃねぇか」

「これがまた難しい話でですね...」

また新しいナプキンを抜いて書き始める。

「例えば、先ほど話した二つのチームが

f (x, y) = x * y;

という関数と

g (x ,y) = y * x;

という二つの関数を作ったとします。さっきまでの流れだと、この二つの関数が同じ入力で同じ値を返す関数であることを確認するためには、xとyに想像がつく限りの組み合わせを総当りで入れて、戻り値が同じであることを確認する作業を時間の限りやるということですよね。」

「まぁ、例え話だとそうだけど、この二つの関数が同じ結果を返すのは見ればわかるよな」

「まぁそうなんですが、それは今は気づかないことにしてこの二つの関数を議論しましょう。たったこれだけの関数でも、32bitなら40億の2乗回の計算をしないと二つの関数が同じ機能を持っていることを保証することはできないということです。これは大変です。」

「気づかなければ、そうだな」

「しかしです、この二つの関数が、任意の入力で必ず同じ値を返すという証明を数学的に書くことができれば、わざわざ40億の2乗回も計算する必要はないわけです。」

「この式なら、証明など書かなくてもいいだろう。」

「僕らは掛け算の計算順は入れ替えても答えが変わらないと学校で習っているからそういうことが言えるわけで、コンピュータはそんなこと知らないんですよ。でも、定理証明機能を持っている言語だと、コンピュータに対して『この二つの関数はどんな入力をしても必ず同じ結果が返ることを示してやるから見てろ』と宣言して、その後にその証明を書いて納得させることが出来るんですよ。」

「証明してくれるんじゃなくて、書くのか!」

「基本的には、書きます。ある程度の範囲なら勝手に証明を導いてくれますが、期待するほどの範囲ではないと思ってください。」

「その証明を、わざわざコンピュータで書く理由はあるのか?」

「コンピュータを使ったほうが楽だから、コンピュータで証明を書くんです。この関数fとgが同じだということを示すのにも数十行のコードが必要になりますが。それに、人間が書いた説明を人間が読んで『確かに同じだね』と納得したところでどこに穴があるかわかりませんし、人間が証明を検証するのは、さっき出た『自動テストの結果を人間が検証する』のと同じ愚を冒すことになります。」

「そんな掛け算ぐらいで何十行も書かないといけないなら、実際の仕事で使えるのかな」

「その辺は考えようで、本気で40億の2乗回テストをするなら、証明を書いたほうが早い場合も多いでしょう。実際のプログラムではもっと入力のパターンは多くなるでしょうから、証明の方が有利になることももっと増えるかもしれません。ただ、我々はこれまで全パターンテストしないで『たぶん大丈夫』と言ってしまっているので、証明を書くことが不経済だと感じるだけなんですよ。」

「プログラムの正しさにそういうコストをかけて構わない業界もあるのかもな・・・」

「ただ、実際に証明を書くのにはかなり勉強が必要なのも事実です。記号論理学とか、数理論理学とかの知識が絶対的に必要になります。その辺はしょうがないといえばしょうがないのですが、ハードルが高いと言われれば否定はできないですね。ただ証明つきのプログラムにはもう一つ機能があるんです。」

「まだあるのか!もう終電近いぞ」

関数について「考え切る」ということ

「この手の言語は、これまでの言語よりもずっと『型』の奥行きが深いんです」

「というと?」

「例えば、『10より小さい整数』というような型が定義できるんですよ。」

「それのどこが嬉しいの?」

「例えばこんな関数の定義を考えてみましょう。」

f ( x : x は20未満の自然数 ) : 戻り値は10未満の自然数 = x / 2

「何これ?」

「f は、20より小さい自然数を取って10より小さい自然数を返す関数で、中身はxを2で割ることだぞと。そんな意味です。xは引数で、コロンの後はその型だと思って読んでください。実際のプログラミングではもう少し別の書き方をしますが。」

「やっぱり嬉しさがわからない」

「この関数が宣言しているものは、『xは20より小さい自然数であることを前提として』、xを2で割るという計算をして、『戻り値が10より小さい自然数であることを保証しましょう』ということなんです。」

「・・・?」

「で、この関数をコンパイルするためには、『xは20より小さい自然数であることを前提とする』と、x / 2 が『10より小さい自然数』に収まることの証明を人間がエッチラオッチラ書かないといけないんですね。それが書けないとコンパイルしてくれない。」

「恐ろしいな」

「恐ろしいんですが、嬉しいこともあるんです。この関数が入力に『20より小さい自然数』を要求しているということは、この関数を呼び出す側も、引数の値がこれを満たすことを証明できてないといけないんです。つまり、呼び出せた、というか呼び出すようなコードがコンパイルできたということは、呼び出す側が持つ前提の元で、引数に渡す数が、呼び出す関数の前提を満たしているということが保証されるんですよ。」

「関数というのは、引数として与えられた前提を元に戻り値の前提を満たすことが証明できるものであって、中で他の関数を呼び出す時も、それに渡す引数が呼び出される関数の前提を満たしていることを証明しないといけないんだな。ってまじかよ」

「で、最初の話に戻るんですが、これだけ厳格に型が定義できてそれがちゃんと運用できれば、配列のインデックスがオーバーランしてしまうこともなくなるんです。なにせオーバーランするような値が引数で入ってくることが不可能になりますから。そういう値が入力されないことが、実行時ではなくコンパイル時に保証されるんです。」

「わからなくもないけど、証明が書けないということはないの?」

「書けない時は、前提か、戻り値の型か、計算のどれかもしくは複数が間違っているか、勉強不足か・・・いずれにしても証明が書けるまでの間に、その関数の隅から隅まで考え尽くす必要がありますから、『何となくできたつもり』のものがリリースされてしまうという事態だけは避けられます。」

「それだと何もリリースされなくなるかも・・・ゴールは遠いな。」

「遠い道のりですね・・・・・でもいつか新婚さんが会社に泊まらなくてもいいような日が来ることを夢見るのも悪くないんじゃないでしょうか」

「それに、最初の問題として人間が『作りたいプログラムの形』を、作る前にちゃんと定義できるのか、という疑問もあるよな。」

「そうなんです。正しくて厳格な仕様書というのは、いうなれば自然言語で書かれたプログラムそのものと言ってもいいわけで、それがプログラムより先に書けるならプログラマはこんな苦労しないよ、という気もしますね。」

「でも、それを言っちゃオシマイだよな・・・」

「昔お世話になったというか、今でもエンジニアとしての心の師匠みたいな人と仕事をさせてもらっていた時があったんですが、その人の口癖が、『この設計書じゃ、まだ考え切れてないね・・・』だったんです。僕は結局その人に一度も褒められることがないまま職場が変わっちゃったんですが、証明を考えてると『考え切る』という言葉の意味が少し分かったような気がしてくるんです。証明を書く、ということを通しての『プログラムの隅々まで漏れなく考えることが強制される経験』に大きな意味があると思うんですよ。」

「・・・酒・・・なくなったな。」

「電車もなくなりましたね。」

こうして神田の夜は更けていく・・・・

 

(終)

 

※ 証明付きのプログラミングに興味を持たれて、『ちょっと試してみたい』、という気になられた方は、ぜひ一度『ソフトウェアの基礎』や『プログラミング Coq』を最初のあたりだけでも読んで、できればCoqをインストールして実際に手を動かして試してみてください。

『ソフトウェアの基礎』

http://proofcafe.org/sf/

『プログラミング Coq 〜 絶対にバグのないプログラムの書き方 〜』

http://www.iij-ii.co.jp/lab/techdoc/coqt/

※ 型が値で修飾される『依存型』というものがどんな感じか見たい方は以下のリンクをClick!

にわとり小屋でのプログラミング

http://yosh.hateblo.jp/entry/2013/12/06/202827

※神田「野らぼー」

http://www.norabow.jp/nightmenu/index.html

 

 

音楽を聴くということ

今日UDA-1の前に座りWalkmanを握り締めて音楽聴いたら、女房が来て「何してるの?」って聞いてきた。
「音楽聴いてんだよ見れば分かるだろ」って答えたらちょっと変な顔して、 「だから音楽聴きながら何してるのよ」って聞き返してくる。
こんなやり取りをしていて、多くの日本人にとって音楽って、いつの間にか「なんかやってる時についでにかけとくもの」になってるんだなぁと思わされた。
僕もこないだまでそうだったので何もいえない。
でも本当久しぶりに、スピーカの前に座って音楽そのものに聴き入るっていう行為に没入してる自分に、女房に言われて初めて気づいた次第。

DACとスピーカ

長らくオーディオ関係から遠ざかっていたのだが、ウォークマンの買い替えと共に何故か再び火が点いてしまった。

先日SONYから発売になったUDA-1というDAコンバータと、それにセットっぽく発売されているスピーカSS-HA3を部屋に連れてきて、そのためにホームセンターで板を買ってきて棚など自作したところ。

http://www.sony.jp/system-stereo/

ホストPCは、ノートとしては静かなMacBookProがあまり使われず放置されていたのでそれを使用している。正直Windowsほどいいソフトが揃っていない気がするのだが、QH77はファンの音がうるさいのでこれでよしとしよう。QH55/Mが出たことでQH55/Jが値崩れしたら、それを買ってこようか思っている。

肝心の音は、この価格でこの音なら十分納得である。日本の住宅事情を考えたシステムというか。棚で頭の高さぐらいまでスピーカを持ちあげてやると、あまり大きな音にしなくとも侮れない音場ができあがる。スピーカの前から離れたくなくなるほどである。流石にドックスピーカとは次元が違う。

カナル型イヤホンXBA-H3の音もなかなかのものだが、ずっとつけていると耳が壊れるのではないかという不安に付きまとわれるので、家にいる時はDACを使うことにする。