Lesson 4

  • Introduction to finite sets
  • Finite graph in SSR
  • Proving Kosaraju's algorithm

Finite sets

In SSR, they are sets over a finite type T

a set encapsulates an indicator function {ffun T -> bool}

sets share the collective predicate _ \in _ with lists


  • path r x p : r relation, x is an element, p is a list (x :: p) is a path starting at x and ending at (last x p) of r related element


  • a graph is manipulated either by its adjacency relation or its adjacency function
  • the functions grel and rgraph let you change representation

Depth-First Search

  • defs f n x v : returns the nodes visited by a dfs at depth n avoiding the nodes in v


  • boolean relation that indicates if two nodes are connected

Kosaraju's algorithm

  • 2 dfs traversals
  • one to build a post-fixed stack
  • one on the reverse graph to collect the components

save script