正式な言語

論理学、数学、コンピューターサイエンス、言語学において、形式言語はアルファベットから取られた文字で構成され、形式文法と呼ばれる一連の特定の規則に従って整形式化された単語で構成されます。

形式言語のアルファベットは、単語と呼ばれる文字列に連結された記号、文字、またはトークンで構成されています。 ^[1]特定の形式言語に属する単語は、整形式の単語または整形式の式と呼ばれることもあります。形式言語は、その形成規則で構成される正規文法や文脈自由文法などの形式文法によって定義されることがよくあります。

コンピュータサイエンスでは、形式言語は、プログラミング言語の文法や自然言語のサブセットの形式化されたバージョンを定義するための基礎として使用されます。自然言語のサブセットでは、言語の単語が意味やセマンティクスに関連付けられた概念を表します。計算複雑性理論では、決定問題は通常、形式言語として定義され、複雑性クラスは、計算能力が限られたマシンで解析できる形式言語の集合として定義されます。論理学と数学の基礎では、形式言語は公理系の構文を表すために使用され、数学的形式主義とは、すべての数学はこのように形式言語の構文操作に還元できるという哲学です。

形式言語理論の分野では、主にそのような言語の純粋に統語的な側面、つまり内部構造パターンを研究します。形式言語理論は、自然言語の統語的規則性を理解する方法として言語学から生まれました。

17世紀、ゴットフリート・ライプニッツは、象形文字を利用した普遍的かつ形式的な言語であるキャラクタリスティック・ユニバーサリスを構想し、記述した。その後、カール・フリードリヒ・ガウスはガウス符号の問題を調査した。^[2]

ゴットロープ・フレーゲは、最初に『Begriffsschrift』（1879年）で概説され、2巻からなる『Grundgesetze der Arithmetik』（1893/1903年）でより完全に開発された記法システムを通じて、ライプニッツの考えを実現しようとしました。 ^[3]これは「純粋言語の形式言語」を説明しました。^[4]

20世紀前半には、形式言語に関連したいくつかの発展があった。アクセル・トゥーは1906年から1914年にかけて、単語と言語に関する4つの論文を発表した。これらの最後の論文は、エミール・ポストが後に「トゥーシステム」と名付けたものを導入し、決定不可能な問題の初期の例を示した。^[5]ポストは後にこの論文を1947年の「半群の単語問題は再帰的に解決不可能である」という証明の基礎として使い、^[6]後に形式言語を作成するための 標準的なシステムを考案した。

1907年、レオナルド・トーレス・ケベドはウィーンで機械図面（機械装置）の記述のための形式言語を導入した。彼は「機械の記述を容易にするための表記法と記号のシステムについて」を出版した。^[7] ハインツ・ゼマネクはそれを工作機械の数値制御のためのプログラミング言語と同等と評価した。^[8]

ノーム・チョムスキーは、チョムスキー階層として知られる形式言語と自然言語の抽象表現を考案しました。^[9] 1959年、ジョン・バッカスはFORTRANの作成に続いて、高級プログラミング言語の構文を記述するためにバッカス・ナウア形式を開発しました。^[10] ピーター・ナウアはALGOL60レポートの秘書/編集者であり、その中でバッカス・ナウア形式を使用してALGOL60の形式部分を記述しました。

形式言語の文脈では、アルファベットは任意の集合であり、その要素は文字と呼ばれます。アルファベットには無限の数の要素を含めることができます。^{[注 1]}しかし、形式言語理論のほとんどの定義では、要素の数が有限のアルファベットを指定しており、多くの結果はそれらのアルファベットにのみ適用されます。通常の意味でのアルファベット、またはより一般的にはASCIIやUnicodeなどの有限の文字エンコーディングを使用することが理にかなっていることがよくあります。

アルファベット上の単語は、任意の有限の文字のシーケンス（つまり、文字列 ）にすることができます。アルファベットΣ上のすべての単語の集合は、通常 Σ ^{* （}クリーネの星を使用）で表されます。単語の長さは、単語を構成する文字の数です。どのアルファベットでも、長さ 0 の単語は 1 つだけあります。これは空の単語で、e、ε、λ、または Λ で表されることがよくあります。連結によって、2 つの単語を組み合わせて新しい単語を作成できます。その長さは、元の単語の長さの合計です。単語と空の単語を連結した結果が、元の単語です。

一部のアプリケーション、特に論理分野では、アルファベットは語彙とも呼ばれ、単語は式または文とも呼ばれます。これにより、文字/単語のメタファーが壊れ、単語/文のメタファーに置き換えられます。

アルファベット Σ 上の形式言語LはΣ ^*のサブセット、つまりそのアルファベット上の単語の集合です。単語の集合は式にグループ化されることもありますが、規則と制約は「整形式の式」を作成するために定式化されることもあります。

通常、自然言語を扱わないコンピュータサイエンスや数学では、「形式的な」という形容詞は冗長であるとして省略されることが多い。

形式言語理論は通常、何らかの構文規則によって記述される形式言語を扱っていますが、「形式言語」という概念の実際の定義は、上記のとおり、与えられたアルファベットから構成される有限長の文字列の（おそらく無限の）集合であり、それ以上でもそれ以下でもありません。実際には、正規言語や文脈自由言語など、規則によって記述できる言語は数多くあります。形式文法の概念は、構文規則によって記述される「言語」という直感的な概念に近いかもしれません。定義を誤用すると、特定の形式言語は、それを説明する形式文法を伴うものと考えられることがよくあります。

次の規則は、アルファベット Σ = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, +, =} 上の 形式言語 Lを記述します。

• 「+」または「=」を含まず、「0」で始まらない空でない文字列はすべて Lに含まれます。
• 文字列「0」は Lにあります。
• 「=」を含む文字列が Lに含まれるのは、「=」が 1 つだけ存在し、それが Lの 2 つの有効な文字列を区切っている場合のみです。
• 「+」を含み「=」を含まない文字列が Lに含まれるのは、文字列内のすべての「+」がLの 2 つの有効な文字列を区切っている場合のみです 。
• 前の規則によって暗示される文字列以外の文字列は Lに含まれません。

これらの規則では、文字列「23+4=555」は Lに含まれますが、文字列「=234=+」は含まれません。この形式言語は、自然数、適切な加算、適切な加算等式を表現しますが、それらの見た目（構文）のみを表現し、それらの意味（意味論）は表現しません。たとえば、これらの規則のどこにも、「0」が数字のゼロを意味すること、「+」が加算を意味すること、「23+4=555」が偽であることなどを示すものはありません。

有限言語の場合、すべての整形式の単語を明示的に列挙することができます。たとえば、言語 LはL  = {a, b, ab, cba}と記述できます。この構成の退化したケースは、単語をまったく含まない空言語です( L  =  ∅ )。

ただし、Σ = {a, b} などの有限 (空でない) アルファベットでも、表現可能な有限長の単語は無限にあります: "a"、"abb"、"ababba"、"aaababbbbaab"、...。したがって、形式言語は通常無限であり、無限形式言語を記述することは、L  = {a, b, ab, cba} と記述するほど単純ではありません。形式言語の例をいくつか示します。

• L = Σ ^{* 、Σ上の}すべての単語の集合。
• L = {a} ^* = {a ⁿ }、ここでn は自然数の範囲であり、「a ⁿ」は「a」がn回繰り返されることを意味します（これは記号「a」のみで構成される単語の集合です）。
• 特定のプログラミング言語で書かれた構文的に正しいプログラムの集合（その構文は通常、文脈自由文法によって定義される）。
• 特定のチューリングマシンが停止する入力の集合。または
• この行にある英数字 ASCII文字の最大文字列の集合、つまり
  集合 {the, set, of, maximal, strings, alphanumeric, ASCII, characters, on, this, line, i, e}。

形式言語は、さまざまな分野でツールとして使用されています。しかし、形式言語理論は、特定の言語（例として扱う場合を除く）にはあまり関心がなく、主に言語を記述するためのさまざまな形式の研究に関心があります。たとえば、言語は次のように表すことができます。

• 何らかの形式文法によって生成された文字列。
• 特定の正規表現によって記述または一致する文字列。
• チューリングマシンや有限状態オートマトンなどのオートマトンによって受け入れられる文字列。
• 何らかの決定手順（一連の関連する YES/NO の質問をするアルゴリズム）によって YES という答えが生成される文字列。

このような形式主義に関してよく尋ねられる質問には次のようなものがあります。

• それらの表現力はどの程度ですか? (形式主義X は形式主義Yが記述できるすべての言語を記述できますか? 他の言語も記述できますか?)
• それらの認識可能性はどの程度ですか? (特定の単語が形式主義Xによって記述された言語に属するかどうかを判断するのはどの程度難しいですか?)
• それらの比較可能性はどの程度ですか? (形式論Xで記述された言語と形式論Yで記述された言語、または再び形式論Xで記述された言語の 2 つの言語が実際に同じ言語であるかどうかを判断するのはどの程度難しいですか?)。

驚くほど多くの場合、これらの決定問題に対する答えは「まったく実行できない」、または「非常に高価である」（どの程度高価であるかの特徴付け付き）です。したがって、形式言語理論は、計算可能性理論と複雑性理論の主要な応用分野です。形式言語は、生成文法の表現力と認識オートマトンの複雑さに基づいて、チョムスキー階層に分類できます。文脈自由文法と正規文法は、表現力と構文解析の容易さの間の適切な妥協点を提供し、実際のアプリケーションで広く使用されています。

言語に対する特定の演算は一般的です。これには、和集合、積集合、補集合などの標準的な集合演算が含まれます。別の演算クラスは、文字列演算の要素単位の適用です。

例:と が共通のアルファベット上の言語であるとします。 ${\displaystyle L_{1}}$${\displaystyle L_{2}}$${\displaystyle \Sigma }$

• 連結は 、が からの文字列であり、が からの文字列である形式のすべての文字列で構成されます。${\displaystyle L_{1}\cdot L_{2}}$${\displaystyle vw}$${\displaystyle v}$${\displaystyle L_{1}}$${\displaystyle w}$${\displaystyle L_{2}}$
• との共通部分は 、両方の言語に含まれるすべての文字列で構成されます。${\displaystyle L_{1}\cap L_{2}}$${\displaystyle L_{1}}$${\displaystyle L_{2}}$
• に関するの補集合は 、に含まれない上のすべての文字列で構成されます。${\displaystyle \neg L_{1}}$${\displaystyle L_{1}}$${\displaystyle \Sigma }$${\displaystyle \Sigma }$${\displaystyle L_{1}}$
• クリーネスター: 元の言語の 0 個以上の単語が連結されたすべての単語で構成される言語。
• 逆転：
  • εを空語とすると、${\displaystyle \varepsilon ^{R}=\varepsilon }$
  • 空でない各単語（ここではアルファベットの要素）について、${\displaystyle w=\sigma _{1}\cdots \sigma _{n}}$${\displaystyle \sigma _{1},\ldots ,\sigma _{n}}$${\displaystyle w^{R}=\sigma _{n}\cdots \sigma _{1}}$
  • 形式言語の場合、.${\displaystyle L}$${\displaystyle L^{R}=\{w^{R}\mid w\in L\}}$
• 文字列準同型

このような文字列演算は、言語のクラスの閉包特性を調べるのに使われる。言語のクラスが特定の演算の下で閉じているとは、その演算をそのクラスの言語に適用すると、常に同じクラスの言語が再び生成される場合を言う。例えば、文脈自由言語は、通常の言語との和集合、連結集合、積集合の下では閉じているが、積集合や補集合の下では閉じていないことが知られている。トリオ理論と抽象言語族理論は、言語族の最も一般的な閉包特性をそれ自体で研究する。^[11]

コンパイラには通常、2 つの異なるコンポーネントがあります。などのツールによって生成されることもある字句解析器lexは、プログラミング言語文法のトークン (識別子やキーワード、数値リテラルや文字列リテラル、句読点、演算子記号など) を識別します。これらのトークン自体は、通常は正規表現によって、より単純な形式言語で指定されます。 最も基本的な概念レベルでは、などのパーサー ジェネレーターによって生成されることもあるパーサーは、ソース プログラムが構文的に有効かどうか、つまり、コンパイラが構築されたプログラミング言語文法に関して適切に構成されているかどうかを判断しようとします。 yacc

もちろん、コンパイラはソース コードを解析するだけではありません。通常は、ソース コードを何らかの実行可能形式に変換します。このため、パーサーは通常、yes/no の回答以上のもの、通常は抽象構文木を出力します。これは、コンパイラの後続のステージで使用され、最終的にハードウェア上で直接実行されるマシン コード、または仮想マシンでの実行を必要とする中間コードを含む実行可能ファイルを生成します。

数理論理学では、形式理論とは形式言語で表現された 文の集合です。

形式体系（論理計算または論理システムとも呼ばれる）は、形式言語と演繹装置（演繹システムとも呼ばれる）から構成されます。演繹装置は、有効な推論規則として解釈できる一連の変換規則、または一連の公理、あるいはその両方から構成されます。形式体系は、1 つ以上の他の式から 1 つの式を導き出すために使用されます。形式言語はその式で識別できますが、形式体系は同様に定理で識別することはできません。2 つの形式体系とがすべて同じ定理を持ちながら、重要な証明理論的方法で異なる場合があります（たとえば、式 A は、一方においては式 B の構文上の帰結であるが、もう一方ではそうではないなど）。 ${\displaystyle {\mathcal {FS}}}$${\displaystyle {\mathcal {FS'}}}$

形式的な証明または導出は、それぞれが公理であるか、または推論規則によってシーケンス内の前の式から従う、整形式の公式 (文または命題として解釈される) の有限シーケンスです。シーケンスの最後の文は、形式システムの定理です。形式的な証明は、その定理が真の命題として解釈できるため便利です。

形式言語は本質的に完全に統語論的ですが、言語の要素に意味を与えるセマンティクスを付与することができます。たとえば、数理論理学では、特定の論理の可能な式の集合が形式言語であり、解釈によって各式に意味 (通常は真理値)が割り当てられます。

形式言語の解釈の研究は、形式意味論と呼ばれます。数理論理学では、これはモデル理論の観点から行われることが多いです。モデル理論では、式に現れる項は数学的構造内のオブジェクトとして解釈され、固定された構成的解釈規則によって、式の真理値がその項の解釈からどのように導き出されるかが決まります。式のモデルとは、式が真となるような項の解釈です。

• 言葉の組合せ論
• 形式手法
• 自由モノイド
• 文法の枠組み
• 数学表記
• 文字列（コンピュータサイエンス）

引用文献

一般的な参考文献

• 「形式言語」、数学百科事典、EMS Press、2001 [1994]
• メリーランド大学、形式言語の定義
• James Power、「形式言語理論と構文解析に関するメモ」、 Wayback Machineで 2007 年 11 月 21 日にアーカイブ、2002 年 11 月 29 日。
• 「形式言語理論ハンドブック」第 1 ～ 3 巻、G. Rozenberg および A. Salomaa (編)、Springer Verlag (1997) のいくつかの章の草稿:
  • Alexandru Mateescu および Arto Salomaa、第 1 巻の「序文」、v ～ viii 頁、および第 1 巻の第 1 章「形式言語: 序論と概要」 1、1–39ページ
  • 盛宇、「正規言語」第 1 巻第 2 章
  • Jean-Michel Autebert、Jean Berstel、Luc Boasson、「文脈自由言語とプッシュダウンオートマトン」、第 1 巻第 3 章
  • Christian Choffrut と Juhani Karhumaki、「言葉の組み合わせ論」、第 6 巻の第 6 章1
  • テロ・ハルジュとユハニ・カルフマキ、「モーフィズム」、第 7 巻第 7 章1、439～510ページ
  • Jean-Eric Pin、「統語的半群」、第 1 巻第 10 章、679 ～ 746 ページ
  • M. Crochemore と C. Hancart、「パターンマッチングのオートマトン」、第 2 巻第 9 章
  • Dora Giammarresi、Antonio Restivo、「二次元言語」、第 4 巻、第 4 章3、215–267ページ