Вы можете использовать предопределенную функцию max, которая принимает набор целых чисел в качестве входных данных и возвращает максимальное число. Входные значения здесь диапазон (совокупность всех значений) функции:
max(ran(f))
Пожалуйста, обратите внимание, что максимум не определен для пустых множеств.
Что касается вашего вопроса о рекурсии или циклах: вы можете фактически определить функцию рекурсивно, но я думаю, что ваш вопрос больше нацелен на то, чтобы вычислить что-то. Это нелегко выразить в Z, и это ИМО - хорошая вещь, потому что она используется для спецификаций, и это не язык программирования. Даже если не будет 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. В более сложных сценариях может быть даже не очевидно, что определенное отношение является функцией вообще, потому что в зависимости от выбранных элементов могут быть вычислены разные результаты.