Блог

Позвольте мне просто сказать, что это для университетского проекта. Я не ожидаю ответа, а скорее «подсказки».

У меня есть схема супермаркета, которая содержит последовательность очередей:

  -- 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 обозначает оператор конкатенации последовательности (раздел 4.5 справочного руководства по Z).

(Пожалуйста, обратите внимание: я не проверял этот пример с помощью средства проверки типов Z, поэтому он, вероятно, содержит какую-то синтаксическую ошибку — но идея должна быть ясна)