第七章 理论的设计和实现
编程语言的设计者与实现者已经创建了形式化，抽象，理论和结构，程序员则使用这些对象。
随着程序的写成，随着引入了名称，程序员创建了新的形式化，新的抽象，理论和结构。
为了让他们的创建物更加地优雅和有用，程序员应该注意到的是他们的角色是理论的使用者
如同理论的设计者和实现者。
栈和队列和树是标准的数据结构，在编程中使用得非常频繁。在本章中，使用应用来
显示这些数据结构的有用性不是目的；我们这个任务留给数据结构的书籍。这些数据
结构出现在这里，是在理论的设计与实现中，作为案例来研究的。这些数据结构中
的每一个都包括了一些项。例如，我们能够对数使用栈，对二进制数的列表使用栈，
甚至是对栈使用栈。在这一章中，X是在数据结构中的项的束（或者是类型）。
7.0 数据理论
7.0.0 数据栈理论
对于编程语言的实现来说，栈是一个非常有用的数据结构。它的特性是在任何
一个时刻，被检索到的或者是删除的，都是保留的项中最新的那一个。
它是一个有理念的结构：最后一个进栈的，是最先一个出栈的。
我们引入了语法 stack , empty , push , pop , 和 top 。非形式化
地说它们的含义如下：
stack 包括了所有的类型为X的栈的元素的束
empty 栈中没有元素
push 这是一个功能，向栈中压入一个新的元素
pop 这是一个功能，向栈外弹出一个最新的元素
top 这是一个功能，得到栈中的最新的一个元素
这里有最开始的四个公理
empty: stack
push: stack→X→stack
pop: stack→stack
top: stack→X
我们需要 empty 和 push 成为栈的组装子。我们用pop
得到栈的一个元素，我们不需要pop成为栈的组装子。一个
组装的公理能以如下的两个方式写出来：
empty, push stack X: stack
P empty ∧ ∀s: stack· ∀x: X· Ps ⇒ P(push s x) ⇐ ∀s: stack· Ps
push被允许对束的并有分配律，还有 P: stack→bin 。为了排除栈的没有
的元素，要求有一个推演公理，它能以许多的方式写出来；这里有两个：
empty, push B X: B ⇒ stack: B
P empty ∧ ∀s: stack· ∀x: X· Ps ⇒ P(push s x) ⇒ ∀s: stack· Ps
根据我们已经有的公理，所有的栈可能都是相同的。为了说明组装子总是能
组装出不同的栈，还要求有两个公理。令s和t是栈的元素，令x和y是X的元素；
那么
push s x empty
push s x = push t y = s=t ∧ x=y
最后，这两个公理是需要的，它说明栈的行为是“后进先出的”
pop (push s x) = s
top (push s x) = x
这就完成了数据的栈的公理了。
数据栈的理论允许我们声明我们要的许多的变量，并且根据公理在表达式中
使用它们。我们能够声明变量a,b，它们的类型是栈，然后写赋值语句
a:= empty 和 b:= push a 2 。
7.0.1 数据栈实现
如果你需要一个栈，在你的编程语言中却没有提供栈，你将不得不使用
已经提供的数据结构来构建你自己的栈。假定列表和函数是已实现的。
那么，通过如下的定义，我们能够实现一个整数的栈。
stack = [*int]
empty = [nil]
push = 〈s: stack→〈x: int→s+[x]〉〉
pop = 〈s: stack→if s=empty then empty else s [0;..#s–1] fi〉
top = 〈s: stack→if s=empty then 0 else s (#s–1) fi〉
为了证明一个理论是被实现的，我们证明
(理论的公理) ⇐ (实现的定义)
换句话说，定义必须满足公理。根据一个分配律，这能够一次成为公理。
例如，最后一个公理变成了
top (push s x) = x
= top (〈s: stack→〈x: int→s+[x]〉〉 s x) = x 替换了push
= top (s+[x]) = x 应用了函数
= 〈s: stack→if s=empty then 0 else s (#s–1) fi〉 (s+[x]) = x 替换了pop
= if s+[x]=[nil] then 0 else (s+[x]) (#(s+[x])–1) fi = x 应用了函数和替换empty
= (s+[x]) (#s) = x 简化了if 和索引
= x = x 索引列表
= T 应用了反身律
栈理论是有一致性的吗？因为我们使用列表的理论实现了它，我们知道
如果列表的理论是一致的，所以栈理论也是一样的。栈是完备的吗？
为了展示一个二进制的表达式是未分类的，我们必须实现栈两次，在一个
栈中让表达式是真命题，在另一个栈中，它是假命题。表达式如下：
pop empty = empty
top empty = 0
在这个实现中是真命题，但是我们能改变实现如下：
pop = 〈s: stack→if s=empty then push empty 0 else s [0;..#s–1] fi〉
top = 〈s: stack→if s=empty then 1 else s (#s–1) fi〉
使得它们是假命题。所以栈理论是不完备的。
栈理论规定了栈的属性。一个人实现了栈，必须确保这些属性都被提供了。
一个使用栈的人必须确保仅有这些属性被依赖。这一点要强调：一个理论是
双方之间的一个合同，他们是实现者和用户。这个合同让每一方清楚了自己的
义务和可能期望的收益。如果有事出错了，它要让是谁出错了这件事是清清
楚楚的。一个理论让一方修改自己的程序而不用知道另一方的程序是如何写的，
成为了可能。在大规模的软件系统的构建上，这是一个必要的原则。在我们
的小例子中，栈的用户不必使用 pop empty =empty ，甚至不知道栈的实现者
提供了它；如果用户需要它，它应该被加入到理论中。
7.0.2 简单数据栈理论
在数据栈的理论中，仅展示了，我们有公理 empty:stack 和 pop:stack→stack；
从这些公理，我们能够证明 pop empty:stack。换句话说，弹出一个空栈，得到了
一个栈，尽管我们不知道它是什么。一个实现者有义务为Pop empty 得到一个栈，
尽管我们不在乎它是什么。如果我们不要弹出一个空栈，那么理论是太强了。我们
应该弱化公理 pop:stack→stack 并且 取消实现者提供这个不要的东西的义务。
更弱一点的公理是：
s empty ⇒ pop s: stack
它说的是弱出一个非空的栈是一个栈，但是其它的公理用了它，所以是不必要的。
相似的是 empty:stack 和 top:stack→X 我们能够证明 top empty:X;
删除公理 top:stack→X 来取消实现者提供一个不必要的结果。
我们可能决定我们关于所有的栈不需要证明所有的公理，也不需要栈的推演。
稍后，我们可能意识到我们根本不需要一个空栈，也不需要测试栈的空。我们
能够总是用一个栈的顶，在大部分的时候，我们都是这么做的。我们能删除公理
empty:stack 和所有的提及empty。我们必须替换这个公理，用一个更弱的公理
stack 不等于 Null,所以我们仍然要声明栈的类型。如果我们要测试一个栈是否为
空，我们能向栈中压入一些特殊的值，这些值不会再压入栈，空性的测试就成了
对栈顶是否是特殊值的测试。
对于大部分的目的，这是足够的，把项压入栈，弹出栈，查看栈顶。我们需要的
理论比之前展示的要简单一些。我们的简单的数据栈理论引入了stack,push,pop
和top ，带有如下的四个公理： 令s是栈的一个元素，令x是X的一个元素; 那么
stack null
push s x: stack
pop (push s x) = s
top (push s x) = x
对于学习栈的目的，作为一个数学的活动，我们要最强的公理来证明尽可能得多。
作一个工程师的活动，理论的设计是一个排除了所有的不想要的实现，仅允许其它
内容的艺术。设计一个强于需要的理论是反生产力要求的，它使得实现更加困难，
它使得理论的扩展更加困难。
