以下内容主要来自维基百科
形式科学是指主要研究对象为抽象形态的科学，如逻辑、数学、计算理论、信息论、统计学等。
专门研究语言的语法的数学和计算机科学分支叫做形式语言理论，它只研究语言的语法而不致力于它的语义。
在计算机科学中，形式语言是：某个字母表上，一些有限长字串的集合，而形式文法是描述这个集合的一种方法。形式文法之所以这样命名，是因为它与人类自然语言中的文法相似的缘故。
形式文法描述形式语言的基本想法是，从一个特殊的初始符合出发，不断的应用一些产生式规则，从而生成出一个字串的集合。产生式规则指定了某些符号组合如何被另外一些符号组合替换。举例来说，假设字母表只包含 'a' 和 'b' 两个字符，初始符号是 'S' ，我们应用下述规则：
1. S -> aSb
2. S -> ba
于是我们可以通过把 "S" 重写为 "aSb"（规则1），我们还可以继续应用这条规则把 "aSb" 重写为 "aaSbb"。这个重写的过程不断重复，直到结果中只包含字母表中的字母为止。在例子中，我们可以得到 S -> aSb -> aaSbb -> aababb 这样的结果。由文法刻画的语言，包含了所有可以这样产生的字串，比如 ba, abab, aababb, aaababbb 等等。
一个形式文法 G 是下述元素构成的一个四元组(N, Σ, P, S)：
- “非终结符号”集合 N。
- “终结符号”集合 Σ ，Σ 与 N 无交。
- 取如下形式的一组“产生式规则” P，
- (Σ ∪ N)*中的字符串 → (Σ ∪ N)* 中的字符串，并且产生式左侧的字符串中必须至少包括一个非终结符号。
- “起始符号”S，S 属于 N。
一个由形式文法 G = (N, Σ, P, S) 产生的语言是所有如下形式的字符串集合，这些字符串全部由“终结符号”集 Σ 中符号构成，并且可以从“初始符号”S 出发，不断应用 P 中的“产生式规则”而得到。
乔姆斯基体系(Chomsky)是刻画形式文法表达能力的一个分类谱系，是由诺姆·乔姆斯基于1956年提出的。它包括四个层次：
- 0-型文法（无限制文法或短语结构文法）包括所有的文法。该类型的文法能够产生所有可被图灵机识别的语言。可被图灵机识别的语言是指能够使图灵机停机的字串，这类语言又被称为递归可枚举语言。注意递归可枚举语言与递归语言的区别，后者是前者的一个真子集，是能够被一个总停机的图灵机判定的语言。
- 1-型文法（上下文相关文法）生成上下文相关语言。这种文法的产生式规则取如 αAβ -> αγβ 一样的形式。这里的A 是非终结符号，而 α, β 和 γ 是包含非终结符号与终结符号的字串；α, β 可以是空串，但 γ 必须不能是空串；这种文法也可以包含规则 S->ε ，但此时文法的任何产生式规则都不能在右侧包含 S 。这种文法规定的语言可以被线性有界非确定图灵机接受。
- 2-型文法生成上下文无关语言。这种文法的产生式规则取如 A -> γ 一样的形式。这里的A 是非终结符号，γ 是包含非终结符号与终结符号的字串。这种文法规定的语言可以被非确定下推自动机接受。上下文无关语言为大多数程序设计语言的语法提供了理论基础。
- 3-型文法（正规文法）生成正规语言。这种文法要求产生式的左侧只能包含一个非终结符号，产生式的右侧只能是空串、一个终结符号或者一个非终结符号后随一个终结符号；如果所有产生式的右侧都不含初始符号 S ，规则 S -> ε 也允许出现。这种文法规定的语言可以被有限状态自动机接受，也可以通过正则表达式来获得。正规语言通常用来定义检索模式或者程序设计语言中的词法结构。
正规语言类包含于上下文无关语言类，上下文无关语言类包含于上下文相关语言类，上下文相关语言类包含于递归可枚举语言类。这里的包含都是集合的真包含关系，也就是说：存在递归可枚举语言不属于上下文相关语言类，存在上下文相关语言不属于上下文无关语言类，存在上下文无关语言不属于正规语言类。
下表总结了上述四种类型的文法的主要特点：
| 文法 | 语言 | 自动机 | 产生式规则 |
|---|---|---|---|
| 0-型 | 递归可枚举语言 | 图灵机 | 无限制 |
| 1-型 | 上下文相关语言 | 线性有界非确定图灵机 | αAβ -> αγβ |
| 2-型 | 上下文无关语言 | 非确定下推自动机 | A -> γ |
| 3-型 | 正规语言 | 有限状态自动机 | A -> aB A -> a |
0型文法
设G=（VN，VT，P，S），如果它的每个产生式α→β是这样一种结构：α∈(VN∪VT)*且至少含有一个非终结符，而β∈(VN∪VT)*，则G是一个0型文法。0型文法也称短语文法。一个非常重要的理论结果是：0型文法的能力相当于图灵机(Turing)。或者说，任何0型文语言都是递归可枚举的，反之，递归可枚举集必定是一个0型语言。0型文法是这几类文法中，限制最少的一个。
1型文法
1型文法也叫上下文有关文法，此文法对应于线性有界自动机。它是在0型文法的基础上每一个α→β,都有|β|>=|α|。这里的|β|表示的是β的长度。
注意：虽然要求|β|>=|α|，但有一特例：α→ε也满足1型文法。
如有A->Ba则|β|=2,|α|=1符合1型文法要求。反之,如aA->a，则不符合1型文法。
2型文法
2型文法也叫上下文无关文法，它对应于下推自动机。2型文法是在1型文法的基础上,再满足：每一个α→β都有α是非终结符。如A->Ba,符合2型文法要求。
如Ab->Bab虽然符合1型文法要求,但不符合2型文法要求，因为其α=Ab，而Ab不是一个非终结符。
3型文法
3型文法也叫正规文法，它对应于有限状态自动机。它是在2型文法的基础上满足:A→α|αB（右线性）或A→α|Bα（左线性）。
如有：A->a,A->aB,B->a,B->cB，则符合3型文法的要求。
但如果推导为:A->ab,A->aB,B->a,B->cB或推导为:A->a,A->Ba,B->a,B->cB则不符合3型方法的要求了。
具体的说，例子A->ab,A->aB,B->a,B->cB中的A->ab不符合3型文法的定义,如果把后面的ab,改成“一个非终结符＋一个终结符”的形式（即为aB）就对了。例子A->a,A->Ba,B->a,B->cB中如果把B->cB改为B->Bc的形式就对了,因为A→α|αB（右线性）和A→α|Bα（左线性）两套规则不能同时出现在一个语法中,只能完全满足其中的一个,才能算3型文法。
注意：上面例子中的大写字母表示的是非终结符,而小写字母表示的是终结符。
扩展巴科斯-瑙尔范式(EBNF)是表达作为描述计算机编程语言和形式语言的正规方式的上下文无关文法的元语法符号表示法。它是基本巴科斯范式(BNF)元语法符号表示法的一种扩展。