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?

[Mario Carneiro]

Python is not a lazy language, so the implementation would be basically the same in that case

[Paige Thomas]

Oh. I thought I had read that the iterators were evaluated lazily?

[Mario Carneiro]

they are lazy, in the sense that an iterator is an object which has a next function, rather than a sequence of values ready to go

[Mario Carneiro]

but you can do objects with a next function in lean too

[Paige Thomas]

Is that different than lazy evaluation?

[Paige Thomas]

I guess I assumed that was required for lazy evaluation.

[Paige Thomas]

This is the Lean function I have for it:

def cartesian_product
  {α : Type} :
  List (List α) → List (List α)
| [] => [[]]
| xs :: xss =>
  let sub_products := cartesian_product xss
  (xs.map (fun val => sub_products.map (fun sub => val :: sub))).flatten

but I'm not sure how to turn it into one with a next function.

[Mario Carneiro]

actually python is doing a bit of language magic here; you missed the use of the yield keyword and your version is not an iterator at all

[Mario Carneiro]

in fact it looks nothing like the python implementation in the docs?

[Paige Thomas]

That was my attempt to just write any function in Lean that computes a cartesian product of n variables.

[Paige Thomas]

I'm not sure how to replicate the Python version in Lean.

[Mario Carneiro]

actually the python docs version is not good either, it is essentially a strict version but the docs say "imagine this but lazy" :upside_down:

[Paige Thomas]

:smile:

[Yakov Pechersky]

There's this: https://more-itertools.readthedocs.io/en/stable/_modules/more_itertools/more.html#partial_product

[Yakov Pechersky]

And also outer_product below that

[Mario Carneiro]

Cartesian product is one of the more complicated operations to iteratorify. Here's an implementation:

def CartesianProduct'.{u} (α : Type u) : List (List α) → Type u
  | [] => PUnit
  | _::xs => List α × α × CartesianProduct' α xs

def CartesianProduct'.mk {α} : ∀ xss, Option (List α × CartesianProduct' α xss)
  | [] => some ([], ⟨⟩)
  | (a::x)::xs =>
    match CartesianProduct'.mk xs with
    | none => none
    | some (l, iter) => some (a::l, x, a, iter)
  | []::_ => none

def CartesianProduct'.next? {α} :
    ∀ xss, CartesianProduct' α xss → Option (List α × CartesianProduct' α xss)
  | [], _ => none
  | _::xss, (l, val, iter) => do
    let (val, l, sub, iter) ←
      ((val, l, ·) <$> next? xss iter) <|> (do
        let (val, l) ← Stream.next? l
        (val, l, ·) <$> CartesianProduct'.mk xss)
    some (val::sub, l, val, iter)

def CartesianProduct (α) := Σ xss, Option (List α × CartesianProduct' α xss)

def cartesian_product_lazy {α : Type} (xs : List (List α)) : CartesianProduct α :=
  ⟨xs, CartesianProduct'.mk xs⟩

def cartesian_product_eager {α : Type} : List (List α) → List (List α)
| [] => [[]]
| xs :: xss =>
  let sub_products := cartesian_product_eager xss
  (xs.map (fun val => sub_products.map (fun sub => val :: sub))).flatten

instance {α} : Stream (CartesianProduct α) (List α) where
  next?
  | ⟨_, none⟩ => none
  | ⟨xs, some (a, iter)⟩ => some (a, ⟨xs, iter.next?⟩)

#eval cartesian_product_eager [[0,1],[0,1],[0,2]]
#eval do
  let mut l := #[]
  for i in cartesian_product_lazy [[0,1],[0,1],[0,2]] do
    l := l.push i
  pure l

[Paige Thomas]

Wow!

[Paige Thomas]

How does this work?

[Paige Thomas]

CartesianProduct' is some kind of data type, a structure maybe?

[Mario Carneiro]

The basic idea of making an algorithm lazy is that every time you yield you need to remember exactly where you are in the algorithm so you can pick back up later. This is a pretty direct translation of your eager implementation, so the state you need to keep track of is the values of the xs, val local variables, as well as a nested iterator for the sub_products variable. You also need to keep around the original list of lists because every time you throw away one of the nested iterators you need to restore it from the beginning again; that's what CartesianProduct'.mk does. Note that the way this is written it assumes the lists are nonempty when inside the inner loops, so CartesianProduct'.mk returns an option for the case where one of the lists is empty.

[Mario Carneiro]

Paige Thomas said:

CartesianProduct' is some kind of data type, a structure maybe?

Yes, in general an iterator is a custom type and a Stream implementation for it

[Mario Carneiro]

Both CartesianProduct' and CartesianProduct are streams; the latter hides the dependent type for an easier API

[Mario Carneiro]

Concretely, if we have yielded the elements up to and not including [0,1,2] in the [[0,1],[0,1],[0,2]] iteration example, then the state will be:

([[0,1],[0,1],[0,2]],
 [([1], 0), ([], 1), ([], 2)])

[Mario Carneiro]

although the definition is written as a recursive type instead of List (List α × α) to ensure the two lists are the same length

[Paige Thomas]

I'm not sure I'm familiar with recursive types. Is that similar to an inductive type?

[Paige Thomas]

or maybe I was, but forgot :(

[Mario Carneiro]

by recursive type I mean a function of type Type defined using def and recursion

[Mario Carneiro]

See CartesianProduct' above for an example

[Paige Thomas]

Sorry, I mean, I'm not sure how to read that code, ie, translate it to English prose. What makes up a CartesianProduct'given that definition? What are some examples of instances of CartesianProduct' and why are they instances?

[Mario Carneiro]

CartesianProduct' is a family of types, so the things in it depends on which element of the family you take. CartesianProduct' A [] is the same as PUnit so it has () as its element, and CartesianProduct' A [xs] is the same as List A x A x PUnit so its elements are like ([a,b,c], a, ()), etc

[Paige Thomas]

Interesting. It seems like the list it is recursing on isn't used other than as something that has a recursive structure? Like, for example, it could be replaced with recursion on a Nat or anything with a similar form?

[Mario Carneiro]

yes, specifically the type only depends on the length of the list

[Mario Carneiro]

it's basically just a List (List A x A) with the same length as xss

[Paige Thomas]

Is it a list of tuples, or a long combined tuple like (List A x A) x ((List A x A) x ... x (List A x A))?

[Aaron Liu]

It's the long combined tuple, but with a PUnit at the end (and also associated a bit differently)

[Aaron Liu]

compare types like Nat.below

[Paige Thomas]

I can't seem to find Nat.below in Mathlib?

[Aaron Liu]

It's one of those secret autogenerated types

[Aaron Liu]

You get one for every recursive inductive type

[Aaron Liu]

They're used to compile recursive definitions

[Paige Thomas]

Oh. Thank you.