forked from Coq-zh/SF-zh
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathExtraction.html
242 lines (176 loc) · 10.9 KB
/
Extraction.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Extraction: 从 Coq 中提取 ML</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>
<body>
<div id="page">
<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'> <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
<ul id='menu'>
<a href='toc.html'><li class='section_name'>目录</li></a>
<a href='coqindex.html'><li class='section_name'>索引</li></a>
<a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>
<div id="main">
<h1 class="libtitle">Extraction<span class="subtitle">从 Coq 中提取 ML</span></h1>
<div class="doc">
<div class="paragraph"> </div>
<a name="lab390"></a><h1 class="section">基本的提取方式</h1>
<div class="paragraph"> </div>
对于用 Coq 编写的代码而言，从中提取高效程序的最简方式是十分直白的。
<div class="paragraph"> </div>
首先我们需要指定提取的目标语言。可选的语言有三种：提取机制最为成熟的
OCaml，提取结果大都可以直接使用的 Haskell，以及提取机制有些过时的 Scheme。
</div>
<div class="code code-tight">
<span class="id" type="keyword">Require</span> <span class="id" type="var">Coq.extraction.Extraction</span>.<br/>
<span class="id" type="var">Extraction</span> <span class="id" type="var">Language</span> <span class="id" type="var">OCaml</span>.<br/>
</div>
<div class="doc">
现在我们将待提取的定义加载到 Coq 环境中。你可以直接写出定义，
也可以从其它模块中加载。
</div>
<div class="code code-tight">
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.Arith</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Init.Nat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.EqNat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ImpCEvalFun</span>.<br/>
</div>
<div class="doc">
最后，我们来指定需要提取的定义，以及用于保存提取结果的文件名。
</div>
<div class="code code-tight">
<span class="id" type="var">Extraction</span> "imp1.ml" <span class="id" type="var">ceval_step</span>.<br/>
</div>
<div class="doc">
Coq 在处理此指令时会生成一个名为 <span class="inlinecode"><span class="id" type="var">imp1.ml</span></span> 的文件，其中包含了提取后的
<span class="inlinecode"><span class="id" type="var">ceval_step</span></span> 以及所有递归依赖的文件。编译本章对应的 <span class="inlinecode">.<span class="id" type="var">v</span></span>
文件，然后看看生成的 <span class="inlinecode"><span class="id" type="var">imp1.ml</span></span> 吧！
</div>
<div class="doc">
<a name="lab391"></a><h1 class="section">控制提取特定的类型</h1>
<div class="paragraph"> </div>
我们可以让 Coq 将具体的 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 定义提取为特定的 OCaml 类型。
对于每一个定义，我们都要指明：
<div class="paragraph"> </div>
<ul class="doclist">
<li> 该 Coq 类型应当如何用 OCaml 来表示，以及
</li>
<li> 该类型的构造子应如何转换为目标语言中对应的标识符。
</li>
</ul>
</div>
<div class="code code-tight">
<span class="id" type="var">Extract</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">bool</span> ⇒ "bool" [ "true" "false" ].<br/>
</div>
<div class="doc">
对于非枚举类型（即构造器接受参数的类型），我们需要给出一个 OCaml
表达式来作为该类型元素上的“递归器”。（想想丘奇数。）
<div class="paragraph"> </div>
（译注：在这一部分，读者可以在为 <span class="inlinecode"><span class="id" type="var">nat</span></span> 指定对应的类型后使用
<span class="inlinecode"><span class="id" type="var">Extraction</span></span> <span class="inlinecode"><span class="id" type="var">plus</span></span> 来得到自然数加法的提取结果，以此加深对“递归器”的理解。）
</div>
<div class="code code-tight">
<span class="id" type="var">Extract</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">nat</span> ⇒ "int"<br/>
[ "0" "(fun x → x + 1)" ]<br/>
"(fun zero succ n →<br/>
if n=0 then zero () else succ (n-1))".<br/>
</div>
<div class="doc">
我们也可以将定义的常量提取为具体的 OCaml 项或者操作符。
</div>
<div class="code code-tight">
<span class="id" type="var">Extract</span> <span class="id" type="var">Constant</span> <span class="id" type="var">plus</span> ⇒ "( + )".<br/>
<span class="id" type="var">Extract</span> <span class="id" type="var">Constant</span> <span class="id" type="var">mult</span> ⇒ "( * )".<br/>
<span class="id" type="var">Extract</span> <span class="id" type="var">Constant</span> <span class="id" type="var">eqb</span> ⇒ "( = )".<br/>
</div>
<div class="doc">
注意：保证提取结果的合理性是<b>你的责任</b>。例如，以下指定可能十分自然：
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">Extract</span> <span class="id" type="var">Constant</span> <span class="id" type="var">minus</span> ⇒ "( - )".
<div class="paragraph"> </div>
</div>
但是这样做会引起严重的混乱。（思考一下。为什么会这样呢？）
</div>
<div class="code code-tight">
<span class="id" type="var">Extraction</span> "imp2.ml" <span class="id" type="var">ceval_step</span>.<br/>
</div>
<div class="doc">
检查一下生成的 <span class="inlinecode"><span class="id" type="var">imp2.ml</span></span> 文件，留意一下此次的提取结果与 <span class="inlinecode"><span class="id" type="var">imp1.ml</span></span>
有何不同。
</div>
<div class="doc">
<a name="lab392"></a><h1 class="section">一个完整的示例</h1>
<div class="paragraph"> </div>
为了使用提取的求值器运行 Imp 程序，我们还需要一个小巧的驱动程序
来调用求值器并输出求值结果。
<div class="paragraph"> </div>
为简单起见，我们只取最终状态下前四个存储空间中的内容作为程序的结果。
（译注：这里的存储空间指作为状态的 <span class="inlinecode"><span class="id" type="var">map</span></span>。）
<div class="paragraph"> </div>
为了更方便地输入例子，我们将会从 <span class="inlinecode"><span class="id" type="var">ImpParser</span></span> 模块中提取出语法解析器。
首先需要正确建立 Coq 中的字符串与 OCaml 中字符列表的对应关系。
</div>
<div class="code code-tight">
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ExtrOcamlBasic</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ExtrOcamlString</span>.<br/>
</div>
<div class="doc">
我们还需要翻译另一种布尔值：
</div>
<div class="code code-tight">
<span class="id" type="var">Extract</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">sumbool</span> ⇒ "bool" ["true" "false"].<br/>
</div>
<div class="doc">
提取指令是相同的。
</div>
<div class="code code-tight">
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Imp</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ImpParser</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
<span class="id" type="var">Extraction</span> "imp.ml" <span class="id" type="var">empty_st</span> <span class="id" type="var">ceval_step</span> <span class="id" type="var">parse</span>.<br/>
</div>
<div class="doc">
现在我们来运行一下生成的 Imp 求值器。首先你应该阅览一下
<span class="inlinecode"><span class="id" type="var">impdriver.ml</span></span>（这并非从某个 Coq 源码提取而来，它是手写的。）
<div class="paragraph"> </div>
然后用下面的指令将求值器与驱动程序一同编译成可执行文件：
<pre>
ocamlc -w -20 -w -26 -o impdriver imp.mli imp.ml impdriver.ml
./impdriver
</pre>
（编译时所使用的 <span class="inlinecode">-<span class="id" type="var">w</span></span> 开关只是为了避免输出一些误报的警告信息。）
</div>
<div class="doc">
<a name="lab393"></a><h1 class="section">讨论</h1>
<div class="paragraph"> </div>
由于我们证明了 <span class="inlinecode"><span class="id" type="var">ceval_step</span></span> 函数的行为在适当的意义上与 <span class="inlinecode"><span class="id" type="var">ceval</span></span>
关系一致，因此提取出的程序可视作<b>已验证的</b> Imp 解释器。
当然，我们使用的语法分析器并未经过验证，因为我们并未对它进行任何证明！
</div>
<div class="doc">
<a name="lab394"></a><h1 class="section">更进一步</h1>
<div class="paragraph"> </div>
有关提取的更多详情见<b>软件基础</b>第三卷<b>已验证的函数式算法</b>中的
Extract 一章。
</div>
<div class="code code-tight">
<span class="comment">(* Sun Jul 7 18:59:02 UTC 2019 *)</span><br/>
</div>
</div>
</div>
</body>
</html>