Catyは既に動いているので、あまり大幅な変更はしたくありません。そもそも、我々のように人的リソースが極小のプロジェクトでは、一度に大きな労力をかけることは不可能なので、ボチボチ・チビチビとやっていくしかないし、それでもそれなりの効果が上がる方法しか採用できません。どうしたらボチボチ・チビチビと機能改善ができるでしょうか。
型安全性の判定系とは、プログラムの型に関する演繹系（deduction system）です。まず、この演繹系があってもなくてもシステム全体に致命的な影響を与えないことが重要です。「ないならないでも動く」ってことです。また、演繹系の出来が悪かったり機能が非力だったりしても、「それなりに使える」ことも条件になります。動かしながら、ボチボチ・チビチビ作るんだから、こういう要求になります。
上記の要求を満たすように演繹系を作っていく際に、演繹系一般に関する洞察がとても役に立ちます。ボチボチ・チビチビ作る方法を示唆してくれます。我々に必要なのは「出来の悪い演繹系に関する理論」なのですが、たいていの演繹系は完璧ではあり得ないので、通常の「演繹系の理論」が出来の悪い演繹系にも適用できます。
内容：
- 決定性を持たない演繹系
- 4値論理／3値論理を使う
- 良い性質と悪い性質
- Catyの型安全性命題
- ダメなプログラムを表す命題
- 良い、悪い、その他
- 判定能力をだんだんに上げる
決定性を持たない演繹系
Sがなんらかの演繹系だとして、P、Qなどは演繹系Sが扱う命題（論理式）だとします。命題Pを演繹系Sで形式的に証明できることを次のように書きます。
- |-S P
これは、Sを外から眺めたメタな主張です。命題Pの否定（があるとしてそれ）を ¬P と書きます。演繹系Sが次の性質を持つとき、決定性を持つと呼ぶことにします。
- どんな命題Pに対しても、|-S P または |-S ¬P 。
この決定性を「完全性」ということもありますが、モデル理論の完全性と紛らわしいので「決定性」にしました。
ゲーデルの定理によれば（「プログラマのための「ゲーデルの不完全性定理」(1)」とか参照）、ある程度の能力を持つ演繹系は決定性を持たなくなります。これは原理的な話ですが、単に演繹系（の実装）の出来が悪くて決定性を持たないことはいくらでもあります。例えば、原理的には決定可能（十分に単純）な体系なのに、そのソフトウェア実装が手抜きであった、てなことです。
演繹系Sを、命題（のデータ）を引数に渡されて計算結果として真偽値を返す関数と考えましょう。すると、Sが決定性を持つことは：
- どんな命題（のデータ）Pに対しても、S(P) = true または S(¬P) = true 。
S(¬P) が必ず S(P) の値の否定となることを仮定すれば、次のように言い換えられます。
- どんな命題（のデータ）Pに対しても、S(P) = true または S(P) = false 。
Sが決定性を持たないときは、次のようになります。
- S(P) = true でもなく S(P) = false でもない命題（のデータ）Pが存在する。
上のようなPは決定不能な命題となります。演繹系が「決定性を持たない」とは、当該演繹系のなかに決定不能な命題が存在することです。原理的に決定不能な状況だけでなく、Sの出来が悪いせいでもかまいません。むしろ、ここで問題にしたいのはSの出来の悪さ＝能力不足です。
4値論理／3値論理を使う
「S(P) = true でもなく S(P) = false でもない」とはどういうことでしょうか。ソフトウェア的に考えると、Sの計算が無限走行をして結果を出さないことです。停止しないので、trueもfalseもありません。無限走行を、⊥（ボトム）という記号で象徴的に表します。⊥を使うと、S(P) の結果は「trueまたはfalseまたは⊥」の3値となります。
実用上は無限走行されると困ります。途中であきらめたことを表す値indefを導入します。S(P) = indef とは、「計算はちゃんと停止したが、trueかfalseかの決定はできなかった」ということです。{true, false, indef, ⊥} の4値真偽値の計算は次の記事で述べています。
演繹系を実現するソフトウェアは、⊥（無限走行）じゃなくてindefを返すように頑張ります、いや頑張らないようにします。頑張らないで早めにあきらめてindefを返せば、無限走行を避けられます。
手違いで無限走行や例外発生があるかもしれませんが、原則的には {true, false, indef} の3値で真偽値計算できるとしましょう。つまり、演繹系を実現するソフトウェアがまともに動いてくれれば、{true, false, indef} のどれかの値が返るとします。
良い性質と悪い性質
我々が実際に行いたいことは、プログラムコードを見て実行時の型安全性（type safeness）を判断することです。ソフトウェアの性質をソフトウェアに判断させたいわけです。演繹系に証明させる命題は、p（小文字ピー）を対象とするプログラムコードとして IsSafe(p) のような形です。
3値の結果を出す判定系を使う場合は、indefの可能性があるので、より精密な結果を得るために複数の命題を組み合わせるのが有効です。その一番単純（だが、割と強力）なケースは、良い性質と悪い性質の2つの命題を組み合わせることです。IsGood(p) と IsBad(p) の2つの命題を使うわけです。具体的にどんな命題を IsGood、IsBad として選ぶかは状況次第です。
一般論をしていても分かりにくいと思うので、Catyの型安全性の判定系で説明をします。
Catyの型安全性命題
Catyは、基本となるコマンドを組み合わせてスクリプトを作り、そのスクリプトを実行させるシステムです。
コマンドとは、1入力1出力の関数のことです。基本となるコマンドは型宣言を持ちます。f:: A->B という形の型宣言は、「コマンドfの入力の型がAで、出力の型がB」という意味です。型はデータの集合を意味するので「型＝集合」と考えてかまいません。以下では、型と集合を区別しません。
fとgがコマンドのとき、その結合（composition）はパイプ記号を使って f | g と書きます。3つのコマンド f, g, h のこの順での結合なら f | g | h です。ラムダ式で書くなら、(f | g | h) ≡ λx.(h(g(f(x)))) です。ここで記号「≡」は、左右は違う記法だが同じ意味だ、ということです。実引数を渡す“適用”もパイプ記号です。
- (a | f | g | h) ≡ (λx.(h(g(f(x)))))(a)
ラムダ式よりずっとスッキリ書けるでしょ :-)
f:: A->B 、g:: C->D だとして、パイプ結合 f | g が型安全とは B⊆C のことです。パイプ記号ごとに集合の不等式（包含関係式）を書いて、すべてのパイプ記号にわたって論理ANDをとれば、それが型安全性を主張する命題になります。つまり、型安全性の命題は、集合に関する連立不等式系の形になります。
h:: E->F だとして、f | g | h の型安全性は、最初のパイプ記号から B⊆C、2番目のパイプ記号から D⊆E です。寄せ集めて (B⊆C ∧ D⊆E)、あるいは連立不等式系の形にして {B⊆C, D⊆E} となります。型変数を含まない場合だけを考えれば、これらは原理的には真偽を決定できる命題です。
ダメなプログラムを表す命題
プログラムpが p ≡ (f | g | h) であり、コマンド f, g, h の型宣言が先の通りだとすると、「pが良いプログラム」であることは次のように表せます。
- IsGood(p) ≡ (B⊆C ∧ D⊆E)
内容的には、2つのパイプ記号の位置で型安全だという主張です（IsSafeと同じ）。
さて、では「pが悪いプログラム」であることはどう表せるでしょうか？ ここで考えている型安全性は、パイプ記号の位置での集合の包含関係に基づくので、悪いプログラムとは、パイプ記号の位置でデータがサッパリ繋がらないプログラムです。
- 最初のパイプ記号の位置でデータがサッパリ繋がらない ≡ (B∩C = 0)
- 二番目のパイプ記号の位置でデータがサッパリ繋がらない ≡ (D∩E = 0)
ここで、0は空集合を意味します。
どちらか一方のパイプが繋がらないと、全体としてデータフロー（制御フローでもある）は脱線するので、「pが悪い」という条件は次のように書けます。
- IsBad(p) ≡ (B∩C = 0 ∨ D∩E = 0)
良い、悪い、その他
先に進む前に注意を； IsGoo(p)∧IsBad(p)、つまり良いプログラムであると同時に悪いプログラムであるpは存在するのでしょうか？ これはあります。f:: A→0、g:: C->D のとき、p ≡ (f | g) に対しては IsGood(p) と IsBad(p) が同時に成立します。このケースでは、fが無限走行したり例外を投げたりするので、入出力の情報だけでは判断ができません。矛盾しているというよりは、判断に別な情報が必要なのです。
念のために、IsReallyGood, IsReallyBad を定義しておきましょう。
- IsReallyGood(p) ≡ (IsGood(p) ∧ ¬IsBad(p))
- IsReallyBad(p) ≡ (IsBad(p) ∧ ¬IsGood(p))
IsReallyGoodとIsReallyBadのもとになるIsGood、IsBadは、真偽（trueまたはfalse）以外にindef（ワカラン、アキラメタ）も返す可能性があるとします。三値の真偽値の組み合わせを考えると、IsReallyGoodとIsReallyBadの可能性は次のようになります。
| B↓G→ | true | false | indef | |
|---|---|---|---|---|
| true | - | 悪い | - | |
| false | 良い | ワカラン | ワカラン | |
| indef | - | ワカラン | サッパリワカラン |
良いプログラムは型安全性（集合の包含関係）の観点からは安心して実行できます（その他の問題は含むかも知れませんが）。悪いプログラムは実行しても常に失敗するので、絶対に実行しちゃいけません。その他はハッキリしません。
判定能力をだんだんに上げる
プログラム（を表すデータ）pを与えられて、IsReallyGood(p)とIsReallyBad(p)を計算する判定系を考えましょう。この判定系が、常にどんなプログラムpに対しても IsReallyGood(p) = indef、IsReallyBad(p) = indef と出力したらまったくの役立たずです。でも、そんな役立たずな判定系から出発して、少しでも機能を追加すると、少しだけ「良いプログラム／悪いプログラム」を識別できるようになります。だんだん判定能力を上げていくと、今まで「ワカラン」と判定されていたものが「良い／悪い」と判定されるようになるでしょう。
いくら頑張っても「ワカラン」が残っても、まーそれはそれでいいのです。型安全だと判定されても、実行時型チェックが省けるとも限りません（型宣言の間違いの可能性がある）。まったくワカランから少しワカルようになるだけでも価値があると思います。そして、継続的な改善／パワーアップができる枠組みが重要だとも思うわけです。
出来の悪い演繹系に関するモデル論の話もあるのですが、それはまた別の機会に。
