「すべての」と「ある」

はじめに

この記事は、PureScriptアドベントカレンダーの２１日目の記事です！

本記事では、全称量化(universal quantification)「∀」と、存在量化(existential quantification)「∃」を、論理とプログラミングという２つの視点から眺めることで理解を深めたいと思います。

論理

おそらくご存知の方も多いと思いますが、もともと∀や∃は論理学から来ている概念です。なので、いきなりプログラミングの話でなく、まずは論理からおさらいしてみましょう。

命題論理

論理とは、「正しい推論とはなにか」を定式化する学問ですが、一口に論理と言っても、いくつかの種類（体系）があります。最もシンプルなのが 命題論理(propositional logic) といわれるもので、命題論理では 命題(propositions) と、いくつかの命題から新たな命題を得るための 論理演算子(logical connectives)を議論の対象にします。

代表的な論理演算子を以下に列挙します:

• 論理包含(logical implication) ⇒
• 論理積(conjunction) ∧
• 論理和(disjunction) ∨
• 同値(equivalence) ⇔

たとえば、A, B, C, ... がそれぞれなんかしらの命題であるとき、これらを使って構成される
A ⇒ B, A ∧ B, (A ⇒ (A ∧ B)) ∨ (B ∨ (C ⇔ D)), ...　もまた命題となります。

論理学の体系とは、これらのconnectivesの使い方(推論規則)のコレクションであるということができます。
そして。各々の推論規則は、"２方向"のルールのペアで与えられます。
１つは、「既存の命題からどうやってそれらの命題とconnectiveで表現される新しい命題を導くか」を与える 導入則(introduction rule) で、もう１つは
「connectiveで表現される命題が既知であるとき、そこからどうやって新しい命題を導くか」を与える 消去則(elimination rule) です。

たとえば、⇒の導入則(⇒-intro)と消去則(⇒-elim)はそれぞれ以下のように表現されます:

⇒-intro

Γ, A ⊢ B
------------
Γ ⊢ A ⇒ B

... 命題Aを前提としたときにBが成り立っていれば、命題 A ⇒ Bを導くことができる.

⇒-elim

Γ ⊢ A   Γ ⊢ A ⇒ B
----------------------
Γ ⊢ B

... 命題Aと、命題A ⇒ Bがともに成り立っていれば、Bを導くことができる.

命題論理では、connectivesに加えて、「⊥」という記号で表現される特別な命題を使います。
これは「偽である命題」を表す記号です。⊥が義であるとは、⊥を結論づける導出は行えないことを意味します。
⊥を基本的な構成子に加えると、論理的否定のconnective ¬は以下で定義することができます:

¬A := A ⇒ ⊥

すなわち、「Aは成り立たない」とは、「Aを仮定すると偽が導かれる」ことであるということができます。

述語論理

さて、まだ記事のタイトルにある「すべての」と「ある」が出てきていません。というのも、これらを扱うには命題論理に「述語(Predicates)」という新たな構成子を追加して拡張した「述語論理(Predicate logic)」だからです。

命題論理では、それ以上分割できない（内部構造を持たない）アトミックな命題と、命題をconnectivesで連結して得られる命題のいずれかしか存在しません。
述語論理では、何かしらの集合Sを考え、Sの要素 に対して命題を対応付ける「命題値関数(proposition-valued functions)」を述語(Predicates)と呼びます。

たとえば、Sとして整数の集合Zをとると、以下のようなものは述語です。

P := λ(x∈Z). x > 2
Q := λ(x∈Z). xは素数
R := λ(x∈Z).P(x) ∧ Q(x) // == λ(x∈S). xは2より大きな素数

ただし、関数を表現するのにラムダ計算の記法 λ(x:T). tを転用しました。

述語自体は命題とは別物であることに注意が必要です。
述語が与えられた時に、その述語から命題を得るために使えるのが 量化子(quantifier) です。

ここで、記事のタイトルにある２つの量化子の１つ、全称量化子(universal quantifier) ∀が登場します。

∀記号は、以下の形で述語Pに作用して新たな命題を構成します:

R = ∀(x∈S). P(x)

この時、述語P(x)における変数xはもはや自由でなく、∀により 束縛されている といいます。
この命題は、「集合Sのどの要素xに対してもP(x)が真であるときに真となる命題」です。

∀量化子にも導入則と消去則の２種類のルールがあります。
まず、簡単な∀-elimがこちらです:

Γ ⊢ ∀(x∈S).P(x)
-----------------      if s ∈ S
Γ ⊢ P(s) 

見ての通りで、∀(x∈S).P(x)が成り立っていれば、適当に選んだSの要素sに対して P(s)が成り立つという主張です。

次に、以下が∀-introです:

Γ, x:S ⊢ P (x)
------------------
Γ ⊢ ∀(x:S). P (x)

これはやや直感的でないかもしれません。少し人語へ意訳すると、
「Sの要素を勝手に（ランダムに）選び、それにxと名前をつけたコンテキストにおいて、
(xの具体的な値に言及することなく) 命題P(x) が導けるなら、述語Pはxの値によらず成り立つ」
といいうことです。

Curry-Howard 同型対応

PAT-interpretation

さて、ようやくここまでのお話をプログラミングに絡める時が来ました。
キーとなるのは、Curry-Howard同型対応(Curry-Howard Isomorphism) です。

Curry-Howard同型対応とは大雑把にいうと、論理学における「命題と証明のなす構造（推論規則）」は、命題を型に、証明をその型を持つ値に置き換えると、綺麗に「型と項のなす構造（型付け規則）」と一致する」というものです。

Curry-Howard同型対応は、PAT-interpretation とも言う事ができます。PATは同時に２種類の読み方ができるオシャレな略語になっていて、

• Proposition-As-a-Type
• Proof-As-a-Term

の二通りの解釈ができます。
前者の読み方で「命題は型と対応する」とも読めますし、後者の読み方で「項（値）は証明に対応する」とも読めます。

この見方によると、型は命題と対応するので、たとえば命題AとかBといったものを、単にプログラミングの文脈では「型AとかBと読み替えなさい」ということです。

そして、「命題Aが成り立つ（正しい）」とは、「命題Aを結論づける導出が行える(i.e.証明可能)」ことを意味します。型Aに属する値 aは、そのような１つの証明に対応するとみなすことができます。

種々のconnectivesもまた、型の世界に対応物が存在します:

• 論理包含A ⇒ Bは、型の世界では関数の型A -> Bに対応します
• conjunction A ∧ Bは、型の世界ではタプル Tuple A Bに対応します。
  PureScriptの標準的なタプルのライブラリpurescript-tuplesが、Tuple構成子の演算子エイリアスを/\にしているのは、真に理にかなっています
• disjunction A ∨ Bは、型の世界ではEither A Bに対応します。
  こちらは/\ほど多用されていない気がしますが、型コンストラクタのEitherにも\/という型演算子エイリアスが定義されています

ちなみに、PureScriptでは、何も属する値のない型: Voidが存在します。
Voidに属する値が存在しないということは、Voidに対応する命題は、それを結論づける導出（証明）ができないということです。

すなわち、Voidは命題⊥に対応することがわかります。

Data.Voidでは、以下のようなシグネチャを持つ関数absurdが提供されています:

absurd :: forall a. Void -> a 

これは、Voidの型の値を受け取ると、任意の型の値を返すことができる関数です。
Void型の値とは、すなわち⊥の証明に対応するわけですから、「⊥を証明できれば、そこからあらゆる命題が証明できる」 という、論理学ではex falso quodlibetと呼ばれるものに対応する関数であることがわかります。
日本風にいうと

女郎の誠と玉子の四角　あれば晦日に月も出る

ってヤツです。

閑話休題。このように論理とプログラミングが一対一に対応するということは、たとえば

(A ⇒ B) ⇒ (¬B ⇒ ¬A)

なる命題はトートロジーか？(i.e. 原子命題A, Bの真偽によらず真であるか)という、純粋に論理学的な問題を、プログラマのタスクに落とし込めることを意味します。

論理学者は、この命題を ⇒-Introなどの推論規則を用いて導出しようとします。
しかし、プログラマにとっては、単に「以下の型を持つ関数を実装せよ」という作業になります:

prf :: (A -> B) -> (B -> Void) -> (A -> Void)
prf = ?

(前のセクションで、命題論理では否定のconnectiveを¬A := A ⇒ ⊥で定義したことを思い出してください)

これは実際に可能で、以下の具体的な関数はこの型を持ちます:

prf :: (A -> B) -> (B -> Void) -> (A -> Void)
prf f p = \a -> p (f a)  

以上の内容を、一旦まとめると以下のような表が書けます:

論理	プログラミング
命題 A	型 A
命題Aの証明	型Aに属する値
Implication A ⇒ B	A -> B
Conunction A ∧ B	Tuple A B
Disjunction A ∨ B	Either A B
Falsity ⊥	Void
Negation ¬A	A -> Void

Where is my ∀?

命題を型、証明を値、いくつかのconnectivesを(->) やTupleなどの型構成子とみなすことで、命題論理が、プログラミングに綺麗に対応することがわかりました。
では、∀や∃などの量化子はどう解釈されるのでしょうか？

まず述語を考えます。述語とは、何らかの集合Sの要素xから命題P(x)を作る「命題値関数」でした。
非常に素直に考えると、プログラミングの型は「値の集合」とみなせるので、
述語とは「型Sの値 xを受け取って型を作る関数」とみなせそうです:

-- 述語のプログラミングにおける対応物(?)
P :: S -> Type
P s = ?

ところが、これはPureScritでは作ることができません。
Pは、Typeのカインドを持つ具体的な型SからカインドTypeへの"関数"ですが、PureScriptでは型SとTyoeは別の階層に属するものなので、このようなものは存在しません。

お察しの良い方はお気づきでしょう。
そう、これはいわゆる「依存型(Dependent types)」です！
述語を正確に型システムにエンコードするには、依存型をもつシステムでなければなりません。
依存型を持つシステムに基づくプログラミング言語はまだそんなに多くなく、PureScriptのようなメインストリームの言語ばかり使っている私のような人間にとって、「型が命題に、項が証明に対応する」と言われても、いまひとつ具体的なイメージで頭に入ってこない原因がここにあると思います。

しかし、PureScriptにもいかにも論理学の∀に対応して”いそう"なコンストラクションが存在します。
そう、forallです。いったいこれは論理的にはどう理解すればいいでしょうか...?

再び論理：２階の述語論理

そこで、前のセクションで見てきた論理とは少し異なる（というより拡張した）体系の論理を眺めてみましょう。
前のセクションの例で出てきた述語

∀n∈Z. nは素数

において、∀が束縛しているのは nです。これは、集合Z上で変化する変数です。
このように、量化記号∀、∃が「述語の変数」を束縛する機能しか持たない体系を、１階述語論理（first ordered predicate logic)　といいます。

これに対し、量化記号が「命題変数」を束縛できるように拡張した体系 ２階述語論理(second ordered predicate logic) を考えてみます。

この体系では、たとえば以下のような命題を書くことができます:

∀P. P ⇒ P

これは、「すべての命題Pについて、P ⇒ Pが真」を表す命題です。
「すべての」が特定集合にかかっているのではなく、命題を表す変数にかかっていることに注目して下さい。
このような量化記号を使えるのが、2階の論理です。

forall＝２階の全称量化子

さて、上の例をもう少し深堀りしてみます。

∀P. P ⇒ P

における P ⇒ Pの部分について、Pは具体的な命題でなく、あらゆる命題を当てはめることのできるプレースホルダーです。
「∀P. P ⇒ P」で１つの命題なのですが、P自体は命題ではないのです。

Pには、具体的な命題を当てはめることで、量化記号をもたない命題を得ることができます。
たとえば、A, Bという原子命題があったとして、
A, B, A ⇒ B, A ⇒ B ⇒ ⊥等はすべて命題ですが、これをPにあてはめた

A ⇒ A
B ⇒ B
(A ⇒ B) ⇒ (A ⇒ B)
(A ⇒ B ⇒ ⊥) ⇒ (A ⇒ B ⇒ ⊥)

などの命題も(もとの量化記号を持った命題が真なら)すべて成り立ちます。
すなわち、Pは命題というより命題変数と呼べるものであることがわかります。

これはPureScriptの何に対応するでしょうか？
「命題を型と見よ」という我々の指導原理によると、命題変数は型をあてはめる型変数に対応します。
というわけで、上の命題に対応するPureScriptの型は

forall a. a -> a

です。これはidentity関数の型です。

identity :: forall a. a -> a 
identity = \x -> x

identity, すなわち型forall a. a -> aを持つ値が存在するということは、これに対応するもとの命題は真ということで、したがって命題変数Pに適当な命題を当てはめて得られる命題はすべて真ということになります。
これはPureScriptでいえば、型変数を適当な型で具象化した型はすべてinhabitant(型Tと持つ値tのことを、型Tのinhabitantといいます)を持つということです。

PureScriptでは、このようなforallを持つ型への具体的な型の代入は、デフォルトではコンパイラが推論してやってくれるのですが、最近のコンパイラはvisible type applicationが入っているので、以下のように@をつけて型変数をvisibleとマークしてあげると

identity :: forall @a. a -> a
identity = \x -> x

このように具体的な型を型変数にあてはめることができるようになります

identity' = identity @(A -> B)

identity'は、命題 (A ⇒ B) ⇒ (A ⇒ B)が成り立つことの証明になっています。

PureScriptにおける forallは、2階命論理に対応物をみることができるということがわかりました！

2階のエンコーディング

ちなみに、2階の量化を許すと、1階論理で公理的に与えられたいくつかのconnectiveは、他のconnectiveを用いて定義できるようになります。

その代表的なものが⊥です。
命題論理では、⊥は単に「Falsity」というメタ的に与えられた定義でしたが、2階の論理ではこれは以下のものとして定義できます:

⊥ := ∀P. P

これはPureScriptでいえば、以下の型に対応します:

type Bottom = forall a. a

実際にこれがData.Voidで定義されているVoidと同型であることは、以下の関数のペアにより確認できます:

v_to_b :: Void -> Bottom
v_to_b v = absurd v

b_to_v :: Bottom -> Void 
b_to_v b = b

forall a. aがVoidと同型であるということは、forall a. aという型がつく値を作ることはできない (もちろん、unsafeCoerceするとかのズルを除く)ということを意味します。
これは、forall をジェネリクスと捉えるプログラマの視点だけでは、なかなか発見しにくい事実かもしれません。

論理積∧／論理和∨もまた、定義可能な記号に成り下がります。

論理積は、以下のように定義できます:

A ∧ B := ∀C. (A ⇒ B ⇒ C) ⇒ C

これはPureScriptでは以下の型に対応します:

type Conj a b = forall c. (a -> b -> c) -> c 

これがConjunctionとして機能することは、以下のようにfst, sndに対応する関数を定義できることから理解できます:

fst' :: forall a b. Conj a b -> a 
fst' c = c \a _ -> a 

snd' :: forall a b. Conj a b -> b 
snd' c = c \_ b -> b

別の見方をすると、forall c. (a -> b -> c) -> cはa /\ bを継続渡しスタイルに変換しているだけと見ることもできますね。

論理和は、以下の論理積で定義されます:

A ∨ B := ∀P. ((A ⇒ P) ∧ (B ⇒ P)) ⇒ P 

これがたしかに論理和であることは、ここでは詳しく述べません。
すぐ次の章で∃を議論する際に明らかとなります。

∃：存在量化子　

∀のことはよくわかったので、次に存在量化子∃の話をしましょう。

1階の述語論理では、∃は∀と同様に、述語から新たに命題を作るものですが、たとえばPが集合S上の述語であれば、

∃x∈S. P(x)

のように作用して、
「述語Pが成り立つようなSの要素xが存在する」
あるいは
「あるx∈Sに対して述語Pが成り立つ」
という命題を作るものです。

ところが、1階論理の∀が依存型を持たないPureScriptに直接的な対応物を見ることができなかったのと同様に、これもまたPureScriptの型システムで対応する型を考えることは難しいでしょう。
そこで、2階論理の範疇で、∃が束縛する変数は命題変数であると考えます。
たとえば、

∃P. A ⇒ P

のように。
2階論理における∀P. ...という命題が、forall p. ...という型に対応したことからの類推で、
∃記号のついた命題は以下のような型に対応すると考えたくなるかもしれません:

exists p. ...

しかし、ご存知のようにPureScriptにはexistsというキーワードはありませんし、このように型をつくることもできません。
PureScriptに限らず、exists（とそれに準ずる構文)を持つ言語というのは稀有です。
というのも、実は∃は∀を用いて表現できるからです。
このことを確かめてみましょう。

PureScriptでは、purescript-existsパッケージで提供されるExistsが、存在型を作るために使うことができます。
Existsは、任意のカインドの型パラメタを1つ持つ型コンストラクタに作用して、そのパラメタについて存在量化した型を生成するコンストラクタです:

type Exists :: forall k. (k -> Type) -> Type

たとえば、Arrayは型コンストラクタを1つとるので、以下のようにExistsを使うことができます:

type SomeArray = Exists Array

SomeArrayの実行時の値自体はIntの配列ですが、型配列の上では要素の型がIntという情報が隠蔽されています。

SomeArrayの型を持つ値は、このようにmkExistsを使って作ることができます:

-- mkExists :: forall f a. f a -> Exists f

xs :: SomeArray
xs = mkExists [1,2,3]

Existsで存在量化された型を使う側は、以下のようにrunExistsを使うことになります。

runExists :: forall f r. (forall a. f a -> r) -> Exists f -> r 

たとえば、以下のようにしてSomeArrayの長さを計算することができます:

elim :: SomeArray -> Int
elim xs = xs # runExists \ys -> Array.length ys

このrunExistsのシグネチャが存在型の本質で、第1の引数である継続がforall a. と存在量化されている型について多相的になっていることがポイントです。
これが、このセクションの最初の方で「∃は∀で表現できる」といったことの理由です。

存在型はADTみたいなもの

一旦存在型ではなく普通のADTに戻ります。
以下の型を考えてください:

data IntOrChar 
  = MadeOfInt Int
  | MadeOfChar Char

IntOrCharの型の値は、Intで生成される場合 「または」Charで生成される場合があるということで、このような代数的データ型はOrの意味合いを持ち、別名sum typeと言われることは多くの方がご存知でしょう。

一方、IntOrCharの値を受け取る側(eliminator!)は、以下のようにパターンマッチをすることになります:

import Data.String.CodeUnits as SCU

f :: IntOrChar -> String
f = case _ of 
  MadeOfInt i -> "Int:" <> show i
  MadeOfChar ch -> "Char:" `SCU.snoc` ch

IntOrCharの型をもつ値があるということは、それを生成する(introduce!)するためにIntとCharのいずれかの値が存在したことは確かなのですが、それがどちらかがわからないため、両方のケースを考慮して２つのブランチがあるわけです。
これは、少し変形すると以下のようになります:

f = case _ of 
  MadeOfInt i -> onInt i
  MadeOfChar ch -> onChar ch
  
  where
  onInt :: Int -> String
  onInt = \i -> "Int:" <> show i
  
  onChar :: Char -> String
  onChar = \ch -> "Char:" `SCU.snoc` ch

つまり、fという関数はIntをStringに移す関数(onInt)とCharをStringに移す関数(onChar)のペアになっています。
すなわち、IntOrChar -> Stringな関数は、実質的に2つの関数のペア

Tuple (Int -> String) (Char -> String)

と同型だとみなせるわけです。
TupleはProduct typeなので、sum と productの役割が導入と消去で入れ替わっているのが興味深いです。

ちなみに、この方向のアナロジーで、ADTをsum type、Tupleをproduct typeと呼ぶなら、関数の型はexponentialで、 A -> Bという型は B^Aと解釈できる¹ので、上の例の関数は

-- IntOrChar = Int + Char

f :: String^(Int + Char) 
  == String^Int * String^Char          -- 指数法則 a^(b + c) == a^b * a^c
  == (Int -> String) * (Char -> String)

となっていることからも理解できますね。

ここで、コンストラクタを１つ増やすと...

data IntOrCharOrBoolean
  = MadeOfInt Int
  | MadeOfChar Char
  | MadeOfBoolean Boolean

eliminatorは考慮するケースが1つ増えるので、3つの関数 Int -> a, Char -> a, Boolean -> aの直積になります。

eliminator :: (Int -> r) /\ (Char -> r) /\ (Boolean -> r) 

この方向でどんどんコンストラクタを増やしていくとどうなるでしょう？
これはもうPureScriptでは書けないですが、概念的には、以下のような「この世に存在するあらゆる型をすべて可能性にいれた究極の直和」ができあがります

(擬似コード)

data UltimateSum 
  = MadeOfInt Int
  | MadeOfChar Char
  | MadeOfBoolean Boolean
  | MadeOfString String
  | MadeOfOrdering Ordering
  | MadeOf ...

このような型を持つ値がもしあるとすれば、それを作るために何かしらの型の値が使われたことは確かです。ただしその具体的な型の情報はわかりません。
これって...存在型っぽいですね！

では、このUltimateSumを受けとって型rの値を返すeliminatorはどのような関数であるべきかといえば、今度はあらゆるケースを網羅する巨大なパターンマッチ、すなわち「究極の直積」

(擬似コード)

type UltimateProduct r 
  = Int -> i
  /\ Char -> r
  /\ Boolean -> r 
  /\ String -> r
  /\ Ordering -> r
  /\ ...

でなければならないでしょう。

もちろん、現実にこのような無限個の要素を持つタプルは作れません。
もしUltimateSumのeliminatorを作りたければ、方法はただひとつ。
単一の関数ですべてのケースを網羅するしかありません。そう、多相関数を使うのです！

type UltimateProduct r = 
  forall a. a -> r

これが、（ハンドウェービングな議論ではありますが）∃は∀で表現できることの理由です。
すなわち、∃で量化された型のeliminatorが∀で量化された多相関数になるということで、
runExistsが多相な継続を受け取ることはこういう理由によります。

以上の考察を済ませ再び論理に戻ると、2階述語論理で∃の定義と消去則が以下のように与えられることも、割と素直に理解できるかと思います:

2nd-ordered encoding of ∃

∃(x∈S).P(x) := ∀A. ∀(x∈S). (P(x) ⇒ A) ⇒ A

∃-elim

Γ ⊢ ∃(x∈S).P(x)   Γ ⊢ ∀(x∈S).(P(x) => A)
------------------------------------------
Γ ⊢ A

まとめ

そんなわけで、PureScript(というよりプログラミング)における∀と∃について、その起源である論理の観点から考えることで、少し深堀りをしてみました!
プログラミングと論理の浅からぬ関係について、面白いと思っていただければ幸いです。

最後に、改めて論理とプログラムの関係を表にまとめておきます

論理	プログラミング
命題 A	型 A
命題Aの証明	型Aに属する値
Implication A ⇒ B	A -> B
Conunction A ∧ B	Tuple A B
Disjunction A ∨ B	Either A B
Falsity ⊥	Void
Negation ¬A	A -> Void
２階の全称量化 ∀P.	多相型 forall a.
∀-消去則	type application @T
２階の存在量化 ∃P.	存在型 Exists
∃-導入則/消去則	mkExists / runExists

1. たとえば、A=Orderingで、B=Booleanの時、OrderingからBooleanへの関数がいくつ作れるのか考えてみてください。 ↩