1

我刚刚观看了一个视频，该视频介绍了基于属性的测试的集成收缩概念。该方法似乎比类型定向收缩具有一些优势，但是在此 reddit 线程中指出，集成收缩方法不适用于单子生成器：

以您的方式进行收缩并不适合生成器的一元样式。这是一个示例，考虑生成一个任意列表（暂时忽略终止）：

do x <- arbitrary
   xs <- arbitrary
   return (x:xs)

现在，收缩的默认行为将首先收缩 x（保持 xs 不变），然后收缩 xs（保持 x 不变），这严重限制了收缩（局部最小值的概念现在不那么强大了）。

我将上述评论读为“集成收缩可能无法提供全局最小反例”。但是，由于hedgehog似乎能够为列表上的失败属性找到最少的反例，我想知道是否有一个示例可以显示上面引用中指出的缺点。

4

2 回答 2

2

在微积分术语中，问题在于您没有遵循负梯度（最陡下降），而是首先沿 1 个轴最小化，然后沿另一个轴最小化。基于这个类比，很容易想出至少一个人为的例子——考虑函数

-- f x y = ((x^2 - 1)^2 - 0.2*x) * ((y^2 - 1/2)^2 - 0.1*y)
f x y = (x^4 - 2.2*x^2 + 1) * (y^4 - 1.1*y^2 + 1/4)

参见 WolframAlpha 上的图。

我们正在测试它的属性f x y > 0，假设一个最小的例子有一个最接近原点的点(0, 0)。根据你第一次开始收缩的地方，你完全有可能最终接近，(±1, 0)因为你x先调整然后不允许y改变太多。但是，在理想情况下，您希望最终到达接近(0, ±1/2)满足最小标准的某个地方。

于 2019-01-29T00:45:07.727 回答
0

仅供参考，这里是一个涉及列表的示例：

{-# LANGUAGE OverloadedStrings #-}

module Main where

import Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range

notLargeOrBothNotEmpty :: Property
notLargeOrBothNotEmpty = property $ do
  xs <- forAll randomIntLists
  ys <- forAll randomIntLists
  assert $ length xs < 4 && (xs /= [] && ys /=[])
  where
    randomIntLists = Gen.frequency
      [ (1, Gen.list (Range.constant 0 1) randomInt)
      , (10, Gen.list (Range.constant 1 100) randomInt)
      ]
    randomInt = Gen.integral (Range.constat 1 10)

main :: IO Bool
main = checkParallel $ 
  Group "Test.Example" [("Produce a minimal counter-example", notLargeOrBothNotEmpty)]

所以刺猬有时会返回列表作为反例( [ 1 , 1 , 1 , 1 ], [])。然而([], [])，是一个较小的反例（有时也由 报告hedgehog）。</p>

在这种情况下，违反属性的条件是：

4 <= length xs || (xs == [] && ys == [])

如果最初找到一个反例，其中ys /= []和4 <= length xs，集成收缩方法将首先尝试收缩xs，然后继续收缩ys保持xs不变，如我在原始问题中引用的帖子中所述。

于 2019-01-29T20:39:39.233 回答