プログラミング言語の概念、パート I:判断と推論規則

素人の視点から見ると、プログラミング言語研究の分野は、専門用語、ギリシャ文字、および奇妙な記号でいっぱいです.一方で、これらの一般的な用語は、プログラミング言語の論文を簡潔にします.他方では、数学的な成熟度だけでなく、それらを理解するための専門知識も必要です。

私はプログラミング言語の基礎コースを受講しているので、一連のブログ投稿で学んだ重要な概念を共有したいと思います.そして、プログラミング言語の神秘的な分野を解明するために、それらを「人間が理解できる」方法で書きたいと思っています.

この素晴らしいコースを提供してくれた Chang 教授と、活発なディスカッション環境を作成してくれたクラスメートに感謝したいと思います。また、これらの投稿の多くのアイデアは教室からもたらされていることを断言する必要があります。クラスのディスカッションで引用することは不可能です.もちろん、すべてのエラーは私自身のものであり、何か問題がある場合は私に連絡してください.

プログラミング言語分野の数学的概念の多くは、命題論理の分野から来ています。したがって、この最初の投稿では、判断の正式な言語に焦点を当てています。 、および推論ルール .

判断

判断は、特定の抽象構文ツリーに関するステートメントまたはアサーションです。以下は、判断に使用する標準的な表記法です1 。 :

<セマンティクス> n nat n は 自然数です n 1 + n 2 = ん n は の合計です n 1 および n 2 τ タイプ τ は タイプです e : τ 式 へ 評価 して τ e ⇓ v 式 へ 評価 して v \begin{aligned}n \ \text{nat} &&\text{$n$ は自然数} \\n_1 + n_2 =n &&\text{$n$ は $n_1$ と $n_2$ の和} \\\tau \ \text{type} &&\text{$\tau$ is type} \\e :\tau &&\text{expression $e$ evaluate to type $\tau$} \\e \Downarrow v &&\text{式 $e$ は値 $v$ に評価されます}\end{aligned} n natn1 +n2 =nτ typee:τe⇓v n は 自然数ですn は n1 と n2 τ の合計です 型式 e 評価 して τexpression e 評価 して v

n などの上記の例に注目してください。 nat n \ \text{nat} n nat,<セマンティクス>n n n は未知の変数です。これらを判断フォームと呼びます そして、実際の値を判定フォームの変数にプラグインして、判定を得ることができます :

<セマンティクス>0 nat 1 nat − 1 nat 「こんにちは、世界！」 nat \begin{aligned}0 &\ \text{nat} \\1 &\ \text{nat} \\-1 &\ \text{nat} \\\text{``Hello, world!''} &\ \text{nat}\end{aligned} 01−1「ハロー、ワールド！」 nat nat nat nat

ご覧のとおり、判定は true または false のいずれかになります。これは、bool を返す関数アプリケーションであると見なすことができます。 .

推論規則

推論規則は、前提を取り、結論を返す論理形式です。一般に、次の標準形式があります:

<セマンティクス>前提 1 前提2 ⋯ 結論 \frac{\text{前提1} \quad \text{前提2} \quad \cdots}{ \text{結論} } 結論前提1前提2⋯

「すべての前提が満たされた場合、結論」と読むことができます。

推論規則によって自然数を帰納的に定義しましょう.

<セマンティクス> ゼロナット \frac{}{\text{zero} \ \text{nat} } zero nat a nat 成功 ( a ) nat \frac{a \ \text{nat}}{\text{Succ}(a) \ \text{nat} } Succ(a) nata nat

この推論規則では、自然数は 0 であるか、別の自然数の連続であると述べています。最初の規則など、前提のない規則は 公理 と呼ばれます。 .

推論規則を使用して構文を記述するのは冗長であるため、構文を記述する一般的な方法は、バッカス標準形 (BNF) のような文法表記法です。プログラミング言語の文法は、帰納的に定義された一連の用語です。 .たとえば、自然数の場合、次のように記述できます

<セマンティクス>nat : : = ゼロ ∣ 成功 ( nat ) \text{\textbf{nat}} ::=\text{ゼロ} | \text{Succ}(\textbf{nat}) nat::=Zero∣Succ(nat)

ただし、推論規則は構文よりもはるかに多くのことを表現できます。たとえば、+ のセマンティクスを定義しましょう。 + + 自然数の演算子:

<セマンティクス>n : nat ゼロ + ん ⇓ ん ( プラスベース ) \frac{n:\text{\textbf{nat}}}{\text{Zero} + n \Downarrow n} (\text{Plus-Base}) Zero+n⇓nn:nat (プラスベース)<セマンティクス> ん 1 : nat n 2 : nat n 1 + n 2 ⇓ ん 成功 ( n 1 ) + n 2 ⇓ 成功 ( ん ) ( プラス誘導 ) \frac{n_1:\text{\textbf{nat}} \quad n_2:\text{\textbf{nat}} \quad n_1 + n_2 \Downarrow n}{\text{Succ}(n_1) + n_2 \Downarrow \ text{Succ}(n)} (\text{プラス誘導}) Succ(n1 )+n2 ⇓Succ(n)n1 :natn2 :natn1 +n2 ⇓n (正誘導)

− のように、さらに演算を定義できます。 - − および × \times ×、推論規則による。別の例、自然数の単一連結リストを見てみましょう:

<セマンティクス>リスト : : = ゼロ ∣ 短所 ( nat , リスト ) \text{\textbf{list}} ::=\text{Nil} | \text{Cons}(\textbf{nat}, \textbf{list}) list::=Nil∣Cons(nat,list)

この文法は、リスト \text{\textbf{list}} list は Nil のいずれかです \text{Nil} Nil または Cons \text{短所} 自然数のコンセルと別の リスト \text{\textbf{list}} list.A <セマンティクス>Nil \text{Nil} Nil は空のリストであり、Cons \text{短所} Cons は、個々の要素を含み、サブリストを指す単一リンク リストの「ノード」です。

「cons」という単語を使用する慣例は、プログラミング言語 Lisp に由来します。cons "construct" または "constructor" として解釈できます。cons in Lisp は、言語の動的型付けの性質により、私たちの定義よりもはるかに柔軟です。

これで、list に対する操作の定義を開始できます。 \text{\textbf{list}} 推論規則のリスト。たとえば、head を定義できます。 リストの最初の要素を取得する関数:

<セマンティクス>l = 短所 ( hd , tl ) 頭 ( 私 ) ⇓ hd ( 頭の短所 ) \frac{l =\text{Cons}(\text{hd}, \text{tl})}{\text{head}(l) \Downarrow \text{hd}} (\text{head-Cons}) head(l)⇓hdl=Cons(hd,tl) (head-Cons)

部分関数、全体関数、およびエラー処理

head のバージョンに注目してください は部分関数です。つまり、すべてのリストが head までの自然数にマッピングされているわけではありません .この特定のケースでは、head(Nil) の意味を定義していません。 .このような部分関数を処理する方法はいくつかありますが、その 1 つは操作を 未定義 のままにしておくことです .このアプローチは C プログラミング言語が採用するものであり、型の安全性は損なわれますが、最適化には最適です。

別のアプローチは、そのような関数呼び出しを「エラー」または「例外」にすることです。

<セマンティクス> 頭 ( ゼロ ) ⇓ エラー ( head-Nil ) \frac{}{\text{head}(\text{Nil}) \Downarrow \text{Error}} (\text{head-Nil}) head(Nil)⇓Error (head-Nil)

そして 3 番目のアプローチは、この演算を合計関数に変換することです:

<セマンティクス> 頭 ( ゼロ ) ⇓ なし ( head-Nil ) \frac{}{\text{head}(\text{Nil}) \Downarrow \text{Nothing}} (\text{head-Nil}) head(Nil)⇓Nothing (head-Nil)<セマンティクス>l = 短所 ( hd , tl ) 頭 ( 私 ) ⇓ 何か(hd) ( 頭の短所 ) \frac{l =\text{Cons}(\text{hd}, \text{tl})}{\text{head}(l) \Downarrow \text{Something(hd)}} (\text{head-短所}) head(l)⇓Something(hd)l=Cons(hd,tl) (head-Cons)

現代のプログラミング言語の多くは、エラー処理戦略において折衷的になっています。たとえば、Rust プログラミング言語は、異なるコンテキストで 3 つのアプローチすべてを提供します。特定の操作については、デフォルトの「安全な」バージョンを 2 番目のアプローチ ( panic ) または 3 番目のアプローチ (Option および Result )、しかし最初のアプローチでは「安全でない」バージョンでもあります。

派生

Succ(Zero) などのナンセンスを簡単に作成できます ⇓ ゼロ \text{Succ(Zero)} \Downarrow \text{Zero} Succ(Zero)⇓Zero では、判断が正しいことを証明するにはどうすればよいでしょうか?判断を証明するには、derivation と書きます (派生ツリーとも呼ばれます) またはプルーフ ツリー ).

導出は常に公理から始まり、証明したい判断で終わります。各ステップで、前の判断に推論規則を適用します。

たとえば、nat の定義で「1 + 1 =2」を証明するには、

下から上に読むと、導出がプログラムの実行に似ていることがわかります。

Succ(Zero) + Succ(Zero)
= Zero + Succ(Succ(Zero))
= Succ(Succ(Zero))

+ の実行を追跡できます 純粋な関数であるため、置換による操作が容易 .つまり、+ 少なくとも私たちが懸念しているレベルでは、決定論的で副作用がありません.

実装の詳細を検討する場合 レジスタやスタック メモリの変更などの場合、純粋な関数はありませんが、これは議論の助けにはなりません.一定レベルの抽象化は、純粋な関数を最適化するのに役立つだけでなく、コンパイラにも役立ちます.

プログラミングとの類似

ここで説明したすべての数学表記には、対応するプログラミングがあります。以下は、数学表記とプログラミングの比較表です:

数学表記 実装
判定フォーム bool を返す関数の関数シグネチャ
判断 関数の適用
推論規則 関数本体
派生 評価/実行

判断フォーム l があるとしましょう ⇓ へ l \Downarrow e l⇓e、関数シグネチャとして記述できます

val head : (l: nat list, e: option(nat)) -> bool

head の推論規則 関数本体として表示できます。

<セマンティクス> 頭 ( ゼロ ) ⇓ なし ( head-Nil ) \frac{}{\text{head}(\text{Nil}) \Downarrow \text{Nothing}} (\text{head-Nil}) head(Nil)⇓Nothing (head-Nil)<セマンティクス>l = 短所 ( hd , tl ) 頭 ( 私 ) ⇓ 何か(hd) ( 頭の短所 ) \frac{l =\text{Cons}(\text{hd}, \text{tl})}{\text{head}(l) \Downarrow \text{Something(hd)}} (\text{head-短所}) head(l)⇓Something(hd)l=Cons(hd,tl) (head-Cons)
let head (l : nat list, e: option(nat)) =
  match l with
  | [] -> false
  | hd::_ -> hd = e

head(Cons(Succ(Zero), Nil)) Succ(ゼロ) \text{head(Cons(Succ(Zero), Nil))} \ \\text{Succ(Zero)} head(Cons(Succ(Zero), Nil)) Succ(Zero) は、

head Cons(Succ(Zero), Nil) Succ(Zero)  (*true*)

例として OCaml 構文を使用しますが、これはどのプログラミング言語にも当てはまります。私のユースケースでの OCaml などの ML ファミリー言語の利点は、nat などの帰納的に定義された型に対する優れたサポートがあることです。 と list .

数学からのリテラル変換は非常に非効率な実装を生成することに注意してください.実際の実装では, おそらく head と書くでしょう. 機能:

let head (l : nat list) =
  match l with
  | [] -> None
  | hd::_ -> Some(hd)

それでもなお、数学表記と実際のプログラミングとの関係を理解することは、概念的には有用です。

判定の「タイプ エラー」

判定や推論ルールを書く際に「型誤り」を起こしやすい。 例えば以下の推論ルールは + と間違っている は自然数ではないので Succ の中に入れることはできません .

<セマンティクス>n 1 : nat n 2 : nat 成功 ( n 1 ) + n 2 ⇓ 成功 ( n 1 + n 2 ) ( 偽プラス帰納的 ) \frac{n_1:\text{\textbf{nat}} \quad n_2:\text{\textbf{nat}}}{\text{成功}(n_1) + n_2 \Downarrow \text{成功}(n_1 + n_2 )} (\text{Bogus-Plus-Inductive}) Succ(n1 )+n2 ⇓Succ(n1 +n2 )n1 :natn2 :nat (Bogus-Plus-Inductive)

抽象構文と値を混在させてツリー ウォーキング インタープリターをコーディングする場合も同様に、この種の間違いを犯しやすくなります。 、判断と推論規則を書くときは、あなた自身です。したがって、精神的な「タイプチェッカー」を構築することは、判断を正しく書くのに非常に役立ちます.

概要

判断と推論規則は、プログラミング言語の正式な定義の基本的な構成要素であり、それらのないプログラミング言語の論文を見つけることは困難です.したがって、そのような表記法で読み書きする方法を理解することは非常に重要です.

<オール>
  • ロバート・ハーパー。 プログラミング言語の実用的な基礎 .ケンブリッジ大学出版局、ケンブリッジ、イギリス、第 2 版、2016.↩