queue

【中文名】队列（中国和台湾译名一致）

可以很形象地想象一群排队的人，很有持续，最早排队的人，在最前面，最早办事，最早离开，所谓先进先出（LILO, first-in, first-out）是也。

【定义】队列是这样一个数据集合：只能访问到最早加入的元素。换句话说，要访问晚一点的元素，得把前面的都移走。基本操作是 add （在队列尾部 rear 添加元素，也称 enqueue），和 delete （在队列头部 front 删除元素，也称 dequeue）。所谓队列的头部(head)，就是第一个元素的位置，尾部(tail)是指最后一个元素的位置。

【操作定义】通过 remove, new 操作能很方便定义 delete (dequeue) 操作。基于公理语义学所有操作定义如下：

1. new() returns a queue
2. front(add(v, new())) = v
3. remove(add(v, new())) = new()
4. front(add(v, add(w, Q))) = front(add(w, Q)) // 这里我的理解是，括号的执行顺序从外到内，才能满足
5. remove(add(v, add(w, Q))) = add(v, remove(add(w, Q))) // 注解同上

注：Q 表示队列，v 和 w 都表示值。

【参考】

• http://xlinux.nist.gov/dads/HTML/queue.html
• http://zh.wikipedia.org/wiki/隊列