quickCheck propositional logic generator

Question

So I have this quickCheck propositional logic generator:

instance Arbitrary Form where
   arbitrary = genForm

genForm = sized genForm'
genForm' 0 = fmap Prop (choose (1,15))
genForm' n | n > 15 = genForm' (n `div` 2)
genForm' n | n > 0 =
          oneof [fmap Prop (choose (1,15)),
                 fmap Neg subform,
                 fmap Cnj subforms,
                 fmap Dsj subforms,
                 liftM2 Impl subform subform,
                 liftM2 Equiv subform subform]
          where subform = genForm' (n `div` 2)
                subforms = resize (n `div` 2) (vector (n `div` 2))

The datatype is defined as follows:

type Name = Int

data Form = Prop Name
          | Neg  Form
          | Cnj [Form]
          | Dsj [Form]
          | Impl Form Form
          | Equiv Form Form
          deriving (Eq,Ord)

The problem is this generator will generate in the form of: +[] (a disjunction of nothing). I don't want my operators to have no nested Prop member as it makes invalid propositional formulas. I want to make sure that there is no option to not have a Prop member at the end.

My thought is that this problem comes from the resize (div n 2). When n is even this will eventually hit 0 and not go further on generating and thus create a empty member. Removing the resize won't help because it then won't generate a ending 'tree'. So it seems to be needed but should be tweaked in some way.

But I'm not great at Haskell and I'm having difficulty debugging/reading the documentation.

What makes those invalid? An empty disjunction is false/bottom, while an empty conjunction is true/top. Indeed, those are the only ways to express those important propositions with your type! — dfeuer
@dfeuer I'm quite unfamiliar with those formulations of ⊤ and ⊥. It definitely sounds correct that they are missing in Form. — Tarick Welling
I guess you could also express true as Prop 0 `Equiv` Prop 0 and false as Prop 0 `Equiv` Neg (Prop 0), but those are neither as compact nor (IMO) as clear as Cnj [] and Dsj []. — dfeuer

Li-yao Xia Li-yao Xia · Accepted Answer · 2020-09-19T18:47:46

Apply vector to a non-zero argument:

subforms = resize (n `div` 2) (vector (1 + (n `div` 2)))

Or use listOf1 arbitrary instead of vector

subforms = resize (n `div` 2) (listOf1 arbitrary)

From a follow-up comment:

even need the generated amount to be at least >2

Apply vector to a length >= 2:

subforms = resize (n `div` 2) (vector (2 + (n `div` 2)))

Or append two elements in front explicitly (using listOf to allow the length to also vary):

subforms = resize (n `div` 2) (listOf2 arbitrary)
  where
    listOf2 :: Gen a -> Gen [a]
    listOf2 gen = liftA2 (:) gen (liftA2 (:) gen (listOf gen))
    -- 1. (listOf gen) to generate a list
    -- 2. Call gen twice to generate two more elements
    -- 3. Append everything together with `(:)`

quickCheck propositional logic generator

2 Answers