RZ系统：将数学理论转化为可实现性解释及程序规范

理论计算机科学电子笔记153（2006）77-92www.elsevier.com/locate/entcs通过可实现性进行安德烈·鲍尔1卢布尔雅那大学数学与物理系斯洛文尼亚卢布尔雅那Christopher A. 磨石2计算机科学系Harvey MuddCollege Claremont，CA，USA摘要我们提出了一个系统，称为RZ，自动生成的程序规格说明，从数学理论。我们将数学理论转化为规范，通过在ML语言中计算它们的可实现性解释，并使用断言（作为注释）进行增强。 虽然系统最适合于描述那些可以很容易地在XML中描述的数据结构，标准语言（例如，有限表示群、实数算术、图形等），它还阐明了数据结构和构造数学之间的关系。关键词：可实现性，构造逻辑，ML。1引言Kleene [6]引入了可实现性作为基于部分可计算函数的直觉算术模型这一思想已被研究和generalized由不同的作者[11，4，5，13]。基于Longley[8]的类型可实现性思想，我们构建了一个工具RZ来将数学理论转化为代码的规范，解释了为了相信我们有一个正确的数学理论实现所必需的东西1电子邮件：Andrej. andrej.com2 电子邮件地址：stone@cs.hmc.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.08.00778A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）77由于可实现性解释验证了直觉主义逻辑的规律，我们的输入理论是直觉主义的或构造性的。因此，RZ提取了构造性理论的计算意义，并将其表达为程序设计规范。我们强调，RZ并不从证明中提取程序-事实上，在我们的系统中没有办法编写证明。我们只是确定程序应该做什么，即，我们为他们提供规格。我们把它留给程序员或其他工具，按照他或她认为合适的方式来构建程序。这使得程序员可以完全自由地编写高效的程序，而不需要直接对应于形式证明。RZ的最初目的是帮助开发可计算数学的数据结构。如果一个人开始实际计算构造性数学理论的可实现性解释，他很快就希望有一种自动化的方法来做这件事。有了像RZ这样的工具，实验和尝试理论的变化就容易得多，直到得到一个合适的规范。RZ也可以用来向程序员解释和教授构造性数学，他们通常接受过经典数学的训练;它将构造性语句转换为易于理解的程序要求（用经典逻辑表示）。我们的RZ实现在Objective Caml [7]中生成接口，但可以很容易地被其他类似的类型化语言采用。我们要求目标语言的基本功能是乘积、函数和和类型，以及对模块接口的支持。本文的结构如下。第2节简要概述了可实现性。在第3节中，我们描述了理论和签名，它们分别是RZ的输入和输出。在第4节中，我们讨论了各种实施点。在第5节中，我们展示了典型的例子，并以第6节结束。2可实现性我们简要地激发了（类型化的）可实现性的主要思想。当我们在编程语言P中表示一组数学对象S时，有两个自然的步骤：首先选择一个底层类型|S|类型的值如何表示，其次指定|S|表示或实现集合S的元素。例如，考虑我们如何表示简单有限有向图（其顶点由整数标记）。作为我们可能选择的底层数据类型|D|= int list_n（int_n）list，并将图G∈D表示为一对列表（v，e），其中v=[x1;. ;xn]是A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）7779|不|=单位|⊥|=单位|x=Sy|=单位|为|φ|∗ |ψ |ψ||φ=φ|为|φ| → |ψ||φ∨ ψ|为|φ|+的|ψ||x ∈ A。φ（x）|为|一|→|φ||x ∈ A。φ（x）|为|一|×|φ|（）DT（）Dx=Sy我的xSy（t1，t2）Dφφ我的t1Dφ和t2Dφt D φ=0我的对于所有的u∈|φ|，if u D φthen tuDInlt D φ我的 t D φinrt D φ我的 tDt D <$x∈A.φ（x）i <$对于所有u∈|一|，如果uDAx则tuDφ（x）（t1，t2）D φ x∈A.φ（x）i ∈ t1DAx和t2Dφ（x）Fig. 1.逻辑学的可实现性解释（提纲）顶点列表和e = [e1;. ;em]是边的列表。 形式上，我们写（v，e）DDG并将其读作观察每个图至少由一对列表实现，并且没有一对列表表示一个以上的图。（通常，大多数图形都由许多不同的列表对）。这使我们得出下面的定义。我们将稍微滥用符号，写成t∈|S|表示t是类型为|S|.定义2.1一个适度集合3是一个三元组（S，|S|其中S是集合，|S|是一个类型，而DS是类型表达式之间的关系|S|和S的元素，满足：(i) 对于每个x∈S，有t∈|S|使得tDSx.(ii) 如果tDSx和tDSy，则x=y。实现函数f：（S，|S|，DS）-（T，|不|，DT）是一个函数f：S→T，其中存在u∈|S| → |不|使得tDSx = tDTf（x）。我们说u实现了f。实现函数f的实现器u通常被称为“f的3Modest sets由Dana Scott命名。它们是80A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）77适度集合和已实现函数构成一类适度集合Mod（P）。在可实现性理论中，这是一个众所周知的具有良好性质的范畴。是正则的和局部双笛卡尔闭的，这使我们能够解释一阶逻辑和丰富的类型理论。在这里，我们只是概述了逻辑的可实现性解释背后的主要思想。详情参见例如[1]在逻辑的可实现性解释中，每个公式φ都被分配了一组实现者，这些实现者可以被认为是证明φ有效性的计算。这种情况有点类似于（但不等同于）将命题作为类型的逻辑转换为类型论，其中，命题对应于相应类型的项。 更准确地说，我们为每个公式φ指定一个基础类型|φ|的实现者。 然而，与命题类型翻译不同的是，|φ|是φ的有效实现子。当t∈|φ|是φ的实现器。基本类型和可实现关系D是归纳定义的关于φ的结构，其轮廓如图1所示。我们说一个公式φ在Mod（P）中是有效的，如果它至少有一个实现者。我们将不再详述涉及适度集合范畴的技术细节，而是具体描述我们的可实现性翻译。不过，有一个技术问题，我们首先要注意。 一个 适度的集合是一个三元组（S，|S|，DS），其中S是任意集合。为一个自动化的系统，如果它不必参考任意集合，而只是编程语言中已经存在的成分，例如类型和表达式集合。直到范畴等价，适度集合可以构造为三元组（|S|，S，S）哪里|S|是一种类型，而SQL是类型表达式的子集|S|，称为总values，4，并且是在S上的等价关系。适度集合的这种表示与原始表示之间的关系如下：• S|S|意识到一些事情，即，有x∈S使得tDSx。这些对应于满足表示不变量的实现，例如，边列表仅提及节点列表中的整数的图，是类型为intlist（int）的所有值的子集int）列表。• t ≠u，如果t和u实现相同的元素，即， 有x ∈ S使得t DS x和u DS x。这种关系等同于相同抽象值的替代具体表示，例如，将两个具体的图表示仅按照节点的顺序或边的顺序进行扩散另一种观点是适度的集合（|S|，S，S）仅引用编程语言中的对象和概念。它更适合我们的目的。4我们不要求一个总值必须是一个终止表达式。A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）7781理论要素设置s [= 集]constc [：set] [= 术语][stable]relationr[：set] [=prop]等价：集合模型M：理论公理a[M：理论][x：集合]=prop命题truefalsenotprop&&支柱||propprop=>prop prop<=>propr[term]term =术语所有[x：set]。propsome[x：set].propunique[x：set].道具集01boolS模型nameset*···*set set->set‘ +· · ·+{x[ ：set] | proposition}设定%关系方面X（术语，··· ，任期）term. n‘匹配项与模式匹配Lam x：设置。术语术语术语术语术语%关系letx%relationinterm=termterm：>set术语：集合x [：set]。 道具letx[：set]=terminterm图二. 输入语言摘要请注意，在上的等价关系也是上的部分等价关系。|S|这表明适度集实际上等价于PER模型。3理论与签名在本节中，我们描述一阶理论和签名。我们的系统将前者转化为后者。3.1理论一个理论是一个数学结构的描述，如一个群，一个向量空间，一个有向图，等等。• 基本集合的列表，• 属于特定集合的基本常数• 特定集合上的基本关系• 公理列表82A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）77举一个简单的例子，考虑一个半群的理论，其中每个元素都有一个（可能是非唯一的）平方根;回想一下，半群是一个具有结合二元运算和一个中立元素的集合。[5]在我们的系统中，它可以写为：理论SQGROUP =thyset sconst e： sconst（*）：s -> s -> s隐式x，y，z： s公理单位x = x * e = x和e * x = xaxiom asynx yz =x *（y * z）=（x * y）* z公理sqrt x= some y. y * y = x端理论是由你的... 端这个理论定义了一个基本集合s和两个基本常数：s的元素e和一个（curried）二进制整数运算符*在设置S。隐式运算符并不是理论本身的一部分，但它向类型检查器发出信号，表明名为x或y或z的绑定变量应该被假设为在s上的范围内，除非另有说明。最后，我们有三个公理。公理论证，例如，x，y，z在结合性公理中，命名公理中出现的自由变量。认为它们是普遍量化的，这并不是一个太大的错误。重要的是要注意，理论不包括证明，而只是公理（和定理）的陈述。因此，尽管公理可以被定义，但人们实际上不能在理论中引用它们除了上面这个例子中所示的那些，我们的系统还支持理论的几个特征;输入语言在图2中进行了总结，其中括号表示可选元素。理论可以声明或定义关系。它们可以是稳定的，即，它们的计算解释是微不足道的（关于这一点的进一步讨论，见第4节）。公理可以在一个理论的所有模型上普遍量化。这对于描述普适性性质很有用，例如代数的初始性或余代数的终结性。这些命题是一阶逻辑中熟悉的命题;唯一性是唯一存在（uniqueexistence）。除了基本的空（0）集和单位（1）集之外，还可以形成卡氏积、函数空间、带标记的不交并、子集，并通过稳定的等价关系的等价物相应的引入和消除形式出现在术语语言中。例如，术语%relation是包含术语的关系下的等价类，而让x%relation=术语2中的术语1将x绑定到术语2中使用的等价类术语1的代表。表达式term：>set将term注入到给定的子集中（记录实际上是-5有平方根的半群的一个例子是用乘法作为二进制运算的复数。A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）7783ing子集的成员），而term：set将term从子集投影到其超集集合中。 描述运算符的值x. prop是唯一满足prop的x;使用它会导致证明恰好存在一个这样的x的义务。3.2签名在逻辑方面，我们有理论描述的模型。因此，在编程方面，我们应该用规范来描述实现。因此，我们的工具将理论转换为签名，这是ML签名允许我们要求某些类型的存在，以及给定类型的这允许可判定的类型检查，但我们需要更多的表达性，以便忠实地翻译理论的内容。因此，我们生成了由断言注释增强的签名，断言注释指定了对值和函数的约束，实现超出了它们的类型。程序员有责任检查实现是否满足这些断言，因为RZ并不试图做任何定理证明。断言是用普通的经典一阶逻辑写的。由于程序员通常没有受过构造性逻辑的训练，这可能会使它更容易验证断言。上面的SQGROUP理论的输出是：模块类型SQGROUP=sigs型（** Assertion per_s = PER（=s=）*）val e： s（** 断言e_total = e：||S||*）val（*）：s-> s-> s（** Assertion（*）_total=all（x：s，y：s）. x=s= y =>all（x'：s，y'：s）. x* ）（**断言单元（x：||S||）= x * e =s= x和e * x=s= x* ）（** 断言砷（x：||S||，y：||S||，z：||S||）=的x *（y * z）=s=（x * y）* z* ）val sqrt： s -> s（**Assertion sqrt（x：||S||）=的sqrt x：||S||和sqrtx * sqrtx =s= x*）结束在ML级别，我们需要一个类型s，以及三个值e、*和sqrt，分别为s、s->s->s和s->s。第三个值是84A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）77从平方根公理，其中有一个非平凡的计算内容，比照。第4.2款。注释中包含其他ML无法表达的需求，这些需求进一步限制了允许的实现。断言PER（=s=）验证了=s=是s上的部分等价关系的要求;它的域||是实现半群元素的s型项的子集，关系=s=标识（可能是不同的）实现相同ab-半群元素的项。||is the subset of terms of type s that realizesemigroup elements, and the relation =s= identifies (possibly different)terms realizing the same ab- stract semigroup element.这些数据一起确定了一个适度的集合。e声明之后的断言断言e实现了一个有效的半群元素，而*之后的断言断言*不能被实现器的选择所限制当然，e和*都必须满足单位公理和无单位公理。最后，从逻辑导出的新函数sqrt必须计算平方根。由于该理论要求平方根的存在性而不是唯一性，因此不要求sqrt相对于s上的部分等价关系是不变的;允许同一半群元素的不同实现子产生不同平方根（的实现子）。3.3参数化理论一个理论可以被其他理论的一个或多个模型参数化。例如，实数的理论实数可以根据自然数的模型N来参数化。自由群的理论可以用生成集来参数化。参数化理论有两个目的。参数化理论的模型是一个通用的实现，给定参数的任何实现，它都会返回结果理论的实现。在ML的层次上，这将是一个从模块到模块的函数，一个所谓的仿函数，因此参数化的理论可以被转换为仿函数的签名。或者，一旦我们描述了一个参数化理论Real，我们可能希望使用它来描述基于自然数的特定模型N1（实现）的实数的单个特定实现;这可以被描述为满足理论Real（N1）的实现。参数化理论的双重性质既是对参数化模型（a λ类型）和可以应用于模型以产生专门理论的东西（aλ）非常令人想起自动机[2]的类型包含。然而，ML不允许函子签名的应用，所以我们在生成签名之前对所有理论应用进行beta-约简;Real（N1）将为直接引用N1而不是泛型参数N的实数实现生成签名。A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）77854执行4.1预翻译在解析之后，我们的实现进行类型检查。类型检查器执行简单的类型重构。我们要求所有绑定变量的类型要么必须在绑定位置给出，要么通过隐式声明给出，要么从它们的定义中显而易见。与ML数据库不同，我们不需要在使用之前定义不相交的联合类型，或者让不同的联合包含不同的标记。因此，在求和之间进行了非常少量的隐式子类型化。否则，如果我们有一个指定的整数队列设置队列const emptyQueueconst enqueue：int* ipequeue-> ipequeueconst dequeue：ipeue->那么公理dequeue emptyQueue =将无法进行类型检查（左侧的最精确集合是两个元素的不相交联合，而右侧的最精确集合是一个元素的不相交联合。）类型检查器还将尝试在set类型和子集类型之间进行转换{x：set|命题}，以便进行类型检查。因此，在本发明中，设定实数设置nz_real = {x：real| not（x= 0）}const one：realconst inv：nz_real -> nz_realconst（*）：real * real-> real公理域（x：real）=not（x=zero）=> x *（inv x）= one是允许的，而不是要求公理域（x：real）=not（x=zero）=> x *（（inv（x：>nz_real））：real）= one在这种情况下，由于：>和：具有计算内容（进入子集涉及到将项与命题的实现者配对;离开子集则是第一次投影），类型检查器在将其传递到翻译阶段之前将前一版本的字段如果86A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）77在理论上不能证明注入到子集中（例如，如果域公理缺少前提not（x=零）），那么理论仍然会翻译，但是生成的断言不会被任何实现所满足4.2可实现性翻译我们首先讨论集合和项的可实现性翻译，然后关注逻辑的翻译，这是有趣的部分。一个集合S被转换成一个适度的集合（|S|，S，S）根据它的结构：基本集被转换成其底层类型是抽象的适度集，乘积被转换成适度集的乘积，函数空间因此，我们简单地使用Mod（P）的丰富的范畴结构来解释所有的集合构造函数。类似地，术语根据其结构被翻译为合适的ML术语。然而请注意，有些项的有效性不能由RZ检查，因为这将要求它证明任意定理。这样一个例子是定义描述运算符x。φ（x），其有效性只能通过证明存在唯一的x满足φ（x）来确认。在这种情况下，RZ发出证明义务，供程序员验证。但是请注意，翻译的术语始终具有有效的ML类型，即使没有满足附带的证明义务。逻辑的可实现性翻译背后的驱动力是一个定理，例如见[12，Thm。4.4.10]，它说，在可实现性解释下，每个公式φ都等价于这样一个公式，非正式地说，此外，公式我们接下来会解释这到底意味着什么在经典逻辑中，一个双重否定的公式φ等价于φ。从结构上讲，这一般不是真的. 要看到这一点，回想一下在构造性逻辑中，<$φ被定义为φ = φ，并观察到<$<$φ的实现者的基本类型是（|φ| →单位）→单位。此类型的条款不能转换为以下类型的条款|φ|以一般的方式（尽管在相反方向上的转换可以很容易地完成，这表明φ意味着φ）。此外，类型的术语（|φ| →unit）→unit不计算任何东西，所以我们不妨用一个特殊的平凡实现器来代替它们，任何计算意义。我们可以把平凡实现子看作是一个证明公式有效性但不计算任何东西的项。在某些情况下，甚至在构造性逻辑中也可能发生φ等价于φ。如果是这样，我们称之为φa-稳定公式，或简称为稳定公式 稳定公式有平凡的实现者，因为它们等价于dou-否定公式。在稳定公式中，几乎负公式是重要的，因为它们在句法上很容易识别：它们是A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）7787J由、=、、=和那些已知稳定的基本谓词的任意组合构建，但和只允许出现在=的左侧。6下面的定理是我们在上面一段中提出的权利要求的精确表述。定理4.1对于每个公式φ，存在一个集合Rφ和一个几乎负的公式φJ，使得在可实现性解释中φ等价于r∈Rφ. φJ（r）。我们省略了这个证明，因为它相当标准，并且涉及到对φ结构的直接归纳。 定理中的集合R φ就是基础类型的项的集合|φ|的实现者，而直观的意义，φJ（r）是RZ通过计算其基础类型来翻译公理φ或它遇到的任何其他命题|φ|并由上述定理得到几乎负的公式φJ。在输出签名中，valr：|φ|（* 断言φ（r）*）这样，公理φ就被分成了它的计算内容r和一个描述r何时是φ的有效实现子的陈述φJ。因为φJ几乎是负数，它没有计算内容，这意味着它的经典和建设性的阅读是一致的。因此，一个构造性的数学家和一个经典的程序员会同意φJ（r）的含义RZ识别几乎为负的公式，并优化掉它们的实现器，如下所述。此外，用户可以声明基本谓词或关系是稳定的，这将在翻译和优化期间被RZ考虑。似乎值得注意的是，稳定命题的计算不相关性类似于Pfenning [9]研究的证明不相关这并不奇怪，因为众所周知的事实是，双重否定享有模态可能性算子的许多形式属性。4.3优化没有建设性内容的命题有平凡的实现者，因此最终的“单元消除”过程既消除了这些，又对结果签名进行了窥视孔简化。如果没有优化器，SQGROUP理论的公理将产生[6]负公式是指完全不包含负和负的公式。88A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）77val unit：s -> top * top（** 断言单元（x：||S||）=的x* e =s= x和e* x =s= x* ）val sqrt：s -> s * top（** Assertion sqrt（x：||S||）=pi0（sqrt x）：||S||和pi0（sqrt x）* pi0（sqrt x）=s= x* ）其中top是平凡实现器的类型;我们使用top而不是unit来强调这些平凡实现器是终止的，因此可以安全地消除;对于unit类型的术语，这不一定是真的。优化器可以很容易地从类型中分辨出unit和assumption公理的实现器是微不足道的，可以丢弃，尽管sqrt不能完全丢弃，但它的部分返回值是不必要的。引用被丢弃或优化的常量的断言会自动重写以保持良好的类型性，并且我们获得了之前显示的SQGROUP的翻译，其中不包含top的出现。5示例可判定集。我们现在考虑可判定集的理论。 在建设性的数学一个集合S被称为可判定的，如果x=y或xRZ的输入为理论DecidableSet = thy sets公理decidable（x：s）（y：s）=（x= y）or not（x= y）end并且输出是模块类型DecidableSet = sigs型（** 断言per_s = PER（=s=）*）valdecidable：s-> s-> 0|'or 1]（**断言decidable（x：S||，y：||S||）=decidable x y ='or0 and x =s = y cor||可判定的x y =对所有的x，y∈S。* ）结束输出签名要求decidable是一个函数，接受两个实化器x和y，并返回两个标记'or0和'or1之一A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）7789x和y是否实现相同的元素。（写作析取是为了强调它是经典的或。这只不过是一个可计算的判定过程，用于判定s关于=s=的等式，正如所预期的那样。我们注意到没有什么要求部分等价关系=s=是可计算的，所以不是每个适度的集合都是可判定的。事实上，有许多自然的和重要的不可计算的部分等价关系的例子，如从自然数到自然数的函数的扩张相等(If我们可以计算地决定两个函数是否总是在相等的参数上给出相等的结果，我们可以构造一个Halting Oracle。自然数。接下来，我们考虑自然数理论。这个例子展示了公理如何被理论参数化。回想一下，自然数是具有一个常数和一个一元运算的初始代数（这样的代数有时也被称为理论迭代=thy set sconst zero： sconst succ： s ->s end理论Nat =thy模型N：迭代公理initial [I：Iteration]= unique（f：N.s -> I.s）。（f N.zero=I.zero和所有（n：N.s）。f（N.succ n）=I.succ（fn））端迭代理论是一个辅助理论。Nat理论假设存在一个理论迭代的模型N，它满足初始性公理，即从N到任何其他迭代理论I都存在一个代数态射。RZ生成的输出如图3所示。初始性公理已被翻译成一个函子，它期望迭代理论的实现I仔细观察这个断言可以发现，它本质上是说实现器通过简单的递归定义了一个从自然数到I.s的选择公理作为第三个例子，我们来看看选择公理的可实现性解释。我们使用公理的公式化，该公理指出每一个全关系都有一个选择函数：（x∈A. y∈B。R（x，y））= g∈B A. x∈A。R（x，g（x））.我们可以把它写成一个由集合A，B和关系R参数化的理论，但为了简单起见，我们使用以下版本：90A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）77模块类型Iteration=sigs型（** Assertion per_s = PER（=s=）*）val zero： s（** 断言zero_total =零：||S|| *）valsucc：s -> s（**断言succ_total =all（x：s，y：s）.x =s= y => succ x =s= succ y *）端模块类型Nat = sig模块N：迭代模块Initial：functor（I：Iteration）->sigvalinitial： N.s ->I.s（** Assertioninitial=(all（x：N.s，y：N.s）。x=N.s=y=> initial x =I.s= initial y）和initial N.zero =I.s= I.zero和(all（n：||N.S||）. initial（N.succ n）=I.s= I.succ（initialn））和（all（u：N.s -> I.s）.(all（x：N.s，y：N.s）。 x =N.s= y => ux=I.s=uy）=> uN.zero =I.s= I.zero和(all（n：||N.S||）. u（N.succ n）=I.s= I.succ（un））=> all（x：N.s，y：N.s）. x=N.s=y =>initial x =I.s= u y）* ）结束结束图三. 理论迭代和自然的理论选择=你的集合a集合b关系r：a * b公理选择=（all（x：a）. 一些（y：b）。r（x，y））=>一些（g：a->b）。all（x：a）. r（x，g（x））端输出如图4所示。 有趣的是，choice，它说choice把一个实现者f作为参数，该语句并输出一对函数，其中第一个是选择函数g，第二个提供了证明选择函数完成其工作的实现者。然而，有一个问题：实现者f不是需要遵守=a=，而选择函数g是。一般来说，choice无法将f转换为a=a=-相关函数。因此，一般来说，选择公理在可实现性解释中是无效的。这是可实现性和命题类型之间的另一个重要区别。6结论和今后的工作通过仅在规范级别进行翻译，RZ在ad-hoc实现和机器生成的实现之间提供了一个有用的中间地带。A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）7791模块类型Choice = siga型（** 断言per_a = PER（=a=）*）类型b（** 断言per_b =PER（=b=）*）类型r（** 断言谓词_r=PREDICATE（r， a * b，榄头(pi0 t =a= pi0 u和pi1t =b= pi1 u））* ）val choice：（a -> b *r）->（a -> b）*（a ->r）（** 断言选择=all（f：a-> b * r）.(all（x：||一||）. pi 0（fx）：||B||和pi 1（f x）|= r（x，pi 0（f x）=>(all（x：a，y：a）。x =a= y => pi0（选择f）x =b= pi0（选择f）y）和（所有（x：||一||）. pi1（选择f）x| = r（x，pi0（choice f）x））*）结束见图4。 理论选择选项。它允许更灵活的实现策略，但依赖于程序员来验证其代码的属性。此外，RZ可以作为向程序员解释构造性数学的一种手段。不了解构造性数学的程序员仍然可以理解翻译的输出，其中涉及抽象类型和（经典）一阶逻辑等熟悉的概念。查看这些例子可以提供原始逻辑背后的必要直觉，并更好地解释为什么一开始就想使用构造性逻辑而不是经典逻辑。由模型参数化的公理（例如，初始化）目前转换为ML函子的 我们已经尝试了将这些公理转换为多态类型的另一种翻译。在这种情况下，自然数的初始val initial：这正是自然数的熟悉迭代器（即，给定一个初始值、一个函数和一个自然数，将该函数多次应用于初始值）。对于程序员来说，这样的类型可以更自然、更简单地理解。翻译背后的理论是很好理解的，是哈珀，米切尔和莫吉的分相翻译[3]。由于ML的局限性，不是每个参数化公理都可以转化为多态性; ML只允许前向量化器，量化器可以在类型范围内，但不能在类型运算符范围内。但是，我们希望在可能的情况下这样做（常见情况）。作为替代方案，我们可以尝试将输出重定向到像Haskell[10]这样的语言，92A. Bauer，CA。Stone/Electronic Notes in Theoretical Computer Science 153（2006）77必要的多态类型，尽管Haskell另一个可能的扩展是允许输入语言中的依赖族。幸运的是，这并不需要找到支持依赖类型的目标语言;我们可以使用底层（非依赖）类型，然后将依赖关系表示为必须为实现进行验证的附加属性。引用[1] A. 鲍尔可计算分析与拓扑学的可实现性方法。博士论文，卡内基梅隆大学，2000年。可参见CMU技术报告CMU-CS-00-164和http://andrej.com/thesis。[2] Nicolas G.德布鲁因对AUTOMATH项目的调查。在J.P.Seldin和J.R.作者声明：To H. B. Curry：Essays in Combinatory Logic，Lambda Calculus，and Formalism，pages 589-606.中国科学院出版社，1980年.[3] 罗 伯特 ·哈 珀， 约翰 ·C.米 切尔 和尤 金尼 奥· 莫 吉。 高阶 模和 相 位区 分。 在Proc.17th ACMSymposium on Principles of Programming Languages（POPL[4] J.M. E海兰有效的地形。在美国。Troelstra和D. Van Dalen，editors，The L.E.J. BrouwerCentenary Symposium，pages 165-216.北荷兰出版社，1982年。[5] J.M. E Hyland，P.T.约翰斯通和A. M.皮茨。荣誉学位理论。数学程序腓Soc. ，88：205[6] S.C. 克林关于直觉数论的解释Journal of Symbolic Logic，10：109[7] XavierLeroy，DamienDoligez， JacquueesGarrigueue uee， DidierR'emy，and J'erEscheromeVouillo n. Objective Caml系统、文档和用户手册-版本3.08。技术报告，INRIA，2004年7月。[8] 约翰·朗利。匹配类型化和非类型化的可实现性。 电动注意Theor。Comput. Sci. ，35，2000。[9] F.芬宁模态类型理论中的内涵性、外延性与证明无关性。在第16届IEEE计算机科学逻辑年会（LICS'01）的会议记录中，第221页。IEEE计算机学会，2001年6月。[10] Simon Peyton Jones，ed. Haskell 98语言。Journal of Functional Programming，13（1），2003年1月。[11] A.S.特罗斯特拉可实现性。在S.R.巴斯，编辑，《证明理论手册》，第407-473页。北荷兰，1998年。[12] A.S. Troelstra和D.范达伦。数学中的建构主义，导论，第1卷。第121号在逻辑和数学基础的研究。1988年北荷兰[13] J. 范·奥斯滕练习实现。阿姆斯特丹大学博士论文，1991年。