找到函数的最小不动点答案

【问题标题】：Find least fixpoint of a function找到函数的最小不动点
【发布时间】：2016-12-20 11:15:00
【问题描述】：

如果我有这个 Haskell 函数：

考虑以下 Haskell 函数 f ：
f :: Int -> Int
f 0 = 1
f x = x * x * f (x - 1)

那我该如何计算它的fixpoint和least fixpoint（封闭形式）？

这个问题的答案是：

这个最小固定点是如何计算的？我试图理解这一点，但仍然没有运气。如果有人可以向我解释这一点，那就太好了。

【问题讨论】：

正如贴出的那样，由于功能严格，所以它是底部。但我猜你可能实际上想要相关函数\f n -> case n of 0->1 ; x->x*x*f(x-1) 的最小不动点，它的类型为(Int -> Int) -> (Int -> Int)，并且有一个非平凡的最小不动点。
不是 1 吗？ f 1 = 1 * 1 * f(0) = 1。在所有其他整数上，f x 与 x 不同，因此 1 是唯一的固定点。
@WaqarAhmed 假设您在作为 CPO 的语义域中工作，您知道要找到最小固定点，您可以从底部元素开始并向上走。因此，在 chi 的代码中输入 f=undefined 并最终得到 \n -> case n of 0-> 1; x -> x*x*undefined (x-1)，这是 1 时 n=0 的函数，否则未定义。现在将此函数设置为f，在0 和1 等情况下，你最终得到的函数都是1。最后，最小不动点是极限：这只是常数函数1 如 V. Semeria 所述。
@WaqarAhmed 确实我错了。考虑当我们有f 0 = 1 和f 1 = 1 而f x = undefined 的情况。现在我们最终得到case n of 0 -> 1; x -> x*x*f(x-1)，对于n=0, 1，它是1，但对于n=2，它是4（因为2*2*f(1) = 2*2*1=4），对于n>2，它是未定义的。在下一步中，您将得到3*3*f(2) = 3*3*4 = 36 等。每次迭代都将f 定义为n 的下一个值n**2 * f(n-1)。 ! 表示 factorial 5! = 5*4*3*2*1 并且由于我们总是将平方相乘，我们最终得到 (n!)**2 = (n*(n-1)*(n-2)*...*1) *(n*(n-1)*(n-2)*...*1) = n**2*(n-1)**2 * (n-2)**2*...*1**2
@V.Semeria 确实1是一个定点；但它并不是标准排序中的最少个固定点，将底部置于1 之下（以及所有其他完全定义的Ints 之下，它们彼此无法比较）。

标签： haskell semantics fixpoint-combinators

【解决方案1】：

不难看出

f x = x * x * f (x-1)
    = x * x * ((x-1) * (x-1) * f (x-2))
    = x * x * ((x-1) * (x-1) * ((x-2) * (x-2) * f (x-3)))
    = ...
    = x * x * ((x-1) * (x-1) * ((x-2) * (x-2) * ... * 1)))

现在在 cmets 中回答您的问题，即当递归结果 f (x-1) 不是平方时，这如何等同于给定公式 (x!)^2，只需重新排列上述因素，使用 (*) 的关联性和交换性而不是 @ 987654325@：

      x * x * ((x-1) * (x-1) * ((x-2) * (x-2) * ... * 1)))
    = x * x * (x-1) * (x-1) * (x-2) * (x-2) * ... * 1
    = (x * (x-1) * (x-2) * ... * 1) * (x * (x-1) * (x-2) * .. * 1)
    = x!                            * x!
    = (x!)^2

【讨论】：