この記事は高知工科大AdventCalendar2017の10日目の記事です．
はじめに
プログラミング言語を作るときにはまず言語設計をしなければなりません．だいたいは以下のものを設計します．
- 文法（構文規則，syntax）
- その言語の構文（文法，具象構文）を定義するもの．
- 意味論（評価規則，semantics）
- 定義した構文規則に則った文字列がどのように評価されるか=どのような意味を持つかを定義するもの
- 型システム（型付け規則）
- 評価結果がどのように型付けされるかを定義するものを型付け規則といい，型システムはその集合
どんな文法にであるかはもちろん，その文法で書かれたものがどのような意味を持つのかは必ず定義する必要はあります（一つ目，二つ目）．三つ目の型システムは型のあるプログラミング言語には必要となります．
これらの規則を表現するときに，自然言語で頑張って書くという方法もありますが，それだとどうしても曖昧性が出てしまったりそもそも面倒くさいです．そこで規則の書き方みたいなものが世の中には存在し，それを使うと規則を厳密にかつ楽に表現できるわけです．また，プログラミング言語関係の論文ではよく使われますし，ネット上の記事でもしばしば存在します．規則を書くことのない人も知っておくことでそれらを読むことができるようになります．といいつつも，書き方の細かいところはわりと記事によって異なるところもあります．今回は基本的な部分を扱います．基本的なところを抑えておけばなんでも読めるはずです．
というわけで，この記事では規則の書き方を中途半端にかつだらだらと書いていきます．読者対象はそれでも読もうと思う人であって，そうじゃない人にとっては以下はゴミカス記事なので早く帰ってアマゾンプライムで冴えカノ8話を観てればいいと思います．
例で扱うプログラミング言語
規則の書き方を伝えるためには例を扱うしか無い，ということで例ではmlをシンプルにした言語（以下，tiny-ml）を使います．
tiny-mlで扱えるのは次のような式のみとします．
- 数値，真偽値
- 四則演算式
- 比較演算式
- 変数束縛式
- 識別子
- if式
- 関数定義式
- 関数適用式（関数呼び出し）
mlをある程度わかっている人はここは飛ばしてください．
数値，真偽値
数値は普通の10進法．
0，1，99，100など．
01，000は扱わない．
真偽値はtrue，false
四則演算式
加算，減算，乗算，除算．
1 + 2，2 - 1，2 * 3，4 / 2など．
この場合の評価結果は3，1，6，2
比較演算式
二値が等価であることを検査する==，
左辺値が右辺値よりも小さい数値であることを検査する<のみとする．
真であればtrue，偽であればfalseを返す．
変数束縛式，識別子
例えば，
let x = 1 in x + 2
と書くと，xに1を束縛してx + 2を評価する，という意味．
この式全体が変数束縛式．letと=とinはキーワード．
inのあとのxが識別子．
識別子は評価されるとその識別子に束縛されている値を返す．
この式の評価結果は3となる．
条件式
例えば，
if x == 0 then y + 1 else y - 1
と書くと，xの評価結果が0ならばy + 1を評価した値を返し，そうでなければy - 1を評価した値を返す．
変数束縛（関数）
tiny-mlでは単純のため引数はひとつしかとれないものとする．
let f x = x * x in f 2
この場合，xを引数にとり，x * xを返す関数をfに束縛し，f 2を評価する．
関数適用式
f 2とあったときは，実引数2で関数fを評価する．したがって，
let f x = x * x in f 2
この式は4を返す．
構文規則
構文規則はBNF（Backus-Naur form）か，BNFの拡張版であるEBNF，もしくはそれに似た何かで書かれます．
BNFは導出規則の集合です．
以下で例として書いている導出規則は，単純のためスペースや改行文字は考慮しません．（なのでちょっと正確でない）
ひとつの導出規則は，例えば次のような書き方をします．
<a> ::= "b" "c"
<a>，"b"，"c"は全てひとつの記号です．<a>のように，<>で囲んだものは非終端記号といい，"b"，"c"は終端記号といいます．導出規則は，上のように::=の左辺は非終端記号，右辺には記号の列を記述します．
この導出規則より，<a>から導出できる文字列はbcのみです．
これだけでは何にもならないので，弄って次の導出規則を書きます．
<a> ::= "b" <d> "c"
<d> ::= <a> | "e"
<d>の導出規則を追加し，<a>の導出規則に<d>を含むようにしました．
<d>の導出規則で|を書きましたが，これは選択の意味で，ここでは<d>は<a>にも"e"にもなるという意味になります．|はいくらでもつなげることができ，<a> | "e" | "f" | "g"のようなこともできます．
この導出規則より<a>から導出できる文字列は，
bec
bbecc
bbbeccc
bbbbecccc
...
というように，n回のb，e，n回のc（nは1以上）になります．
このように，BNFで非終端記号の導出規則を列挙することで，導出できる文字列を示します．
あるBNFの記述から導出できる文字列が，あるプログラミング言語が受理できるプログラムであるとするとそのBNFの記述はそのプログラミング言語の文法です．
tiny-mlの構文規則
tiny-mlの構文規則をBNFで書いてみます．読めば直感的にわかると思います．
<program> ::= <expr> // tiny-mlのプログラム
<expr> ::= <let-fun-expr> // 変数束縛式（関数）
| <let-expr> // 変数束縛式
| <apply-func> // 関数適用式
| <if-expr> // if式
| <bin-expr> // 二項演算式（四則演算と比較演算）
| <number> // 数値
| <bool> // 真偽値
| <identifier> // 識別子
<let-fun-expr> ::= "let" <identifier> <identifier> "=" <expr> "in" <expr>
<let-expr> ::= "let" <identifier> "=" <expr> "in" <expr>
<apply-func> ::= <identifier> <expr>
<if-expr> ::= "if" <expr> "then" <expr> "else" <expr>
<bin-expr> ::= <expr> <bin-op> <expr>
<bin-op> ::= "+" | "-" | "*" | "/" | "==" | "<"
<bool> ::= "true" | "false"
書いているときに思ったのですが<number>と<identifier>はBNFで与えるものではないですね．<number>は数値の集合，<identifier>は識別子の集合です．
一応正規表現で与えておくと，<number>は0|[1-9][0-9]*，は[a-zA-Z]+です．
評価規則（semantics）
ここからはプログラムの意味の定義の仕方とかを説明します．
「型システム入門」通称TAPLには，「意味論の形式化には三つの基本的なアプローチがある」と操作的意味論，表示的意味論，公理的意味論というものがあることが説明されています．私はよくわかりません．
操作的意味論はなんとなくわかるきがするというのと，殆どの場合は操作的意味論が使われているみたいなので，それを説明します．
環境
といいつつ，その前に環境というものについて説明します．
プログラミング言語の世界における環境（environment）とは，識別子と値の組の集合です．ここでは識別子idと値valの組をid=valと書くことにします．これは変数idにvalが束縛されていることを意味します．識別子と値の組の集合は，[id1=val1,id2=val2,...]というように書くことにします．
例えば，xに1，yに2が束縛されている場合だと，[x=1,y=2]と書きます．
また，ある環境$\rho$（ろー）の下である式$exp$を評価するとき，$exp\ \rho$と書くことにします．
例えば，x + yを環境[x=1,y=2]の下で評価するとき，x + y [x=1,y=2]と書きます．これの評価結果は3です．
環境$\rho$に新しくz=3を追加するときは，$[z=3]\rho$と書きます．
小ステップスタイル
操作的意味論には，小ステップスタイルで書く方法と大ステップスタイルで書く方法があります．
小ステップスタイルは，評価の各ステップに着目し，評価を1ステップ進める毎にどのように式が値に書き換わるかを示します．
条件式
if式の評価規則を例に書きます．
{\rm if}\ {\rm true}\ {\rm then}\ t_2\ {\rm else}\ t_3\ \rho \rightarrow t_2\ \rho \\
{\rm if}\ {\rm false}\ {\rm then}\ t_2\ {\rm else}\ t_3\ \rho \rightarrow t_3\ \rho \\
\frac{t_1\ \rho \rightarrow t_1'\ \rho}{{\rm if}\ t_1\ {\rm then}\ t_2\ {\rm else}\ t_3\ \rho \rightarrow {\rm if}\ t_1'\ {\rm then}\ t_2\ {\rm else}\ t_3\ \rho}
ただし$t_i$は式です．
$\rightarrow$は，評価を1ステップだけ進める，の意味です．
つまり，一つ目の規則は条件式の部分の値がtrueであるときに評価を1ステップすすめると，if式の項は$t_2$に書き換わる，ということになります．
環境は変化しません．
二つ目の規則はfalseのときで，elseの$t_3$に書き換わる規則です．
三つ目の規則は他とは少し違います．あの横線は，線より上の式のようになるならば下の式が成り立つというように読みます．
つまり，$t_1$の評価を1ステップ進めたときに$t_1'$になるならば，${\rm if}\ t_1\ {\rm then}\ t_2\ {\rm else}\ t_3$の評価を1ステップ進めると${\rm if}\ t_1'\ {\rm then}\ t_2\ {\rm else}\ t_3$に書き換わる，という意味になります．
まとめると，条件式の部分がtrueでもfalseでもない式であれば，三つ目の規則を適用して条件式を1ステップずつ評価していき，trueかfalseになったところで一つ目か二つ目の規則が適用されます．
変数束縛
let式も書いてみます．
let式は変数束縛するので環境が変化します．
{\rm let}\ var\ {\rm =}\ val\ {\rm in}\ t_2\ \rho \rightarrow t_2\ {\rm [}var{\rm =}val{\rm ]}\rho
\\
\frac{t_1\ \rho \rightarrow t_1'\ \rho}{{\rm let}\ var\ {\rm =}\ t_1\ {\rm in}\ t_2\ \rho \rightarrow {\rm let}\ var\ {\rm =}\ t_1'\ {\rm in}\ t_2\ \rho}
$var$は変数名となる識別子，$val$は真偽値か数値とします．
一つ目の規則が意味するのは，「${\rm let}\ var\ {\rm =}\ val\ {\rm in}\ t_2$の評価を1ステップ進めると，$var{\rm =}val$の新しい組を環境に追加し，その環境で$t_2$を評価する」，です．
これによって値$val$を変数$var$に束縛して$t_2$を評価するということが表現できます．
大ステップスタイル
大ステップスタイルは，式は最終的に値に評価されることを直接定式化したもの（TAPL）．
項$t$が最終的に値$val$に評価されるとき，大ステップスタイルでは$t\Downarrow val$と書きます．
条件式
大ステップスタイルでif式の評価規則を書くと次のようになります．
\frac{t_1\ \rho\ \Downarrow {\rm true}\ \ t_2\ \rho \Downarrow val_2}{{\rm if}\ t_1\ {\rm then}\ t_2\ {\rm else}\ t_3\ \rho \Downarrow val_2}
\\
\frac{t_1\ \rho\ \Downarrow {\rm false}\ \ t_3\ \rho \Downarrow val_3}{{\rm if}\ t_1\ {\rm then}\ t_2\ {\rm else}\ t_3\ \rho \Downarrow val_3}
一つ目の規則は，$t_1$を評価して最終的にtrueになり，かつ$t_2$を評価して最終的に$val_2$になるならば，${\rm if}\ t_1\ {\rm then}\ t_2\ {\rm else}\ t_3$は最終的に$val_2$に評価される，ということを意味します．
二つ目も同様です．
型付け規則
型付け規則は，項がどのようにして型付けされるかを説明・表現します．
前提
ここでは，式や値$t$が，型${\rm T}$（${\rm T}$は型変数）であることを，$t:{\rm T}$と書きます．
また，存在する型はBool型とNumber型のみとします．
型環境
型環境は，項とその型の組の集合です．ここでは型環境を$\Gamma$と書きます．
型環境に変数xと型${\rm T}$の組を追加するとき，つまりxを${\rm T}$で型付けするとき，$\Gamma,x:{\rm T}$と書きます．
型環境$\Gamma$の下でxの型が${\rm T}$であるとき，$\Gamma\vdash x:{\rm T}$と書きます．
また，型環境$\Gamma$においてxの型は${\rm T}$と仮定することを，$x:{\rm T}\in\Gamma$と書きます．
型付け規則の書き方の例
リテラル
まず，リテラルの型です．
{\rm true}:{\rm Bool} \\
{\rm false}:{\rm Bool} \\
number:{\rm Number}
ただし，$number$は数値です．
そのまんまです．
変数
\frac{var_1:{\rm T}_1\in \Gamma}{\Gamma \vdash var_1:{\rm T}_1}
$\Gamma$の型環境において変数$var_1$の型は${\rm T}$であるとき，出現する$var_1$の型は${\rm T}$．
変数束縛
let式です．
変数束縛するので型環境も変化します．
\frac{\Gamma,t_1:{\rm T}_1 \vdash t_2:{\rm T}_2}{\Gamma \vdash {\rm let}\ var_1\ {\rm =}\ t_1\ {\rm in}\ t_2:T_2}
$t_1$の型は${\rm T_1}$であるということを$\Gamma$の型環境に追加し，更にその型環境の下で$t_2$の型が${\rm T_2}$であれば，${\rm let}\ var_1\ {\rm =}\ t_1\ {\rm in}\ t_2$の型は${\rm T_2}$．
関数
${\rm T_1}\rightarrow {\rm T_2}$は，型${\rm T_1}$の値を引数にとって，型${\rm T_2}$の値を返す関数の型を意味します．
\frac{\Gamma,var_1:{\rm T}_1 \vdash t_1:{\rm T}_2\ \ \ \ \Gamma,f_1:{\rm T_1}\rightarrow {\rm T_2} \vdash t_2:{\rm T_3}}{\Gamma \vdash {\rm let}\ f_1\ var_1\ {\rm =}\ t_1\ {\rm in}\ t_2:T_3}
$var_1:{\rm T}$を$\Gamma$に追加した型環境の下で$t_1:{\rm T_2}$であり，また$f_1:{\rm T_2}$を$\Gamma$に追加した型環境の下で$t_2:{\rm T_3}$であるとき，$\Gamma$の下での${\rm let}\ f_1\ var_1\ {\rm =}\ t_1\ {\rm in}\ t_2$の型は${\rm T_3}$．
日本語で書くとなにがなんだかわからなくなってきた．
関数適用
\frac{t_1:{\rm T_1}\in \Gamma\ \ \ \ f_1:{\rm T_1}\rightarrow {\rm T_2}\in \Gamma}{\Gamma \vdash f_1\ t_1:T_2}
型環境$\Gamma$の下で，$t_1:{\rm T_1}$かつ$f_1:{\rm T_1}\rightarrow {\rm T_2}$であるとき，$f_1\ t_1$の型は${\rm T_2}$．
まとめ
- 構文規則はBNFで．
- 評価規則は操作的意味論の小ステップスタイルと大ステップスタイル
- 型付け規則は型環境とかをつかっていいかんじに
参考文献
- 型システム入門
- Essentials of Programming Languages
おわりに
だらだらした文章でごめんなさい．
こんな長々してるけど実際問題，規則は読めばなんとなくわかる．