tnomuraのブログ

因果関数

ラッセルのパラドックスを含まず、内包的定義に制約がなく、論理と集合が同値として扱えるモデルを考えた。領域 D が有限集合なので有限集合のモデルだが無限集合を扱う場合の帰納的定義の base case として使える。モデルの概要は次のようになる。

個体の集合である領域 D を考える。個体は命題の主語となることができる。述語は、個体の１変数関数で値に真偽のいずれかをとる。述語は領域 D の全ての要素に対し定義される。述語 A は領域 D の要素の１変数関数であり、命題 A とは個体と述語のペアである。また、命題 A の真理値は、個体に述語 A を関数適用したときの値で真または偽である。また、述語 A を関数適用したときの真理値が真の個体を集めると、それは領域 D の部分集合である。これを、述語 A の真理集合と呼ぶ。これらの述語 A, 命題 A, 真理集合 A は便宜的に同じ記号 A で表しても型の違いから混同せずに済む。

述語 A には無数の関数を考えることができるが、その真理集合は全て領域 D の部分集合なので、同じ真理集合をもつ述語は同値である。また、述語の論理和、論理積、否定の真理集合は、集合の和集合、積集合、補集合に同型対応している。

領域 D について、任意の命題 (x, A) は真または偽の真理値を持つので、命題についての排中律が成立している。

また、命題の含意は A -> B = ¬A ∨ B であるので、含意の真理集合は補集合を c(A) で表すことにすると、c(A) ∪ B である。ただし、これは命題 A の主語と命題 B の主語が一致している場合である。すなわち命題が (x, A) と (x, B) の場合だ。

一方、命題を主語と述語で構成する場合、命題間の主語が一致しない場合もある。すなわち命題 (x, A) と命題 (y, B) の場合だ。この場合主語の間の関連性がないので、上の議論は必ずしも当たらない。

そこで、因果関数 f : A -> B を考える。因果関数という用語はないが、この記事では、これを仮定してみる。これは、単に集合 A から 集合 B への関数である。そうして、含意の定義をこの因果関数を含んだものに変更する。すなわち、

A -> B <=> x ∈ A -> f(x) ∈ B

である。これはまた、次のように変形できる。

A -> B <=> ¬ (x ∈ A) ∨ (f(x) ∈ B)

これは述語 A と述語 B の主語が同じ x である場合もふくむ含意の一般化になっている。また、含意をこのように定義することによって主語にかかわらず命題 A と 命題 B の含意を考えることができる。

領域 D とその部分集合を考えるのは１階述語論理のモデルである。含意を上のように定義することによって、この述語論理のモデルの中に、命題論理を埋め込むことができる。また、逆に１階述語論理は命題論理の拡張であるということができる。

このことは、含意が論理演算のなかで特殊な位置にあることを示している。しかし、このような定義をすることで、領域 D の命題をその真理集合と同一視でき、主語にかかわらず命題論理を構築できる。

このモデルでは個体と集合は区別されるのでラッセルのパラドックスは起こらない。集合の集合のようなものを考えるときは、集合を要素とする新たな領域を考え、その部分集合を集合の集合とする。このモデルの命題は個体と述語のペアであり、集合は命題の真理集合と同値になる。また、集合の演算と命題の演算によって命題と集合は同型である。このモデルは、おそらく、ラッセルの階型理論に対応するもので、また、型付きラムダ計算で完全に記述できる。

自分自身を要素として含む集合のような自己言及は、上のモデルでは表現できない。これは集合と個体を等しく要素として含むような領域 D を考える必要があるが、この場合、領域 D が有限集合でも無限集合でも、領域 D の冪集合全てを領域の要素で表すことはできないので、不完全な記述になってしまう。おそらく、ラッセルのパラドックスもゲーデルの不完全性定理もこのようなシステムで発生するパラドックスである。

自分がモデル化しようとしている数学的対象をどのモデルで表現するかは、その目的によって異なってくる。また、その限界を知っていれば安全に使うことができる。したがって、ラッセルのパラドックスが集合論の致命的な瑕疵とはいえないような気がする。

ここで述べたモデルを考えたわけは、「論理を集合と考える図解ができないか」という問題提起からだ。ここで、述べたモデルを使う限りは論理と集合は同値である。これは論理を集合として学ぶことができることを意味している。集合や論理を初めて学ぶときに、ラッセルのパラドックスによる論理に対する根底から揺さぶられるような不信感を、論理に対して持たなくて済むのが最大の利点だ。

含意と関数

一階述語論理では含意は真理集合の包含関係で説明されることが多い。たとえば「死すべき者」の集合は「人間の集合」を含んでいる。したがってある要素 x が人間であれば、それは死すべき者であるという推論ができる。あるいは、全ての人間は死すべき者であるという推論も可能だ。

しかし、「西の空が赤いから、明日は晴れだ」という含意についてはそれが成立しない。「西の空が赤い」という命題の主語は「西の空」で、「明日は晴れだ」の主語は「翌日」だが、それらの真理集合間に包含関係はないからだ。

そこで、述語を真理集合の包含関係に求めるのではなく、西の空が赤いという命題の真理集合と、翌日は晴れだという命題の真理集合を考える。「赤い」西の空を要素とする集合 A と 晴れている翌日の集合を B とし、集合 A の要素に集合 B を対応させる関数 f(x) を考えると、f :  A -> B である。そうして A の f による像 f(A) が B の部分集合のとき A -> B という含意が真となる。任意の x ∈ A について f(x) ∈ B だからだ。つまり、西の空が赤いとき翌日は全て晴れている。

この観点から「人間である」という集合の真理集合と「死すべき者である」という述語の真理集合の関係も同様の図式で説明ができる。すなわち「人間の集合」H から「死すべき者の集合」M の間に写像 g : H -> M が存在し g(H) ⊂ M である。ただし、この場合 g は H -> H の恒等写像になる。このことが H と M の包含関係と繋がっている。つまり、真理集合の包含関係は含意の特殊な条件下の現象だ。

このような含意の定義は、ラムダ計算でも定義することができる。真理集合 A の要素を x とすると x の型は A である。すなわち x : A である。このとき真理集合 B の要素を返すラムダ項 B を考える。これを x : A でラムダ抽象すると、λx.B : A -> B は真理集合 A から真理集合 B への関数であり、真理集合 A の要素 x に対し、B x は真理集合 B の要素である。すなわち、型 A の任意の x について B x は真理集合 B の要素であるから、A -> B の含意が成立する。すなわち命題 A が真の場合命題 B は常に真である。

すなわち含意 A -> B が成立することと、ある関数 f : A -> B が定義できることは同値なのである。

このように含意を真理集合の包含関係ではなく真理集合間の関数の存在ととらえることで、命題論理と一階述語論理に共通して適用できる含意を定義することができる。

カリー・ハワード同型対応

カリー・ハワード同型対応とは、

プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワードにより最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。

Wikipedia より引用

要するに、型付きラムダ計算のプログラムを作ると、プログラムは命題論理学の証明に対応し、プログラムの型は命題に対応しているということだ。どうやら、型付きラムダ計算でプログラムを作って、そのうちの型シグネチャーを取り出すと、論理学の証明になってしまうらしい。

例えばデータ型が B 型のラムダ項 M があって、それをデータ型 A の変数で関数抽象すると次のようになるが、

[x : A]
...
M : B
-------------
λx.M: A -> B

という型付きラムダ計算のプログラムは、論理学の推論の

[A]
...
B
-------------
A -> B

と対応している。また、関数適用もつぎのように modus ponens と対応している。

M : A -> B, N : A
----------------------
M N : B

A -> B, A
-----------------
B

データ型と命題が対応していると言われても、何それ？という感じがするが、データ型 A のことを考えるとこれは {x | x ∊ A} という集合だ。x ∊ A という命題は、x が A に属していれば x ∊ A は真になる。

ラムダ項 N の型が A であるということは、ラムダ項 N について N ∊ A は真であるということを意味する。またラムダ項 M が A -> B 型の関数であるということは、M を 任意の N ∊ A に関数適用したときその値は全て型 B であるということを意味している。すなわち N ∊ A であれば、M N ∊ B である。

そこで命題 A を x ∊ A とおき、命題 B を y ∊ B と置くと、関数型 A -> B は x ∊ A ならば Mx ∊ B という命題であり、任意の x ∊ A について、Mx ∊ B であるということになり、命題 A が真であれば命題 B が真であることが分かる。すなわち A -> B, A => B である。

また、x ∉ A であれば、A -> B は型エラーとなるので A -> B が真であるという仮定は失われる。modus ponens は A -> B と A が同時に真であるときにのみ B が真であるという推論は正しい。

型 A や 型 B には任意の集合を取ることができるから、これらは x ∊ A や y ∊ B によって任意の命題に変えることができる。M N という関数適用は x と y の間に y = M x という関係を定義するが、これは A -> B という関数型によって抽象化される。このことは、逆に A -> B によって示される命題の含意について、集合 A と 集合 B の内的な関連性を示唆する。

関数型プログラミングと論理学の間には、単なる同型対応だけではなく、意味論的にも関連があるような気がする。

集合と要素の所属関係のみですべてが表現できるか

ラッセルの集合「自分自身を要素として含まない集合の集合」のような自己言及のある集合は、ベン図をもとにした集合からは作ることができなかった。

そこで、集合も個体も等しく対象として同等にみることにして、それらの集合を領域と考える。領域の要素間に所属関係を導入するとこれを利用して「自分自身を要素として含む」などの自己言及が定義できる。任意の対象同士の所属関係は領域の全ての要素について定義できるから、このモデルですべての集合が定義できるように思える。しかしそうではない。詳しい議論は過去記事の

集合とは何か

ラッセルのパラドックスのどこがいけないか

にまとめている。自己言及のあるシステムは、集合としては特殊なシステムである。ラッセルのパラドックスはその特殊なシステムで発生した議論なのだ。

有限集合のみで構成される世界

有限集合のみで構成される世界を考えてみた。まず、有限集合を有限個集めてみる。次にそれらの集合とその要素ををすべて集めて領域 R を作る。すると、領域 R はそのような集合の系の全ての要素と集合を含むことができる。そのような世界では、全ての集合について集合和、共通部分、補集合などの全ての演算が閉じている。

しかし、それらの集合の演算を定義するためには、要素と集合の所属関係が定義されていなければならない。それは、領域 R の要素の直積を作り、所属関係があれば 1 なければ 0 となるような対照表を作ればいい。そのような対照表には領域全ての要素について互いの所属関係が記述される。

ところが、この対照表は領域の直積であるので、それは領域には含まれない。つまり、有限集合を有限個集めた領域にあっても、集合の所属関係のような基本的な関係でさえ、領域内で完結することができない。それらは集合の世界の外の論理になるのだ。

また、この対照表自体にも問題がある。この対照表は n 個までの集合しか表現できないが、領域に n 個の要素がある場合、それらの要素を含む可能な集合は 2^ n 個になるからだ。この意味でも領域 R の要素では全ての集合を表せないことが分かる。

おそらく、集合の数や要素の数を無限に増やしてもこれらの事情は変わらないのではないだろうか。

ラッセルのパラドックスのようなものも、本来は集合の領域内で完結できないはずの論理を、その集合の領域内で完結させようとしたところに問題が発生したのではないだろうか。

そこで、どのような集合の系であれば、論理と整合性を保てるのだろうかと考えてみた。最も単純なモデルは、領域 R を先に決めておいて、集合とはその部分集合だけを指すことにする場合だ。一言で言うとベン図の世界だ。このモデルでは集合を表すのに領域の要素は用いない。集合の名前空間は領域とは別のところに作る。そうすると、領域の要素数による集合の名前空間の制限がないので、領域で考えられる可能な集合を列挙することができる。

そこで、領域 R で考えられる全ての集合を指す名前空間を Set とする。Set と 領域 R の直積から真理値への関数を elem :: Set -> R -> Bool とすると、これは領域 R の部分集合と領域 R の要素の間の全ての帰属関係を記述できる。また、Set を行に、R の要素を列に並べて elem の値を表にした対照表を作ると、これは n × (2^n) の表になる。この対照表は領域 R の部分集合を全て記述することができる。このとき、Set に集合和、共通部分、補集合などの集合演算を定義することができ、それは Set について閉じている。

また述語 P(x) を

P(x) = elem (S, x)

で定義できて、P(x) は領域 R の全ての要素について True または False の値をとる。このような定義ではなく任意の述語 Q(x) を考えこれは R の要素 x について True または False の値を取るものと考えると、これは P(x) = elem (S, x) のどれかと一致する。すなわち、任意の述語 Q(x) は elem (S,x) のどれかと同値である。このモデルについては、素朴集合論の演算と、一階述語論理について閉じている。これが、論理と整合性のある素朴集合のモデルだ。このモデルには自分自身を要素とする集合は存在しない。名前空間が異なるので、帰属関係が定義できないからだ。

集合には冪集合が存在する。それは Set の要素の集合である。したがって、集合 S の冪集合の名前空間は Set とは異なる名前空間になる。また、集合の直積 A × B もまた、Set とは異なる名前空間に属する。このように、集合の集合のような Set の要素から作られる集合は Set とは異なる名前空間を与えると、ラッセルのパラドックスのような矛盾は一切生じない。

このような型付きラムダ計算ではどのように集合が複雑に構成されていっても論理との矛盾が生じないのではないだろうか。型付きラムダ計算は煩雑に見えるが、Haskell でプログラムが自在に記述できるのを見ると。取扱はそうむずかしいものでもないような気がする。

型なしラムダ計算とラッセルのパラドックス

型なしラムダ計算の学習をしていたら、これが、ラッセルのパラドックスをすっきり説明できるのではないかと思いついたので書いてみる。

初めに、集合を全て集めたクラスを考える。そのクラスについて述語 P(x) と集合 P を次のように定義する。

x ∈ P ⇔ P(x) = True

P(x) は集合 x を引数とし、真か偽の真理値をとる関数である。これは集合の内包的定義を用いると次のように表せる。

P = {x | P(x) = true }

これは P(x) が真となるような集合 x を集めると集合 P になることを示している。

そこで、上の定義を利用してラッセルのパラドックスにあるような x ∈ x のような自己言及を定義できないかどうか考えてみるが、これは上の定義から次のようになる。

x ∈ x ⇔ x(x) = True

この定義には、しかし問題がある。x(x) の右側の x は述語でなければならないのに対し、左側の x は集合であるからだ。集合 x を集合の関数である述語として使うのは問題があるので、本来 x(x) のような自己言及は上のような集合の内包的定義では定義できない。

そこで少し工夫をして集合を表すのに述語を使うことを考えてみる。つまり集合 P の述語 P(x) で集合を表すことを考える。P(x) は集合ではないが P = {x | P(x)} のようにいつでも内包的定義で集合にすることができる。そして集合 P の集合 a への関数適用を次のように定義する。

P a(x) = P(a(x))

こうすれば述語 P の引数は述語であり、述語 a(x) を引数とすることができる。そうして P (a(x)) は述語になる。このようにすれば、集合の世界と、集合の述語からなる世界の対応が作られるので、集合の述語の世界で x(x) のような自己言及を作ることができる。述語 P(x) を集合 P と同一視し、述語 a(x) を A として集合 A と同一視することにすると、上の関数適用は、

P A = (P . a) (x)

となる。これで、めでたく集合 P を 集合 A に関数適用できることになる。もちろん自己言及 X X も可能である。全てが関数である述語の世界を考えると自己言及は可能になる。

そこで、関数適用 P A に対し関数抽象 λ を導入すると、次の λA.(P A) は集合 A を引数とし集合 P A を返す関数となる。

λA.(P A)

したがって、

(λA.(P A)) B = (P B)

である。さらに、

λPA.(P A)

は集合 P を引数とし、集合 A を引数とする関数 λA.(P A) を返す高階関数である。これは集合と集合の関数適用を考えたときに、集合が型のないラムダ計算のなかに埋め込まれることを意味している。集合の述語は型のないラムダ計算の要素と考えることができるのだ。このように集合の述語による言及が型なしラムダ計算の世界で表現できることが分かったので、集合の自己言及を型なしラムダ計算の枠組みで考えてみる。

さて、集合 A を集合 A に自己言及させた次のラムダ項は何になるのだろうか。

A A

これは A が A に属していれば true で属していなければ false である。ただし、この true や false はラムダ計算の世界で定義されたものになる。

したがって、上の自己言及を λ 抽象した次のラムダ項は任意の集合についてそれが自分自身を要素としていれば true 要素としていなければ false を返す述語になる。

λx.(x x)

また、集合をラムダ計算に埋め込むことで、上の述語は集合と同一視することができる。したがって、次のラムダ項は自分自身を要素として含む集合が自分自身を集合として含むかどうかを判別する関数適用になる。

(λx.xx) (λx.xx)

しかし、これは次のように β 簡約しても無限に自分自身となるのでどうやっても true にも false にもたどり着くことができない。

(λx.xx) (λx.xx) = (λx.xx) (λx.xx) = (λx.xx) (λx.xx) = ...

それではラッセルの集合はどうだろうか。これは自分自身を要素としては含まない集合の集合だから次のようになる。

￢(λx.xx)

これが自分自身を要素として含むかどうかの関数適用は次のようになる。

(￢(λx.xx))(￢(λx.xx)) = ￢(￢(λx.xx))(￢(λx.xx)) = ￢(￢(￢(λx.xx))(￢(λx.xx)))) = ...

と、これもやはり true にも false にもたどり着けない。

自分自身を要素として含む集合や、自分自身を要素として含まない集合は本来は内包的定義にそぐわない表現だが、自然言語で表現すると見逃がしやすい。ふつうに考える集合の世界には、これらの述語は発生しないはずだ。ただし、これはラムダ計算の体系の中では表現できる。しかし、この場合もまた不動点コンビネータを形成してしまうので真理値を得ることはできない。

ラッセルのパラドックスは結局のところ内包的定義としては表現できない定義を導入したためにおこったものではないだろうか。自己言及を含む述語は集合の定義には使えないのだ。

自己言及を含む内包的定義は、型不適合で排除できる。素朴集合論を型つきラムダ計算の枠組みで記述出来たら、ラッセルのパラドックスは発生しないので矛盾が起きなくなるのではないだろうかと思うが、それを検証する知識がない。

GitHub にアカウントを作った

GitHub にアカウントを作りました。ラムダ計算機がダウンロードできます。その他の使い方は勉強中。というかよく分かりません。

https://github.com/tnomura9/lambda-calculus

Git とは何か

GIT についての TeckAcademy の Youtube の動画が分かりやすかった。

はじめての GIT 入門講座

ラムダ計算 SKI コンビネータ 4

ラムダ計算

Y - コンビネータを SKI に変換してみた。Y - コンビネータの定義は次のようになる。

Y = λf.(λx.fxx)(λx.fxx)

手順は次のようになる。まず、lambda.hs を起動して、:load コマンドで設定ファイルを読み込み SKI コンビネータを使えるようにする。

C:\Users\****>runghc lambda.hs
lambda> :load
filename: defined.txt
lambda>

Y - コンビネータの body 部分は λx.fxx の自己言及になっているのでまず fxx を SKI コンビネータに変換したあと Yf = S(fxx)(fxx)f を作った。最後に (Yg) 3 で3の階乗を計算した。g は設定ファイルに記述した階乗のプログラム。

lambda> (f (x x))　......　fxx を取り出す。
(f (x x))
lambda> (((K f) x) (((S I) I) x))　......　f -> (K f) x, xx -> SIIx へ変形
(f (x x))
lambda> (((S (K f)) ((S I) I)) x)　......　S(Kf)(SII)x で x をくくりだす
(f (x x))
lambda> (((((K S) f) (K f)) ((S I) I)) x)　......　SKY -> (KSf)(Kf) に変形
(f (x x))
lambda> (((((S (K S)) K) f) ((S I) I)) x)　......　S(KS)Kf で f をくくりだす
(f (x x))
lambda> (((((S (K S)) K) f) ((K ((S I) I)) f)) x)　......　(S(KS)Kf)(K(SII)f) に変形
(f (x x))
lambda> ((((S ((S (K S)) K)) (K ((S I) I))) f) x)　......　S(S(KS)K)(K(SII)f で f をくくりだす
(f (x x))
lambda> (= M ((S ((S (K S)) K)) (K ((S I) I))))　.......　M = S(S(KS)K)(K(SII))
lambda> (= Ys ((S M) M)))　......　Ys = SMM
lambda> ((Ys g) 3)　......　(Ys g) 3 で factorial 3 を計算
(ls.(lz.(s (s (s (s (s (s z))))))))　......　factorial 3 = 6

SKI - コンビネータでも自己言及関数のテストができた。

ラムダ計算 SKI コンビネータ 3

ラムダ計算

ラムダ記法の関数を SKI コンビネータで表すのは機械的にできる。次の３つのルールを機械的に適用していくだけだ。

１）λx.M = M ... λ抽象は外して良い

２）((x z) (y z)) = (S x y) z ..... (x z) (y z) の形の関数適用は変数 z をくくり出せる。

３）x = I x ..... 変数 x だけの項は (I x) の形に変えることができる。

４）a = (K a) x ..... 項 a は (Ka) x の形に変えることできる。このとき、(K a) を関数適用する x は任意の項を使うことができる。

このルールに従って、前回も紹介した、

λxyz.x(yz)

を SKI コンビネータで置き換えてみると、次のようになる。

lambda> (lx.(ly.(lz.(x (y z)))))
(lx.(ly.(lz.(x (y z)))))
lambda> (x (y z)) ...... ルール１）を使ってラムダ抽象を除去して body だけにする。
(x (y z))
lambda> (((K x) z) (y z)) ..... ルール４）を使って x --> (K x) z にする。
(x (y z))
lambda> (((S (K x)) y) z) ..... ルール２）を使って z をくくりだす。
(x (y z))
lambda> (((((K S) x) (K x)) y) z) .... ルール４）を使って S -> (K S) x にする。
(x (y z))
lambda> (((((S (K S)) K) x) y) z) ..... ルール２）を使って x をくくりだす。
(x (y z))
lambda> (= M ((S (K S)) K)) .... 求めるコンビネータは S(KS)K である。
lambda> (((M x) y) z)
(x (y z))

ラムダ記法の関数は、atom か、関数抽象か、関数適用のどれかで記述されているので上のルールを適用していけば、どのようなラムダ項も SKI コンビネータで記述することができる（はずだ）。

しかし、上のルールは変数が１回しか現れないときは機械的に適用できるが、(x (x x)) の様に同じ変数が何回も現れる場合は適用できるのだろうか。

lambda> (x (x x))
(x (x x))
lambda> (x ((I x) (I x)))
(x (x x))
lambda> (x (((S I) I) x))
(x (x x))
lambda> ((I x) (((S I) I) x))
(x (x x))
lambda> (((S I) ((S I) I)) x)
(x (x x))
lambda> ((S I) ((S I) I))
(lz.(z (z z)))

問題ないようだ。