`contains`

definition

show as: view math explainer →

module: IndisputableMonolith.Ethics.StakeGraph
domain: Ethics
line: 15 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethics.StakeGraph on GitHub at line 15.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  12
  13namespace StakeGraph
  14
  15def contains (xs : List Stakeholder) (s : Stakeholder) : Bool :=
  16  xs.any (fun x => decide (x = s))
  17
  18def neighbors (G : StakeGraph) (nodes : List Stakeholder) (s : Stakeholder) : List Stakeholder :=
  19  nodes.filter (fun t => G.edge s t)
  20
  21def reachable (G : StakeGraph) (nodes : List Stakeholder) (src dst : Stakeholder) : Bool :=
  22  let rec dfs (front : List Stakeholder) (visited : List Stakeholder) : Bool :=
  23    match front with
  24    | [] => False
  25    | v :: vs =>
  26        if decide (v = dst) then True else
  27        let nbrs := neighbors G nodes v
  28        let fresh := nbrs.filter (fun w => ¬ contains visited w)
  29        dfs (vs ++ fresh) (v :: visited)
  30  dfs [src] []
  31
  32def mutualReachable (G : StakeGraph) (nodes : List Stakeholder) (s t : Stakeholder) : Bool :=
  33  reachable G nodes s t && reachable G nodes t s
  34
  35def hasCycle (G : StakeGraph) (nodes : List Stakeholder) : Bool :=
  36  nodes.any (fun s => G.edge s s)
  37  || nodes.any (fun s =>
  38        nodes.any (fun t => (¬ decide (s = t)) && mutualReachable G nodes s t))
  39
  40end StakeGraph
  41end Ethics
  42end IndisputableMonolith
  43

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.