efficient truth table iteration

Stream: general

[Paige Thomas]

I'm wondering what the most efficient way might be to iterate through all of the possible assignments of true and false to a list of strings, which allows stopping part way through if a condition is met. I have code that will generate all of the possible assignments, but it doesn't permit stopping, and I'm guessing it might not be all that efficient:

def ValuationAsListOfPairs : Type := List (String × Bool)
  deriving Inhabited


def gen_all_valuations_as_list_of_list_of_pairs :
  List String → List (ValuationAsListOfPairs)
| [] => [[]]
| hd :: tl =>
  let left := List.map (fun (l : ValuationAsListOfPairs) =>
    (hd, false) :: l) (gen_all_valuations_as_list_of_list_of_pairs tl)

  let right := List.map (fun (l : ValuationAsListOfPairs) =>
    (hd, true) :: l) (gen_all_valuations_as_list_of_list_of_pairs tl)

  left ++ right


#eval gen_all_valuations_as_list_of_list_of_pairs ["P", "Q"]
-- [[("P", false), ("Q", false)], [("P", false), ("Q", true)], [("P", true), ("Q", false)], [("P", true), ("Q", true)]]

Honestly, I'm also generally not really sure about what kind of tricks there are to make Lean, or functional code in general, faster.

[Mario Carneiro]

generating large lists is generally a bad idea if it's not a mandatory part of the output. Can you write an inefficient function which does what you want? The current MWE does not have anything about a condition, and if you are returning a list of results then it's not clear what it means to stop early

[Aaron Liu]

I can do something like this efficiently in haskell, because haskell is a lazy language. However, if I do this in Lean, which is a strict language, Lean will eagerly generate the entire list, even if it is not used.

[Aaron Liu]

You may want to consider using docs#MLList (monadic lazy list) and friends.

[Mario Carneiro]

Here's a basic version which searches for the first valuation satisfying a condition:

def ValuationAsListOfPairs : Type := List (String × Bool)
  deriving Inhabited

def find_valuation (f : ValuationAsListOfPairs → Bool) :
  List String → ValuationAsListOfPairs → Option ValuationAsListOfPairs
| [], v => if f v then some v else none
| hd :: tl, v =>
  find_valuation f tl ((hd, false) :: v) <|>
  find_valuation f tl ((hd, true) :: v)

#eval find_valuation (fun (v : List _) => ("P", true) ∈ v ∧ ("Q", false) ∈ v) ["P", "Q"] []

[Mario Carneiro]

it's always possible to express haskell style lazy evaluation programs in a strict language, but you may have to "turn the control flow inside out". This is what haskell has to do in the end to generate code anyway. (It's easiest to explain with an example. The above program is the equivalent of the haskell program that generates a lazy list and then uses head <| filter on it)

[Paige Thomas]

Interesting, thank you. What does the memory usage look like? Does it store all of the previously generated valuations in memory, or discard each one after it has been checked?

[Paige Thomas]

That is, does the memory usage grow to $2^{n}$ if it never satisfies the condition, or remain at $n$?

[Paige Thomas]

(I'm not sure how to tell if it is tail recursive or not)

[Paige Thomas]

I wonder if it would be more useful to Mathlib to generalize this to something like the lazy Cartesian product of an arbitrary list of lists, where this case would be passing n lists of [true, false] to that function. (ie, Python's itertools.product)

[Paige Thomas]

(Unless the generalization makes the simpler case less efficient)

[Mario Carneiro]

That definition is not tail recursive, but the recursion has height n, not 2^n. And it does not buffer previous results, so the memory usage should be O(n) as well.

[Paige Thomas]

How could I go about seeing that it is not tail recursive? Is there a way I can add in print statements to see what is on the call stack? Would that help me tell?
Can it be made tail recursive?

[Paige Thomas]

I'm just thinking it would be fun to have the fastest possible brute force check for a propositional formula being satisfiable along with a proof that the check is correct.

[Yury G. Kudryashov]

It isn't tail recursive because it calls itself twice.

[Paige Thomas]

I see. I guess there isn't really any way around that.

[Henrik Böving]

You could in principle manage recursive calls on a heap allocated structure like a List or Array instead and then write a tail recursive procedure that pushes and pops from that

[Paige Thomas]

I see. Would that improve the speed?

[Paige Thomas]

Mario Carneiro said:

it's always possible to express haskell style lazy evaluation programs in a strict language, but you may have to "turn the control flow inside out". This is what haskell has to do in the end to generate code anyway. (It's easiest to explain with an example. The above program is the equivalent of the haskell program that generates a lazy list and then uses head <| filter on it)

Is there a way to do this generically? If I have an arbitrary function that generates a list, can I wrap it somehow, or pass it as an argument to another function that will make it evaluate lazily, without changing its code?

[Mario Carneiro]

No. A function which produces a lazy list in haskell can be converted once and for all to a strict function, but the conversion result is a stream generator with type B x (B -> Option (A x B)) instead of List A.

[Mario Carneiro]

If you have a strict function which produces a List A then the damage is already done and it cannot be undone by applying more functions afterwards

[Paige Thomas]

Hmm. But a lazy function can be written in Lean from scratch? For example, I could write a Lean version of the Python iterools.product function that evaluates lazily?