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

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

2009-10-23 (金)

快復傾向

| 08:48 | 快復傾向を含むブックマーク

インフルエンザじゃなかった。風邪、直ってきた。

けど、温度差過敏体質の僕には、みなさんが快適と感じる10度から20度の気温が鬼門だから、しばらくは要注意。つうか、7月末から8月(気温≧25度)を除いて年中要注意。四季のある国には、ほんとに向いてないわ。

確かになー

| 08:45 | 確かになーを含むブックマーク

次男:「あの人、大臣なんでしょ?」
父親:「うん。前原 …えーと、国土交通大臣かな」
次男:「あの大臣さ、ラクダに似てるよね」

うん、よく似てる。

当方記事には過ぎた続編、よみがえる妄想*1

| 10:39 | 当方記事には過ぎた続編、よみがえる妄想*1を含むブックマーク

ちょうど3年前(2006年10月28日)のエントリー「古典論理は可換環論なんだよ」へのトラックバック、「なんだろな」とか病み上がりのモンヤリ頭でたどってみました。ンガッ。id:tri_iro さん、この書きっぷり、こりゃ基礎論のプロですよね -- 「ゲーデルの不完全性定理を代数学を使って表現してみた」

僕は、古典論理と可換環の関係を、初等的計算を愚直にガリゴリやれば分かる範囲でとりあえず書いてみたのですが、tri_iroさんがより発展的で深い内容、なんと2007年の結果を示唆するようなところまで書いてくれました。「続き」とかいうと失礼になりそう、レベルが違い過ぎますからね。

再帰的可算イデアルとか実効的閉集合とかになると、僕はもうよく知らない。「3. スペクトルの空間: 記述集合論,再帰理論,位相と測度」以降に書いてある話は「ほえー、そんなことがあるんですか」という感じ。いやー、すごいもんですな。

それで思い出してみると、「古典論理と可換環の関係」に何で僕が興味を持ったかというと、「コンパクト性定理はなんで『コンパクト』っていうんだ?」とかどうでもいい好奇心もあったし、「古典論理は可換環論なんだよ」の最後で述べたように、手計算だけ頑張れば割と面白い結果が出るので楽しいって理由があります。

もうひとつの下心として、例によって計算(computation、主にコンピュータの行為)の話に適用できないかなーと探っていた(妄想していた)のです: p, q などを古典論理の命題(構文的には論理式)として、M, N などをモデルとします。M |= p は「Mがpを満足(充当、satisfy)する」ことを表すとしましょう。ライプニッツは「性質で区別できないモノは同じとみなせ」と言ったとか言わないとかなんで、「すべてのpに対して M |= p ⇔ N |= p」のとき M ≡ N と定義します。

いま定義した関係≡はモデル全体の集まりModel(集合かどうかは不明)の上の同値関係になります。Model/≡ は、Modelより小さくなってはいますが、これだけではあまりハッキリとしません。ところが、{p∈命題 | M |= p} のほうはブール代数のイデアル(フィルターと言っても事実上同じ)になり、このイデアルと(Model/≡)の要素が1:1に対応します。多少のゴニョゴニョで、(Model/≡)をハッキリとした位相空間と捉えていいことになります。

モデル全体という茫漠とした集まりに自然な同値関係を入れると、サイズの小さな集合*2になるばかりか、位相まで付いて来るという実にありがたい状況。古典命題論理の場合では、モデルとはいっても、命題変数への真偽値割り当てに過ぎないので、モデル全体をイメージできないわけでもないですが、もっと事情が複雑になると、モデル全体はほんとにとらえどころがありません。

計算で便利に使える論理として、状態遷移による作用を様相オペレータと考えた一種の様相論理があります。そのモデルの全体は余代数の圏としていちおう定式化はできます。が、適当な同値関係で割ってサイズの小さな集合になれば扱いやすいし、なんらかのスペクトルとしての位相(ないしは位相もどき)が入ればもっと扱いやすいでしょう。

ちょと考えた後で、これは、僕の知っている道具、僕の知力・気力ではジェンジェンできそうにない、と判断してサッサとあきらめました。計算向け論理のスペクトルって誰か作っているんかな? ご存知の方、教えてください。

ソフトウェアの意味論は何のため/誰のために必要か

| 12:32 | ソフトウェアの意味論は何のため/誰のために必要かを含むブックマーク

Catyを素材/具体例として、表題のような話をします。


Catyの用途はWebフレームワークだけど、構造としてはCatyスクリプトのインタープリタの形になっています。スキーマ言語だのテンプレート言語だのもあるんですが、これらの言語もCatyスクリプトを補助する役割だと言えます。実装言語であるPythonでさえ、Catyスクリプトのプリミティブ・コンポネントである“コマンド”を書くための言語だと位置づけることができます。

Catyシステム内で支配的な立場にあるCatyスクリプトは、たいそうな言語かというと、実に低機能なんです。自分では何も出来ない王様であるCatyスクリプトのもとで、コマンドが兵隊、スキーマが参謀、テンプレートが交渉人といった役割でしょうか。これら配下の者達がそれなりに頑張るので、王様は大雑把な短い指示をすれば済む、というわけ。

こういう構造なので、Catyスクリプトは、プログラミング言語としては珍しい要求のなかにいます -- それは「できるだけ低機能であれ」です。Catyスクリプトが計算や制御の能力を持つと、厳密分離の原理が破れてしまうので、低機能にとどめる必要があるのです。結果的に、Catyスクリプトの言語仕様はオモチャ(Toy Language)のように単純です。

実用システムの中核部が単純なプログラミング言語になっているという状況は、なかなかに興味と食指をそそられます。(自分でそういう状況にしているのだろう、と言われれば、まーそうですけど。)プログラミング言語が単純だと、普通では出来ないことが出来る可能性があります。例えば、完全な意味論(semantics)を提供することです。

プログラミング言語がある程度の規模と複雑性を持てば、意味論を構成するのは大変な労力となります。しかし、Catyスクリプト程度に単純であれば、意味論を完全に書き下すことも出来ない作業ではありません。実際、僕はやるつもりです。

さて、そんなことして何かいいことあるのか? まず仕様が明確になります。これは、テストを作る指針を与えます。CatyのテストはCatyスクリプト(の機能拡張版)で書ける(はず)なので、自分の正しさを自分で書き下せ、自分で確認できます。インタプリタが動き出せば*3、自己完結的で実行可能な correctness の定義が得られます。

正しさの基準が「形式的な記述」と「実行可能なモノ」として存在することは、技術的/実用的に望ましいことです。しかし、僕が「より重要だ」と思うのはメンタルな効果です。ソフトウェアに意味論(モデル)が在るということは、不安を解消し自信を持つために絶大な効果があります。

ソフトウェアの設計と実装には、常に不安が付きまといます。それを払拭する方法は色々あります。精神論と根性論はまったく何の役にも立ちません、むしろ有害です。経験と勘は役に立ちますが正しい保証がありません。歪んだ経験と間抜けな勘だとたぶん失敗するでしょう。イチかバチかに賭ける人もいますが、そんなことで博打を打つのは僕はイヤです。無鉄砲と勇気を混同しちゃいけない。

適切な手順で作成された意味論は、万能完璧ではないけれど、ある範囲内で正しさの保証を与えてくれます。「ある範囲内で正しさが保証」されていれば、自信と余裕が生まれます。周辺部分で遊びや実験を入れてもいいだろうし、負けてもダメージのない(勝てば十分うれしい)博打を打つことだってできます。

すべてが曖昧であやふやな状況下で、不安と戦い続けるのは心理的にキツすぎます。僕には耐えられそうにありません。いや、耐えられない。耐えられなかった。だからもうイヤなんです。ほんとに二度とゴメンだ。

つまり、拠り所となる意味論を構成することは、僕が(たぶんKuwataさんも)不安に苛<さいな>まれず、穏やかな精神状態でいるために必須の作業なのです。


今書いたことは当事者の問題で、大部分の人には興味がないことでしょう。特に、Catyがほんとのターゲットにしている人々=プログラマではないWeb制作者には、まったくどうでもいい余計な話です。

ある人にこう忠告されました; 僕がCatyの意味論やら何やらを書いたり話したりすると、難解な印象を振りまいて、Catyのプロモーション上は悪影響がある。はい、そのとおりだと思います。困ったもんだ。

Catyに関する2つのお知らせ

| 18:05 | Catyに関する2つのお知らせを含むブックマーク

Catyと言えば:

BPStudy#26 にて、Catyをご紹介します。僕は、事の発端とかドウデモイイコトはしゃべりますが、実質の内容はKuwataさんのプレゼンとなるでしょう。

リリース2は、今週は間に合いません。予想より作業量が多かったのと、Kuwataさんも僕も、なぜか揃って今週は病気でダウン -- これじゃダメだわ。リリース2では、Webサイト作成機能はだいぶ変わります。スンマセン。来週以降です。

*1[追記]見出しから「る」を取りました。「る」があると、「過ぎたは及ばざるがごとし」を連想されそうだから。用法としては、「ウチの息子には過ぎた嫁でございます」とか使う「過ぎた」です。「できが良すぎる」の意味。[/追記]

*2[追記]日本語が大変曖昧でした。集合のなかでサイズが小さなモノのことではなくて、集合であることがすなわちサイズが小さいことだって意味です。[/追記]

*3:インタプリタの作成途中では、手作業+目視か、実装言語によるテストコードを使うことになります。