一様性原理

長谷川の一様性原理：

 f:A+X→B+X, g:A+Y→B+Y, ψ;X→Y,  f;(B+ψ) = (A+ψ);g

 -----------------------------------------------------[HU]

 Tr(f)  = Tr(g) : A→B

プロトキン（Plotkin）の一様性原理：

 f:A+X→X, g:A+Y→Y, ψ;X→Y,  f;ψ = (A+ψ);g

 -----------------------------------------------------[PU]

 Fix(f);ψ = Fix(g) : A→Y

クリーネ／コゥゼン（Kleene/Kozen）の一様性原理：

 f:X→X, g:Y→Y, ψ;X→Y,  f;ψ = ψ;g

 -----------------------------------------------------[KU]

 Rep(f);ψ  = ψ;Rep(g) : X→Y

クリーネ／コゥゼンの帰納原理（スター帰納法）：

 f:X→X, ψ;X→Y,  f;ψ ≦ ψ

 -----------------------------------------------------[KI-1]

 Rep(f);ψ ≦ ψ : X→Y
 g:Y→Y, ψ;X→Y,  ψ;g ≦ ψ

 -----------------------------------------------------[KI-2]

 ψ;Rep(g) ≦ ψ : X→Y