プログラミング言語を定義する：整数とブーリアン

翻訳：English • 日本語

この投稿のシリーズでは、私達は小さなプログラミング言語を形式手法で定義します。その定義についてLeanを使い定理を証明します。

初めに

様々なプログラミング言語が存在しますが、多くには正式な定義はありません。言語の大半は、実装により定義されています。

実装で定義を

LLというプログラミング言語があるとすれば、LL言語の実装は、ppというLL言語のプログラムをインプットとして、ppによる何らかのアウトプットを作り出し、もしくはppを無効として拒絶するプログラムです。

それで、実装がppを拒絶しなければ、ppはLL言語のプログラムだ、という定義を立てます。

しかし、言語には複数の実装があって、その実装らは同じプログラムに違う行動を取ったら、どちらの実装は本当に言語の定義だと言い切れますか。

仕様で定義を

この問題を解決する方法の一つは、言語の仕様を書くことです。この仕様は人間の言語で書かれています。仕様を参考にし、開発者らは実装を作り上げるのです。

C、C++、Go、JavaScript（最も正しい名前は ECMAScript）などの言語はこのように仕様されています。

数学で仕様を

しかし、言葉だけではなく数学でも仕様を書けます。このように仕様された言語の例はStandard ML、Pony、WebAssembly。

数学で言語を仕様することはたやすくできることでもないのかもしれませんが、そこにある利益が本当です。

まず、数学的な仕様は一義的で、曖昧では断じてありません。それに比べれば、人間言語だけで書かれた仕様は時に曖昧で分かりにくいです。

更に、形式手法を使えば、その仕様に関して定理が証明できます。これは、仕様にバグや誤りなどがないことを言い切れる証拠になります。

プログラミング言語を定義することで、この仕様の仕方を調べましょう。

「発言」という小さな言語

まずは言語に名をつけるのです。

プログラミング言語を実装することについて傑作であるブログがあります。作者がそのブログでしたように、英語の「utterance」という言葉を他の言語に翻訳することで、私達の言語を名付けるとしましょう。私自身の興味のある言語である日本語を目的の言語にします。従って私達の言語を「発言」と名付けておきましょう。

今のところ、発言には整数とブーリアンだけです。

整数を123\mathsf{123}か−456\mathsf{-456}か0\mathsf{0}のような定数の式で表します。整数は無限なので、定数も無限です。整数の最大限などの実用的な配慮を今のところ無視します。

ブーリアンの真をtrue\mathsf{true}で、偽をfalse\mathsf{false}で表記します。

最後に、条件式を追加します：

if e1 then e2 else e3\mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3

これはまずe1e_1を評価します。次に

発言は小さな言語であることは意図的です。言語その物がそれ程複雑ではないから、その言語を仕様する形式手法は少しでも慣れやすくなる、というのは目的です。

構文規則

BNFのような形式文法で式の構文規則を定義します。任意な型をτ\tau、式をeeという変数で表します。

整数は無限で書くのは面倒になるから、n‾\overline{n}は任意な整数だとします。

e::= n‾∣ true∣ false∣ if e1 then e2 else e3 \begin{aligned} e ::= \ & \overline{n} \\ | \ & \mathsf{true} \\ | \ & \mathsf{false} \\ | \ & \mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3 \end{aligned}

これは、eeという式が整数定数か、ブーリアン定数か、条件式だということです。

条件式には他の式e1e_1、e2e_2、e3e_3が含まれていることを注意してください。

動的意味論

式をどう評価するかを定義します。これは動的意味論と言います。動的意味論の定義の仕方はいくつかありますが、私達は構造操作的意味論にします。

その為、判断を二つ作り上げます。判断は推測規則で定義されます。

値：e vale \ \mathsf{val}

一つ目の判断はe vale \ \mathsf{val}。「eeは値だ」と読みます。値というのは評価し終わった式のことを言います。

まず、整数定数は値です。この事実を推測規則で表記します。

n‾ val \frac {} {\overline{n} \ \mathsf{val}}

推測規則は分数に見え、前提が上で一つの結論が下です。この規則には前提がないから線の上には何もありません。

ブーリアン定数も値だと、二個の規則で表します。

true val \frac {} {\mathsf{true} \ \mathsf{val}} false val \frac {} {\mathsf{false} \ \mathsf{val}}

発言ではこれらだけが値です。しかし条件式はどうでしょう。

踏み出し：e↦e′e \mapsto e'

値でない式をどう評価するかを定義します。

第二の動的意味論の判断であるe↦e′e \mapsto e'は「eeが一歩を踏み出しe′e'になる」と読みます。

これで「式を評価する」というのは式が値になるまで新たな式へと踏み出すということになります。

発言では、唯一踏み出せる式は条件式です。まず、そのif\mathsf{if}とthen\mathsf{then}の間にあるe1e_1という式が踏み出すことができればそのe1e_1を囲む条件式自体が他のe2e_2やe3e_3を変えずに踏み出せます。

e1↦e1′if e1 then e2 else e3↦if e1′ then e2 else e3 \frac {e_1 \mapsto e_1'} { \begin{aligned} &\mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3 \mapsto \\&\mathsf{if} \ e_1' \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3 \end{aligned} }

そして、e1e_1が値だったらどうするか定義します。true\mathsf{true}だったらe3e_3を無視しながらe2e_2に踏み出します。

if true then e2 else e3 ↦e2 \frac {} { \mathsf{if} \ \mathsf{true} \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3 \ \mapsto e_2 }

false\mathsf{false}だったら逆にe2e_2を無視しならがe3e_3に踏み出します。

if false then e2 else e3↦e3 \frac {} { \mathsf{if} \ \mathsf{false} \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3 \mapsto e_3 }

これで動的意味論の定義を完了したのです。

しかし問題が発生しました。

問題

先、式の評価を定義しました：

「式を評価する」というのは式が値になるまで新たな式へと踏み出すということになります。

しかしこの定義では評価できない式が存在してしまいます。例えば：

if 1 then 2 else 3 \mathsf{if} \ \mathsf{1} \ \mathsf{then} \ \mathsf{2} \ \mathsf{else} \ \mathsf{3}

この式は踏み出せません。なぜならe1e_1がtrue\mathsf{true}かfalse\mathsf{false}か踏み出せる場合だけ踏み出しを定義しました。e1e_1が整数である場合、何も定義しなかったのです。

なのに、この式は値でもないのです。この式は嵌ったとしか言えません。

選択肢は二つあります。まずこのような式に対応する為、動的意味論に推測規則を追加する手があります。例えば次の規則で C 言語を真似します：

if 0 then e2 else e3↦e3 \frac {} { \mathsf{if} \ \mathsf{0} \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3 \mapsto e_3 } n‾≠0if n‾ then e2 else e3↦e2 \frac {\overline{n} \ne \mathsf{0}} { \mathsf{if} \ \overline{n} \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3 \mapsto e_2 }

これは0\mathsf{0}をfalse\mathsf{false}とし、他の整数をtrue\mathsf{true}とします。

二番目の手は「有効な式」を定義し、その有効な式だけを評価します。ここではその選択肢にします。

どの式が有効か定義する為、静的意味論を導入します。

静的意味論：e:τe: \tau

静的意味論は、有効な式ということを定義します。

まず、型というという概念を紹介します。今のところ型は整数とブーリアンです。

τ::= Int∣ Bool \begin{aligned} \tau ::= \ & \mathsf{Int} \\ | \ & \mathsf{Bool} \end{aligned}

次、e:τe: \tauという判断を定義します。「eeの型はτ\tauだ」という意味です。それで「有効な式」というのは、或る型τ\tauが存在しe:τe: \tauが事実だということになります。

e:τe: \tauの規則を作り上げることにより定義します。整数定数の式の型は整数で、ブーリアンは同様です。

n‾:Int \frac {} {\overline{n}: \mathsf{Int}} true:Bool \frac {} {\mathsf{true}: \mathsf{Bool}} false:Bool \frac {} {\mathsf{false}: \mathsf{Bool}}

条件式は、e1e_1の型はブーリアンであることを前提とします。e2e_2とe3e_3の型は任意で同じというのも前提です。そしてその型は条件式の型になります。

e1:Boole2:τe3:τif e1 then e2 else e3:τ \frac { e_1: \mathsf{Bool} \hspace{1em} e_2: \tau \hspace{1em} e_3: \tau } {\mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3: \tau}

e1e_1の型はブーリアンだから先のような式はもう静的意味論により禁止されています：

if 1 then 2 else 3 \mathsf{if} \ \mathsf{1} \ \mathsf{then} \ \mathsf{2} \ \mathsf{else} \ \mathsf{3}

これで静的意味論を完了しました。

定理

今になって、発言についての定理を宣言し証明できます。

まずは「進歩」の定理。進歩は、型のある式は値か踏み出せると言います。

For all ee and τ\tau, if e:τe: \tau, then e vale \ \mathsf{val} or there exists e′e' such that e↦e′e \mapsto e'.

静的意味論を紹介する前、或る式は踏み出せないし、値でもないという問題がありました。しかし静的意味論を使い、定理の前提を強化し、定理を証明可能にするのです。

次は「維持」です。維持は、型のある式が踏み出せれば、その踏み出された式も同じ型を持つと言います。

For all ee and e′e' and τ\tau, if e:τe: \tau and e↦e′e \mapsto e', then e′:τe': \tau.

それらを合わせて次の「安全」定理の出来上がりです。

For all ee and τ\tau, if e:τe: \tau, then e vale \ \mathsf{val} or there exists e′e' such that e↦e′e \mapsto e' and e′:τe': \tau.

とりわけ注目して欲しいのは、e↦e′e \mapsto e'の場合、e′:τe': \tauも事実。これでまた安全定理をe′e'に使えます。

証明はGitHubにあります。

次の投稿では、関数を発言に追加します。