# SK logic in egglog: part 3, falsifying myself

Posted on by Chris Warburton

Update: part 4 is here

In the previous part we learned some background theory about SK logic, and built up our notion of equality from simple identity (`==`), through equivalence of `Normal` forms (`normalEq`) up to full extensional equality (`extEq`). In this post we’ll investigate these definitions more thoroughly. Whilst the eventual aim is to find the mistake I’d made in egglog, the best path forward is to question and test our understanding as a whole.

## False confidence

The properties we’ve written so far give us some confidence that our definitions make sense, and our theory of their behaviour holds up, since falsify was unable to disprove anything with a counterexample. However, our confidence shouldn’t be too high, since most of those properties have two branches: the situation we care about, and a fallback which is trivially `True`. If the former is quite rare, finding no counterexamples may not tell us very much.

For example, consider `agreeOnExtensionalInputs (n, x, y, inputs)`, which asserts that whenever `extensionalInputs` claims `x` and `y` are extensionally equal for `i` symbolic inputs, they agree on any sequence of `i` concrete input values. This assertion has many caveats:

• Unless `x` and `y` are extensionally equal, or happen to match a form that `provablyDisagree` can recognise, then `extensionalInputs x y` will never finish. In that case we are merely asserting the fallback of `runDelayOr True`, not learning anything about extensional equality.
• In those cases that `extensionalInputs x y` would finish, it must take no more than `n` steps to avoid that fallback.
• When `x` and `y` `provablyDisagree`, `extensionalInputs` gives `Nothing` and we’re merely asserting the other fallback: `Now True`.
• When `extensionalInputs` gives `Just 0`, `x` and `y` are `normalEq`, so our assertion overlaps with other properties we’ve already established.

None of these make the property false; but they weaken the evidence that it provides. We can see this more clearly by “labelling” each situation, and having `falsify` report statistics on how common each was. Unfortunately this requires us to return more than just a `Bool`, so we need to leave the world of simple predicates (and hence cross-framework compatibility). Every property-checker provides its own alternative implementations for such features: in `falsify` it’s the `Property` type. Here’s a pretty direct translation of `agreeOnExtensionalInputs` as a `Property`, with each of the above cases labelled:

``````agreeOnExtensionalInputsStats g =
testProperty "agreeOnExtensionalInputs" \$ do
(n, x, y, ins) <- gen g
let check Nothing  = Now (Left "Not equal")
check (Just i) = Right . (i,) . same <\$> sAt i (agree x y ins)
label "Identical" [show (x == y)]
case runDelayOr (Left "Timeout") (extensionalInputs x y >>= check) n of
Left msg         -> label "result" [msg]
Right (i, True ) -> label "i" [show i] *> label "result" ["True"]
Right (i, False) -> fail ("Disagree on " ++ show (sTake i ins))

-- | Split the first 'n' elements off a 'Stream'.
sSplitAt :: Integral n => n -> Stream a -> ([a], Stream a)
sSplitAt = go []
where go acc n         xs | n <= 0 = (reverse acc, xs)
go acc n (Cons x xs)         = go (x:acc) (n - 1) xs

-- | Take the first 'n' elements of a 'Stream' as a list.
sTake :: Natural -> Stream a -> [a]
sTake n = fst . sSplitAt n``````
``````main = defaultMain (agreeOnExtensionalInputsStats
(tuple4 genFuel genCom genCom genComs))``````
``````agreeOnExtensionalInputs: OK (0.13s)
100 successful tests

Label "Identical":
98.0000% False
2.0000% True

Label "i":
8.0000% 0

Label "result":
14.0000% Not equal
78.0000% Timeout
8.0000% True

All 1 tests passed (0.13s)
``````

The results will vary depending on the random seed (which changes every time this page gets rendered), but I’ve seen around ⅓ resulting in `Timeout`, around ⅗ with `Not equal`, and only a handful resulting in `True`. Most of the latter agree on 0 inputs, making them `normalEq` and hence bypassing the use of symbolic execution. The only good news is that `x` and `y` were hardly ever identical!

Here are similar results for other properties (their definitions are hidden in the following fold-out section, since the logic hasn’t changed):

Labelled properties…
``````notUnnormalEqToItselfStats g =
testProperty "notUnnormalEqToItself" \$ do
(n, x) <- gen g
case runDelayOr Nothing (Just <\$> normalEq x x) n of
Nothing           -> label "result" ["Timeout"]
Just (Same _)     -> label "result" ["True"   ]
Just (Diff x' y') -> fail (show x' ++ " =/= " ++ show y')

normalEqImpliesAgreeStats g =
testProperty "normalEqImpliesAgree" \$ do
(n, f, g, xs) <- gen g
case runDelay n (tuple2 (normalEq f g) (sHead (agree f g xs))) of
Now got@(Same _  , Diff _ _) -> fail (show got)
Now     (Same _  , Same _  ) -> label "result" ["Same Same"]
Now     (Diff _ _, Same _  ) -> label "result" ["Diff Same"]
Now     (Diff _ _, Diff _ _) -> label "result" ["Diff Diff"]
Later   _                    -> label "result" ["Timeout"  ]

skNeverDisagreesWithSKSKKKStats g =
testProperty "skNeverDisagreesWithSKSKKK" \$ do
(n, xs) <- gen g
let f = App s k
g = App (App s (App k (App s k))) (App k k)
case runDelayOr Nothing (Just <\$> sAt (2 + n) (agree f g xs)) n of
Nothing             -> label "result" ["Timeout"]
Just     (Same _  ) -> label "result" ["True"]
Just got@(Diff _ _) -> fail (show got)

agreementIsMonotonicStats g =
testProperty "agreementIsMonotonic" \$ do
((n, m), (f, g), xs) <- gen g
case runDelay n (tuple2 (sAt  n      (agree f g xs))
(sAt (n + m) (agree f g xs))) of
Now got@(Same _  , Diff _ _) -> fail (show got)
Now     (Same _  , Same _  ) -> label "result" ["Same Same"]
Now     (Diff _ _, Same _  ) -> label "result" ["Diff Same"]
Now     (Diff _ _, Diff _ _) -> label "result" ["Diff Diff"]
Later   _                    -> label "result" ["Timeout"  ]

normalEqImpliesEverAgreeStats g =
testProperty "normalEqImpliesEverAgree" \$ do
(n, x, y) <- gen g
let go d = runDelayOr Nothing (Just <\$> d)
case (go (same <\$> normalEq x y) n, go (everAgree x y) (triangle n)) of
(Nothing   , _         ) -> label "result" ["Timeout"]
(Just False, _         ) -> label "result" ["Unequal"]
(Just True , Just True ) -> label "result" ["True"   ]
(Just True , Nothing   ) -> fail "everAgree timed out"
(Just True , Just False) -> fail "Didn't agree"

commuteStats f g = do
(x, y) <- gen g
case (f x y, f y x) of
(True , True ) -> label "result" ["Both"   ]
(False, False) -> label "result" ["Neither"]
(True , False) -> fail "f(x, y) but not f(y, x)"
(False, True ) -> fail "f(y, x) but not f(x, y)"

unequalArgCountCommutesStats =
testProperty "unequalArgCountCommutes" .
commuteStats unequalArgCount

provablyDisagreeCommutesStats =
testProperty "provablyDisagreeCommutes" .
commuteStats provablyDisagree

symbolGivenUnequalArgsCommutesStats g =
testProperty "symbolGivenUnequalArgsCommutes" \$ do
(f, x, y) <- gen g
commuteStats (liftFun2 symbolGivenUnequalArgs f) (pure (x, y))

extEqGeneralisesEqAndNormalEqAndEverAgreeStats g =
testProperty "extEqGeneralisesEqAndNormalEqAndEverAgree" \$ do
(n, x, y) <- gen g
let go l d = case runDelay n d of
Now   b -> label l [show b   ] >> pure (Just b)
Later _ -> label l ["Timeout"] >> pure Nothing
ext <- go     "extEq" (            extEq x y)
evr <- go "everAgree" (        everAgree x y)
nml <- go  "normalEq" (same <\$> normalEq x y)
eql <- go     "equal" (pure  \$      (==) x y)
case ext of
Nothing    -> label "result" ["Timeout"]
Just True  -> label "result" ["Equal"  ]
Just False -> case (evr, nml, eql) of
(Just True, _        , _        ) -> fail "everAgree but not extEq"
(_        , Just True, _        ) -> fail  "normalEq but not extEq"
(_        , _        , Just True) -> fail        "== but not extEq"
(_        , _        , _        ) -> label "result" ["Unequal"]``````
``````main = defaultMain \$ testGroup "Stats"
[ notUnnormalEqToItselfStats
(tuple2 genFuel genCom)

, normalEqImpliesAgreeStats
(tuple4 genFuel genCom genCom genComs)

, skNeverDisagreesWithSKSKKKStats
(tuple2 genFuel genComs)

, agreementIsMonotonicStats
(tuple3 (tuple2 genFuel genFuel) (tuple2 genCom genCom) genComs)

, normalEqImpliesEverAgreeStats
(tuple3 genFuel genCom genCom)

(tuple2 genSymCom genSymCom)

, unequalArgCountCommutesStats
(tuple2 genSymCom genSymCom)

, symbolGivenUnequalArgsCommutesStats
(tuple3 (Gen.fun (Gen.bool False)) genSymCom genSymCom)

, provablyDisagreeCommutesStats
(tuple2 genSymCom genSymCom)

, agreeOnExtensionalInputsStats
(tuple4 genFuel genCom genCom genComs)

, extEqGeneralisesEqAndNormalEqAndEverAgreeStats
(tuple3 genFuel genCom genCom)
]``````
``````Stats
notUnnormalEqToItself:                     OK (0.03s)
100 successful tests

Label "result":
5.0000% Timeout
95.0000% True
normalEqImpliesAgree:                      OK (0.07s)
100 successful tests

Label "result":
79.0000% Diff Diff
9.0000% Same Same
12.0000% Timeout
skNeverDisagreesWithSKSKKK:                OK (1.04s)
100 successful tests

Label "result":
100.0000% Timeout
agreementIsMonotonic:                      OK (0.93s)
100 successful tests

Label "result":
100.0000% Timeout
normalEqImpliesEverAgree:                  OK (0.05s)
100 successful tests

Label "result":
9.0000% Timeout
7.0000% True
84.0000% Unequal
100 successful tests

Label "result":
2.0000% Both
98.0000% Neither
unequalArgCountCommutes:                   OK (0.03s)
100 successful tests

Label "result":
100.0000% Neither
symbolGivenUnequalArgsCommutes:            OK (0.03s)
100 successful tests

Label "result":
100.0000% Neither
provablyDisagreeCommutes:                  OK (0.02s)
100 successful tests

Label "result":
2.0000% Both
98.0000% Neither
agreeOnExtensionalInputs:                  OK (0.13s)
100 successful tests

Label "Identical":
100.0000% False

Label "i":
7.0000% 0
1.0000% 1

Label "result":
11.0000% Not equal
81.0000% Timeout
8.0000% True
extEqGeneralisesEqAndNormalEqAndEverAgree: OK (0.24s)
100 successful tests

Label "equal":
98.0000% False
2.0000% True

Label "everAgree":
92.0000% Timeout
8.0000% True

Label "extEq":
12.0000% False
80.0000% Timeout
8.0000% True

Label "normalEq":
86.0000% False
6.0000% Timeout
8.0000% True

Label "result":
8.0000% Equal
80.0000% Timeout
12.0000% Unequal

All 11 tests passed (2.61s)
``````

Again, the exact distribution of these tests will vary from run to run; but I’ve seen some that always time-out, or never satisfy the required preconditions, etc. Sometimes this is a legitimate problem with our logic: for example, the properties `skNeverDisagreesWithSKSKKKStats` and `agreementIsMonotonic` always hit a timeout, since they are using the same `Fuel` parameter as the number of inputs and number of steps before timing out. We can avoid this by using separate parameters for each:

``````skNeverDisagreesWithSKSKKKFixed g =
testProperty "skNeverDisagreesWithSKSKKK" \$ do
(n, m, xs) <- gen g
let f = App s k
g = App (App s (App k (App s k))) (App k k)
case runDelayOr Nothing (Just <\$> sAt (2 + n) (agree f g xs)) (m + n) of
Nothing             -> label "result" ["Timeout"]
Just     (Same _  ) -> label "result" ["True"   ]
Just got@(Diff _ _) -> fail (show got)

agreementIsMonotonicFixed g =
testProperty "agreementIsMonotonic" \$ do
((i1, i2), n, (f, g), xs) <- gen g
case tuple2 (runDelay n (sAt  i1       (agree f g xs)))
(runDelay n (sAt (i1 + i2) (agree f g xs))) of
Now got@(Same _  , Diff _ _) -> fail (show got)
Now     (Same _  , Same _  ) -> label "result" ["Same Same"]
Now     (Diff _ _, Same _  ) -> label "result" ["Diff Same"]
Now     (Diff _ _, Diff _ _) -> label "result" ["Diff Diff"]
Later   _                    -> label "result" ["Timeout"  ]``````
``````main = defaultMain (skNeverDisagreesWithSKSKKKFixed
(tuple3 genFuel genFuel genComs))``````
``````skNeverDisagreesWithSKSKKK: OK (1.28s)
100 successful tests

Label "result":
78.0000% Timeout
22.0000% True

All 1 tests passed (1.28s)
``````
``````main = defaultMain (agreementIsMonotonicFixed
(tuple4 (tuple2 genFuel genFuel)
genFuel
(tuple2 genCom genCom)
genComs))``````
``````agreementIsMonotonic: OK (1.26s)
100 successful tests

Label "result":
2.0000% Diff Diff
98.0000% Timeout

All 1 tests passed (1.26s)
``````

Property-checkers, including `falsify`, allow us to “discard” uninteresting cases, which aborts the current call; generating another input to check instead. Discarded calls do not count towards the reported total, so they avoid the false confidence issue we saw above. The downside is that extra calls make the test slower; and it will be abandoned entirely if too many are discarded (for `falsify`, the default limit is 100 in a row). Depending on the property checker that may be considered a test failure: `falsify` only considers abandoned tests to have failed if there were no successful calls.

In the following fold-out section we refactor our properties again, to discard any branches that are “uninteresting”, like timeouts:

``````notUnnormalEqToItselfDiscard g =
testProperty "notUnnormalEqToItself" \$ do
(n, x) <- gen g
case runDelayOr Nothing (Just <\$> normalEq x x) n of
Just (Same _)     -> pure ()
Just (Diff x' y') -> fail (show x' ++ " =/= " ++ show y')

testProperty "normalEqImpliesAgree" \$ do
(n, f, g, xs) <- gen g
case runDelay n (tuple2 (normalEq f g) (sHead (agree f g xs))) of
Now got@(Same _  , Diff _ _) -> fail (show got)
Now     (Same _  , Same _  ) -> pure ()
Now     (Diff _ _, _       ) -> discard

testProperty "skNeverDisagreesWithSKSKKK" \$ do
(n, m, xs) <- gen g
let f = App s k
g = App (App s (App k (App s k))) (App k k)
case runDelayOr Nothing (Just <\$> sAt (2 + n) (agree f g xs)) (m + n) of
Just     (Same _  ) -> pure ()
Just got@(Diff _ _) -> fail (show got)

testProperty "agreementIsMonotonic" \$ do
((i1, i2), n, (f, g), xs) <- gen g
case tuple2 (runDelay n (sAt  i1       (agree f g xs)))
(runDelay n (sAt (i1 + i2) (agree f g xs))) of
Now got@(Same _  , Diff _ _) -> fail (show got)
Now     (Same _  , Same _  ) -> pure ()
Now     (Diff _ _, _       ) -> discard

testProperty "normalEqImpliesEverAgree" \$ do
(n, x, y) <- gen g
let go d = runDelayOr Nothing (Just <\$> d)
case (go (same <\$> normalEq x y) n, go (everAgree x y) (triangle n)) of
(Nothing   , _         ) -> discard
(Just False, _         ) -> discard
(Just True , Just True ) -> pure ()
(Just True , Nothing   ) -> fail "everAgree timed out"
(Just True , Just False) -> fail "Didn't agree"

testProperty "agreeOnExtensionalInputs" \$ do
(n, x, y, ins) <- gen g
let check Nothing  = pure discard
check (Just i) = pure . (i,) . same <\$> sAt i (agree x y ins)
if x == y
else do (i, b) <- runDelayOr discard (extensionalInputs x y >>= check) n
label "i" [show i]
if b
then pure ()
else fail ("Disagree on " ++ show (sTake i ins))

testProperty "extEqGeneralisesEqAndNormalEqAndEverAgree" \$ do
(n, x, y) <- gen g
let go l d = case runDelay n d of
Now   b -> label l [show b   ] >> pure (Just b)
Later _ -> label l ["Timeout"] >> pure Nothing
ext <- go     "extEq" (            extEq x y)
evr <- go "everAgree" (        everAgree x y)
nml <- go  "normalEq" (same <\$> normalEq x y)
eql <- go     "equal" (pure  \$      (==) x y)
case ext of
Just True  -> pure ()
Just False -> case (evr, nml, eql) of
(Just True, _        , _        ) -> fail "everAgree but not extEq"
(_        , Just True, _        ) -> fail  "normalEq but not extEq"
(_        , _        , Just True) -> fail        "== but not extEq"
(_        , _        , _        ) -> discard``````
``````main = defaultMain \$ testGroup "Discard"
(tuple2 genFuel genCom)

(tuple4 genFuel genCom genCom genComs)

(tuple3 genFuel genFuel genComs)

(tuple4 (tuple2 genFuel genFuel) genFuel (tuple2 genCom genCom) genComs)

(tuple3 genFuel genCom genCom)

(tuple4 genFuel genCom genCom genComs)

(tuple3 genFuel genCom genCom)
]``````
``````Discard
notUnnormalEqToItself:                     OK (0.04s)
normalEqImpliesAgree:                      OK (0.92s)
skNeverDisagreesWithSKSKKK:                OK (5.08s)
agreementIsMonotonic:                      FAIL (0.84s)

Use -p '/agreementIsMonotonic/' to rerun this test only.
normalEqImpliesEverAgree:                  OK (0.71s)
agreeOnExtensionalInputs:                  OK (1.42s)

Label "i":
96.6102% 0
3.3898% 1
extEqGeneralisesEqAndNormalEqAndEverAgree: OK (2.85s)

Label "equal":
77.0000% False
23.0000% True

Label "everAgree":
100.0000% True

Label "extEq":
100.0000% True

Label "normalEq":
3.0000% False
97.0000% True

1 out of 7 tests failed (11.87s)
``````

Discarding works very well for some tests, e.g. `notUnnormalEqToItself` only hit a few timeouts, which caused a handful of extra calls. Other tests struggled, making over 1000 extra calls; some were abandoned after reaching the limit of 100 discards in a row; and some of those gave up without a single success, causing the overall test suite to fail.

## Smarter generators

One way to avoid excessive discards is to move logic into our data generators. This isn’t a magic bullet, but it can be useful if acceptable values are reasonably common; if retrying a generator is faster than discarding a test; and for retrying parts of an input, rather than starting from scratch.

For example, the following generator only produces `Normal` values, by running `reduce` on generated `Com` values. That’s undecidable from within a property, but actually quite easy in a generator, since we’re free to discard problematic values and try again:

``````-- | Like genComN, but reduces its outputs to normal form. The fuel
-- | bounds the size of the initial expression (before it's reduced), and
-- | the number of steps to attempt when normalising.
genNormalN :: Fuel -> Gen Normal
genNormalN n = shrinkWith shrinkNormal \$ do
c <- genComN n                  -- Generate a Com value c
runDelayOr (genNormalN n)       -- Fall back to generating a fresh Com
(pure <\$> reduce c)  -- Try to reduce c to a Normal value
n                    -- Give up after n steps

-- | Generates (relatively small) Normal values
genNormal :: Gen Normal
genNormal = genNormalN limit

-- | Generates a 'Stream' from the given generator
genStream :: Gen a -> Gen (Stream a)
genStream g = Cons <\$> g <*> genStream g

-- | Generates a 'Stream' of 'Normal' values of the given size
genNormalsN :: Fuel -> Gen (Stream Normal)
genNormalsN = genStream . genNormalN

-- | Generates a 'Stream' of reasonably-sized 'Normal' values
genNormals :: Gen (Stream Normal)
genNormals = genNormalsN limit``````

### A minor digression about shrinking

Property-checkers which generate inputs randomly, like `falsify`, may stumble across monstrous counterexamples full of irrelevant structure that is tedious for users to tease apart and find the underlying problem. To reduce this burden, all such checkers will attempt to “shrink” the counterexamples they find, in the hope of discarding irrelevant parts: when a counterexample is found, a “shrinker” turns it into a list of possible alternatives. If that list is empty, shrinking stops and the counterexample is shown to the user. If the list is not empty, the property is retried with the first alternative: if the property holds then the next alternative is tried, and so on. If an alternative is found for which the property does not hold, then we’ve found a smaller counterexample. The shrinking process is repeated for this smaller counterexample, and so on until there are no alternatives remaining (either because the counterexample cannot be shrunk, like an empty list; or the property held for every smaller alternative).

There is no precise definition for what “shrinking” means, other than a requirement to avoid cycles: if `foo` can be shrunk to `bar`, then `bar` should not also shrink to `foo`, or else the above algorithm can get stuck in a loop.

QuickCheck implements shrinking alongside, but separately, to its data generators. A QuickCheck-style shrinker is a value with the following type:

``type Shrink a = a -> [a]``

That is, a function which takes as input the value we want to shrink, and outputs a list (potentially empty!) of “smaller” alternatives. For example, we could shrink a `Com` value in several ways:

• Replace leaf values with `K` (the simpler of the two basis values). We can’t replace `K` with itself, since that’s a cycle, so it has no alternatives.
• Replace branches (`App` values) with `S` or `K`, since leaves are smaller.
• Replace branches with either of their children.
• Shrink either of a branch’s children.
``````shrinkCom :: Shrink Com
shrinkCom (C   "K") = []
shrinkCom (C     _) = [k]
shrinkCom (App l r) = interleave
[ [ k, s ]
, filter (`notElem` [k, s]) [ l, r ]  -- Avoid duplicating k or s
,      App l <\$> shrinkCom r
, flip App r <\$> shrinkCom l
]

-- | Alternate taking elements from each list.
interleave :: [[a]] -> [a]
interleave ((x:xs):ys) = x : interleave (ys ++ [xs])
interleave ([]    :ys) =     interleave  ys
interleave  []         = []``````

The `shrinkNormal` function we reference above is a simple wrapper around `shrinkCom`, which discards non-`Normal` values:

``````shrinkNormal :: Shrink Normal
shrinkNormal = keep . shrinkCom . toCom
where keep []     = []
keep (c:cs) = case toNormal c of
Left  _ ->     keep cs
Right n -> n : keep cs``````

We use `shrinkWith shrinkNormal` in our definition of `genNormalN` so that the shrinking algorithm described above will get smaller alternatives by calling our `shrinkNormal` function. That would be the norm in QuickCheck (or its descendents, like ScalaCheck), but `falsify` is a bit smarter: it doesn’t need custom shrinking functions, since its able to re-run its generators on smaller (trees of) random numbers. Such an “integrated shrinking” approach is usually good enough, and saves us a bunch of effort (after all, we’ve got this far without having to know about shrinking!). Unfortunately, integrated shrinking doesn’t work well for smarter generators that perform a search, like `genNormalN`: there’s no reason to expect that re-running the search with some smaller random numbers will find a smaller result. Indeed it may find no result, and get stuck recursing forever. When writing such “smart” generators, it’s hence worth thinking about their shrinking behaviour, and whether it would be prudent to override.

Here are a few more general-purpose shrinkers (in a scrap your type classes style):

``````-- | Shrink the elements of a tuple.
shrink2 :: Shrink a -> Shrink b -> Shrink (a, b)
shrink2 sA sB (x, y) = interleave [(,y) <\$> sA x, (x,) <\$> sB y]

-- | Shrink the elements of a tuple.
shrink3 :: Shrink a -> Shrink b -> Shrink c -> Shrink (a, b, c)
shrink3 sA sB sC (x, y, z) = unpack <\$> shrink2 sA (shrink2 sB sC) (x, (y, z))
where unpack (x', (y', z')) = (x', y', z')

-- | Shrink a list, by dropping and shrinking its elements
shrinkL :: Shrink a -> Shrink [a]
shrinkL _  []  = []
shrinkL sA [x] = [] : (pure <\$> sA x)
shrinkL sA xs  = [] : shrinkElems
where len         = length xs
shrinkElems = do
i <- [0..len-1]
case splitAt i xs of
-- Try dropping or shrinking the ith element
(pre, a:suf) -> (pre ++ suf) : ((pre ++) . (:suf) <\$> sA a)
_            -> []``````

### Revisiting our roots

Since `Normal` values reduce immediately, their `normalEq` result is always `Now`, and hence they can be compared with any amount of `Fuel` without timing out. This fixes our very first property, that all values are `normalEq` to themselves!

``````normalsAreNormalEqToThemselves :: (Fuel, Normal) -> Bool
normalsAreNormalEqToThemselves (n, x) = normalEqToItself (n, toCom x)``````
``main = check normalsAreNormalEqToThemselves (tuple2 genFuel genNormal)``
``````normalsAreNormalEqToThemselves: OK (0.05s)
100 successful tests

All 1 tests passed (0.05s)
``````

The following generator makes a `Set` of values which satisfy some given binary predicate. The most straightforward way to implement this would be generating sets of values over and over until we eventually find one that fits our criteria. However, it may be quite rare for values to satisfy that predicate and attempting to generate multiple at once will just compound that rarity.

Instead, our “smart” generator can be more efficient by accumulating values until any combination of them satisfies our criteria (exploiting the so-called “birthday paradox”):

``````-- | Accumulate more and more values from the given 'Gen', until we find 'n'
-- | that satisfy the given relation. The 'i' parameter allows for flexibility.
genMatchingN :: Ord o
=> Natural
-> (i -> Gen o)
-> (i -> o -> o -> Bool)
-> Shrink o
-> i
-> Gen (Set o)
genMatchingN n g match shr i = shrinkWith shrink (go Map.empty)
where go xss = do
x <- g i
let k    = case filter (match i x) (Map.keys xss) of
y:_ -> y
_   -> x
-- Append x to the Set which matches k (or empty, if not present)
xs   = Map.findWithDefault Set.empty k xss
case Set.insert x xs of
xs -> if len xs >= n
then pure xs
else go (Map.insert k xs xss)

-- Try shrinking the elements individually, keeping any that still match
shrink =
filter ((== n) . len) . (Set.fromList <\$>) . shrink' . Set.toList

shrink' []     = []
shrink' (x:xs) =
keep (interleave [(:xs) <\$> shr x, (x:) <\$> shrink' xs])

len = fromIntegral . Set.size

keep []           = []
keep (    []:xss) = keep xss
keep ((x:xs):xss) =
(if all (match i x) xs then [x:xs] else []) ++ keep xss

-- | Accumulate more and more values from the given 'Gen', until we find two
-- | that satisfy the given relation. The 'i' parameter allows for flexibility.
genMatching :: Ord o
=> (i -> Gen o)
-> (i -> o -> o -> Bool)
-> Shrink o
-> i
-> Gen (o, o)
genMatching g match shr i = genMatchingN 2 g match shr i >>= get
where get s = case Set.toList s of
x:y:_ -> pure (x, y)
_     -> genMatching g match shr i -- absurd but fall back to retrying

-- | Generate pairs of unequal 'Com' values which have the same 'Normal' form.
genNormalEqN :: Fuel -> Gen (Com, Com)
genNormalEqN = genMatching genComN matchNormalEqN shrinkCom

matchNormalEqN n x y = x /= y && runDelayOr False (same <\$> normalEq x y) n

genNormalEq :: Gen (Com, Com)
genNormalEq = genNormalEqN limit``````

This generator greatly reduces discards for a property like `normalEqImpliesAgree`:

``````main = defaultMain . normalEqImpliesAgreeDiscard \$ do
(x, y) <- genNormalEq
tuple4 genFuel (pure x) (pure y) genComs``````
``````normalEqImpliesAgree: OK (0.59s)

All 1 tests passed (0.59s)
``````

### Hedging our bets

Unlike `normalsAreNormalEqToThemselves`, which relies on `genNormal` to avoid timeout counterexamples, the smart generator for `normalEqImpliesAgree` is purely an optimisation. For that reason, I actually prefer to mix in a few inputs from the original “dumb” generator: that way, we don’t need to trust the smart generator to completely cover the input space; and we leave open the possibility for the dumb generator to stumble on to a different form of counterexample. The simplest way to mix two generators is via the `Gen.choose` function, which uses each half of the time; but that would increase the number of discards more than I would like. Instead we’ll use the more sophisticated `Gen.frequency`:

``````main = defaultMain . normalEqImpliesAgreeDiscard \$ do
(x, y) <- Gen.frequency
[ (9, genNormalEq           )
, (1, (tuple2 genCom genCom)) ]
tuple4 genFuel (pure x) (pure y) genComs``````
``````normalEqImpliesAgree: OK (0.57s)

All 1 tests passed (0.57s)
``````

### A trickier case

We can use a similar approach for `agreementIsMonotonic`, generating a pair of values which only agree on a non-zero number of inputs:

``````-- | Generate a pair of 'Com' values which agree on the given number of inputs,
-- | within the given amount of 'Fuel'.
genAgreeFromN :: Natural -> Fuel -> Gen (Com, Com)
genAgreeFromN lo = genMatching genComN (matchAgreeFromN lo) shrinkCom

matchAgreeFromN lo n x y = case runDelayOr Nothing (extensionalInputs x y) n of
Just i  -> i >= lo
Nothing -> False

-- | Generate a pair of 'Com' values which agree on 1 or more inputs. This tends
-- | to avoid values which agree on 0 inputs, i.e. with equal 'Normal' forms,
-- | and hence exercise the symbolic execution more thoroughly.
genAgreeN = genAgreeFromN 1

-- | Generate pairs of reasonably sized values which agree on 1 or more inputs.
genAgree = genAgreeN limit``````
``````main = defaultMain . agreementIsMonotonicDiscard . Gen.frequency \$
[(9, smart), (1, dumb)]
where dumb  = tuple4 (tuple2 genNat genNat)
genFuel
(tuple2 genCom genCom)
genComs
smart = do
n      <- (10 +) <\$> genFuel
(x, y) <- genAgreeN n  -- Generate values that agree on some inputs
case runDelay n (extensionalInputs x y) of  -- Find how many inputs
Now (Just i) -> tuple4
(tuple2 (pure i) genNat)
(pure n)
(pure (x, y))
(fmap toCom <\$> genNormals)  -- Normal values don't need any Fuel
_ -> smart  -- absurd, but retry as a fallback
genNat = fromIntegral <\$> genFuel``````
``````agreementIsMonotonic: OK (115.21s)

All 1 tests passed (115.21s)
``````

This test now takes a lot longer to run than the others, due to the more precise precondition we require of the generator. I see that as a good investment, since we’re now maxing-out our CPU in a (reasonably targeted) attempt to find mistakes in our reasoning; which seems preferable to the original test, which quickly gave up even trying. Since the number of runs is configurable, we can choose a low number for a fast feedback cycle during development, and crank it up for a more thorough check like a pre-push git hook or a continuous integration server.

## Thoroughly checking extensionality

Most of the checks so far have been focused on implementation details, like the definition of “agreement” and the particular patterns of disagreement we’re looking for. Now I want to focus on extensional equality itself, and its implications.

### Extensionally equal values are indistinguishable

The main reason we care about extensional equality is that it’s broad enough to relate all values which are indistinguishable within SK. This is also known as observational equivalence (SK is such a simple language that these notions end up coinciding!).

As a consequence, extensionally equal values are interchangable: swapping any part of an SK expression for an extensionally-equal alternative should make no observable difference to the result; i.e. the results should themselves be extensionally equal. We can represent such “swapping” using a zipper datastructure:

``````-- | A path down a binary tree
type Path = [Either () ()]

-- | Replace a part (identified by 'Path') of the first 'Com' with the second.
swapPart :: Path -> Com -> Com -> Com
swapPart p whole part = unzipCom (part, position)
where (_, position) = focus whole p

-- | Represents a 'Com' with one of its sub-expressions "focused"
type ComZipper = (Com, [Either Com Com])

-- | Turns a 'ComZipper' back into a 'Com'
unzipCom :: ComZipper -> Com
unzipCom (x, xs) = case xs of
[]         -> x                       -- x is the root, return it as-is
Left  r:ys -> unzipCom (App x r, ys)  -- x is a left child with sibling r
Right l:ys -> unzipCom (App l x, ys)  -- x is a right child with sibling l

-- | Focus on a particular sub-expression of the given 'Com', at a position
-- | identified by the given 'Path' (stopping if it hits a leaf).
focus :: Com -> Path -> ComZipper
focus x = go (x, [])  -- Start focused on the root
where go (App l r, xs) ( Left ():p) = go (l,  Left r:xs) p  -- Focus on left
go (App l r, xs) (Right ():p) = go (r, Right l:xs) p  -- Focus on right
go z             _            = z  -- Reached a leaf or end of Path

-- | Generate a 'Path' through a binary tree (e.g. 'Com').
genPathN :: Fuel -> Gen Path
genPathN n = Gen.list (to n) (go <\$> Gen.bool False)
where go False =  Left ()
go True  = Right ()

-- | Generate a reasonably small 'Path' through a binary tree (e.g. 'Com')
genPath :: Gen Path
genPath = genPathN limit``````
Checking `ComZipper`

We can sanity-check our `ComZipper` implementation using the property that turning them back into a `Com` value doesn’t depend on which part was “focused”:

``````unzipComIgnoresLocation = testProperty "unzipComIgnoresLocation" \$ do
c <- gen genCom
p <- gen genPath
let c' = unzipCom (focus c p)
if c == c' then pure () else fail (show (c, c'))``````
``main = defaultMain unzipComIgnoresLocation``
``````unzipComIgnoresLocation: OK (0.02s)
100 successful tests

All 1 tests passed (0.02s)
``````

Swapping-out part of an arbitrary expression, even one in `Normal` form, may result in a value which loops forever. For example, consider a classic infinite loop like `S(SKK)(SKK)(S(SKK)(SKK))`:

• The expression `SKK` acts as an identity function, reducing to its first input value: `SKKx → Kx(Kx) → x`.
• Let’s abbreviate `SKK` as `I`, so our loop can be written `SII(SII)`.
• Applying the `S` rule, we get `SII(SII) → I(SII)(I(SII))`.
• Since `Ix` reduces to `x`, both of those `I(SII)` values reduce to `SII`.
• Hence `I(SII)(I(SII)) → SII(SII)`, which is what we started with!
• Therefore our original expression `S(SKK)(SKK)(S(SKK)(SKK))` reduces to itself, over and over, forever.

Note that the repeated component `S(SKK)(SKK)` is itself in `Normal` form, since each `S` is only applied to two args. Applying `K` to that, like `K(S(SKK)(SKK))`, is also `Normal`. If we swap-out that `K` for `S(SKK)(SKK)`, we’ll get our infinite loop.

Undecidability makes it impossible, in general, to avoid creating such loops; so we need our generator to retry if it can’t normalise a swapped-out expression in a reasonable number of steps:

``````genSwappableExtEqValsN :: Fuel -> Gen (Com, Com, [Either Com Com])
genSwappableExtEqValsN n = shrinkWith zShrink \$ do
-- Generate a pair of extensionally-equal Coms. Avoid normally-equal values,
-- since they don't need symbolic execution.
(x, y) <- genMatching genNormalComN matchNontriviallyExtEq shrinkCom n
-- Generate a ComZipper whose focus can be swapped-out with 'x' or 'y'
-- without diverging
zs <- genZipperFor x y
pure (x, y, zs)
where genZipperFor x y = do
(_, zs) <- focus <\$> genComN n <*> genPathN n
if checkZs (x, y, zs) then pure zs else genZipperFor x y

checkZs (x, y, zs) =
let go = isJust . countLaters n . reduce . unzipCom . (, zs)
in go x && go y

zShrink = filter checkZs
. shrink3 shrinkCom shrinkCom (shrinkL (const []))

-- | More efficient alternative to 'genComN': biased towards smaller values, and
-- | only generates 'Normal' forms.
genNormalComN = (toCom <\$>) . genNormalN

-- | Whether two 'Com' values are 'extEq' but *not* 'normalEq' (within 'Fuel').
matchNontriviallyExtEq :: Fuel -> Com -> Com -> Bool
matchNontriviallyExtEq n x y = runDelayOr False (            extEq x y) n
&& runDelayOr False (diff <\$> normalEq x y) n``````

Now we can generate extensionally-equal values, an expression to plug them into, and a `Path` describing where to plug them in, filtered such that they both reduce to a `Normal`. However, one problem remains: we have no idea how much `Fuel` will be needed to find when those swapped-out expressions begin to agree. We can re-use our double-negative trick of being “not unequal”:

``````extEqCannotBeDistinguished = testProperty "extEqCannotBeDistinguished" \$ do
-- Use the smart generator 90% of the time, allow 10% to be unconstrained
(x, y, zs) <- gen \$ Gen.frequency
[ (9, genSwappableExtEqValsN limit)
, (1, tuple3 genCom genCom (snd <\$> (focus <\$> genCom <*> genPath)))
]
let (x', y') = (unzipCom (x, zs), unzipCom (y, zs))
case (runDelayOr False (extEq x y) limit, runDelay limit (extEq x' y')) of
(True, Now True ) -> pure ()
(True, Now False) -> fail (show x' ++ " /= " ++ show y')
``main = defaultMain extEqCannotBeDistinguished``
``````extEqCannotBeDistinguished: OK (19.67s)

All 1 tests passed (19.67s)
``````

However, this doesn’t give us much confidence since we can only prove inequality in certain specific cases. Expressions which are unequal in a way we can’t prove will give a never-ending sequence of `Later`, and hence be discarded. There is a way we can assert that all the results are extensionally equal, by removing the timeout: that’s risky, since if we’re wrong then one of those never-ending sequences will cause our test suite to run forever!

``````-- | Runs a 'Delay' value to completion. This may run forever!
unsafeRunDelay :: Delay a -> a
unsafeRunDelay (Now   x) = x
unsafeRunDelay (Later x) = unsafeRunDelay x

extEqAreInterchangable = testProperty "extEqAreInterchangable" \$ do
-- For safety, we can only use the smart generator
(x, y, zs) <- gen \$ genSwappableExtEqValsN limit
let (x', y') = (unzipCom (x, zs), unzipCom (y, zs))
case (unsafeRunDelay (extEq x y), unsafeRunDelay (extEq x' y')) of
(True, True ) -> pure ()
(True, False) -> fail (show x' ++ " /= " ++ show y')
``main = defaultMain extEqAreInterchangable``
``````extEqAreInterchangable: OK (20.09s)
100 successful tests

All 1 tests passed (20.09s)
``````

(If you look at this page’s Markdown source you’ll see that I’m actually a coward, since I’m wrapping the above Haskell process in a timeout of a few minutes, just in case!)

### Extensionally unequal values are distinguishable

When two values are extensional unequal, there exist input values for which they disagree. Note that we can’t test this by just generating some input values and asserting that they disagree, since some inputs may happen to agree by coincidence. Instead, we’ll generate a `Stream` of input `Stream`s, and check for disagreement on all of them, and interleave their execution using `race`:

``````-- | Generate a pair of 'Com' values which are extensionally unequal
genExtUneqN :: Fuel -> Gen (Com, Com)
genExtUneqN = genMatching genComN uneq shrinkCom
where uneq n x y = runDelayOr False (not . isJust <\$> extensionalInputs x y) n

genExtUneq = genExtUneqN limit

extUneqWillDisagree = testProperty "extUneqWillDisagree" \$ do
(x, y) <- gen genExtUneq
len    <- gen genFuel
inputs <- gen genInputs
let result = race (sAt len . agree x y <\$> inputs) >>= findDisagreement
pure (unsafeRunDelay result)
where genInputs = Cons <\$> genComs <*> genInputs
findDisagreement (x, _, xs) = if diff x
then pure ()
else race xs >>= findDisagreement``````
``main = defaultMain extUneqWillDisagree``
``````extUneqWillDisagree: OK (0.78s)
100 successful tests

All 1 tests passed (0.78s)
``````

### Transitivity

The transitive property holds for all of the notions of equality we’ve seen so far: when `foo` equals `bar` and `bar` equals `baz`, then `foo` must equal `baz`:

``````-- | Assert that the function 'eq' is transitive for the three given args.
assertTrans eq x y z = case (eq x y, eq y z, eq x z) of
(    _, False,    _) -> discard
( True,  True, True) -> pure ()
_                    -> fail "Not transitive"

eqIsTransitive = testProperty "eqIsTransitive" \$ do
-- Can't use genMatching, since Set will discard == values
let g xs = do
x <- genCom
let got = x : filter (== x) xs
if length got >= 3 then pure got else g (x:xs)
(x:y:z:_) <- gen \$ Gen.shrinkWith (shrinkL shrinkCom) (g [])
assertTrans (==) x y z
where

normalEqIsTransitive = testProperty "normalEqIsTransitive" \$ do
let g  = genMatchingN 3 genComN matchNormalEqN shrinkCom limit
eq = matchNormalEqN limit
(x:y:z:_) <- gen \$ Set.toList <\$> g
assertTrans eq x y z

everAgreeIsTransitive = testProperty "agreeIsTransitive" \$ do
let g      = genMatchingN 3 genNormalComN (matchAgreeFromN 1) shrinkCom limit
eq x y = runDelayOr False (everAgree x y) (limit * limit)
(x:y:z:_) <- gen \$ Set.toList <\$> g
assertTrans eq x y z

extEqIsTransitive = testProperty "extEqIsTransitive" \$ do
let g      = genMatchingN 3 genNormalComN (matchAgreeFromN 1) shrinkCom limit
eq x y = runDelayOr False (extEq x y) (limit * limit)
(x:y:z:_) <- gen \$ Set.toList <\$> g
assertTrans eq x y z``````
``````main = defaultMain \$ testGroup "transitivity"
[ eqIsTransitive
, normalEqIsTransitive
, everAgreeIsTransitive
, extEqIsTransitive
]``````
``````transitivity
eqIsTransitive:       OK (0.44s)
100 successful tests
normalEqIsTransitive: OK (1.50s)
100 successful tests
agreeIsTransitive:    OK (65.64s)
100 successful tests
extEqIsTransitive:    OK (59.20s)
100 successful tests

All 4 tests passed (126.78s)
``````

## Falsifying myself

Thanks to this in-depth testing, I eventually discovered the problem I was having in egglog: expressions containing symbolic variables were being used interchangably with concrete (variable-free) expressions. When we use symbolic execution to check for agreement, we are assuming that each symbol represents an input our expressions have been applied to: if those expressions already contain symbols, that assumption no longer holds, and our conclusions about agreement may be wrong.

Let’s walk through a simple example, with the expressions `SKK` (concrete) and `Kx` (which contains the symbol `x`). These don’t agree on 0 inputs, but if we apply them to a single symbolic input `x`:

• The first expression reduces like `SKKx → Kx(Kx) → x`
• The second expression reduces like `Kxx → x`

Hence these seem to agree! Unfortunately, this is actually just a coincidence, caused by the appearance of the symbol `x` in the latter expression. If we apply these expressions to any input value other than `x`, they will disagree! To see this, notice that the first expression `SKK` is an identity function: it returns its argument unchanged; whilst the second, `Kx`, ignores its argument and always returns `x`. They only agree when the argument is also `x`: but if that is the first symbol we’re using to check agreement, we will mistakenly conclude that these expressions are extensionally equal!

Once we’ve made such a mistake, all `Com` expressions will quickly merge into one big equivalence class, due to the properties described above. To see why, consider an arbitrary value `A`: if we apply our first expression to this we get `SKKA` which is equal to `KA(KA)` and ultimately to `A`. However, we can also swap-out that `SKK` for the “equal” expression `Kx`, giving `KxA` which is equal to `x`. Hence this mistaken equality between `SKK` and `Kx` can be used to “prove” that any value is equal to `x`; and therefore, by transitivity, equal to any other value!

I believe this is why my implementation of extensional equality in egglog caused everything to collapse: once symbolic expressions started leaking into equivalence classes of concrete expressions (due to my unhygenic mixing of the two) the inevitable consequences quickly unfolded, thanks to egglog’s powerful Equation Graph machinery.

## Conclusion

I’m pretty happy that I took this little diversion to double-check my assumption about using symbolic computation to “fake” universal quantification. It was a fun little exercise to learn the particular API features of `falsify`, which seems very promising. My initial tests were quick and direct to write, but they didn’t yield any new information. This didn’t give me much confidence, as I suspected they weren’t exploring much of the search space: and adding instrumentation proved as much. Using discards as a guard-rail against triviality, plus some careful thought on how to avoid slamming into them repeatedly, ultimately lead to some more in-depth understanding of what assumptions we can and can’t make in this context.

My ultimate realisation, that it’s the “leaking” of symbolic values that caused the collapse I was seeing, did not come directly from a failing `falsify` test. However, it did come from clarification of my mental model, and that clarification was largely thanks to these `falsify` tests. That’s actually a truism I’ve learned with experience: whether a test failure is caused by a bug in an application, or “just” a bug in the tests, those are both symptoms of a bug in our understanding; which is the most important part.

With this Haskell digression over, future installments will switch back to egglog and make sure that we don’t check agreement with expressions that already contain symbolic values. There are several mechanisms we can use to avoid this, and I’ve already confirmed that a simple `isConcrete` precondition is enough to prevent the prior collapse. Stay tuned Go here for part four!