
論理学、数学、コンピュータ科学、言語学において、形式言語とは、「アルファベット」と呼ばれる集合から記号が取られた文字列の集合のことである。
形式言語のアルファベットは、文字列(「単語」とも呼ばれる)に連結される記号から構成されます。 [ 1 ]特定の形式言語に属する単語は、整形式語と呼ばれることもあります。形式言語は、正規文法や文脈自由文法などの形式文法によって定義されることがよくあります。
コンピュータ科学において、形式言語は、とりわけプログラミング言語や制御自然言語(すなわち、自然言語の部分集合を形式化したもの)の文法を定義する基礎として用いられる。計算複雑性理論においては、決定問題は通常、形式言語として定義され、複雑性クラスは、計算能力が限られた機械でも解析可能な形式言語の集合として定義される。論理学および数学の基礎においては、形式言語は公理系の構文を表すために用いられ、数学的形式主義とは、数学のすべてをこのように形式言語の構文操作に還元できるという哲学である。
形式言語理論の分野は、主にそのような言語の純粋に統語的な側面、つまりその内部構造パターンを研究します。形式言語理論は、自然言語の統語的規則性を理解する方法として、言語学から生まれました。[ 2 ]
17世紀、ゴットフリート・ライプニッツは、象形文字を利用した普遍的で形式的な言語である「普遍的特徴」を構想し、記述した。その後、カール・フリードリヒ・ガウスはガウス符号の問題を研究した。[ 3 ]
19世紀半ば、ジョージ・ブールはブール代数の分野を確立しました。これは、真理値と集合演算子を用いて論理演算を形式的に記述する方法です。彼の著書『思考の法則の調査』の中で、彼は論理的推論が記号方程式によって表現および操作できることを示しました。[ 4 ]
ゴットロープ・フレーゲは、ライプニッツの思想を記法体系を通して実現しようと試み、その体系は最初に『概念書』(1879年)で概説され、彼の2巻からなる『算術の基本法則』(1893/1903年)でより詳細に展開された。[ 5 ]これは「純粋言語の形式言語」を記述したものである。[ 6 ]
20世紀前半には、形式言語に関連するいくつかの発展があった。アクセル・トゥーは1906年から1914年の間に、単語と言語に関する4つの論文を発表した。これらの最後の論文では、エミール・ポストが後に「トゥーシステム」と呼んだものが導入され、決定不能問題の初期の例が示された。[ 7 ]ポストは後にこの論文を基に、1947年に「半群の単語問題は再帰的に解けない」という証明を行い[ 8 ] 、後に形式言語を作成するための標準システムを考案した。
1907年、レオナルド・トーレス・ケベードはウィーンで機械図面(機械装置)の記述のための形式言語を導入した。彼は「機械の記述を容易にするための表記法と記号体系について」を出版した。[ 9 ]ハインツ・ゼマネクはこれを工作機械の数値制御のためのプログラミング言語と同等と評価した。[ 10 ]
ノーム・チョムスキーは、チョムスキー階層として知られる形式言語と自然言語の抽象的な表現を考案した。[ 11 ] 1959年、ジョン・バッカスは、 FORTRANの作成に携わった後、高水準プログラミング言語の構文を記述するためにバッカス・ナウア記法を開発した。[ 12 ]ピーター・ナウアはALGOL60レポートの秘書兼編集者であり、ALGOL60の形式部分を記述するためにバッカス・ナウア記法を使用した。
形式言語の文脈では、アルファベットは任意の集合であり、その要素は文字と呼ばれます。アルファベットは無限個の要素を含むことができますが[注1 ]、形式言語理論におけるほとんどの定義では有限個の要素を持つアルファベットが指定されており、多くの結果は有限個の要素を持つアルファベットにのみ適用されます。アルファベットを通常の意味で、あるいはより一般的にはASCIIやUnicodeなどの有限文字エンコーディングとして使用する方が理にかなっている場合が多いです。
アルファベット上の単語は、任意の有限文字列(つまり文字列)です。アルファベットΣ上のすべての単語の集合は、通常、Σ *(クリーネスターを使用)で表されます。単語の長さは、その単語を構成する文字の数です。任意のアルファベットに対して、長さが0の単語は1つだけ存在し、それは空語で、e、ε、λ、あるいはΛなどで表されます。連結によって、2つの単語を組み合わせて新しい単語を作成できます。新しい単語の長さは、元の単語の長さの合計です。単語と空語を連結した結果は、元の単語になります。
特に論理学などの分野では、アルファベットは語彙とも呼ばれ、単語は数式や文とも呼ばれます。これは文字と単語の比喩を打破し、単語と文の比喩に置き換えます。
空でない集合が与えられた場合形式言語以上は、、 どこは、上のすべての可能な有限長の単語の集合です。我々はそれをセットと呼ぶアルファベット一方、形式言語が与えられた場合以上単語整形式であるのは、同様に、表現整形式であるのは、時には、形式的な言語以上すべての可能な整った単語を作成するための明確なルールと制約のセットがあります。。
自然言語を通常扱わないコンピュータ科学や数学では、「形式的」という形容詞は冗長なため省略されることが多い。一方、「形式言語」とだけ言うこともできる。「アルファベットが文脈から明らかである。
形式言語理論は通常、何らかの構文規則によって記述される形式言語を扱いますが、「形式言語」という概念の実際の定義は、上記のとおり、与えられたアルファベットから構成される有限長の文字列の集合(場合によっては無限)に過ぎません。実際には、正規言語や文脈自由言語など、規則によって記述できる言語は数多く存在します。形式文法の概念は、構文規則によって記述される「言語」という直感的な概念により近いかもしれません。定義の誤用として、特定の形式言語には、それを記述する形式文法が付随していると考えられることがよくあります。
以下の規則は、アルファベット Σ = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, +, =}上の形式言語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} と書くほど単純ではありません。以下に、形式言語の例をいくつか示します。
形式言語は、複数の分野でツールとして使用されています。しかし、形式言語理論は、特定の言語(例として挙げる場合を除く)に関心を持つことはほとんどなく、主に言語を記述するためのさまざまな種類の形式体系の研究に関心を持っています。たとえば、言語は次のように表すことができます。
こうした形式主義に関してよく聞かれる質問には、以下のようなものがある。
驚くべきことに、これらの決定問題に対する答えは「全く不可能」または「非常にコストがかかる」(そのコストの程度を示す)であることが非常に多い。そのため、形式言語理論は計算可能性理論と複雑性理論の主要な応用分野となっている。形式言語は、生成文法の表現力と認識オートマトン(自動機械)の複雑さに基づいて、チョムスキー階層に分類することができる。文脈自由文法と正規文法は、表現力と構文解析の容易さの間の良い妥協点を提供し、実用的なアプリケーションで広く使用されている。
メタ構文とは、プログラミング言語または形式言語の構文を定義するために使用される構文です。メタ構文は、自然言語またはコンピュータプログラミング言語のいずれかを記述するために使用されるメタ言語の句と文の許容される構造と構成を記述します。[ 13 ]コンピュータ言語で広く使用されている形式メタ言語には、バッカス・ナウア記法(BNF)、拡張バッカス・ナウア記法(EBNF)、ワース構文記法(WSN)、拡張バッカス・ナウア記法(ABNF)などがあります。
メタ言語はそれぞれ独自のメタ構文を持ち、各メタ構文は終端記号、非終端記号、およびメタ記号から構成されます。単語やトークンなどの終端記号は、定義される言語における独立した構造です。非終端記号は構文カテゴリを表し、n個の要素からなる部分集合で構成される1つ以上の有効な句構造または文構造を定義します。メタ記号は、特定のメタ構文において、指示的な目的のための構文情報を提供します。終端記号、非終端記号、およびメタ記号は、すべてのメタ言語に共通して適用されるわけではありません。
一般的に、トークンレベル言語(正式には「正規言語」と呼ばれる)のメタ言語には非終端記号がありません。これは、これらの正規言語ではネストが問題にならないためです。特定の言語を記述するためのメタ言語である英語にはメタシンボルは含まれていません。これは、すべての説明を英語の表現で行うことができるためです。再帰言語(正式には文脈自由言語と呼ばれる)を記述するために使用される特定の形式的なメタ言語のみが、メタ構文に終端記号、非終端記号、およびメタシンボルを含んでいます。
言語に対する操作には、いくつかの共通するものがあります。これには、和集合、積集合、補集合といった標準的な集合演算が含まれます。また、文字列演算を要素ごとに適用する操作も、一般的な操作の一つです。
例:そして共通のアルファベット上の言語である。
このような文字列操作は、言語クラスの閉包特性を調査するために使用されます。言語クラスは、そのクラス内の言語に操作を適用すると、常に同じクラスの言語が再び生成される場合、特定の操作に関して閉じていると言えます。たとえば、文脈自由言語は、正規言語との和集合、連結、および積集合に関して閉じていることが知られていますが、積集合や補集合に関しては閉じていません。トリオ理論と抽象言語族理論は、言語族の最も一般的な閉包特性をそれ自体で研究します。[ 14 ]
コンパイラは通常、2つの異なるコンポーネントから構成されます。字句解析器は、場合によってはなどのツールによって生成されlex、プログラミング言語の文法のトークン(識別子やキーワード、数値リテラルや文字列リテラル、句読点、演算子記号など)を識別します。これらのトークン自体は、通常、正規表現を用いて、より単純な形式言語によって指定されます。最も基本的な概念レベルでは、構文解析器は、場合によってはなどの構文解析器生成器によって生成され、yaccソースプログラムが構文的に有効かどうか、つまり、コンパイラが構築されたプログラミング言語の文法に関して整形式であるかどうかを判定しようとします。
もちろん、コンパイラはソースコードを解析するだけでなく、通常は実行可能な形式に変換します。そのため、パーサーは通常、イエス/ノーの回答だけでなく、抽象構文木などの出力を生成します。これは、コンパイラの後続の段階で使用され、最終的にハードウェア上で直接実行されるマシンコード、または仮想マシンでの実行を必要とする中間コードを含む実行可能ファイルが生成されます。

数理論理学において、形式理論とは、形式言語で表現された一連の文のことである。
形式体系(論理計算、または論理システムとも呼ばれる)は、形式言語と演繹装置(演繹システムとも呼ばれる)から構成される。演繹装置は、有効な推論規則として解釈できる変換規則の集合、公理の集合、またはその両方から構成される。形式体系は、1つ以上の他の式から1つの式を導出するために使用される。形式言語はその式によって識別できるが、形式体系は同様にその定理によって識別することはできない。2つの形式体系そして同じ定理をすべて含んでいても、証明論的に重要な点で異なる場合がある(例えば、ある式Aは、ある式Bの構文上の帰結であるが、別の式Bではそうではない)。
形式的な証明または導出とは、整形式な式(文または命題と解釈できる)の有限列であり、各式は公理であるか、または推論規則によって列内の先行する式から導かれる。列の最後の文は、形式体系の定理である。形式的な証明は、その定理が真の命題として解釈できるため有用である。
形式言語は本質的には構文的なものですが、言語の要素に意味を与える意味論を付与することができます。例えば、数理論理学では、特定の論理式の可能な式の集合が形式言語であり、解釈によって各式に意味(通常は真偽値)が割り当てられます。
形式言語の解釈を研究する学問は、形式意味論と呼ばれます。数理論理学では、これはしばしばモデル理論を用いて行われます。モデル理論では、式に含まれる項は数学的構造内の対象として解釈され、固定された構成的解釈規則によって、式の項の解釈から式の真偽値をどのように導き出すかが決定されます。式のモデルとは、式が真となるような項の解釈のことです。
アルファベットは有限集合である。