Bottom-up, one SCC at a time
A whole program’s predicates form a dependency graph.
Group each cycle of mutually recursive predicates into one strongly connected component:
The SCCs form layers, evaluated bottom-up: each SCC runs the naive evaluation from the previous slide once everything below it is finished.