I am trying to build a logic sentence (such that only m propositions out of n propositions can be true) with a double loop, but get confused by the "|" token. I cannot find its precise meaning on Hoogle. The select gives a list of lists, a list of indexes that can be selected. With the indexes i want to build a conjunction of positive "selected" propositions and negative "non-selected" propositions. What am i doing wrong with the following code?

genXorM :: Int -> Int -> Form 
genXorM n m = Disj [Conj [Neg $ PrpF $ P x, PrpF $ P y] | z <- select, y <- [0 .. n] \\ z, x <- z]  where
  select = combinations m [0 .. n]

CodePudding user response：

genXorM :: Int -> Int -> Form 
genXorM n m = Disj [Conj [Neg $ PrpF $ P x, PrpF $ P y] | z <- select, y <- [0 .. n] \\ z, x <- z]  where
  select = combinations m [0 .. n]

You have a “triple loop” here. It says:

• For every combination z of m propositions:
  • For every proposition y not in z:
    • For every proposition x in z:
      • Produce the formula ¬x ∧ y

If I understand correctly that you want a conjunction of all the selected propositions x with the negation of all the non-selected ones y, that could be written with list comprehensions like this:

genXorM :: Int -> Int -> Form 
genXorM n m = Disj
  [ Conj
    ([PrpF (P p) | p <- x]
         [Neg (PrpF (P n)) | n <- y])
  | x <- select
  , let y = [0 .. n] \\ x
  ]
  where
    select = combinations m [0 .. n]

Or without them, for example, using map and some helper functions to break down the problem into smaller pieces:

genXorM n m = Disj (map conjoin selected)
  where
    selected = combinations m [0 .. n]
    conjoin z = Conj (map positive z    map negative (complement z))
    positive = PrpF . P
    negative = Neg . positive
    complement x = [0 .. n] \\ x