语言的形式定义
http://zh.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E8%AF%AD%E8%A8%80
字母表 Σ 为任意有限集合，ε 表示空串， 记 为{ε}，全体长度为 n 的字串为， 为， 语言 L 定义为的任意子集。
注记： 的空子集 ∅ 与 {ε} 是两个不同的语言。
语言间的运算
语言间的运算就是 Σ*幂集上的运算。
- 字符串集合的交并补等运算。
- 连接运算：L1L2 = { xy | x 属于L1并且 y 属于L2 }。
- 幂运算：Ln = L … L （共 n 个 L 连接在一起），L0 = {ε}。
- 闭包运算：L* = L0∪L1∪…∪Ln∪…。
- 右商运算：L1/L2 = {x | 存在 y 属于L2使得 xy 属于L1}。
- 设 S ⊆ Σ* 是一个语言，S 的补语言定义为集合 {ω | ω ∈ Σ* 且 ω ∉ S}
语言的表示方法
一个形式语言可以通过多种方法来限定自身，比如：
在数学、逻辑和计算机科学中，形式语言（英语：Formal language）是用精确的数学或机器可处理的公式定义的语言。
文法的分类
http://zh.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E6%96%87%E6%B3%95#.E4.BE.8B.E5.AD.90
某些类型的文法及其产生的语言得到了细致的研究并被单独命名。最常见的文法的分类系统是诺姆·乔姆斯基于1956年发展的乔姆斯基谱系，这个分类谱系把所有的文法分成四种类型：无限制文法、上下文相关文法、上下文无关文法和正规文法。四类文法对应的语言类分别是递归可枚举语言、上下文相关语言、上下文无关语言和正规语言。这四种文法类型依次拥有越来越严格的产生式规则，同时文法所能表达的语言也越来越少。尽管表达能力比无限制文法和上下文相关文法要弱，但由于能高效率的实现，四类文法中最重要的是上下文无关文法和正规文法。例如对上下文无关语言存在算法可以生成高效率的LL分析器和LR分析器。
乔姆斯基体系是刻画形式文法表达能力的一个分类谱系，是由诺姆·乔姆斯基于1956年提出的。它包括四个层次：
- 0-型文法（无限制文法或短语结构文法）包括所有的文法。该类型的文法能够产生所有可被图灵机识别的语言。可被图灵机识别的语言是指能够使图灵机停机的字串，这类语言又被称为递归可枚举语言。注意递归可枚举语言与递归语言的区别，后者是前者的一个真子集，是能够被一个总停机的图灵机判定的语言。
- 1-型文法（上下文相关文法）生成上下文相关语言。这种文法的产生式规则取如 αAβ -> αγβ 一样的形式。这里的A 是非终结符号，而 α, β 和 γ 是包含非终结符号与终结符号的字串；α, β 可以是空串，但 γ 必须不能是空串；这种文法也可以包含规则 S->ε ，但此时文法的任何产生式规则都不能在右侧包含 S 。这种文法规定的语言可以被线性有界非确定图灵机接受。
- 2-型文法生成上下文无关语言。这种文法的产生式规则取如 A -> γ 一样的形式。这里的A 是非终结符号，γ 是包含非终结符号与终结符号的字串。这种文法规定的语言可以被非确定下推自动机接受。上下文无关语言为大多数程序设计语言的语法提供了理论基础。
- 3-型文法（正规文法）生成正规语言。这种文法要求产生式的左侧只能包含一个非终结符号，产生式的右侧只能是空串、一个终结符号或者一个非终结符号后随一个终结符号；如果所有产生式的右侧都不含初始符号 S ，规则 S -> ε 也允许出现。这种文法规定的语言可以被有限状态自动机接受，也可以通过正则表达式来获得。正规语言通常用来定义检索模式或者程序设计语言中的词法结构。
正规语言类包含于上下文无关语言类，上下文无关语言类包含于上下文相关语言类，上下文相关语言类包含于递归可枚举语言类。这里的包含都是集合的真包含关系，也就是说：存在递归可枚举语言不属于上下文相关语言类，存在上下文相关语言不属于上下文无关语言类，存在上下文无关语言不属于正规语言类。
下表总结了上述四种类型的文法的主要特点：
| 文法 | 语言 | 自动机 | 产生式规则 |
| 0-型 | 递归可枚举语言 | 图灵机 | 无限制 |
| 1-型 | 上下文相关语言 | 线性有界非确定图灵机 | αAβ -> αγβ |
| 2-型 | 上下文无关语言 | 非确定下推自动机 | A -> γ |
| 3-型 | 正规语言 | 有限状态自动机 | A -> aBA -> a |
自动机或自动机器（英语：Automaton，复数：Automata）是种能够自己运作的机器或机器人。
图灵机（英语：Turing machine），又称确定型图灵机，是英国数学家阿兰·图灵于1936年提出的一种抽象计算模型，其更抽象的意义为一种数学逻辑机，可以看作等价于任何有限逻辑数学过程的终极强大逻辑机器。
其它等价的计算模型ü
除了图灵机以外，人们还发明了很多其它的计算模型。包括：
巴科斯范式（英语：Backus Normal Form，缩写为 BNF），又称为巴科斯-诺尔范式（英语：Backus-Naur Form，也译为巴科斯-瑙尔范式、巴克斯-诺尔范式），是一种用于表示上下文无关文法的语言，上下文无关文法描述了一类形式语言。它是由约翰·巴科斯（John Backus）和彼得·诺尔（Peter Naur）首先引入的用来描述计算机语言语法的符号集。
尽管巴科斯范式也能表示一部分自然语言的语法，它还是更广泛地使用于程序设计语言、指令集、通信协议的语法表示中。大多数程序设计语言或者形式语义方面的教科书都采用巴科斯范式。在各种文献中还存在巴科斯范式的一些变体，如扩展巴科斯范式 EBNF 或扩充巴科斯范式 ABNF。
