1 + 1 = 2 をプログラミングで理解する

TypeScript

Legalscape のしろくまです。

自然数の集合論的定義（フォン・ノイマンの構成）は空集合の公理と無限の公理を利用して 以下のようになります。

  • 0 = ∅
  • 1 = {0} = {∅}
  • 2 = {0, 1} = {∅, {∅}}
  • 3 = {0, 1, 2} = {∅, {∅}, {∅, {∅}}}
  • ・・・

また加算は S(n) = n ∪ {n} としたとき、以下のように再帰的に定義されます。

  1. A + 0 = A
  2. A + S(B) = S(A + B)

しかしながら以上の説明で物事が理解できるのは1 + 1 = 2を証明できる人だけなので、皆さまのお子様は満足しないかもしれません。

ところで、 TypeScript では再帰的に型を定義したり、infer したりすることが可能なので
上記の定義を簡易的にシミュレートすることが可能です。
never 型が登場するなど粗さはありますが、以下のように書けます。

type ZERO = [];
type S<T> = T extends (infer U)[] ? [...T, T] : never;

type ADD<A, B> = B extends S<infer C> ? S<ADD<A, C>> : A;
type N_1 = S<ZERO>;
type N_2 = ADD<N_1, N_1>;
type N_4 = ADD<N_2, N_2>;

// 以下はコンパイル可能
const x: N_1 = [[]];
const y: N_2 = [[], [[]]];

読んでいるだけだと、数学的な定義を読んでいるのとほぼ変わらない感覚かと思いますのでPlaygroundで数字を変化させたり、定義を操作してみると実感を得られるのではないかと思います。

これでお父さんが 1 + 1 = 2 の証明を求められた場合でも、
TypeScript が得意なお子さんであれば実感を伴った説明をすることができます。

Legalscape では TypeScript が得意なエンジニアを随時募集しております。