このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

シーケント計算と圏論(続きみたいな)

うううう、今日も寒い。

昨日、シーケント計算の話をしました。ここ最近、プログラムの解析にシーケント計算が使えるんじゃないかと思っているんですよ。シーケント計算の背景には、単なる圏よりはむしろ複圏/多圏(multicategory/polycateogry)があるので、年末年始に複圏/多圏について調べようとしたんですが、結局あんまりやれなかったですねぇ。

とりあず、プログラム解析に使うという立場から、シーケント計算の基本概念とか用語とかを圏論絡みでまとめておきます。全然系統的じゃないですけど。

内容:

複圏、多圏、高次圏

雰囲気的な大雑把な話に過ぎませんが、複圏、多圏、高次圏について紹介します。

圏は、矢印と両端の点(それがイッパイあるかも)から成り立っていると言ってよいでしょう。射は、・―→・ という形ですから。で、複圏の構成要素はカラスの足跡みたいな形です。次のような感じ。

・
 \
・――→・
 /
・

矢印をいくら繋いでも1本の線の形ですが、カラスの足跡を繋ぐとツリーの形となります。複圏はツリーの計算体系ということになります。複圏の射は、domainが複数あるので、多変数関数あるいは多項演算を表現しているとみなせます。普通の圏が 1-in 1-out の関数(のようなモノ)を扱うのに対して、複圏は n-in 1-out の関数(のようなモノ)を扱うのです。

多圏は、n-in m-out の関数(のようなモノ)を扱う計算体系です。多圏の構成要素は次のような形状です。

・
 \ /→・
・― 
 / \→・
・

この図形は蜘蛛に似てるので、僕は個人的にスパイダーと呼んだりしています。蜘蛛の形をいくつか繋ぐと、一般的な有向グラフができます。つまり、多圏は有向グラフの計算体系ということになります。

圏/複圏/多圏は、線状の矢印/ツリー/有向グラフと、だんだんと複雑な図形になりますが、いずれも0次元の点と1次元の線から構成されています。もっと高次元の図形を考えることができます。それが高次圏です。2次元の圏が高次圏の入り口です。点と線以外に、面あるいは膜のようなモノを考えます。面の境界は線(射)と点(対象)からなります。2次元でも十分に難しくて、面の形状や繋ぎ方のルールにより、さまざまなバリアントがあります。

複圏/多圏/高次圏を導入すると、複雑な組み合わせ的図形とそれらの図形の操作を扱うハメになります。なかなかにメンドクサイし、現時点では誰もよく分かってないような状況に遭遇したりもします。しかし、シーケント計算の自然なモデルは高次多圏であるように思えます。

証明系と証明可能性

証明系とか演繹系とか呼ばれるシステムは、そのなかで形式化された証明が行えるような記号操作系です。証明系の詳細は詮索しないことにして、とある証明系をSとします。Sにおける論理文(logical sentence)をα、βなどのギリシャ小文字で表すことにします。Sがシーケント計算の体系なら、α、βなどはシーケントを表します。

Sにおいて、「α1, α2, ..., αn を仮定したら、βが証明できる」という内容的な(メタな)主張を、α1, α2, ..., αn |-S β と書くことにします。「|-」という記号(ターンスタイル)は、Sに属するものではなくて、Sについて語る外側の言語(メタ言語)に属するものです。

Sが標準的なシーケント計算の体系のとき、α1, α2, ..., αn |-S β の意味をもう少しハッキリとさせましょう; Sがシーケント計算ベースの証明系なら、推論図がいくつか(無限個でもよい)備わっています。推論図を組み合わせれば証明図となります。証明図の一番上に登場する、つまり自分より上がないシーケントを始式と呼びます。証明図の一番下に登場するシーケントは終式です。

これで、Sにおける証明可能性の意味を述べる準備が出来ました。まず、次の主張は同じ意味です。

  • α1, α2, ..., αn を仮定したら、Sでβが証明できる。
  • α1, α2, ..., αn |-S β
  • α1, α2, ..., αn を始式として、βを終式とするSの証明図が存在する。

「|-」の左側が空であってもよいとします。このときは:

  • 何も仮定せずにSでβが証明できる。
  • |-S β
  • 始式を持たず、βを終式とするSの証明図が存在する。
-S β であるとき、シーケントβがSで証明可能といいます。シーケントβが ⇒ A という形(左が空、右に1個の命題)のとき、Aが証明可能と呼び、同じ記号を流用して、 -S A と書きます。つまり、次は同じ意味です。
  • |-S (⇒ A)
  • |-S A

シーケント証明系と複圏/多圏/高次圏

シーケント証明系を圏論的に解釈する話を少しします。

圏論の筆算としてのシーケント計算」でも述べたように、「命題←→対象、シーケント←→射」という対応が基本になります。A ⇒ X という形のシーケントならこの対応で解釈できます。しかし、A, B ⇒ X, Y となると、単なる圏では解釈できません。古典論理のように、左右のカンマの意味が異なるなら、2つのモノイド積を持つ圏が必要になります。コンパクト論理ならモノイド圏でも大丈夫です。

話を簡単にするために、コンパクト論理のシーケントを考えることにします。この場合、左右のカンマをどちらもモノイド積に対応させて解釈できます。しかしそうすると、A, B ⇒ X, Y と A×B ⇒ X×Y の違いは(意味論的に)説明できなくなります。

そこで多圏を使いましょう。圏Cの対象のリストの集合(クリーネスター)|C|* を考えて、|C|* を対象類とする新しい圏類似の構造を作ります。これが、もとのモノイド圏Cから作った自由多圏(直観主義論理のシーケントなら自由複圏)です。シーケントは、自由多圏の射(多射)として解釈されます。カット規則が多射の結合を与えます。

推論図や証明図は、仮定となるシーケント(始式)群から結論(終式)のシーケントへと至る流れです。これは、射(1セル)と射を結ぶ2次元の射(2セル)に対応します。つまり、シーケントの証明は2次元の多圏において解釈されます。証明図の変形を考えれば、それは3次元の射(3セル)となり、3次元の多圏が登場します。

というわけで、シーケント証明系の圏論的解釈には、複圏/多圏/高次圏が現れます。カリー/ハワード対応により、プログラムと論理は対応するはずですから、プログラムの意味論や解釈にも複圏/多圏/高次圏が現れるのは避けがたいでしょう。避けられないなら、プログラムの解析に複圏/多圏/高次圏をどう使うかを正面から考えるのが得策でしょう、たぶん。