Вернуть наибольшее или наименьшее значение Z, формальный метод

Question

Я новичок в Z записи,

Допустим, у меня есть функция f, определенная как X |-> Y, где X - строка, а Y - число.

Как я могу получить наибольшее значение Y в этой функции? Существует ли "цикл" в формальном методе, чтобы я мог решить его с помощью цикла?

Я знаю, что в нотации Z есть рекурсия, но, основываясь на предоставленном материале, я обнаружил, что она применима только в мультимножестве или сумке, может ли она применяться в функции?

Любое дополнительное ссылочное приложение 'loop' или приложение рекурсии будет оценено. Извините за мой английский.

Answer 1

Вы можете просто использовать предопределенную функцию max который принимает набор целых чисел в качестве входных данных и возвращает максимальное число. Входными значениями здесь являются диапазон (набор всех значений) функции:

max(ran(f))

Обратите внимание, что максимум не определен для пустых наборов.

Что касается вашего вопроса о рекурсии или циклах: вы на самом деле можете определить функцию рекурсивно, но я думаю, что ваш вопрос направлен больше на способ вычисления чего-либо. Это нелегко выразить в Z, и это хорошо для IMO, потому что оно используется для спецификаций и не является языком программирования. Даже если бы не было max или же ran функция, вы все равно можете указать номер m вы ищете по:

\exists s:String @ (s,m):f /\
  \forall s2:String, i2:Z @ (s2,i2):f ==> i2 <= m

(" m это значение f принадлежащих к s и все остальные ценности i2 из f меньше или равны ")

После привыкания к стилю его обычно лучше понять, чем любой другой язык программирования (за исключением того, что вы пытаетесь описать сам алгоритм, а не его ожидаемый результат).#

Просто для справки: пример рекурсивного определения (назовем его rmax) для максимума будет состоять из базового варианта:

\forall e:Z @ rmax({e}) = e

и рекурсивный случай:

\forall e:Z; S:\pow(Z) @
    S \noteq {} \land
    rmax({e} \cup S) = \IF e > rmax(S) \THEN e \ELSE rmax(S)

Но учтите, что это все еще не "правило вычисления" rmax так как e во втором правиле может быть произвольный элемент S, В более сложных сценариях может даже не быть очевидным, что определенное отношение вообще является функцией, потому что в зависимости от выбранных элементов могут быть вычислены разные результаты.