我正在阅读一本介绍形式验证算法和 Haskell Discrete Mathematics with Haskell 的书，在那里我发现了一个归纳定义函数的反例：
f91 :: Int -> Int
f91 x = if x > 100
then x - 10
else f91 . f91 $ x + 11
如果参数范围在 0 到 100 之间，这个递归函数承诺返回 91：我希望有人能向我解释这个递归函数的算法是如何工作的。
你见过麦卡锡 91 函数吗？
假设您从一个 value 开始x > 100，那么结果很简单x - 10，因此是一个91以后的 value 。
现在假设值是 from90到100。然后f91取else分支并x + 11在101和之间111。第一个f91应用程序将所有值带到范围内91 - 101；只101满足 的then第二个应用的分支，f91因此结果 ( x - 10) 是91。
对于所有其他值，我们得到的范围内102 - 111的else分支。但是else分支适用f91 . f91于该值；由于所有值都是> 100，第一个f91将值降低到92 - 101，其中仅101通过> 100第二个的条件f91并变为91。
其余的值经过相同的循环，直到全部变为91。假设您在11下面有不同的值区间100。第f91一个使该区间高于该区间100，然后91以相同的方式从区间的较高端开始不断减小值。请参阅维基百科页面中链接的归纳证明。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句