曖昧な用語法の研究

論理屋が論理的な語りをしない／出来ない、という現実がある。諺に、「医者の不養生」「紺屋（こんや or こうや）の白袴」とかあるけど、ちょっと違うな。他人のために尽くしていて自分には手が回らない、ってのとは違う。「儒者の不身持（じゅしゃのふみもち）」「坊主の不信心（ぼうずのふしんじん）」、だいたいあってる気がするが、ドンピシャじゃない。

諺はいいとして、論理学や論理ソフトウェア（自動証明系、証明支援系、論理型プログラミング言語など）の用語法の混乱・混沌が悲惨に酷い事は、それ自体が興味と研究の対象になる気がする。酷いと愚痴を言っているだけでなくて、どう酷くて、なぜそんなに酷いのか、どうやって酷さを解消するのか、を真面目に考えてみる。

事例としては、Isabelleを使う。今現に悩んでいるし。Isabelleの公式（パッケージ同梱）文書は1600ページ（ちょうど）ある（Isabelleの文書 - 檜山正幸のキマイラ飼育記 メモ編）。他に、isar-overview, 1990manual, foundationあたりを対象にすればいいだろう。

曖昧性（多義性）は文脈により解決されると考えられるが、文脈とは何か？ がわからない。曖昧語と非曖昧語の対応関係を解釈（意味写像）と考えて、解釈の非曖昧性＝確定性が増すような現象を定式化できればいいのだろう、たぶん。

Isabelleで分かったことのひとつは、実装で使っているプログラミング言語、データ構造、アルゴリズムが、コミュニティ（主にポールソンとウェンツェル）が使う用語法に大きな影響を与えていることだ。彼らにとっては自明で当然であっても、大部分の人にとって実装内部は知らない世界。それで齟齬が生まれる。

上記のことは、1980年代、90年代の資料を読んで分かった。いつでも、そのような由来まで分かるわけではない。「なんかの事情で、変な呼び名や言い方が発生し、それがコミュニティに定着した」という程度の予想しかできないだろうが、まーそれでもいい。