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

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

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

参照用 記事

述語論理: カリー/ハワード/ランベック対応と推論・型つけ規則

推論規則〈inference rule〉と型つけ規則〈typing rule〉の両方を含むシステムで使いやすいものがないかな、と探していました。僕が思う“使いやすい”とは:

  1. 意味論〈セマンティクス〉はハイパードクトリン。
  2. カリー/ハワード/ランベック対応と相性がよい。
  3. 自然演繹としてもシーケント計算としても使える。

これらの条件をまーまー満たすシステムを見つけたので紹介します。これから紹介する推論規則/型つけ規則は、次のバーケダル*1/ビージャック*2の論文にあるものを僅かに変更したものです。

$`\require{color}
\newcommand{\KW}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Arr}{\Rightarrow }
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
%`$内容:

ハブ記事:

記法に関する注意

ターンスタイル記号 '$`\vdash`$' は、証明可能性〈導出可能性〉を表すメタ述語記号としても、シーケントの区切り記号としても使われます。このオーバーロードは混乱・誤解をまねくリスクがありますが、広く採用されているので、ここでもシーケントの区切り記号に '$`\vdash`$' を使います。区切り記号としてのターンスタイルは、特に何かを主張するものではなくて、単に“区切りに使う変な矢印”です。

バーケダル/ビージャックのテキストに従い、論理式は $`\varphi, \psi, \chi`$ などのギリシャ文字小文字で表します。論理式を並べたリストを命題コンテキスト〈proposition context〉と呼び、ギリシャ文字大文字 $`\Theta, \Xi`$ などで表します。命題コンテキスト内の論理式には名前〈ラベル〉を付けてもかまいません。次の一番目はラベルなしの命題コンテキスト、二番目はラベル付きの命題コンテキストです*3

  1. $`\Theta = (\varphi_1, \cdots, \varphi_n)`$
  2. $`\Theta = (A_1: \varphi_1, \cdots, A_n:\varphi_n)`$

ターンスタイル記号の左に命題コンテキスト、右に単一の論理式を配置した記号的表現がここで扱うシーケント〈sequent〉です。シーケントは次の形です。

$`\quad \Theta \vdash \psi`$

左側の命題コンテキストを展開して書けば:

  1. $`\quad (\varphi_1, \cdots, \varphi_n) \vdash \psi`$
  2. $`\quad (A_1: \varphi_1, \cdots, A_n:\varphi_n) \vdash \psi`$

リストを囲む丸括弧はしばしば省略されます。

  1. $`\quad \varphi_1, \cdots, \varphi_n \vdash \psi`$
  2. $`\quad A_1: \varphi_1, \cdots, A_n:\varphi_n \vdash \psi`$

$`(\varphi)`$ と $`\varphi`$ は同一視され、リストの連接記号にもカンマが流用されます(そういう習慣なのです)。

さて、論理式には自由変数(自由な対象変数〈個体変数〉)が登場するでしょう。それらの自由変数の型を指定するために型コンテキスト〈{type | typing} context〉を使います。型コンテキストは次の形です。

$`\quad (x_1:\sigma_1, \cdots, x_n:\sigma_n)`$

ここで、$`x_1, \cdots, x_n`$ は変数記号で、$`\sigma_1, \cdots, \sigma_n`$ は型項〈type term〉です。型項は型を表す記号的表現ですが、その意味論は後述します。

型項はギリシャ文字小文字 $`\sigma, \tau, \rho`$ などで表します。型コンテキストはギリシャ文字大文字 $`\Gamma, \Delta`$ などで表します。これもバーケダル/ビージャックに従っています。

型コンテキストを伴ったシーケントは次のように書きます。

$`\quad \Gamma \mid \Theta \vdash \psi`$

以下常に、$`\Theta, \psi`$ 内に出現するすべての自由変数記号は、$`\Gamma`$ で型宣言されていると仮定します。

$`M`$ が値を表す項のとき、型判断〈{type | typing} judgement〉は通常次の形に書きます。

$`\quad \Gamma \vdash M:\tau`$

しかし、ターンスタイル記号をさらにオーバーロードするのはキビしい(僕が耐えられない)ので、型判断の構文は次のように変更します。

$`\quad M:\Gamma \to \tau`$

型判断とシーケントの意味論を、ハイパードクトリン(「述語論理: ベース圏と論理代数の圏」に簡単な説明があります)により行うとき、普通の矢印はベース圏〈base category〉の射、ターンスタイルはファイバー〈fibre | fiber〉の射と区別できて混乱が少なくなります。

構文論と意味論

構文論と意味論をごく手短に説明します。

型項は、基本型〈{primitive | basic} type〉を表す記号から、型構成子記号〈type constructor symbol〉を使って組み立てます。ここで使う型構成子記号は:

  1. '$`\times`$' : 直積型〈ペア型〉を構成する。
  2. '$`\Arr`$' : 指数型〈アロー型 | 関数型〉を構成する。
  3. '$`+`$' : 直和型〈タグ付きユニオン型 | バリアント型〉を構成する。

記号 '$`\Arr`$' は論理記号の含意〈implication〉とオーバーロードしているので注意してください(指数型と含意はカリー/ハワード/ランベック対応で対応します)。

基本型のなかでも特に基本的な型は次の記号で表します。

  1. $`1`$ : 終対象型〈ユニット型 | シングルトン型〉
  2. $`0`$ : 始対象型〈エンプティ型 | ネバー型〉

なお、バーケダル/ビージャックは直和型と始対象型は扱っていません。カリー/ハワード/ランベック対応をより徹底するために追加しました。

値を表す項(単に〈term〉と呼ぶ)は、基本関数を表す記号から型付きラムダ式〈型付きラムダ項〉の構文で組み立てます。項 $`M`$ が型コンテキスト $`\Gamma`$ のもとで型 $`\tau`$ を持つことを、

$`\quad M: \Gamma \to \tau`$

と書くのでした(型判断)。

型項と項の意味は、ハイパードクトリン $`(\cat{C}, \cat{L}, \mrm{Pred})`$ のベース圏により与えます。特に $`\cat{C} = {\bf Set}`$ とした場合が標準的です。型構成子記号 '$`\times`$'、'$`\Arr`$'、'$`+`$' は、常識的な直積、指数、直和で解釈できます。項の解釈は関数〈写像〉ですが、複数引数単一戻り値になるので複関数〈multifunction〉と呼びましょう。今詳しくは述べませんが、

  • 関数〈function〉は、圏 $`{\bf Set}`$ の射
  • 複関数〈multifunction〉は、圏 $`{\bf Set}`$ から作った複圏〈multicategory〉の複射〈multimorphism | multiarrow〉
  • 多関数〈polyfunction〉は、圏 $`{\bf Set}`$ から作った多圏〈polycategory〉の多射〈polymorphism | polyarrow〉*4

です。

今回の定式化では、複圏(オペラッド〈operad〉ともいう)と複射〈複アロー〉を使っています。潜在的に多圏と多射〈多アロー〉も使っているのですが、表立って多圏・多射が現れないようにしています。

型項と項の意味はスコットブラケット $`\left[\!\left[ - \right]\!\right]`$ を使って記述します。以下は、バーケダル/ビージャックからのコピー(PDFからの画像)です。バーケダル/ビージャックの $`\to`$ を我々は $`\Arr`$ 、$`\vdash`$ を $`\to`$ としています。直和型と始対象型は含まれませが、見当はつくでしょう。

シーケント(命題コンテキストと結論である論理式)の意味は、ハイパードクトリンのファイバー方向の圏によって意味を与えます。$`\left[\!\left[ \Gamma \right]\!\right] = X`$ とすると、次のシーケントの意味は $`\mrm{Pred}[X]`$ のなかの射になります。

$`\quad \Gamma \mid \Theta \vdash \psi`$

カリー/ハワード/ランベック対応

型項と項は、ハイパードクトリンのベース圏に意味を持ちます。一方、命題、命題コンテキスト、シーケントはハイパードクトリンのファイバー方向の圏に意味を持ちます。ベース方向の圏とファイバー方向の圏(たくさんある)は別な圏ですが、そっくりな構造を持ちます。「そっくりだ」という主張がカリー/ハワード/ランベック対応です。

この後で、推論規則〈inference rule〉と型つけ規則〈typing rule〉を列挙しますが、それらはカリー/ハワード/ランベック対応で次のように対応します。

一般概念 ファイバー方向 ベース方向
恒等射 IDENTITY-PROP IDENTITY
複結合 CUT MCOMP
破棄射 WEAK-PROP DEL
コピー射 CONTR-PROP COPY
対称射 EXCH-PROP SYMM
終射 TRUE FIN, UNIT
始射 FALSE INI
デカルト積 AND-I PROD, PAIRING
第一射影 AND-E1 PROJ1
第ニ射影 AND-E2 PROJ2
デカルト余積 OR-E COPROD, COPAIRING
第一入射 OR-I1 INJ1
第ニ入射 OR-I2 INJ2
無限デカルト積 ALL-I -
成分〈射影〉 ALL-E -
無限デカルト余積 SOME-E -
余成分〈余射影〉 SOME-I -
カリー化 IMP-I ABS
適用 IMP-E APP

規則の書き方

バーケダル/ビージャックからの推論規則のコピー(PDFからの画像)は以下です。

推論規則の記述にほとんど常に使われる横棒を使う方式です。が、これをうまくレイアウトするのは大変なので、英語風キーワード(緑色)を使うことにします。

$`\KW{If we have }\text{横棒の上段}\\
\KW{Then using } \text{規則の名前}\\
\KW{We have }\text{横棒の下段}
%`$

横棒の上段が複数あるときは $`\KW{And}`$ で並べます。

型つけ規則も同じ記法で記述します。項の実際の構成を省略するので、型つけ規則は(通常より)簡略に書けます。

ここから先は推論規則と型つけ規則の列挙です。個々の規則の解説はまた別の機会に。

ファイバー方向複圏構造の基礎

IDENTITY-PROP

ファイバー方向恒等射の存在

$`\KW{If we have nothing}\\
\KW{Then using }\text{IDENTITY-PROP}\\
\KW{We have }\Gamma \mid \varphi \vdash \varphi
%`$

CUT

ファイバー方向複結合の存在

$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{And } \Gamma \mid \Xi, \varphi \vdash \psi\\
\KW{Then using }\text{CUT}\\
\KW{We have }\Gamma \mid \Theta, \Xi \vdash \psi
%`$

WEAK-PROP

ファイバー方向破棄射の存在

$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{WEAK-PROP}\\
\KW{We have }\Gamma \mid \Theta, \psi \vdash \varphi
%`$

CONTR-PROP

ファイバー方向コピー射の存在

$`\KW{If we have } \Gamma \mid \Theta, \varphi,\varphi \vdash \psi\\
\KW{Then using }\text{CONTR-PROP}\\
\KW{We have }\Gamma \mid \Theta, \varphi \vdash \psi
%`$

EXCH-PROP

ファイバー方向対称射の存在

$`\KW{If we have } \Gamma \mid \Theta, \varphi, \psi, \Xi \vdash \chi\\
\KW{Then using }\text{EXCH-PROP}\\
\KW{We have } \Gamma \mid \Theta, \psi, \varphi, \Xi \vdash \chi
%`$

ベースとファイバーの関係

WEAK-TYPE

射影多関数による引き戻し

$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{WEAK-TYPE}\\
\KW{We have }\Gamma, x:\sigma \mid \Theta \vdash \varphi
%`$

CONTR-TYPE

コピー多関数による引き戻し

$`\KW{If we have } \Gamma, x:\sigma, y:\sigma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{CONTR-TYPE}\\
\KW{We have } \Gamma, x:\sigma \mid \Theta[x/y] \vdash \varphi[x/y]
%`$

EXCH-TYPE

対称多関数による引き戻し

$`\KW{If we have } \Gamma, x:\sigma, y:\rho \mid \Theta \vdash \varphi\\
\KW{Then using }\text{EXCH-TYPE}\\
\KW{We have } \Gamma, y:\rho, x:\sigma \mid \Theta \vdash \varphi
%`$

SUBSTITUTION

任意の複関数による引き戻し

$`\KW{If we have } \Delta, x:\sigma, \Delta' \mid \Theta \vdash \psi\\
\KW{And } M: \Gamma \to \sigma\\
\KW{Then using }\text{SUBSTITUTION}\\
\KW{We have } \Delta, \Gamma, \Delta' \mid \Theta[M/x] \vdash \varphi[M/x]
%`$

論理記号の導入・消去

TRUE

ファイバー方向終射の存在

$`\KW{If we have nothing}\\
\KW{Then using }\text{TRUE}\\
\KW{We have } \Gamma \mid \Theta \vdash \top
%`$

FALSE

ファイバー方向始射の存在

$`\KW{If we have nothing}\\
\KW{Then using }\text{FALSE}\\
\KW{We have } \Gamma \mid \Theta, \bot \vdash \psi
%`$

AND-I

ファイバー方向デカルト積の存在

$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{And } \Gamma \mid \Theta \vdash \psi\\
\KW{Then using }\text{AND-I}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi \land \psi
%`$

AND-E1

ファイバー方向第一射影の存在

$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi \land \psi\\
\KW{Then using }\text{AND-E1}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi
%`$

AND-E2

ファイバー方向第ニ射影の存在

$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi \land \psi\\
\KW{Then using }\text{AND-E2}\\
\KW{We have } \Gamma \mid \Theta \vdash \psi
%`$

OR-E

ファイバー方向デカルト余積の存在

$`\KW{If we have } \Gamma \mid \Theta, \varphi \vdash \chi\\
\KW{And } \Gamma \mid \Theta, \psi \vdash \chi \\
\KW{Then using }\text{OR-E}\\
\KW{We have } \Gamma \mid \Theta, \varphi\lor \psi \vdash \chi
%`$

OR-I1

ファイバー方向第一入射の存在

$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{OR-I1}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi\lor \psi
%`$

OR-I2

ファイバー方向第ニ入射の存在

$`\KW{If we have } \Gamma \mid \Theta \vdash \psi\\
\KW{Then using }\text{OR-I1}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi\lor \psi
%`$

IMP-I

ファイバー方向カリー化

$`\KW{If we have } \Gamma \mid \Theta, \varphi \vdash \psi\\
\KW{Then using }\text{IMP-I}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi\Imp \psi
%`$

IMP-E

ファイバー方向適用射の存在

$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi \Imp \psi\\
\KW{And } \Gamma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{IMP-E}\\
\KW{We have } \Gamma \mid \Theta \vdash \psi
%`$

ALL-I

ファイバー方向無限デカルト積の存在

$`\KW{If we have } \Gamma, x:\sigma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{ALL-I}\\
\KW{We have } \Gamma \mid \Theta \vdash \forall x:\sigma.\varphi
%`$

ALL-E

ファイバー方向無限デカルト積の成分 $`M/x`$

$`\KW{If we have } \Gamma \mid \Theta \vdash \forall x:\sigma.\varphi\\
\KW{And } M:\Gamma \to \sigma\\
\KW{Then using }\text{ALL-E}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi[M/x]
%`$

SOME-E

ファイバー方向無限デカルト余積の存在

$`\KW{If we have } \Gamma, x:\sigma \mid \Xi, \varphi \vdash \psi\\
\KW{And } \Gamma \mid \Theta \vdash \exists x:\sigma. \varphi\\
\KW{Then using }\text{SOME-E}\\
\KW{We have } \Gamma \mid \Theta, \Xi \vdash \psi
%`$

SOME-I

ファイバー方向無限デカルト余積の余成分 $`M/x`$

$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi[M/x]\\
\KW{And } M : \Gamma \vdash \sigma\\
\KW{Then using }\text{SOME-I}\\
\KW{We have } \Gamma \mid \Theta \vdash \exists x:\sigma. \varphi
%`$

ベース方向複圏構造の基礎

IDENTITY

ベース方向恒等射の存在

$`\KW{If we have nothing}\\
\KW{Then using }\text{IDENTITY}\\
\KW{We have } \Gamma, x:\sigma \to \sigma
%`$

MCOMP

ベース方向複結合の存在

$`\KW{If we have }\Gamma, x:\sigma, \Gamma' \to \tau\\
\KW{And } \Delta \to \sigma\\
\KW{Then using }\text{MCOMP}\\
\KW{We have } \Gamma, \Delta, \Gamma' \to \tau
%`$

DEL

ベース方向破棄射の存在

$`\KW{If we have }\Gamma \to \tau\\
\KW{Then using }\text{DEL}\\
\KW{We have } \Gamma, x:\sigma \to \tau
%`$

COPY

ベース方向コピー射の存在

$`\KW{If we have }\Gamma, x:\sigma, y:\sigma \to \tau\\
\KW{Then using }\text{COPY}\\
\KW{We have } \Gamma, x:\sigma \to \tau
%`$

SYMM

ベース方向対称射の存在

$`\KW{If we have }\Gamma, x:\sigma, y:\rho \to \tau\\
\KW{Then using }\text{SYMM}\\
\KW{We have } \Gamma, y:\rho, x:\sigma \to \tau
%`$

ベース方向複圏その他

FIN

ベース方向終射の存在

$`\KW{If we have nothing}\\
\KW{Then using }\text{FIN}\\
\KW{We have } \Gamma \to 1
%`$

INI

ベース方向始射の存在

$`\KW{If we have nothing}\\
\KW{Then using }\text{INI}\\
\KW{We have } \Gamma, x: 0 \to \tau
%`$

PROD

ベース方向デカルト積の存在

$`\KW{If we have } \Gamma \to \sigma\\
\KW{And } \Gamma \to \tau\\
\KW{Then using }\text{PROD}\\
\KW{We have } \Gamma \to \sigma \times \tau
%`$

PROJ1

ベース方向第一射影の存在

$`\KW{If we have } \Gamma \to \sigma \times \tau\\
\KW{Then using }\text{PROJ1}\\
\KW{We have } \Gamma \to \sigma
%`$

PROJ2

ベース方向第ニ射影の存在

$`\KW{If we have } \Gamma \to \sigma \times \tau\\
\KW{Then using }\text{PROJ2}\\
\KW{We have } \Gamma \to \tau
%`$

COPROD

ベース方向デカルト余積の存在

$`\KW{If we have } \Gamma, x:\sigma \to \rho\\
\KW{And } \Gamma, y:\tau \to \rho \\
\KW{Then using }\text{COPROD}\\
\KW{We have } \Gamma, z:(\sigma + \tau) \to \rho
%`$

INJ1

ベース方向第一入射の存在

$`\KW{If we have } \Gamma, z:(\sigma + \tau) \to \rho\\
\KW{Then using }\text{INJ1}\\
\KW{We have } \Gamma, x:\sigma \to \rho
%`$

INJ2

ベース方向第ニ入射の存在

$`\KW{If we have } \Gamma, z:(\sigma + \tau) \to \rho\\
\KW{Then using }\text{INJ1}\\
\KW{We have } \Gamma, y:\tau \to \rho
%`$

ABS

ベース方向カリー化

$`\KW{If we have } \Gamma, x:\sigma \to \tau\\
\KW{Then using }\text{ABS}\\
\KW{We have } \Gamma \to \sigma \Imp \tau
%`$

APP

ベース方向適用射の存在

$`\KW{If we have } \Gamma \to \sigma \Imp \tau\\
\KW{And } \Gamma \to \sigma\\
\KW{Then using }\text{APP}\\
\KW{We have } \Gamma \to \tau
%`$

*1:バーケダルは英語読み https://www.howtosay.co.in/pronounce/birkedal-in-english/ から。北欧の人名らしく、原音は https://www.howtopronounce.com/danish/birkedal または https://ja.howtopronounce.com/birkedal

*2:https://ja.howtopronounce.com/bizjak

*3:一部だけラベルを付けるでもかまいません。ここらへんは何でもありで自由です。

*4:"polymorphism" は「多相」と被る〈コンフリクトする〉のであまり使われません。