Z 符号：序列序列 - 求和

问题描述

我只想说这是一个大学项目。我不希望得到答案，而希望得到更多的“提示”。

我有一个超市的架构，其中包含一系列队列：

+-- Supermarket-------
|queues: seq Queue
----------------------

这是我定义队列的方式：

+-- Queue ----------
|length: ℕ
--------------------

我希望定义一个模式来返回排队等候的客户总数。到目前为止，我有：

+--TotalQueueCustomers----
|Ξsupermarket: Supermarket
|totalCustomers!: ℕ
|-------------------------
|totalCustomers = total θ supermarket
--------------------------

我正在努力定义 total 函数。它需要“循环”每个队列中的每个客户并对他们的 length 求和。这是我目前所拥有的：total = q: Queue ⦁ q.length ↦ q.length

有什么想法吗？

解决方法

您可以通过使用基本情况（无队列）并指定如何计算附加队列来归纳地定义函数：

total: seq Queue → ℕ
---
total(∅) = 0
∀ q: Queue; qs: seq Queue ⦁ total( <q> ^ qs ) = q.length + total(qs)

<q> 是具有单个元素 q 的序列，a ^ b 表示序列连接运算符（Z 参考手册的第 4.5 节）。

（请注意：我没有用 Z 类型检查器检查这个例子，所以它可能包含某种语法错误 - 但这个想法应该很清楚）