0

我是 Z 表示法的新手，

假设我有一个函数 f 定义为 X |--> Y ，其中 X 是字符串，Y 是数字。

如何在此函数中获得最高 Y 值？形式方法中是否存在“循环”，所以我可以使用循环来解决它？

我知道 Z 表示法中有递归，但根据提供的材料，我发现它只适用于 multiset 或 bag，它可以适用于函数吗？

“循环”或递归应用程序的任何额外参考应用程序将不胜感激。对不起我的英语不好。

4

1 回答 1

1

您可以只使用max将一组整数作为输入并返回最大数的预定义函数。这里的输入值是函数的范围（所有值的集合）：

max(ran(f))

请注意，没有为空集定义最大值。

关于您关于递归或循环的问题：您实际上可以递归地定义一个函数，但我认为您的问题更多地针对一种计算方法。这在 Z 中不容易表达，这是 IMO 的一件好事，因为它用于规范，而不是编程语言。即使没有maxorran函数，您仍然可以通过以下方式指定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。在更复杂的场景中，定义的关系可能根本不是一个函数，因为根据选择的元素可以计算出不同的结果。

于 2016-02-18T05:56:48.160 回答