形式文法是形式語言理論中的基本概念，它提供了一種方法來描述和分析字元串的集合。形式文法被嚴格定義為四元組G=(N,Σ,P,S)，其中：
N是非終結符的集合。
Σ是終結符的集合，且N和Σ是互斥的。
P是產生式的集合，每個產生式具有形式α→β，其中α和β是包含非終結符和終結符的字串，α至少包含一個非終結符。
S是文法的開始符號，屬於N。
形式文法產生的語言是由開始符號S推導出來的所有終結符號串的集合，這些字元串可以通過不斷套用產生式規則來獲得。基於產生式的特點和限制，形式文法可以分為不同的類型，包括0型（無限制文法）、1型（上下文有關文法）、2型（上下文無關文法）和3型（正則文法），這些類型的文法在複雜性上依次降低，它們分別對應於不同的計算模型和語言類，如0型文法對應於圖靈機，1型文法對應於非確定型線性有界自動機，2型文法對應於非確定下推自動機，而3型文法則被有限狀態自動機接受。
這些不同類型的文法為形式語言理論提供了重要的工具，用於分析和分類各種語言。每種類型的文法都有其特定的套用場景和研究價值。