DraonAbyss

函数语言程序设计

C++(3) CodeForces(23) LeetCode(3) 安全编程(1) 密码学基础(17) 无线网络安全(5) 笔记(16) 算法设计与分析(22) 编译原理与技术(16) 网络安全数学基础(3) 计算机逻辑基础(8) 题解(37)

/ 注册

全部文章 / 函数语言程序设计（共40篇）

【Coq】？Rel II 基本性质来自专栏

基本性质 Basic Properties 任何人都知道，上过离散数学本科课程的人，一般来说，关于关系有很多话要说，包括对关系进行分类的方法（如自反、传递等），关于某些类型的关系可以一般证明的定理，从一个关系到另一个关系的构造，等等。例如。。。偏函数 Partial Functions 集合X上的...

2021-12-13

0 572

【Coq】？Rel I 关系来自专栏

这一短小的（可选的）章节发展了一些关于Coq中二元关系的基本定义和几个定理。关键定义在实际使用的地方重复（在编程语言基础的Smallstep一章中），因此已经熟悉这些概念的读者可以安全地浏览或跳过本章。然而，关系也是使用Coq的基本推理工具开发工具的一个很好的练习来源，因此在IndProp一章之后查...

2021-12-13

0 410

【Coq】？ Maps III 总地图来自专栏

总地图本章中我们的主要工作是建立一个部分映射的定义，该定义在行为上与我们在列表一章中看到的部分映射相似，另外还有关于其行为的伴随引理。不过，这次我们将使用函数而不是键值对列表来构建映射。这种表示法的优点是它提供了一个更为扩展的映射视图，其中以相同方式响应查询的两个映射将被表示为字面上相同的东西（...

2021-12-06

0 396

【Coq】？ Maps II 标识符来自专栏

标识符首先，我们需要一个用于索引到地图中的键的类型。在Lists.v中，我们为类似的目的引入了一个新的类型id；在这里以及其他软件基础中，我们将使用Coq标准库中的字符串类型。为了比较字符串，我们定义了函数eqb_string，它在内部使用Coq的字符串库中的函数string_dec。 Defi...

2021-12-06

0 517

【Coq】？ Maps I Coq标准库来自专栏

地图（或字典）是普遍存在的数据结构，尤其是在编程语言理论中；在接下来的章节中，我们将在许多地方需要它们。他们还利用我们在前几章中看到的思想做了一个很好的案例研究，包括用高阶函数构建数据结构（从基础和多边形）和使用反射来简化证明（从IndProp）。我们将定义两种类型的映射：total maps（总...

2021-12-06

0 465

【Coq】18 Tactics I 应用策略来自专栏

本章介绍了几个额外的证明策略和策略，使我们能够开始证明函数程序更有趣的属性。我们将看到：如何在“向前”和“向后”证明中使用辅助引理；如何对数据构造函数进行推理——特别是如何利用它们是内射的和不相交的事实；如何强化归纳假设，以及何时需要强化；和关于如何通过案例分析进行推理的更多详细信息。 ...

Coq 函数语言程序设计

2021-11-11

1 855

【Coq】17 Poly III 附加练习来自专栏

附加练习 Additional Exercises 57: 2 stars, standard (fold_length) 列表上的许多常见功能可以按折叠方式实现。例如，以下是长度的替代定义： Definition fold_length {X : Type} (l : list X) : nat ...

Coq 函数语言程序设计

2021-11-11

0 980

【Coq】16 Poly II 作为数据的函数来自专栏

作为数据的函数 Functions as Data 与大多数现代编程语言一样——特别是其他“函数”语言，包括OCaml、Haskell、Racket、Scala、Clojure等——Coq将函数视为一级公民，允许它们作为参数传递给其他函数、作为结果返回、存储在数据结构中等。高阶函数 Higher-...

Coq 函数语言程序设计

2021-11-11

0 606

【Coq】15 Poly I 多态性来自专栏

多态性 Polymorphism 在本章中，我们将继续发展函数式编程的基本概念。关键的新思想是多态性（将函数抽象为它们所操作的数据类型）和高阶函数（将函数视为数据）。我们从多态性开始。多态列表 Polymorphic Lists 在上一章中，我们一直在处理只包含数字的列表。显然，有趣的程序还需要能...

Coq 函数语言程序设计

2021-10-27

0 1082

【Coq】14 Lists V 局部映射来自专栏

局部映射 Partial Maps 作为在Coq中如何定义数据结构的最后一个例子，这里有一个simple _partial map_data类型，类似于大多数编程语言中的map或dictionary数据结构。首先，我们定义一个新的归纳数据类型id作为部分映射的“键”。 Inductive id I...

Coq 函数语言程序设计

2021-10-27

0 655