形式言語（けいしきげんご、）は、その文法（構文、統語論）が、場合により意味（意味論）も形式的に与えられる（形式体系を参照）言語である。形式的ではないため、曖昧さが残されたり話者集団により用法が変化する自然言語に対し、プログラミング言語を含む一部の人工言語や機械可読なドキュメント類などの形式言語は、用法の変化に厳格である。本項は形式的な統語論である構文の形式的な定義と、形式文法を扱う。形式意味論も参照。
定義 形式言語の理論、特にオートマトン理論と関連した理論において、言語はアルファベットの列（語 word）の集合である。
長さゼロの空単語（Empty Word, 記号 、、）も含む。チューリングマシンの言語は単なる文字列で、他のチューリングマシンを含む数学的構造を扱うためには、符号化してその数値を解釈するプログラムを埋め込む必要がある。チューリングマシンは十分に強力で、この手法を用いると、あらゆる列挙可能な構造の扱いが可能である。チューリングマシンの数値表現は、チューリングマシンの表記 (description) と称する。
あるチューリングマシンが存在して、言語に属するすべての語 w に対して動作させると受理状態で停止し、属さない語は受理しないとき、言語はチューリング認識可能という。言語に属さないときは必ず拒否状態で停止する場合、言語はチューリング判別可能であるという。2者の違いは、一部の入力に対してチューリングマシンが停止しない場合の有無である。チューリングマシンTMの言語 L(TM) は、テープに w をセットしたあと、TMを動作させると受理状態に入って停止するような w の集合からなる言語、即ちTM認識可能な言語である。
この言語には以下のような演算が定義される。ここで、 と は共通のアルファベットから構成される言語であるとする。 「連結」 は、文字列群 から構成される。ここで、 は に含まれる文字列で、 は に含まれる文字列である。 「積集合」 は、 にも にも含まれる文字列の集合である。 「和集合」 は、 か に含まれる文字列の集合である。 の「補集合」は、 に含まれない全ての文字列の集合である。 「商集合」 は、 に含まれる文字列 に対して、 に含まれる文字列 が存在するときに、全ての に相当する文字列群から構成される。 「クリーネスター」 は、 という形式の全文字列群から構成される。ただし、 は に含まれ、 である。注意すべきは、 の場合もあるので、空文字列 も含まれるという点である。 「反転」 は、 の全文字列を反転させた文字列群から構成される。 と の「シャッフル」とは、 で表される全文字列から構成される。ここで、 で、 を連結した は に含まれる文字列であり、 を連結した は に含まれる文字列である。
モデル理論において、言語は定数記号、関数記号、述語記号の集合である。
形式文法
形式言語は、形式文法と密接な関係がある。例として、次のような文脈自由文法の構文規則があるとき、 名詞句 ::= 名詞 | 形容詞 名詞 | 名詞句 "を" 動詞 "ている" 名詞句 動詞 ::= "見" 名詞 ::= "猿" | "飼育員" 形容詞 ::= "小さい" 以下のように規則を再帰的に適用して、言語要素（名詞句）の列挙が可能である。 （猿 飼育員 小さい猿 小さい飼育員） （猿 飼育員 小さい猿 小さい飼育員 猿を見ている猿 猿を見ている飼育員 猿を見ている小さい猿 …… 小さい猿を見ている猿 ……） （猿 飼育員 小さい猿 小さい飼育員 猿を見ている猿 …… 猿をみている猿を見ている猿 …… 小さい猿を見ている猿を見ている小さい飼育員を見ている猿 ...） ...
このような操作を任意回繰り返して、文の集合として当該言語が得られる。
チョムスキー階層では形式文法が階層を構成するとしており、生成する言語では、言語の認識に必要な最小のオートマトンが、階層を構成して出現する。
その他
言及される分野 「人や計算機の如何なる記号変換能力から如何なる思考能力や計算能力が生まれるか」を学問として扱う数理論理学の研究対象で、哲学・言語学・計算機科学・数学基礎論・数理心理学などに有用である。これらの分野は、如何なる形式言語を研究すべきかの文法論（構文論・統辞論）や形式言語の意味論や演繹論を扱う。
形式言語に加えて検証や証明などの仕組みを併せた場合は、形式手法と表現する。
自然言語への応用
チョムスキーは、自然言語を比較的単純な形式言語のモデルに当てはめて分析する言語学を提唱した。音素や語幹などを素記号として扱う。実際の自然言語では構文規則や文法は自然発生的であり、形式言語の構文規則と異なり明確な規定に難がある。
素朴な文法論の主張は、形式言語の理論と見做すことが可能で例記する。 品詞にはこのようなのものがある。 この語はあの品詞に属す。 この品詞に属す語をこの活用と組み合わせと順序とで並べると文（や句や節）になる。 このような文法論はすなわち、素記号とは何かを定めてそれらから文を作る構文規則を定める、形式言語の理論である。形式言語論を用いた文法論は、実言語との比較で自然言語の特徴を際立たせ、自然言語の理解に寄与する。
脚注