帰納的に定義された構造

リスト

集合 X, Y に対して、X×Y, X+Y を、 以下の条件をみたす写像が存在する集合とします。
  1. p: X×Y→X, p(X×Y) = X
  2. q: X×Y→Y, q(X×Y) = Y
  3. s = t ⇔ p(s) = p(t) ∧ q(s) = q(t)
  4. i: X→X+Y
  5. j: Y→X+Y
  6. i(X)∪j(Y) = X+Y
  7. i(X)∩j(Y) = φ
集合 T を、以下の条件をみたす写像が存在する最小のものとします。
  1. nil ∈ T
  2. cons: E×T→T
  3. p: cons(E×T)→T, p(cons(x, y)) = x
  4. q: cons(E×T)→T, q(cons(x, y)) = y
x∈T に対して、T(x) を
  1. x∈{nil} ⇒ T(x)={nil}
  2. x∈X, y∈Y ⇒ T(cons(x, y))=cons(X, Y)
と定義します。 T' = T+E+{0} として、p', q': T'→T'
  1. p': T'→T', x∈cons(E×T) のとき p'(x)=p(x), それ以外のとき p'(x)=0
  2. q': T'→T', x∈cons(E×T) のとき q'(x)=q(x), それ以外のとき q'(x)=0
と定義します。 S を p', q' で生成される T'→T' の部分集合とします。 x∈T に対して、dom(x, T+E)={f∈S|f(x)∈T+E}, dom(x, E)={f∈S|f(x)∈E} と定義します。 x∈T に α: dom(x, E)→E, α(f)=f(x) を対応させます。 dom(x, E) = {p', p'q', p'q'q', …} となります。 これを {0, 1, 2, …, n} と考えると、 x∈T に α: {0, 1, 2, …, n}→E を対応させることができます。 この対応は次の方法でも定義できます。
  1. x∈cons(y, z)、 y に g: Y→W, z に h: Z→W が対応しているとき、 x に f: Y+Z→W, y∈Y のとき f(y)=g(y), z∈Z のとき f(z)=h(z) を対応させます。
x∈T に β: dom(x, T+E)→{nil, cons}+E, f(x)∈{nil}のときβ(f)=nil, f(x)∈cons(T, T)のときβ(f)=cons, f(x)∈Eのときβ(f)=f(x) を対応させます。 x∈T に対して ψ(x): {0}→T, ψ(x)(0)=x とします。 f: X→T, g: Y→T に対して cons~(f, g): X×Y→T, cons~(f, g)(x, y)=cons(f(x), g(y)) として、 e∈E に対して、e~: {0}→T を e~(0)=e として、 nil~: {0}→{nil} を nil~(0)=nil として Γ を e~, nil~, cons~ を有限回合成したもの全体とします。 f∈dom(x, T+E) に対して ψ(x)=γδ, γ(f(x))=x となる γ∈Γ, δ∈Γ が存在します。 δ は項 x の一部に現れる項に対応します。 項 x の項 δ のところを項 y で置き換えた項は γ(y) となります。

2分木

集合 T を、以下の条件をみたす写像が存在する最小のものとします。
  1. atom: A→T
  2. cons: T×T→T
  3. r: atom(A)→A, r(atom(x)) = x
  4. p: cons(T×T)→T, p(cons(x, y)) = x
  5. q: cons(T×T)→T, q(cons(x, y)) = y
x∈T に対して、T(x) を
  1. x∈atom(A) ⇒ T(x)=atom(A)
  2. x∈X, y∈Y ⇒ T(cons(x, y))=cons(X, Y)
と定義します。 T' = T+A+{0} として、r', p', q': T'→T'
  1. r': T'→T', x∈atom(A) のとき r'(x)=r(x), それ以外のとき r'(x)=0
  2. p': T'→T', x∈cons(T×T) のとき p'(x)=p(x), それ以外のとき p'(x)=0
  3. q': T'→T', x∈cons(T×T) のとき q'(x)=q(x), それ以外のとき q'(x)=0
と定義します。 S を r', p', q' で生成される T'→T' の部分集合とします。 x∈T に対して、dom(x, T+A)={f∈S|f(x)∈T+A}, dom(x, A)={f∈S|f(x)∈A} と定義します。 x∈T に α: dom(x, A)→A, α(f)=f(x) を対応させます。 この対応は次の方法でも定義できます。
  1. x∈atom(A) のとき、x に f:{0}→A, f(0)=r(x) を対応させます。
  2. x∈cons(y, z)、 y に g: Y→W, z に h: Z→W が対応しているとき、 x に f: Y+Z→W, y∈Y のとき f(y)=g(y), z∈Z のとき f(z)=h(z) を対応させます。
x∈T に β: dom(x, T+A)→{atom, cons}+A, f(x)∈atom(A)のときβ(f)=atom, f(x)∈cons(T, T)のときβ(f)=cons, f(x)∈Aのときβ(f)=f(x) を対応させます。 x∈T に対して ψ(x): {0}→T, ψ(x)(0)=x とします。 f: X→T, g: Y→T に対して cons~(f, g): X×Y→T, cons~(f, g)(x, y)=cons(f(x), g(y)) として、 a∈A に対して、a~: {0}→T を a~(0)=atom(a) として Γ を a~, cons~ を有限回合成したもの全体とします。 f∈dom(x, T+A) に対して ψ(x)=γδ, γ(f(x))=x となる γ∈Γ, δ∈Γ が存在します。 δ は項 x の一部に現れる項に対応します。 項 x の項 δ のところを項 y で置き換えた項は γ(y) となります。

参考文献

  1. 小野寛晰: 情報代数, 共立出版, 1994.