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

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

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

参照用 記事

自然言語混じり形式証明の意味論と最近の型理論

ひと月以上前(4月6日)「自然言語混じり形式証明の意味論」という記事を書きました。そこに、5つの過去記事へのリンクがあります。それら一群の記事で、「自然言語文がコメントや補足説明ではなくて、形式証明の正式な一部となるような証明記述言語が使えるようになるだろう」という予測と期待を述べました。$`\newcommand{\M}[1]{ \left[\!\left[{#1}\right]\!\right] }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\hyp}{\text{-} }
`$

ここしばらく(4月21日以降)、「最近の型理論」と題したシリーズ記事を書いています。最初の記事は「最近の型理論: 宇宙と世界、そして銀河」です。このシリーズの目的は、「階層化された宇宙達を備えた型理論」の紹介と解説です。

最近の型理論をおさえておきたいと思った動機は、自然言語混じり形式証明の意味論の定式化のためです。「自然言語混じり形式証明の意味論」において、自然言語混じり形式証明の意味論〈セマンティクス | スコットブラケット〉を二種類に分けました。

  1. 表示的意味論: 証明記述 $`\Omega`$ の意味 $`\M{\Omega}_\mrm{D}`$ (D は Denotational から)は、なんらかの圏論的構造内の概念的事物だとします。
  2. 翻訳意味論: 証明記述 $`\Omega`$ の意味 $`\M{\Omega}_\mrm{C}`$ (C は Compile から)は、自然言語を含まない証明記述形式言語のソースコード断片だとします。

翻訳により意味が保存されることは、次の図式が可換になることです。

$`\require{AMScd}
\quad \begin{CD}
\text{自然言語混じり形式言語} @>{ \M{\hyp}_\mrm{D} }>> \text{意味領域}\\
@V{ \M{\hyp}_\mrm{C} }VV @|\\
\text{純形式言語} @>{ \M{\hyp}_\mrm{D} }>> \text{意味領域}
\end{CD}`$

実際に翻訳意味論(のスコットブラケット)を考えてみると、上の図式では粗っぽすぎるようです。もう少し詳細化すると次のようです。

$`\xymatrix@C+3pc@R+3pc{
\text{自然言語混じり形式言語} \ar[r]^{ \M{\hyp}_\mrm{DE} } \ar[d]^{ \M{\hyp}_\mrm{C} }
&\text{外部的意味領域} \ar@/^1.5pc/[d]^{\text{内部化}}
\\
\text{純形式言語} \ar[r]^{ \M{\hyp}_\mrm{DI} }
&\text{内部的意味領域} \ar@/^1.5pc/[u]^{外部化}
}`$

表示的意味論をさらに二つに分けました。

  1. 外部的表示的意味論: 証明記述 $`\Omega`$ の意味 $`\M{\Omega}_\mrm{DE}`$ (E は External から)は、伝統的な非形式的記述の意図に近い概念的事物だとします。
  2. 内部的表示的意味論: 証明記述 $`\Omega`$ の意味 $`\M{\Omega}_\mrm{DI}`$ (I は Internal から)は、ソフトウェア実装に近い概念的事物だとします。

自然言語混じり形式証明は、論理学の教科書に書いてあるような命題や証明、そして日常的・非形式的な記述の習慣に基いています。その意味論は、ソフトウェア実装のもとになる意味論とは相当に隔たりがあります。単一の意味論で論じるのは無理があるので、意味領域も分けました。

二つの意味領域は、「外部」と「内部」と名付けていますが、外部・内部の意味は、以下の記事で述べた内部・外部の概念です。

外部的意味領域は、$`{\bf Set}`$ や $`{\bf SET}`$ のようなコア銀河(「最近の型理論: 宇宙と世界、そして銀河」参照)を環境とする概念的事物達から構成されます。一方の内部的意味領域は単一のデカルト閉圏〈銀河〉のなかにある対象・射だけから構成されます。

概念的意味領域にある諸々の概念的事物を、内部的意味領域であるデカルト閉圏に押し込めてしまう操作が内部化(あるいはレイフィケーション)です。逆に、デカルト閉圏内の対象・射をデカルト閉圏の外に取り出すことが外部化(あるいは反レイフィケーション)です。

自然言語混じり形式言語の意味論を構成するときは、自由度が高い外部的意味領域を使い、ソフトウェア実装(に近いモノ)の純形式言語の意味論は内部的意味領域を使います。自然言語混じり形式言語の議論(構文論も含める)では伝統的な自然演繹やシーケント計算を使い、純形式言語の議論では依存型付きラムダ計算を中心に考えます。

大枠は以上に述べたような形でよいでしょうが、“自然言語混じり記述”特有の問題も生じます。例えば、何の構造的パターンもなく文・論理式を並べただけでも、暗黙のパターンが推測・適用される点などは“自然言語混じり記述”特有です(「証明と計算は同じこと: 形式証明におけるノードとコネクター」参照)。

というわけで、「自然言語混じり形式証明の意味論」と「最近の型理論」は並行して進めていくつもりです。

シリーズ・ハブ記事: