HashSet

Std.HashSet は、「重複のない集まり」を表すデータ構造です。 { .. } という記法で具体的に HashSet の項を定義することができます。

import Lean

open Std

/- info: Std.HashSet.ofList [1, 2, 3] -/
#eval ({1, 2, 3, 1, 1} : HashSet Nat)

HashSetの記法

HashSet は { a₁, a₂, ... } という構文で定義することができるのですが、この記法は HashSet 専用のものではなくて型クラスで定義されているものなので、期待されている型が HashSet だとわかっていなければ人間にとっても Lean にとっても解釈に紛れが発生します。そのため、HashSet を #eval したときは HashSet.ofList を使った表記が選ばれます。

insert 関数で要素を挿入することができますが、同じ要素を複数回挿入しても１つしか保持されません。

/- info: Std.HashSet.ofList [1] -/
#eval show (HashSet Nat) from Id.run do
  -- 空の `HashSet` を作成
  let mut s : HashSet Nat := {}
  -- `1` を２回挿入
  s := s.insert 1
  s := s.insert 1
  s

HashSet 同士の比較

2 つの s t : HashSet があるとき、「s と t のすべての構成要素が等しい」というのは、s = t ではなくて s ~m t または HashSet.Equiv s t で表現されます。

s = t は「内部実装まで含めて完全に等しい」という意味になってしまうことに注意してください。

open HashSet

example : (HashSet.ofList [1, 2]) ~m (HashSet.ofList [2, 1]) := by
  refine Equiv.of_forall_mem_iff ?_
  grind

特長

基本的なコレクション型である List と比較すると、HashSet には「要素が存在するか判定するのが高速」という特徴があります。 (要素の挿入や削除も高速ですが、ここでは存在判定に着目します。)

List では要素を順にたどって調べる必要があるのでサイズに対して線形時間かかってしまう一方で、HashSet は（良いハッシュ関数が与えられているという条件下で、平均的に）定数時間で判定することができます。実際に実験して List より高速であることを確かめたのが次のコードです。

import Lean

open Std

/-- HashSetとListで処理を共通化するための型クラス -/
class DS (col : Type) (α : Type) where
  /-- 要素があるか判定する -/
  contains : col → α → Bool

  /-- ランダムな要素を生成する -/
  gen : IO col

/-- 長さ `n` で、中身の値が 0 以上 `bound` 以下であるようなリストをランダム生成する -/
def randList (n : Nat) (bound : Nat) : IO (List Nat) := do
  let mut out := []
  for _ in [0 : n] do
    let x ← IO.rand 0 bound
    out := x :: out
  return out

/-- 実験に使用するリスト・HashSet のサイズ -/
private def sampleSize := 1000_000

/-- 実験に使用するための巨大なリストをランダム生成する -/
private def genSampleList : IO (List Nat) := do
  let size := sampleSize
  let lst ← randList size (size * 1000)
  return lst

/-- 実験に使用するための巨大な HashSet をランダム生成する -/
private def genSampleHashSet : IO (HashSet Nat) := do
  let lst ← genSampleList
  return HashSet.ofList lst

instance : DS (List Nat) Nat where
  contains := fun lst => lst.contains
  gen := genSampleList

instance : DS (HashSet Nat) Nat where
  contains := fun s x => s.contains x
  gen := genSampleHashSet

/-- 試す回数 -/
private def trial_time := 100

/-- `contain`を実行するのにかかる平均時間 -/
@[noinline]
def containAvgTime (type : Type) [inst : DS type Nat] : IO Nat := do
  let col ← inst.gen
  let mut total_time := 0
  let mut useless := false -- 実行時に最適化されないように、無駄な計算をする
  for i in [sampleSize : sampleSize + trial_time] do
    let start_time ← IO.monoNanosNow
    let b := inst.contains col i
    let end_time ← IO.monoNanosNow
    useless := !useless && b -- 無駄な計算をする
    let elapsed := end_time - start_time
    total_time := total_time + elapsed
  return total_time / trial_time

def main : IO Unit := do
  let list_avg_time ← containAvgTime (type := List Nat)
  IO.println s!"Average time for list.contains: {list_avg_time} ns"

  let hash_avg_time ← containAvgTime (type := HashSet Nat)
  IO.println s!"Average time for hashSet.contains: {hash_avg_time} ns"

  if list_avg_time < hash_avg_time then
    throw <| .userError s!"List is faster: {list_avg_time} ns < {hash_avg_time} ns"

#eval main

舞台裏

なぜ HashSet では要素が存在するかの判定が高速なのでしょうか？また HashSet α を構築するには Hashable α のインスタンス（つまり α 上のハッシュ関数）が必要ですが、なぜ必要なのでしょうか？こういった疑問に答えるには、HashSet の内部実装を知る必要があります。

実際の Lean 標準ライブラリにおける実装を紹介することはかないませんが、ここでは Array を使った チェイン法(chaining) と呼ばれる方法による実装コードを紹介します。1（これは例示のためのトイ実装ですが、それほど本質は損なわれていません）

import Lean

open Std

namespace Playground

variable {α : Type} [Hashable α] [BEq α]

/-- チェイン法（chaining）による HashSet の実装 -/
structure HashSet (α : Type) where
  /-- 内部データとしての配列 -/
  data : Array (List α)
  /-- data のサイズ -/
  size : Nat

/-- 空の HashSet。空リストばかり格納されている。 -/
def HashSet.empty (size := 10000) : HashSet α :=
  { size := size, data := Array.replicate size [] }

/-- UInt64 を Nat に自動で変換する -/
instance : Coe UInt64 Nat where
  coe n := n.toNat

/-- HashSet に新しい要素を挿入する -/
def HashSet.insert (s : HashSet α) (x : α) : HashSet α :=
  -- 内部にある配列を取得する
  let data := s.data

  -- 加えようとしている要素のハッシュ値を計算して、
  -- それをインデックスとして内部の配列にアクセスする
  let idx := hash x
  let list : List α := data[(idx : Nat) % data.size]!

  -- 既に x が存在する場合とそうでない場合で場合分けをする
  if list.contains x then
    -- 既に存在する場合はそのままの HashSet を返す
    s
  else
    -- 存在しない場合
    -- そのインデックスにあるリストに要素を追加する
    let newData := data.set! idx (x :: list)

    -- 新しいデータを持つ HashSet を返す
    { size := data.size, data := newData }

/-- HashSet に要素があるか判定する。
ハッシュ関数でインデックスを計算するので高速に判定できる。-/
def HashSet.contains (s : HashSet α) (x : α) : Bool :=
  -- 内部にある配列を取得する
  let data := s.data

  -- 加えようとしている要素のハッシュ値を計算して、
  -- それをインデックスとして内部の配列にアクセスする
  let idx := hash x
  let list : List α := data[(idx : Nat) % data.size]!

  -- そのリストに x が含まれているかどうかを返す
  list.contains x

/-- HashSet から要素を削除する。
ハッシュ関数の値でインデックスがわかるので高速に削除できる。-/
def HashSet.erase (s : HashSet α) (x : α) : HashSet α :=
  -- 内部にある配列を取得する
  let data := s.data

  -- 加えようとしている要素のハッシュ値を計算して、
  -- それをインデックスとして内部の配列にアクセスする
  let idx := hash x
  let list : List α := data[(idx : Nat) % data.size]!

  -- x が存在しない場合はそのままの HashSet を返す
  if !list.contains x then
    s
  else
    -- 存在する場合は、x を除いたリストを作成して新しい HashSet を返す
    let newData := data.set! idx (list.erase x)
    { size := data.size, data := newData }

/-- HashSet をリストに変換する。この操作には、`Ω(|s.size|)` の時間がかかる。 -/
def HashSet.toList (s : HashSet α) : List α := Id.run do
  let mut result : List α := []
  -- 内部の配列をすべて結合してリストにする
  for x in s.data do
    result := x ++ result
  return result

-- contains 関数のテスト
#guard show Bool from Id.run do
  let mut set : HashSet Nat := HashSet.empty
  set := set.insert 1
  set := set.insert 2
  set.contains 1

-- 削除のテスト
#guard show Bool from Id.run do
  let mut set : HashSet Nat := HashSet.empty
  -- 1 を２回挿入
  set := set.insert 1
  set := set.insert 1
  -- 1 を削除する
  set := set.erase 1
  ! set.contains 1

/- info: [2, 1] -/
#eval show (List Nat) from Id.run do
  let mut set : HashSet Nat := HashSet.empty
  -- 1 を２回挿入
  set := set.insert 1
  set := set.insert 1
  set := set.insert 2
  -- HashSet をリストに変換して返す
  set.toList

end Playground

使用例

足して 0 になるペアがあるか判定する

整数からなるリスト l : List Int が与えられたとします。このとき、l の中に足して 0 になるペアが存在するかどうかを判定する問題を考えます。

この問題は HashSet を使うと次のように O(|l|) 時間で解くことができます。要素が存在するかどうかを判定するのが高速という特徴が生かされていることに注目してください。もし List を使っていたら、要素が存在するかどうかの判定に Ω(|l|) 時間かかってしまうので、全体で Ω(|l|²) 時間かかってしまいます。

def findSumZeroPair (l : List Int) : Bool := Id.run do
  -- 今までに見た要素を保持するための HashSet
  let mut seen : HashSet Int := {}

  for x in l do
    -- x の補数を既に見つけていたら true を返す
    if seen.contains (-x) then
      return true

    -- そうでなければ、単に x を HashSet に追加して次へ
    seen := seen.insert x

  return false

文字列の部分文字列を重複を除いて全列挙する

文字列 s := c₀c₁..cₙ に対して、s に含まれる連続する文字列 cₖcₖ₊₁..cₗ を「s の部分文字列」といいます。

与えられた s : String に対して、s のすべての部分文字列を求める関数を考えます。このとき、部分文字列をどう数えるかの流儀が少なくとも２通り考えられます。

  • s から切り出す位置が異なっていても、文字列として同じならば部分文字列としても同じ
  • s から切り出す位置が異なっていれば、部分文字列として異なる

前者の解釈を採用したとするなら、その関数の型は String → HashSet String であるべきです。そうすれば型からより多くの情報が得られるほか、重複を除くための処理が簡潔になるからです。

/-- ある文字列の部分文字列を重複を除いて全列挙する -/
def allSubstrings (s : String) : HashSet String := Id.run do
  let mut result : HashSet String := {}
  for j in [1 : s.length + 1] do
    for i in [0 : j] do
      let sub := s.extract ⟨i⟩ ⟨j⟩
      result := result.insert sub
  return result.insert ""

#guard (allSubstrings "aaa").toList = ["", "aaa", "a", "aa"]

#guard (allSubstrings "abc").toList = ["", "abc", "bc", "c", "a", "ab", "b"]

  1. チェイン法によるハッシュテーブルの実装については、詳しくは Pat Morin著・堀江、陣内、田中訳「みんなのデータ構造」（ラムダノート）を参考にしてください。 ↩