引用

Polikarpova N, Kuraj I, Solar-Lezama A. Program synthesis from polymorphic refinement types[J]. ACM SIGPLAN Notices, 2016, 51(6): 522-538.

摘要

本文提出了一种合成递归函数的方法，该方法能够满足以多模态细化类型(Polymorphic Refinement Type)形式给出的规范。这类规范非常适合使用程序合成解决，其原因有二：首先，这些规范会提供表达能力和可判定性的独特组合，使针对非平凡(Nontrivial)程序的自动化验证变得可行，进而使非平凡程序的合成变为可能；其次，一种为程序指定的、基于类型的规范通常可以被有效地拆解成一系列独立的子规范，用于分别描述目标程序不同组件。由此，合成器可以考虑更少的组件这，并大大缩减搜索空间的规模。本文提出的程序合成过程的核心就是一种基于细化类型的、支持规范分解的全新算法。

本文对提出的合成算法进行了原型实现，并利用大量程序合成问题对其进行了评估。基于评估结果作者发现：相比于现有技术，本文的原型实现具备更加优秀的可拓展性和可用性、合成出的程序也更加复杂(合成的目标是排序算法、平衡搜索树相关操作)。此外，本文提出的原型实现还优化了许多现有程序合成基线问题的解决过程，体现为更加简洁直观的用户输入。

关键词：程序分析；函数式编程；细化类型；谓词抽象

引言

实现可扩展的程序合成的关键是实现模块化验证(Modular Verification)。模块化使得合成器能够独立地筛选候选子程序，从而缩减通过组合子程序得到的搜索空间的大小。

仅使用简单的粗粒度类型不足以精确地描述程序合成的目标。因此，现有的方法往往会利用一些其他的规范来补充类型信息，例如：输入输出示例(Input-output Examples)和前后置条件(Pre-Conditions and Post-Conditions)等。遗憾的是：目前，相应的验证过程很少能够达到和类型检查(Type Checking)对等的模块化程度，这从根本上限制了上述技术的可拓展性。

本工作实现了一个新颖的系统：该系统通过充分利用细化类型(Refinement Type)的优势、使用可判定逻辑谓词(Predicates from Decidable Logic)对类型进行修饰，进一步发展了类型制导的程序合成。比如：假设用户打算合成一个复制函数 replicate。给定自然数 n 和值 x，replicate 能够输出一个列表，列表的成员是值 x 的 n 个副本。在本文提出的程序合成系统中，用户可以通过提供以下签名来描述自己的程序合成意图：

其中：返回值的类型使用谓词 len v = n 进行了细化，将函数返回的列表的长度限定为 n；Nat 则是{v: Int|v≥0}的缩写，表示大于等于 0 的整型。给定上述签名、结合 List 类型的定义以及一组标准的整型组件(包括 zero 值、减量函数和不等式判定法则)，本文提出的系统可以在几分之一秒内生成可验证的 replicate 实现，合成结果如图 1 所示。

图1 包含细化类型的、replicate函数的签名&程序合成结果

上述示例很好地展示了参数多态性(Parametric Polymorphism)约束程序行为的能力：图 1 中的签名并没有明确说明返回列表中的每个元素都必须等于 x，但程序合成器依旧成功满足了这条语义要求。参数多态性与细化类型相结合则可以在类型系统(Type System)内实现全面的高阶推理(High-Order Reasoning)，对应上述例子即：replicate 的调用者可以使用任意细化类型实例化参数 α。对于值 x 包含的任意特性，replicate 的合成结果能够保证 α 每个元素都能拥有相同的特性。

作者将局部流动类型检查(Local Liquid Type Checking)和程序项枚举(Exhaustive Enumeration of Program Terms)相结合，实现了原型程序合成器 SYNQUID，并以不同类型的 64 个合成问题为基准，通过实验评估了 SYNQUID 的性能。实验结果表明：SYNQUID 可以处理大多数相对棘手的基准测试；与现有技术相比，SYNQUID 解决合成问题花费的时间通常较短或相当。与基于示例的工具(Example)相比，SYNQUID 的规约往往更加简洁，却生成的解决方案通常是可验证的；与基于 Hoare 风格推理的工具相比，SYNQUID 特有的自动细化推理功能保证了其能够验证并合成更加复杂的程序。

概览

SYNQUID 在一种类 ML 核心语言中运行，该语言由条件(Conditional)、代数数据类型(Algebraic Datatype)、模式匹配(Pattern Matching)、参数多样性(Parametric Polymorphism)和固定点(Fixpoint)等多种要素组成。遵循流动类型框架(Liquid Type Framework)，作者为这种语言配备了一般可确定细化类型(General Decidable General Refinement Type)。在 SYNQUID 的类型系统中，细化类型以{B|φ}的形式表示，其中：φ 是用于描述程序变量和特殊值变量 v 的细化谓词(Refinement Predicate)，通常不会在程序中出现；基础类型则可以组合成形如x:Tx → T2依赖方程类型(Dependent Function Type)，其中x可能在*T2*的细化谓词中出现。本文提出的框架与细化谓词的确切逻辑无关，只要求这些细化谓词的布尔组合是可确定的即可。

合成问题由(1)目标细化类型 T，(2)类型环境(Type Environment)Γ 和(3)逻辑限定词集合 Q 三部分定义。合成问题的解则是一个程序项(Program Term)_t_，它在环境 Γ 中具有类型T。环境中包含一系列合成器可用的类型签名(可能是数据类型构造函数、库函数或局部变量)，以及在合成t时可能出现的任意路径条件。限定词是一组来自细化逻辑的谓词，通常被用作未知细化(Unknown Refinement)和分支界限(Branch Guard)的构件块(Building Block)。本文的系统。

给定一个合成问题，SYNQUID 将采用(1)选取 Γ 的一个构件，或是(2)将问题递归地拆解成相对简单的子问题并生成子解ti来分而治之的方式构建候选解。

由于拆解通常不完全，因此不能保证通过组合ti获得合成所需的类型候选对象T。为了确保获得的候选对象是可用的解决方案，系统会生成子类型约束(Subtyping Constraint)。如果生成的候选解不能满足这些约束，系统将回溯并选择另一种子问题解决方案的组合、或者采用另一种迥然不同的方式对问题进行拆解。通常来说：通过分解合成问题得到的子合成目标越明确，则 SYNQUID 需要回溯的次数就越少。

SYNQUID 语言

该部分主要介绍本文为具有细化类型的核心编程语言设计的类型检查算法的三个方面。该算法将用于验证程序合成得出的候选结果。为了实现自动化、易拓展的面向程序合成的类型机制，需要解决两个要求：第一个要求与类型推断(Type Inference)的数量有关。类型检查机制可以使用高阶的注解，即：用户规定的合成目标，但不能依赖除此之外的任何注解。此外，类型检查机制必须能够推断出所有多态实例的类型，以及匿名函数的参数；第二个要求是类型检查机制需要能够在本地完成类型错误探测。直观地，如果一个程序子项造成的类型错误与它的上下文无关，类型检查算法就相应地可以在不分析上下文的情况下，检测并报告该错误。

语法和类型

图2 程序项和类型

SYNQUID 语言的语法如图 2 所示。

程序项：本工作对细化语言(Language of Refinement)和程序语言(Language of )进行了区分：前者由细化项(Refinement Type)构成，包含多个 Sort ∆；解释后的符合和 Sort 依赖于选中的细化逻辑。本文将布尔 Sort B 称为公式。

类型和模式：SYNQUID 语言类型有两种类型(1)标量，即通过公式细化的基础类型，或(2)依赖函数类型(Dependent Function Type)。基本类型包括：基本数据类型(Primitive)、类型变量以及带有零或多个类型参数的用户自定义数据类型。数据类型的构造函数可以简单地表示为必须包含类型： α1…αm, T1 → Tk → Dα1…αm的函数。上下文类型(Contextual Type)由一对变量的绑定序列和一个描述这些变量的类型组成，用于协助精准类型检查。

环境、格式正确性和子类型化：类型环境 Γ 是一组变量绑定x:T和路径条件 φ 的序列。环境中所有路径变量的合取用 P(Γ)表示。如果一个公式 φ 是一种布尔 Sort，且其中的每个自由变量都和 Γ 中对应的类型绑定，那么就成 φ 在环境 Γ 中是格式正确的，记做 Γ ├ φ。格式正确对象向类型拓展的过程如图 3 所示。

图3 格式正确性和子类型化

往返类型检查

在双向系统中，程序分析过程一般从使用类型检查规则传播顶层注解开始。该过程通常采用自顶向下的顺序，在遇到一个系统无法适用任何规则的程序项t时停止。这时，系统将切换到自底向上模式，开始推断t的类型T’，并检查T’是否是目标类型的子类型。如果检查失败，则舍弃t。双向类型传播是一个“全有或全无(All-or-Nothing)”的过程：如果一个程序项的检查问题无法完全拆分成其子项的检查问题，系统就会放弃目标类型的所有信息并转而使用纯自顶向下推导。作者认为：目标类型的某些信息可以在自顶向下阶段保留，协助系统进行本地错误探测。为此，作者将双向推导判断(Bidirectional Inference Judgement)修改为一种加强判断: Γ├t↓T↑T’，内容如下：在环境 Γ 中，以已知类型 T 为基准检验项 t，并生成更强的类型 T’。作者将根据此判断方式设计得出的类型系统称作“往返(Round-trip)类型系统”，因为它会先自顶向下、再自底向上地传播类型。

健壮性和完整性

当以一个模式S, T├Qt↓S检查任意 SYNQUID 程序项t都存在一组限定符 Q’和一个模式 S’，使得自底向上系统可以藉由 t, T├Q’t::S推断出S’和 T├S’<:>S时，往返类型检查是健壮(Sound)的。注意：自底向上的类型推断可能比类型检查更加严格地要求更多限定符：在自底向上的系统中，生成分支语句和抽象更加需要类型是流动性的。往返系统可以通过分解目标类型来获取程序项类型，不符合上述流动性限制。然而，在实际应用中，上述差异却可以基本忽略。原因在于：类型推断算法可以从顶级目标类型和组件函数的前提条件中提取出缺失的限定符。只要 Q 包含足够的限定符，那么就可以保证目标模式进和构件函数的前提条件是具有流动性的(T├QS)，记做 ├QΓ，并由此可以推断出：Q’=Q。

这里给出定义健壮性和完整性的两个定理：