自然言語混じり形式証明の意味論 - 檜山正幸のキマイラ飼育記 (はてなBlog)

一連の話の“流れ”（以下の記事群参照）として、自然言語混じり形式証明の意味論に少し触れておきます。昨日の記事への追記・補足の位置付けです。

自然言語も形式言語も、素材は文字の並びです。その文字の並びを構文解析して、意味を与えます。自然言語の意味論は難しいですが、形式言語〈人工言語〉は言語仕様として何らかの意味論が与えられています。自然言語混じり形式証明は、自然言語が混じっているとはいいながら、形式的定義が可能な言語なので、構文構造や意味構造を形式的に与えることができるはずです。$`\newcommand{\M}[1]{ \left[\!\left[{#1}\right]\!\right] }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\hyp}{\text{-} }
`$

文字の並びとして与えられた自然言語混じり形式証明記述を、ギリシャ文字大文字で表すことにします。例えば $`\Omega`$ のように。ここでは、構文解析過程には注目しないので、文字の並びを構文解析してできたデータ構造、例えばツリーも同じ $`\Omega`$ で表すことにします。

意味論は、構文的オブジェクト $`\Omega`$ にその意味 $`\M{\Omega}`$ を対応させます。意味として何を採用するかに2つの選択肢があります。

表示的意味論：意味 $`\M{\Omega}_\mrm{D}`$ は、多圏〈polycategory〉の多射〈polyarrow〉*1だとします。
翻訳意味論：意味 $`\M{\Omega}_\mrm{C}`$ は、自然言語を含まない証明記述形式言語のソースコード断片だとします。

下付きの D, C はそれぞれ Denotational, Compile のつもりです。

表示的意味論のターゲット（意味写像の行き先）に多圏を選んでいるのは、意味論を作るのが一番楽そうだからです。この点については昨日の記事「証明と計算は同じこと：形式証明におけるノードとコネクター」で書いています。多圏の解説は次の記事にあります。

述語論理：様々な多圏達の分類整理

翻訳意味論では、例えばLean 4のような既存の証明記述言語にコンパイル〈トランスパイル〉します。自然言語混じり形式証明を既存の証明検証系でチェックしたいときは、このようなコンパイルが必要です。もっとも、近い将来に証明ソフトウェアが自然言語混じり形式証明を直接解釈できるようになれば、このようなコンパイルは不要となりますが。

自然言語混じり形式証明の記述言語を $`\mathscr{N}`$ 、表示的意味論の意味領域である多圏を $`\cat{P}`$ とすれば、表示的意味論は（詳細はともかく）次のような形になります。

$`\quad \M{\hyp}_\mrm{D} : \mathscr{N} \to \cat{P}`$

翻訳意味論（コンパイル）のターゲット言語を $`\mathscr{L}`$ とすると、翻訳意味論は次の形になります。

$`\quad \M{\hyp}_\mrm{C} : \mathscr{N} \to \mathscr{L}`$

ターゲット言語である $`\mathscr{L}`$ の表示的意味論が、同じ多圏 $`\cat{P}`$ を意味領域とするなら、次の図式は可換であること（意味の保存）が要求されます。

$`\require{AMScd}
\quad \begin{CD}
\mathscr{N} @>{ \M{\hyp}_\mrm{D} }>> \cat{P}\\
@V{ \M{\hyp}_\mrm{C} }VV @|\\
\mathscr{L} @>{ \M{\hyp}_\mrm{D} }>> \cat{P}
\end{CD}`$

「証明と計算は同じこと：形式証明におけるノードとコネクター」で、意味領域側のノードとコネクターについて述べました。自然言語混じり形式証明の記述言語 $`\mathscr{N}`$ で記述された証明の構文的オブジェクト $`\Omega`$ は、ノード相当部分とコネクター相当部分に切り分けることができます。

構文オブジェクト $`\Omega`$（例えばツリー）の部分構文オブジェクト $`\Phi_1, \Phi_2, \cdots, \Phi_n`$（例えばサブツリー達）を切り出すと、これらの意味 $`\M{\Phi_1}, \M{\Phi_2}, \cdots, \M{\Phi_n}`$ は$`n`$個の多射となります。$`\Omega`$ からコネクター情報を絞り出して、幾つかの多射 $`\M{\Phi_1}, \M{\Phi_2}, \cdots, \M{\Phi_n}`$ 達をコネクター達で繋ぎ合わせる作業を繰り返せば意味論が完成します。

が、構文オブジェクトからコネクター情報を絞り出すのが難しい。それは、自然言語および自然言語を前提とした証明フォーマットでは、コネクター情報が明示的でないからです。習慣・伝統・暗黙の了解のなかに、コネクター情報が隠されているみたい。ここらへんは、実際にハンドコンパイル作業をして暗黙ルールを探るしかないでしょうね。とりあえずハンドコンパイルやってみようかな。

シリーズ・ハブ記事：

チャットAIで形式証明も自然言語混じりで書ける（はず）

*1:多射を polymorphism ともいいますが、多相の意味のポリモーフィズムとかぶってしまうので、polyarrow とか polymap の使用が多いです。