2012年6月23日土曜日

例外のない法則は存在するか

自己言及のパラドックスの一例として、「例外のない法則はない」があげられることがある。なぜならもしこの言明が普遍的に妥当するとすると、一種の法則になってしまうわけで、そうすると自分自身の例外、つまり例外のない法則があってしまうことになる。

もっとも、これがパラドックスになるには、「例外のない法則はない」が真である、という前提がいる。もし、これを認めなければこれはパラドックスではなく、例外のない法則があることの証明と見なせる。つまり背理法を使って、例外のない法則がないとすると、上の議論から例外のない法則があることになってしまって仮定と矛盾するから、仮定の否定、例外のない法則があるが成り立つ。


この手の議論は古代からいろいろあると思うし、ツッコミどころ満載だと思うのだけど、ここでは上の証明に含まれる具体例、という観点から考えてみたい。とは言うものの、上の証明は背理法を使っているので、そのままでは具体例を抽出できない。しかし証明を少し変えることで、具体例を与える証明を作ることができる。

まず、「何か(状況や立場によらず)例外のない法則が存在する」という文を考える。もし、これに例外があれば、「例外のない法則は存在しない」ことになる。しかしこれは上の議論からありえない。よって、この文自体が例外のない法則といえる。

つまり、上の証明に含まれる具体例は「何か(状況や立場によらず)例外のない法則が存在する」というこれまた自己言及的な文である。とすると、上の証明はあまり面白くないもののように私には思える。多分、本当に普遍的であることを示したいのは、数学とかある種の倫理規範とか言うものであるのだろうから。


(ちょっと論証に無理があったかな。)

2012年6月17日日曜日

モデル検査の「モデル」とは

モデル検査の「モデル」とは何かを少し考えてみたい。というか考えるも何もモデル検査の開発者の一人Clarkeの文章を発見したので、それを報告するだけなのだけど。

まず、最近の一般的な理解は、どうもソフトウェアやハードウェアを単純化した「モデル」、ということであるらしい。例えば、Wikipediaには

モデル検査(Model Checking)とは、形式システムアルゴリズム的に検証する手法である。ハードウェアソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様時相論理の論理式の形式で記述することが多い。

とある。またPrinciple of Model Checking
 
には
Model-based verification techniques are based on models describing the possible system behavior in a mathematically precise and unambiguous manner... ...This provides the basis for a whole range of verification techniques ranging from an exhaustive exploration (model checking) to experiments with a restrictive set of scenarios in the model (simulation), or in reality (testing).

とあって、「モデル駆動テスト」などのモデルと同じ意味だとしているみたい。 まあ、モデル駆動開発のモデルはUMLだったりして数学的に厳密とは限らないから、この本の言っているモデルとはちょっと違うけど。

でもそれは私の認識とは違っていて、私の認識では、モデル検査の「モデル」は数理論理学の「モデル」から来ている。数理論理学では、論理式で表された言明や公理と、それを満たしたり満たさなかったりする構造の対を考えるのだけど、構造が言明を満たしている時、その構造はその言明の「モデル」という。

ただ、何を典拠にそういう認識を正当化したら良いか分からなかったところに、Clarkeの文章 The Birth of Model Checking を発見した。これによると、

The Model Checking problem is easy to state: Let M be a Kripke structure (i.e., state-transition graph). Let f be a formula of temporal logic (i.e., the speci cation). Find all states s of M such that M; s |= f. We used the term Model Checking because we wanted to determine if the temporal formula f was true in the Kripke structure M, i.e., whether the structure M was a model for the formula f.
ここで、モデル検査では時相論理式というもので仕様を書くわけだけど、それに対応する構造はKripke構造と言われる。システムの状態遷移は簡単にKripke構造と見なせるわけだけど、そうみなしたときあるシステムが与えられた時相論理式のモデルになっているかを判定するのがモデル検査、とClarkeは言っている。というわけで、私の認識は正しいことになると思う。Clarkeは引き続いてこうも言っている。
Some people believe erroneously that the use of the term "model" refers to the dictionary meaning of this word (e.g., a miniature representation of something or a pattern of something to be made) and indicates that we are dealing with an abstraction of the actual system under study.
というわけで、モデル検査の「モデル」を考えているシステムを単純化したもの、という見方はすくなくとも原義からは離れた見方だということになる。

ただ、モデル検査を売り込むとき、モデル駆動開発のモデルと(暗に)同一視させることが行われているような気がして、多分、元々の意味は忘れられて行くんでしょうね。

2012年6月10日日曜日

ソフトウェアテスト技法ドリル



仕事で役に立つかと読んだ。うーん、どうだろう。仕事に役に立つかどうかは別として、なんかかっこよくないというか、未来じゃない。結構最近書かれた本なんだけどね。

まず最初に、仕様書を3色ボールペンを使って色をつけながら読むことを薦めているんだけど、紙に印刷するのか、分厚くなるんだろうなという感じ。確かに紙のほうが集中して読める気がするし、4色ボールペンは私もよく使っているけど、でも未来じゃない気がする。p83の「オブジェクト指向開発の場合は、データが隠蔽されてクロスリファレンスを解析しにくい場合もあるかもしれません。ところが実際にやってみると多くのケースで隠蔽がきちんと実装されていないためクロスリファレンスが取れるようです」には笑ってしまった。ちゃんと実装されていないことに依存するテスト技法って。

ここで「未来」てどういうことかというと、多分「そういうことができるのか!」、「そういうやり方をするのか!」という驚きのことだと思う。その点、この本にはそういう驚きがない気がする。教科書的な本ではなくて、テスト技法の著者独自のまとめがしてあるのだけど、それがなんかふーんという感じがしてしまうのだ。

それはさておき、真面目な話。この本はテスト技法そのものよりも、テストの考え方に重点をおいたものだ。それがどの程度価値があるかは、テストについてあまり勉強したことが無いので何とも言えないけれど。テスト技法についてもいろいろ紹介されているが(著者考案のHAYST法とか)あまり深くないので、この本を読んだだけではあまり分からなかった。一度テストについて勉強した人が、それを体系的に理解し直す本と言った感じ。

で、実務に役に立ったかというと、とりあえず5W1Hの定義を確認するのに使った。それ以外はまだだけど、これから使うかもしれない。









2012年6月2日土曜日

コーヒーの芳香を記述してみよ!

という文章がヴィトゲンシュタインの哲学探究にあったと思う。そのあと、「新しい言葉を用意すればいいのか。」と続いたはず。

これを読んだ時は、なるほどなあ、記述なんてできないよなあと思ったんだけど、2,3年前近所にスペシャリティコーヒーの店ができて、まさにコーヒーの芳香を記述している業界があることを知った。

スペシャリティコーヒーとは、正確な定義はないそうだが、上記のようなコーヒーの利き味(カッピングという)ができる専門家(カッパー)が(通常、個別に農場から)直接買い付けたコーヒーのことを言うようだ。カッピングといって、テイスティングと言わないのは、主観を排除して客観的な評価を行うからだとのこと。

カッピングで芳香をどうやって記述するかというと、例えば「バニラのような」とか「はちみつのような」、「花の香り」といったようにたとえで記述する。コーヒーに花の香がするんだろうかと少し思ったけど、そう言われて飲んでみると確かに果実のような香りがしたりする。これはスペシャリティコーヒーとして売られているものが、香り高いものだということもあるのだろう。実際、普通のコーヒーとは全然違う味がする。まあ、私は「はちみつのような」とか細かくは分からないんだけど。

カッピングでは味を記述するだけではなくて、味の点数化も行う。私もちょっとやらせてもらったけど、点数化するところまでは無理だった。これも客観的なものを目指していて、実際熟練したカッパー同士では、スコアリングが大体一致するとのこと。

カッパーになるには、今のところとくに資格試験のようなものはなくて、他のカッパーから認められれば良いそうだ。カッパーとして認められるまでは、自分で豆を焙煎してカッピングして、他のカッパーの意見を聞いて…ということを繰り返すらしい。

さて、このことから分かる教訓だが、まずアナロジーというのは我々の言語を拡張する強力なメカニズムだということが分かると思う。それから、ある「言語ゲーム」が社会で認められるためには、その言語ゲームについて一致する集団があることが、少なくとも条件の一つ(必要条件とも十分条件とも思わないが)になるということが分かるのではないか。私は、哲学探究の、いわゆる私的言語について議論しているとされる部分はよく理解出来ていないし、特に私的言語の不可能性を主張するするつもりもないのだけど、「社会的に認められた言語」になるためにはそれを一貫して使うことができる言語使用者の集団がある、ということがわりと自明な条件だとは言えると思う。