标签：总结 语法 断言 PFPL rule judgement 表达式 Gamma
总结形式化语言的相关概念。源自于教材Practical Foundations for Programming Languages。这个总结作为辅助阅读资料，无法代替教材本身。
Chapter1: Abstract Syntax
抽象语法。用树状结构表达。书中的内容不关注具体的语法，仅仅关注语法片段（句法）对应的树，以及树中的标识符（类似于变量）的绑定关系（类似于变量的赋值）。这本书主要关注语法的结构化信息，对于语法最后是如何用字符串表达的并不关心。
abstract syntax tree。 抽象语法树，经常用\(a\)表示。叶子被称作variables，非叶节点（内部节点）被称作operators。
sort。语法树的类型。不同类型的语法树对应不同形式的语法。比如SQL语句和一般的C++编程是用的不同的语法。经常用\(s\)表示。经常用\(S\)表示sort的集合。
variable。未指定的或者通用的语法片段。一个未知的占位符，其具体的含义与其替代者有关。经常用\(x\)表示。用\(\chi\)表示集合。用\(\chi_s\)表示对应类型的所有变量的集合。我们可以使用\(A[\chi]=\{A[\chi]_{s \in S}\}\)来代表类型为\(s\)的语法树，这个语法树中的变量是类型\(s\)的、以及所有operator在连接不同子树之后也是类型\(s\)的。当然，也可以使用\(A[\chi_{1}, \chi_{2}]\)来并联多个集合。
operator。语法树的内部（非叶）节点。通常使用\(o\)来表示。\(O\)用来表示operator的集合。其子节点被称作argument（参数）。其内部包含一个叫做arity的概念来表达operator及其参数的类型。用\(o(a_1;...;a_n)\)代表一个包含了语法树\(a_1\)到\(a_n\)作为子节点的operator。
arity。元数。一般用变量\(\alpha\)表示。其完整表示为\((s_1,...,s_n)s\)，其代表对应的operator为类型\(s\)，带有\(n\)个参数（子节点），每个参数的类型为\(s_1\)到\(s_n\)。通过将arity考虑在内。我们可以使用\(O_\alpha\)来表示相同arity的operator的集合。
structural induction。结构归纳。 如果要证明语法树\(a\)满足某一个属性\(P\)，即\(P(a)\)。我们只需要证明1）\(a\)中所有的变量\(x\)满足属性\(P\)；2）每一个operator在连接了其子树（参数）之后所形成的新 抽象语法树也满足属性\(P\)。在全局不明朗，变量替代关系复杂的树状结构中，结构归纳只证明小的单元，然后推广至全局的方法来证明语法树的性质。
substitution。替代。用一个语法片段去代替语法树中的一个变量。\([b/x]a\)代表用语法树b替代语法树\(a\)中所有命名为\(x\)的变量。
abstrast binding tree。抽象绑定树。解决变量的作用域问题。在语法片段中，如果变量\(x\)特指是语法树\(a\)中的\(x\)，需要将变量写成\(x.a\)。这是相对于abstract syntax tree唯一的区别。这是x被称作绑定变量（减occur free）。抽象绑定树可以用于表达函数式编程、匿名函数和lambda文法。在文法中，函数的声明和函数调用可能出现在一行代码中。这时绑定变量就更像是匿名函数的形参和局部变量，这些绑定变量是不会在匿名函数外面被替换和赋值的。
abstractor。抽象绑定树相比抽象树，加入的新语法。即abstract binding tree中的operator中的argument的新名字。使用\(x_1,...,x_n.a\)表达绑定在语法树\(a\)中的变量\(x_1\)到\(x_n\)，变量可以进一步写成向量\(\vec{x}.a\)来简介表达。从此之后，operator的子节点变成了abstractor。abstractor感觉像匿名函数的声明。
generalized arity。广义的元数。扩大了arity的原始定义。表示为\((v_1,...,v_n)s\)。其中\(s\)为operator的类型，\(v\)是valence，直译是化合价的意思，代表一个语法抽象树（原子）和其绑定的变量（化学键）。\(v\)可以进一步表达为\(s_1,...s_n.s\)和\(\vec{s}.s\)，其中s是argument（连在operator下面的一个小语法树）的类型，\(s_1\)到\(s_n\)是每一个绑定的变量的类型。
fresh renaming。重命名操作。在抽象绑定树中存在嵌套关系，即一个抽象绑定树是另外一个抽象绑定树的子树。如果这个时候两个层次的抽象绑定树的绑定变量的名字是一样的，会造成歧义，故需要引入重命名，让其中一个语法树的绑定变量的名字错开。
\(\alpha\)-equivalent。\(\alpha\)等价。如果两个abt可以通过改变变量名来使得二者完全相同，那么这两个abt被称作\(\alpha\)等价。
occur free。一个变量如果在一个abstractor中是occur free的，代表这一变量是可以被替换（substitution）的。但是如果一个变量是被绑定的，那它就是不能被替换的。这里涉及到自由变量和绑定变量的区别维基百科---自由变量与绑定变量。简单来说，绑定变量是一种形式上的变量，可以类比于编程语言中函数声明中的形参和函数内的局部变量。这种变量本质上是被固定在了一个作用域中，用以介绍一段逻辑，外部的赋值不会影响到函数内部。自由变量是真正的、实际的变量，可以被替换（在编程语言中称为赋值），可以理解为编程语言中的全局变量。
symbolic parameter（symbol）。符号参数。抽象语法并不在任何时候都包含固定的operator。有时，一个operator是否可用与当前语法的上下文有关。我们使用symbolic parameter，或者symbol来表示operator的集合的索引，只有symbolic parameter是活跃的，对应的那些operator才是可用的，用\(u\)表示，用\(U\)代表symbol的集合。\(o[u]\)表示与symbol \(u\)对应的operator \(o\)。语法绑定树的定义可以进一步扩展，用\(B[U;\chi]\)代表语法绑定树的集合，包含了符号集合\(U\)和变量集合\(\chi\)。与variable（变量）一样，symbol也支持绑定到一定的语法树中，比如abstractor \(u.a\)。symbol和variable在重命名上是完全一致的，只要不产生新的冲突，但是除此之外，symbol就有所不同，symbol不是一个占位符，不能被替换。
Chapter 2: Inductive Definitions
归纳定义。一种编程语言的基本工具。用递归的方式来做出定义。structural induction是一种特殊的归纳定义。
judgment。判断，也被称作assertion，断言。judgement是一种对于语法树性质和多个语法树关系的描述。
judgement form。判断形式，也称作谓词predicate。判断中的性质与关系。用\(J\)去表示。谓词是归纳定义的定义对象。
instance of judgement form。谓词的实例，也就是谓词加上主语subjects。主语表达了性质与关系所作用的对象。使用\(a\ J\)或者\(J\ a\)代表语法（绑定）树满足谓词\(J\)。有时候如果主语暂时缺席，那就变成\(-\ J\)或者\(J\ -\)用一个占位符来代替。在有些语境下主语并不重要，这个时候可以直接使用\(J\)来表达整个断言。
rule。规则。写成\(\frac{J_1,...,J_k}{J}\)的形式，上面的断言是被称作rule的前提premise，下面的被称作rule的结论conclusion。读作前提对于结果是充分的sufficient。如果一个rule没有前提，那么其就被称作公理axiom。对于某一个谓词inductive definitions由一系列的rule构成。rule的集合一般写做\(R\)。
iff。当且仅当。iff会连接两个断言，代表二者之间是相互推导，充分必要的关系。
rule scheme。规则族。rule中的judgement的主语有时是一个变量，因为变量可以无限地被替换。带有变量的rule本质上是一堆rule的集合，称为规则族，对于主语的不同的、具体的替换构成规则族的一个实例，也就是规则。
derivation。推导。证明一个judgement有效的过程。推导过程从公理开始，通过连接不同rule的前提和结论，最终在推导过程的尾部案得到某一个judgement。一般用符号\(\nabla\)来表示。
closed under。闭包。一个在不同领域有不同具体含义的概念。如果一个judgement可以通过一系列给定rule来推导得出，那么我们就可以说这个judgement闭包于这些rule。closed under说明了rule对于judgement的推导是充分的，即通过给定的rule可以找到一种方式来证明judgement的有效性。可以用拓扑学和集合论和角度来解释闭包这个概念。通过组合rule可以得到很多的推理路径（有向图），这些路径中节点是judgement，边是rule（边的起点是premise，终点是conclusion）。那么通过组合各种各样的rule可以得到命题的集合，如果一个judgement包含在所有rule的合理组合而形成的图中，那么这个judgement就是这些rule的一个闭包。
strongest judgement。强断言。是一种相比闭包更为严格的条件。如果一个judgement闭包与给定的rule，并且能且只能由给定的rule推导得出，那么就可以将其称为闭包于给定rule的strongest judgement。这些rule对于strongest judgement的推导是必要的。
rule induction。规则归纳。归纳定义（inductive definition）的一种方式。规则归纳出现在我们要推理的judgement（所定义的性质）既是一推rule要推理的目标，又存在于这些rule的前提之中。所谓”我推理我自己“。数学归纳法就是一个规则归纳，即通常中一个基础的对象对应的断言出发，然后通过加入一个假设（归纳假设），扩展到整个值域。rule induction必须保证judgement是strongest judgment。PFPL在为什么要strongest judgment，没说明原因。我猜测只有strongest judgment才能保证对于一个推理的路径是唯一的，从而使得归纳过程可以无限递归下去。或者如果在前提中包含了目标judgement的rule集合不是唯一的推理路径，那么可能使用普通的、不递归的其他方式也可以推理出目标judgement，rule induction就不是必须的。
Chapter 3: Hypothetical and General Judgements
这一章节包含了两种进阶的断言。与Chapter 2介绍的judgement不同（这一章将这类断言称作basic judgement），Chapter 3中的断言更像是“断言的断言”，与之前的以语法树为对象的断言不同，这一章的断言的对象也是断言。这一章的两种断言，一个是hypothetical judgement，研究的是假设与可推理性，还有可接受性。另外一种断言是general judgment，研究的是断言的变量（见variable的概念）的不同重命名和替换以及断言的符号参数（见symbolic parameter的概念）的重命名对于断言有效性的影响。此外，这一章还给出了两种进阶的断言对应的rule和rule induction（归纳定义）。
derivability judgement。可推导性断言，假设性断言的一种。这类断言可以表达为\(J_1,...,J_k\vdash_RK\)。其中\(J\)和\(K\)都代表断言，\(J\)可以进一步称为假设（hypothesis），可以用符号\(\Gamma\)和\(\triangle\)代表所有假设的集合。\(R\)代表规则的集合。\(\vdash\)是可推导的意思，可以不带假设，单独使用\(\vdash_R\Gamma\)表示，代表\(R\)中的规则可以推导出\(\Gamma\)中所有的judgement。这个断言可以表达为本质相同的四种意思：
- 假设所有的\(J\)都成立，进一步利用\(R\)中的规则可以推导出\(K\)；
- 将\(J_1,...,J_k\)全部视为公理\(\frac{}{J_1},...,\frac{}{J_k}\)，那么可以依据\(R\)中的rule和这些公理，即\(R\cup\frac{}{J_1},...,\frac{}{J_k}\)，找到一条使\(K\)成立的推导（\(\vdash_{R\cup\frac{}{J_1},...,\frac{}{J_k}}K\)）。这一解释可以帮助我们理解derivability judgement的一系列性质。
- 规则\(\frac{J_1,...,J_k}{K}\)可以推导自\(R\)中的规则。
stability of derivability judgement。可推导性断言的稳定性。扩展可推导性断言中的规则集合不会影响可推导性断言的有效性。如果\(\Gamma\vdash_RJ\)，那么\(\Gamma\vdash_{R\cup R'}J\)。
reflexivity of derivability judgement。可推导性断言的反射性。每个（假设中的）断言都是自身的结论，这个很好理解。即\(\Gamma,J\vdash_RJ\)。
weakening of derivability judgement。可推导性断言的弱化。增加的额外假设，不影响可推导性。即若\(\Gamma\vdash_RJ\)成立，\(\Gamma,K\vdash_RJ\)也成立。\(K\)为额外增加的假设。
transitivity of derivability judgement。可推导性断言的传递性。如果假设中的一部分断言可以从另外的假设和规则集合\(R\)中推导出来，那么这部分断言是可以忽略的。即如果\(\Gamma,K\vdash_RJ\)并且\(\Gamma\vdash_RK\)，那么\(\Gamma\vdash_RJ\)。\(K\)能被剩下的部分假设\(\Gamma\)以及规则\(R\)推导出来，所以\(K\)可以被忽略。
admissibility judgement。可接纳性断言，另一种假设性断言。如果规则可以推导出某些judgement，那么也一定能推导出另外的judgement。表达为\(\Gamma\models_RJ\)。有本质相同的两种意思：
- 假设（如果）\(\vdash_R\Gamma\)成立，那么\(\vdash_RJ\)也成立。
- 设\(\Gamma\)中的断言为\(J_1,...,J_n\)。那么\(\frac{J_1,...,J_n}{J}\)相对于\(R\)是可接受（admissible）的。如果可以推出前期，那么结论也一定是成立的。
如果假设\(\Gamma\)中的断言实际上没法被\(R\)中的规则推导出来，那么这个admissibility judgement只能说是“虚真的”（vacuously true）。admissibility judgement能够成立通常是因为\(R\)对于断言假设的推理路径可以“经过”可接纳性断言的结论。admissibility是一种比derivability更宽松的断言，有时候\(\Gamma\vdash_RJ\)不成立，但是\(\Gamma\models_RJ\)是成立的。
no stability of admissibility judgement。可接受性断言的不稳定性。扩展可接受断言的rule集合\(R\)并不能保证可接受性断言的继续成立。因为新加入的规则会改变\(R\)对于断言假设推理路径，从而反而使得可接受性断言不成立。但是如果扩展的rule相对于\(R\)是可接受（admissible）的，那么这个rule的扩展就不影响admissibility judgement的有效性。因为此时R对于rule前提的推导是经过rule的结论的。rule的扩展相当于在R原来的推理路径上加上“回头路”，不影响原本推理路径所经过的断言，也就不影响可接受性断言本身。
reflexivity of admissibility judgement。可接受性断言的反射性。如果假设相对于\(R\)是可推导的，那么显而易见，与假设相同的结论也是可推导的。即\(J\models_RJ\)。
weakening of admissibility judgement。可接受性断言的弱化。增加断言的假设不影响断言是否成立。即如果\(\Gamma\models_RJ\)那么\(\Gamma,K\models_RJ\)。新增加的假设不影响对于原来假设的推理路径，也就不影响推理路径经过断言\(J\)。
transitivity of admissibility judgement。可接受性断言的传递性。如果一部分假设相对于剩余的假设和rule集合是可接受的，那么这部分假设可以不需要。即如果\(\Gamma,K\models_RJ\)并且\(\Gamma\models_RK\)，那么\(\Gamma\models_RJ\)。如果\(K\)已经在\(R\)对于\(\Gamma\)的推理路径中经过了，那就不需要再做出假设了。
formal derivability judgement。形式可推导断言。代表两组断言之间存在可以推导的关系，但是不关心具体是怎么推导的。即\(\Gamma\vdash J\)，代表存在某种方式使得\(\Gamma\)中的judgement可以推导出\(J\)中的judgement。这一概念为derivability judgement多了一种解释：\(\Gamma\vdash_RJ\)代表了形式可推导断言\(\Gamma\vdash J\)可以推导自规则集合\(R\)。
hypothetical rule。假设规则。在premise和conclusion中包含formal derivability judgement的规则：
\[\frac{\Gamma\Gamma_1\vdash J_1 \ ... \ \Gamma\Gamma_n\vdash J_n}{\Gamma\vdash J} \]其中\(\Gamma\)被称作全局假设（global hypothesis），\(\Gamma_1,...,\Gamma_n\)，称作对应前提的局部假设（local hypothesis）。与basic judgement的推导一样，formal derivability judgement的证明会依赖假设规则集合\(R\)来做出推理。因为这里是假设断言的范畴，所以形式可推导断言的证明除了依赖于\(R\)还会依赖于derivability judgement的性质（见derivability judgement部分的介绍）。此外，一般来说，可以规定在\(R\)中的所有rule的全局假设是统一的。故假设规则可以简化为更局部的形式：
\[\frac{\Gamma_1\vdash J_1 \ ... \ \Gamma_n\vdash J_n}{J} \]hypothetical rule induction。假设规则归纳，由一系列rule对于形式可推导断言某一性质的定义\(P(\Gamma\vdash J)\)（猜测可能是形式可推导断言中的语法树的性质）。与之前rule induction所表达的归纳定义是一个意思。都是为了某一性质在rule前提与假设之间的传递。在假设规则中，具体说，如果\(P(\Gamma\Gamma_1\vdash J_1),...,P(\Gamma\Gamma_n\vdash J_n)\)都被满足，那么\(P(\Gamma\vdash J)\)也能被满足。在此基础上，就可以进行归纳定义。
uniformity of rules。rule的一致性。集合\(R\)中的rule如果是满足一致性的，那么其中任意一个rule中的变量和symbol被重命名、被替换所产生的rule也被包含在\(R\)中。
general derivability judgement。一般性可推导断言。关注断言中的语法树的variable的renaming和substitution以及symbolic parameter的renaming对于可推导性的影响（详见Chapter 1）。用符号\(\Gamma\vdash_{R}^{U;\chi}J\)来代表\(\Gamma\)可以通过规则集\(R\)推导出\(J\)。在这一可推导性断言中的所有variable包含集合\(\chi\)中，所有的symbol包含在集合\(U\)中。对于一个一般性可推导断言，如果有可推导性断言\(\Gamma\vdash_{R}^{\chi\ Y}J\)，\(\chi\)和\(Y\)都是变量的集合，其中\(Y\)中都是可以随意命名和替换的变量，那么一般性可推导断言可以将“自由”的变量放到外面去。\(Y|\Gamma\vdash_R^\chi J\)，代表Y中的变量无论怎么赋值和重命名，都不改变可推导性。此外这里要求\(R\)中的规则是满足uniformity的。当然，symbolic parameter的重命名也是一样的。可以用双杠放在更前面来表示：\(V||Y|\Gamma\vdash_R^{U,\chi}J\)，\(V\)是可以随意命名的symbol。
formal generic judgement、generic rule、generic inductive definition。与formal derivability judgement、hypothetical rule、hypothetical rule induction的定义类似。
Chapter 4: Statics
（编程语言）静力学。用以在程序编写完之后、运行之前检查程序的语法。主要以表达式的类型检查为主。
abstract syntax。抽象语法。本质上是对于语法树的描述，包含了一系列的operator及其arity。BNF范式是表达语法的常用方法。从类型检查的角度来说，一个语法表中包含两种sort的语法，一种是表达式，即expression；另一种是表达式的类型，即type。注意sort与type两个概念的区别。sort是abt的种类（例如表达式是一种abt，是一种语法类型），type是表达式的类型（有类似于编程语言中的数据类型）。
typing judgment。类型系统中有关类型的断言。 表达为一般性假设断言，声明一个表达式的类型。\(\chi|\Gamma\vdash e:\tau\)（”\(:\)“用来表达类型），代表表达式\(e\)的类型（type）为\(\tau\)。\(\chi\)代表上下文中的变量集合，这些变量是可以被随意替换和重命名的。在这一语境中，假设\(\Gamma\)被称为类型上下文（type context），代表表达式上下文的中的（\(\chi\)中的）变量类型（有时表达式\(e\)的类型由其上下文中其他变量的类型决定）。\(x\in dom(\Gamma)\)代表变量\(x\)没有出现在类型上下文中（fresh）。
typing rule。类型系统中的规则。用来定义一个表达式的type的推理，前提是一般是其子表达式的type，结论一般是这些子表达式（作为abt中的变量）构建的更大表达式的type。也有一些rule是没有前提的axiom，强制规定某种表达式的type，通常是针对的非常简单的表达式，比如编程语言中变量（这里指的不是abt的变量）和常量。typing rule是强烈语法导向的，一般来一条语法规则对应一个typing rule。
unicity of typing。类型的独特性。对于每一对上下文\(\Gamma\)和表达式\(e\)，最多只能有一个类型\(\tau\)使得\(\Gamma\vdash e:\tau\)。
inversion for typing。类型的倒置。根据表达式，可以反推出其表达式的类型以及表达式中变量（语法的、abt的变量）的类型。
weakening of statics。静力学的弱化。在假设中增加不存在于typing context（\(\Gamma\)）的\(x:\tau\)，不影响这一typing context中表达式的类型。
substitution of statics。静力学的替换原则。表达式本质上是一个abt，将abt中的变量替换为与这个变量type相同的子abt，不影响外层的表达式的类型。替换原则类似于软件中调用过程，我们在调用一个函数时本质上调用的是函数的签名，但是最终这个签名会被函数的实现替换。abt、expression的本质就是一个代码段。
decomposition of statics。静力学中的分解。替换的逆过程。表达式中的子表达式可以分离出来，并且在对应位置放上变量。可以将一个表达式分解为等效的两个小表达式。
introduction and elimination。语法构建的两种形式：介绍和消除。introduction直接决定了一个值的type（什么是什么），elimination决定了怎么用同一个类型的一系列值在计算之后去形成另一个类型（让复杂的、带有变量的表达式最终简化为自身的introduction form）。
closed expression。封闭的表达式。当表达式中的所有的variable所代表的子表达式都计算成值（value）了，当前表达式已经可以被直接计算为值了，那么这一表达式称为封闭表达式。
Chapter 5: Dynamics
代码动力学。主要是研究代码怎么被执行的。主要包含了三种动力学：structural dynamics（表达式在一步步执行中的变化），contextual dynamics（对于一个多层嵌套的复杂表达式来说，表达式不同部分的执行顺序），equational dynamics（表达式之间的等效关系）。在这一章中，编程语言的表达式（expression）基本等同于计算机程序（program）或者指令（instruction）。
transition system。变迁系统。类似于状态机。变迁系统中包含一系列state（状态）。包含initial（起始状态）和final（终结状态）作为一开始的状态和结束的状态。以及它们之间变迁的方式。如果每一个状态最多只有一个后继状态，那么就说这一变迁系统是确定的（deterministic）。
transition judgement。变迁断言。用\(s\longmapsto s'\)代表state \(s\)和state \(s'\)之间的转换。另外，如果强调两个状态之间包含多步的变迁。\(s\longmapsto^* s'\)代表两个状态的变迁是0步或者多步的。当然也可以通过将星号变成一个数字来表达两个状态的变迁步骤的数量，比如\(s\longmapsto^0 s\)或者\(s\longmapsto^k s\)。
transition sequence。变迁序列。如果state \(s_0,...,s_n\)依次变迁，\(s_0\)是起始状态，那么这个序列叫做变迁序列。如果\(s_n\)之后没有状态了， 这一序列被称作最大的（maximal）。如果\(s_n\)是终结状态，那么这个序列是完整的（complete）。
structural dynamics。结构动力学。将语言的表达式视为state，那么就可以针对一个语言建立一个表达式的变迁系统，表达了表达式的变化关系。比如\(plus(num[n_1];num[n_2])\longmapsto num[n]\)。这些变化都有前提，都有对应的rule。rule分为两种，\(\frac{n_1+n_2=n}{plus(num[n_1];num[n_2])\longmapsto num[n]}\)叫做指令变迁（instruction transition），代表一个expression真正执行产生的变迁，反应了其原始语义。还有一种叫搜索变迁，表达了一个表达式内部的指令（子表达式）的计算顺序（规定计算过程），比如\(\frac{e_1 \ val \ \ \ \ e_2\longmapsto e_2'}{plus(e_1;e_2)\longmapsto plus(e_1;e_2')}\)代表operator plus的第一个参数先变迁（计算）到一个具体的值之后才能变迁（计算）第二个参数所对应的表达式。
by-value and by-name interpretation。按值解释和按名字解释。值，value，被认为是一个表达式变迁过程的final state。从introduction and elimination的角度来说，introduction form就是一个表达式已经不可再算的最终状态，就是value，elimination form就是用rule来规定表达式的内部子表达式的计算，直到子表达式都变成了introduction form。按值解释，是在一个子表达式的实例带入母表达式的对应变量之前先计算出值。按名字解释，子表达式在带入之前不进行任何计算而直接带入。二者的存在都是为了在执行的过程中省计算量，当一个表达式在程序中（其他表达式中）出现多次时，by-value可以将多次对于一个子表达式的计算合并成一次计算，但是对于一个注定不会被算到的子表达式来说，by-value的策略就会产生额外的、不需要的计算，这种情况时by-name的方式是更好的。
contextual dynamics。上下文动力学。结构动力学的变体，为了进一步强调指令执行的顺序。上下文动力学包含了结构动力学也包含的指令变迁，只是符号变成了单纯的箭头\(plus(num[n_1];num[n_2])\longrightarrow num[n]\)。而结构动力学中的搜索变迁在上下文动力学中变成执行上下文（evaluation context），用\(\varepsilon\)表示 。执行上下文是一个被挖掉一部分的表达式，是下一个要执行的表达式（指令）的母表达式的其他部分。被挖掉的部分被称作hole，用符号\(\circ\)表示。\(\circ\)中的表达式就是下一个要执行的指令。使用符号\(e'=\varepsilon\{e\}\)代表上下文\(\varepsilon\)中的孔洞被表达式\(e\)填满之后形成了完成表达式\(e'\)。那么上下文动力学就能表达为\(\frac{e_0\longrightarrow e_0'}{\varepsilon\{e_0\}\longmapsto \varepsilon\{e_0'\}}\) 。
equational dynamics。等价动力学。与结构或者上下文动力学都不同，等价动力学研究程序之间的等价关系。这一等价关系被称为定义等价性或者计算等价性。等价的概念可以表达为\(\chi|\Gamma \vdash e\equiv e':\tau\)。一般隐含地要求\(e\)的类型和\(e'\)是一样的。两个表达式等价，说明两个表达式最终可以变迁到相等大小的值上。同时等价也有结构化的性质，自身与自身是等价的（反射性），\(\equiv\)两侧的内容可以交换（交换性），\(e \equiv e'\)以及\(e' \equiv e''\)那么\(e'\equiv e''\)（传递性）。
Chapter 6: Type Safety
类型安全。类型安全代表程序在语法上完全正确。Statics和Dynamics都可以保证类型安全，Statics主要在运行前通过type system保证，Dynamics主要通过transition system来检查运行时错误。
type safety。类型安全，类型安全要满足两个条件。第一个称为preservation（类型保存），代表一个变迁断言\(e\longmapsto e'\)前后的两个状态的type必须是一样的，即如果\(e:\tau\)，那么\(e':\tau\)。第二个条件称为progress，代表如果一个表达式不是值，那么它就应该可以变迁下去。
run-time error。运行时错误。有些错误在静力学阶段难以通过类型系统推断出来，那么在动力学阶段加入名为error的表达式和相关变迁规则来处理就可以，一旦出现错误的前提，那么直接变迁出error来弹出错误即可。而与一般编程语言的异常处理一样，在变迁系统中除了要规定错误的产生的直接rule之外，还需要给出子表示中的错误怎么从外层表达式传递的问题，即当子表达式变迁到error之后，外层表达式也要变迁到error。
Chapter 7: Evaluation Dynamics
计算动力学。有时候为了简化dynamics的表达，我们需要仅仅关注表达式的计算结果，而对于其具体的执行过程乃至类型安全的检查都不在意，那么我们可以使用evaluation dynamics。
evaluation judgement。计算断言。表达为\(e\Downarrow v\)，代表封闭表达式\(e\)（见chapter 4）可以计算出值\(v\)，用结构动力学可以表达为\(e\longmapsto^* v\)。此外，一个表达式\(e\)的计算结果和其在变迁系统的后继表达式\(e'\)的计算结果是一致的，即如果\(e\longmapsto e'\)并且\(e'\Downarrow v\)，那么\(e\Downarrow v\)。
rule of evaluation dynamics。计算动力学中的规则。一个语法的计算动力学由一大堆规则构成，规则前提是一个表达式中子表达式的结果以及表达式自身的语义，规则的结论是表达式自身的计算结果。例如，\(\frac{e_1\Downarrow num[n_1]\ \ e_2\Downarrow num[n_2]\ \ n_1+n_2=n}{plus(e_1;e_2)\Downarrow num[n]}\)。与之前的动力学不同，计算动力学不是语法导向的，不是每一个语法表达式都对应一个动力学规则。
goes wrong。（一个表达式）发生错误。结构动力学通过声明什么样的语法是合法的，来检查错误，不合法的程序会在statics和dynamics过程中违背type safety的preservation和progress的范畴，在变迁过程中被卡住。与结构动力学相反，计算动力学省略了中间过程，所以只能显示地声明什么样的表达式是错误的。所以计算动力学难以进行类型检查，因为在表达式的无穷嵌套和组合中，正确的情况是少的，错误的情况是多的，所以穷尽所有的错误是不现实的。但是依旧有一种断言来定义一个表达式的错误：\(e??\)。
cost dynamics。开销动力学。结构动力学天然地表达了时间复杂度，通过看两个表达式之间变迁的步骤。但是evaluation dynamics因为省略了结构动力学中的中间步骤，所以对于开销的表达就需要额外的定义，通过扩展计算断言为\(e \Downarrow^k v\)代表表达式\(e\)需要\(k\)步来变迁到值\(v\)，等效于\(e\longmapsto^k v\)。开销动力学包含了一系列由扩展过的evaluation judgement构成的rule，比如\(\frac{e_1\Downarrow^{k_1} num[n_1]\ \ e_2\Downarrow^{k_2} num[n_2]}{plus(e_1;e_2)\Downarrow^{k_1+k_2+1} num[n]}\)。
标签：总结,语法,断言,PFPL,rule,judgement,表达式,Gamma 来源： https://www.cnblogs.com/duzhenblog/p/16179226.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。