显示集成收缩限制的示例

Example that shows the limitations of integrated shrinking

我刚刚看到 a video that presents the notion of integrated shrinking for property based tests. The approach seems to have some advantages over type directed shrinking, however it was pointed out in this reddit thread 集成收缩方法不适合单子生成器的情况:

Doing shrinking in your way does not fit well with a monadic style for generators. Here is an example, consider generating an arbitrary list (ignore termination for now):

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

Now, the default behavior of your shrinking would first shrink x (holding xs constant), and then shrink xs (holding x constant), which severely limits the shrinking (the concept of local minimum is now a lot less strong).

我把上面的评论读成"integrated shrinking might fail to provide a global minimum counter example"。但是,由于 hedgehog 似乎能够找到列表中失败属性的最小反例,我想知道是否有一个示例可以显示上面引用中指出的缺点。

用微积分术语来说,问题是您没有遵循负梯度(最速下降),而是首先沿一个轴最小化,然后沿另一个轴最小化。基于这个类比,很容易想出至少一个人为的例子——考虑函数

-- 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)

See plot on WolframAlpha.

我们正在针对 属性 f x y > 0 对其进行测试,假设一个最小的示例将有一个最接近原点 (0, 0) 的点。根据您首先开始收缩的位置,您完全有可能最终接近 (±1, 0),因为您先调整 x,然后不允许 y 有太大变化。但是,在理想情况下,您希望最终接近 (0, ±1/2) 以满足最小标准。

仅供参考,这里有一个涉及列表的例子:

{-# 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)]

所以hedgehog有时会return作为列表( [ 1 , 1 , 1 , 1 ], [])的反例。然而 ([], []) 是一个较小的反例(有时 hedgehog 也会报告)。 

在这种情况下,违反属性的条件是:

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

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