1週間前、私はPOPLプログラミング言語の原則に関する記事が「知的脅迫」の基準を満たさなければ出版に受け入れられないと冗談を言いました。 もちろん、これは真実ではありませんが、実際には、プログラミング言語に関する記事は実務家にとって特に恐ろしいように見えます（または、学者は実際にコンピューターサイエンスの別の分野で働いています！）。 それらには、「判断」、「操作上のセマンティクス」などの数学記号とフレーズが詰め込まれています。 微妙な録音オプションは多数ありますが、基本的にいくつかの基本概念を理解することで、記事の要旨を把握できます。 そのため、別の科学記事に関する話の代わりに、プログラミング言語のトピックに関する科学記事のデコードに関する短い実用的なガイドを今日書いた方が良いと思いました。 ここでは、Benjamin Pearceの著書 『プログラミング言語の種類』を信頼できる情報源として参照します。

構文

clear：構文から始めましょう。 構文は、言語で使用できる文（つまり、どのプログラムを作成できるか）を示します。 構文には、構成要素である一連の用語が含まれています。 Pierceから次の例を取り上げます。

t ::= true false if t then t else t 0 succ t pred t iszero t
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

記号t



が出現する場所であれば、どの用語でも置き換えることができます。 記事で用語が言及されている場合、異なる用語を区別するために添え字付きのt



がよく使用されます（たとえば、 $$$t_1$ 、 $$$t_2$ ） 多くの用語は次のように呼ばれます $$$\ tau$ 。 シンボルと混同しないでください $$$T$ これは伝統的に型を示すために使用されます。



上記の例では、 if



自体は用語ではないことに注意してください（トークン、この場合はキーワードトークン）。 この用語は、 if t then t else t



条件式if t then t else t



。



用語は計算可能な式であり、適切に構築された環境での計算の最終結果はvalueである必要があります 。 値は用語のサブセットです。 上記の例では、値はtrue



、 false



、 0



、およびsucc



操作を連続して0



適用することによって作成できる値（ succ 0, succ succ 0, ...



）です。

意味論

言語の用語に何らかの意味を与えたい。 これはセマンティクスです。 プログラムの価値を判断するにはさまざまな方法があります。 ほとんどの場合、 操作上のセマンティクスと表示上のセマンティクスへの参照に出くわします。 これらのうち、動作セマンティクスが最も一般的です。 用語を計算する抽象マシンのルールを設定することにより、プログラムの意味を決定します。 仕様は一連の計算ルールの形式を取ります -少し後で検討します。 この世界観では、用語t



の値 （意味）は、マシンが到達する最終状態（値）であり、 t



を初期状態で実行しています。 表示的セマンティクスでは、既存のセマンティックドメイン内の数学的オブジェクト（たとえば、数字や関数）が用語値として使用され、解釈関数は言語の用語をターゲットドメイン内の同等の用語と関連付けます。 そのため、この領域で用語が表すもの（または示すもの）を示します。



また、著者は、小さなステップ（小さなステップ）の操作上のセマンティクスと大きなステップ（大きなステップ）の操作上のセマンティクスに言及している場合があります。 名前が示すように、これは、各ルールが適用されたときに抽象マシンがどれだけ大きく飛躍するかを示します。 小さなステップのセマンティクスでは、用語は徐々に意味が変わり、最終的に意味になるまで一度に1ステップずつ書き換えられます。 大きなステップを持つセマンティクス（別名「自然なセマンティクス」）では、用語からその最終的な意味まで1ステップで進むことができます。



小さなステップのセマンティクスエントリには、次のようなものが表示されます。 $$$t_1 \右矢印t_2$ そのために何を読むべきか $$$t_1$ で計算 $$$t_2$ 。 （下付き文字の代わりに、ストロークを使用できます。たとえば、 $$$t \右矢印t '$ ） これは判断としても知られています。 矢印 $$$\右矢印$ 計算の1ステップを表します。 会ったら $$$t_1 \右矢印^ {*} t_2$ 、それは「ワンステップ計算を繰り返し適用した後」を意味します $$$t_1$ 最終的にに移動しました $$$t_2 ’$ 「。



セマンティクスでは、大きな矢印で別の矢印が使用されます。 だから何 $$$t \下向き矢印v$ 用語を意味する $$$t$ 計算の結果、私はに切り替えました $$$v$ 。 ステップが小さいセマンティクスとステップが大きいセマンティクスが同じ言語で使用される場合、 $$$t \右矢印^ {*} v$ そして $$$t \下向き矢印v$ 同じことを意味します。



規則によれば、規則は大文字と呼ばれます。 運が良ければ、著者は追加のヒントとして接頭辞「E-」を計算ルールに追加します。



例：



trueの場合t ₂ else t ₃ $$$\右矢印$ t ₂ （E-IFTRUE）



通常、計算ルールは推論ルールのスタイルで定義されます。 例（E-IF）：

$$

$$\ frac {t_1 \ \ rightarrow t '_ {1}} {\ mathrm {if} \ t_1 \ \ mathrm {then} \ t_2 \ \ mathrm {else} \ t_3 \ rightarrow \ mathrm {if} \ t'_1 \ \ mathrm {then} \ t_2 \ \ mathrm {else} \ t_3}$$

これは、「除数で指定されている場合、分母にあると結論付けることができます」と読む必要があります。 つまり、この特定の例では、「If $$$t_1$ に表示 $$$t '_ {1}$ この場合 $$$\ mathrm {if} \ t_1 ...$ に表示 $$$\ mathrm {if} \ t'_1 ... ’$ 。

種類

プログラミング言語は特定の型システムを持つ必要はありません（型付けされていない場合もあります）が、ほとんどの言語にはあります。

「型システムは、計算する値の型に応じて言語表現を分類することにより、プログラムに特定の型の動作がないことを証明するための柔軟に制御された構文手法です」-Pierce、「プログラミング言語の型」。

コロンは、特定の用語が特定のタイプに属することを示すために使用されます。 例えば $$$t：T$ 。 式が存在する型が存在する場合、用語は正しく型付けされた（または型付けされた）と見なされます $$$t：T$ 。 計算ルールがあるので、入力ルールがあります。 また、推論規則のスタイルで定義されることも多く、名前は接頭辞「T-」で始まる場合があります。 例（T-IF）：

$$

$$\ frac {t_1：\ mathrm {Bool} \ \ t_2：\ mathrm {T} \ \ t_3：\ mathrm {T}} {\ mathrm {if} \ t_1 \ \ mathrm {then} \ t_2 \ \ mathrm { else} \ t_3 \：\ \ mathrm {T}}$$

これは、「用語1はタイプBoolに属し、用語2および3はタイプTに属するため、用語「if term 1 then term 2 else term 3」はtype Tに属する」と読み替える必要があります。



関数（ラムダ抽象化）では、引数の型と戻り値も監視します。 タイプを指定することにより、関連する変数に注釈を付けることができます。 $$$\ lambda x.t$ 書ける $$$\ lambda x：\ mathrm {T_1}。 t_2$ 。 ラムダ抽象化のタイプ（引数が1つの関数の場合）は、次のように記述されます。 $$$\ mathrm {T_1} \ \右矢印\ \ mathrm {T_2}$ 。 これは、関数が型の引数を取ることを意味します $$$\ mathrm {T_1}$ そして、次のような結果を返します $$$\ mathrm {T_2}$ 。



引き出しルールには、誘導可能性の兆候が表示されます-回転式改札口の形のオペレーター $$$\ vdash$ 。 手段 $$$P \ vdash Q$ 「QはPから推定できる」または「PはQを意味する」と読む必要があります。 例えば $$$x：\ mathrm {T_1} \ vdash t_2：\ mathrm {T_2}$ 「xがタイプT1に属するという事実から、タイプt2はタイプT2に属するということになります。」



関数内の自由変数の型への変数のバインドを追跡します。 これを行うには、タイピングコンテキスト （タイピング環境）を使用します 。 変数名を値に変換する使い慣れた環境として想像してください。ただし、ここでのみ変数名を型に変換します。 慣例に従って、ガンマ記号（ $$$\ガンマ$ ） 慣例により、説明のない科学記事によく見られます。 ロープにぶら下がっている型で変数を修正する絞首台を想像することで、その意味を思い出しました。 しかし、別の方法があるかもしれません！ これは、フォームで頻繁に発生するトリプルリレーションにつながります $$$\ガンマ\ vdash t：\ mathrm {T}$ 。 次のようになります。「入力コンテキストから $$$\ガンマ$ つまり、用語tはタイプTに属します。 コンマ演算子は展開します $$$\ガンマ$ 右側に新しいバインディングを追加する（例： $$$\ガンマ、x：\ mathrm {T}$ ）



これをすべて組み合わせて、次のようなルールを取得します（この場合、ラムダ抽象化のタイプを決定します）。

$$

$$\ frac {\ Gamma、x：\ mathrm {T_1} \ vdash t_2：\ mathrm {T_2}} {\ Gamma \ vdash \ lambda x：\ mathrm {T-1} .t_2：\ mathrm {T_1} \ rightarrow \ mathrm {T_2}}$$

規則を解読します：「（分子で示されているもの）をx1に制限するタイピングコンテキストから、t2がタイプT2に属している場合、同じタイピングコンテキストで（分母で示される部分）、式 $$$\ lambda x：\ mathrm {T_1} .t_2$ タイプに属する $$$\ mathrm {T_1} \右矢印\ mathrm {T_2}$ 「。

型の安全性

Jane Austenが型システムに関する本を書いたなら、彼女はおそらくそれを「昇進と保存」と呼んでいたでしょう（実際、そのタイトルで多くの興味深いエッセイを書くことができると思います！）。 型システムは、計算プロセス中に適切に型付けされた用語がストールしない場合、「安全」（型安全）と見なされます。 実際には、これは、推論ルールのチェーンにおいて、最終的な意味がなければどこにも行き詰まらないことを意味します。同時に、さらなるプロモーションのためにルールを適用する能力もありません（著者は「行き詰まり」と「行き止まりに終わる」というフレーズを使用することがわかります-これはまさにその意味です）。 正しくタイプされた用語が行き止まりにならないことを実証するには、プロモーションと保存の定理を証明するだけで十分です。

• プロモーション 正しく入力された用語は、行き止まりになることはありません（この値、または計算規則に従って次のステップを実行できます）。
• 保存しています。 正しく入力された用語が計算ステップを実行する場合、結果の用語も正しく入力されます。

なぜこれが重要なのかを明確に示すことなく、著者がプロモーションと保護について話しているのを見ることがあります。 これで理由がわかりました！

教会、カレー、ハワード、Ho

以下に、知っておくと面白いと思われるいくつかのことを示します。

• Curryのスタイルに従って言語を定義するには、まず用語の文法を定義し、次にその動作を定義し、最後に「動作が好ましくない特定の用語を拒否する」タイプシステムを追加します。 セマンティクスは、類型化よりも早く発生します。
• 教会のスタイルに従って言語を定義する際に、タイピングはセマンティクスよりも先に行われるため、誤ってタイプされた用語の動作は何かという質問は決してしません。
• カリー-ハワード対応は、型理論と論理の間の対応であり、論理ステートメントは型システムで型として扱われます。 （「タイプとしてのステートメント」のアナロジー）。 この対応は、ある領域から別の領域に結果を転送するために使用できます（たとえば、線形ロジックから線形型のシステムへ）。
• HoarロジックまたはHoarトリプルは、{P} C {Q}という形式の式を参照します。 これは、「前提条件Pが真の場合、Cコマンドが実行され（終了する場合）、事後条件Qが真になります」と読む必要があります。

実際、私はコミュニティで何が起こっているのかを見ているだけの興味を持った部外者です。 プログラミング言語の専門家としてこれを読み、開業医のチートシートに含まれるべきより多くのものを知っているなら、コメントで知らせてください！