型宣言、ホーアトリプル、関数定義は同じもの

内容：

1. 型宣言とホーアトリプル
2. 関数定義とホーアトリプル
3. ホーア論理とホーアセオリー
4. 伴意順序
5. いろいろな概念を統合できるかな

型宣言とホーアトリプル

fが関数だとして、f:X→Y という形はfの型宣言だとみなせます。話を簡単にするために、「型とは集合だ」と考えましょう。これから考える集合 A, B, C などは十分にに大きな集合Uの部分集合だとします。コンピュータで計算する関数に関しては、そんなUが存在します。

p, q などが論理式だとして、ホーアトリプルを p{f}q の形で書きます。pが事前条件、fが実行文（を表す関数）、qが事後条件です。ホーアトリプル p{f}q の意味は次のとおりです。

• p(x) が成り立つ状況で f をすると、q(f(x)) が成り立つ。

論理記号で書けば、∀x.[p(x)⊃q(f(x))] です。ここで、「⊃」は「ならば」を意味する含意記号です。

ホーアトリプルを少し書き換えてみます。A = {x∈X | p(x)}, B = {y∈Y | q(y)} という集合を定義すると、p{f}q は次のように書けます。

• x∈A ならば f(x)∈B

あるいは、fによる集合Aの像を f[A] と書くことにすれば次のようになります。

• f[A]⊆B

さて、型宣言 f:X→Y の意味をあらためて考えてみると、「x∈X ならば f(x)∈Y」、あるいは f[X]⊆Y ってことです。つまり、ホーアトリプルと変わらないですね。

ホーアトリプル p{f}q において、論理式（条件式）p, q の代わりに集合を書いてもいいとすると、A{f}B のようになります。この書き方を使うと、f:X→Y は X{f}Y ってことです。

関数定義とホーアトリプル

関数を定義するときは、なんらかの式を使う時が多いですね。例えば、f(x) := x*x + 3 とか。しかし、式を使わなくても対応関係が定まればいいので、x∈X と f(x)∈Y の組 (x, f(x)) を全部列挙してしまえば関数を完全に定義したことになります。

関数の定義域Xが無限集合だと“列挙”は（人間には）無理ですが、有限集合なら列挙可能です。例えば、X = Y = {1, 2, 3} だとしましょう。次の列挙により関数が定まります。

1. f(1) = 2
2. f(2) = 1
3. f(3) = 2

今、A = {1}, B = {2}, C = {3} と置くと、f(1) = 2 とは、f[{1}] = {f(1)} = {2} ですから、f[A] = B と書けます。あるいは、f[A]⊆B でも同じことです。これは、ホーアトリプルの形式 A{f}B で表記してもいいですね。先の関数定義は次のホーアトリプル群と同じです。

1. A{f}B
2. B{f}A
3. C{f}B

つまり、ホーアトリプルの事前条件／事後条件をうんと絞り込んでしまえば、関数の対応関係を完全に決定できることになり、関数定義そのものになります。

A, B, C は既に定義した集合として、D = {2, 3} とします。次のようなホーアトリプル群を考えます。

1. A{f}B
2. B{f}A
3. C{f}D

三番目の C{f}D は、 f(3)∈{2, 3} のことですから、f(3) の値は決定できません。しかし、2か3のどちらだという情報は含まれます。別な解釈として、集合 {2, 3} が f(3) の値だと考えれば、これもまた関数定義です。これは、非決定性の関数を定義したことになります。

ホーア論理とホーアセオリー

関数の型宣言、ホーアトリプル、関数定義は、結局は同じものです。どの程度まで関数（写像）を決定するか、という程度の差があるだけです。以下では、中庸の存在であるホーアトリプルを基準に考えましょう。

A{f}B のような集合を使ったホーアトリプルは、次の論理式に翻訳できるのでした。

• ∀x.[x∈A ⊃ f(x)∈B]

含意「⊃」以外に連言「∧」も入れた論理式を考えれば、含意連言論理ができます。必要があれば否定も入れて、古典論理のすべての能力を使ってもいいでしょう。

{A{f}B, B{f}A, C{f}D} のようなホーアトリプルの集合は、連言で解釈します。つまり、3つのホーアトリプルからなる集合は、次の1つの論理式と同じです。

• A{f}B ∧ B{f}A ∧ C{f}D

完全に展開すれば：

• ∀x.[x∈A ⊃ f(x)∈B] ∧ ∀x.[x∈B ⊃ f(x)∈A] ∧ ∀x.[x∈C ⊃ f(x)∈D]

ホーアトリプルをベースとしたホーア論理式に、適当な公理と推論規則を入れると証明系（proof system）ができます。この証明系が、通常ホーア論理と呼ばれているものです。

証明系としてのホーア論理の証明可能性を |- で表します。α₁, α₂, ..., α_n, β がホーア式（ホーア論理の論理式）だとして、α₁, α₂, ..., α_n |- β とは、「α₁, α₂, ..., α_n を仮定してβが証明できる」ことです。あるいは、「単一の論理式 α₁∧α₂∧ ... ∧α_n を仮定してβが証明できる」と言っても同じです。

ホーア式の集合Tが次の性質を持つときセオリーと呼びます*1。

• α₁, α₂, ..., α_n ∈T、α₁, α₂, ..., α_n |- β ならば、β∈T 。

つまり、セオリーとは証明に関して閉じている論理式の集合のことです。論理式の集合Γが与えられると、その集合を含む最小のセオリーTh(Γ)が決まります。これは、証明という“演算”に関する閉包です。

伴意順序

{α₁, α₂, ..., α_n} と {β₁, β₂, ..., β_m} がホーア式の集合のとき、{α₁, α₂, ..., α_n} が {β₁, β₂, ..., β_m} を伴意（entail）するとは次のことだとします。

• 任意の i = 1, 2, ..., m について、α₁, α₂, ..., α_n |- β_i が成立する。

{α₁, α₂, ..., α_n} を仮定すれば、β_i 達は証明できるということです。別な言い方をすると、β_i∈Th({α₁, α₂, ..., α_n}) です。Th({β₁, β₂, ..., β_m}) ⊆ Th({α₁, α₂, ..., α_n}) とも書けます。

この伴意関係を記号「|⇒」を使って次のように書きます。

• {α₁, α₂, ..., α_n} |⇒ {β₁, β₂, ..., β_m}

伴意関係は順序関係なので、伴意順序（entailment order）とも呼ぶことにします。

いろいろな概念を統合できるかな

ホーア式の集合 {α₁, α₂, ..., α_n} があると、これは型宣言の集まりとも、ホーアトリブルによる仕様の記述とも、非決定性関数の定義ともみませます。もうひとつの集合 {β₁, β₂, ..., β_m} とのあいだに伴意関係があれば、それは次のような解釈ができます。

• 型宣言のあいだに互換性がある。
• 特定の仕様がより一般的な仕様に適合している。
• 実装が仕様を満たしている。

ホーア式の集合は、論理的な操作の対象となると同時にプログラムの仕様や実装（定義）を記述しています。ここでは、プログラムは部分関数や非決定性の関数でモデル化されています。非決定性の関数とは関係（relation）と言っても同じです。そして、関数や関係の背後にはSetやRelのような圏があります。

圏Setや圏Relと、伴意順序のような順序を一緒に扱えないでしょうか？ そのひとつの候補が順序付き関係の圏ORelです。もちろん、インスティチューションやインデックス付き圏や構文生成モナドなどの他の方法もありますが、ホーアセオリーと順序付きの圏は割と相性が良さそうです。

*1:セオリーは、ホーア論理に特有のものではなくて、論理一般に関して定義できる概念です。