データ型の数学基礎理論として代数

データ型の数学基礎理論として代数は、プログラミング/モデリングにおける最も基本的な代数の使い方である。ここではまず、データ型の数学基礎理論として代数を見る。

1. まず、代数データ型とは

データ型と代数データ型(Algebraic Data Type)

Wikipediaによると,

代数的データ型 - Wikipedia

代数的データ型(英: Algebraic data type)とはプログラミングにおけるデータ型の一種で、他のデータ型を当該代数的データ型のコンストラクタで包んだデータを値とする。この包まれたデータはコンストラクタの引数である。他のデータ型と異なり、コンストラクタが実行されることはなく、データを操作するにはパターンマッチを使ってコンストラクタからデータを抜き出さねばならない。


最も典型的な代数的データ型は2つのコンストラクタからなるリストである。1つは空のリストを表す Nil または []、もう1つは Cons、::、: などと表記されるコンストラクタで、短いリストに新たな要素を組み合わせるのに使われる(例えば (Cons 1 '(2 3 4)) あるいは 1:[2,3,4])。


代数的データ型の特殊な例として、プロダクト型(1つのコンストラクタだけを持つ)と列挙型(引数なしの多くのコンストラクタを持つ)がある。代数データ型は複合型(他のデータ型を組み合わせて形成される型)の一種である。


コンストラクタなしでモジュール外にエクスポートされた場合、代数的データ型は抽象データ型の一種でもある。そのような型の値の操作は、その型と同じモジュールで定義された関数を使ってのみ可能となる。


集合論において代数的データ型と等価なものとして非交和がある。この集合の各元はタグ(コンストラクタと等価)とそのタグに対応する型のオブジェクト(コンストラクタの引数と等価)で構成される。

代数データ型の理論とは,

ちなみに代数データ型における代数の特徴は以下に表れている.

  1. 演算が閉じていること

以下を参照

代数系(algebraic system)

閉じた演算

代数系 (S,*) の閉じた演算とは、演算結果も S に含まれる演算のことです。


定義1) (S,*) が閉じている def= ∀u,v ∈S , u*v∈S


 例えば、偶数の集合は演算 +,− のもとで閉じている(closed) といいます。しかし、奇数の集合に関して演算 +,− は計算結果が奇数でないため、閉じているとはいえません。整数の集合の演算÷も閉じていません。 代数系では閉じた演算が基本です。

  1. Inductive な定義が使われること

データ型の数学基礎理論として代数のまとめ

型とは集合のことである.よって,型を定義することとは,集合を定義することである.代数データがではそうした型を集合として定義するものである.代数データ型とは再帰的なデータ型のことである.
代数を用いて集合を柔軟に定義すると考えることもできるだろう。

一方で代数が集合とその上の演算から派生する数学ということからすると、演算を再帰的にもちいて集合を定義する代数データ型の代数とは少し違う代数としての役割が気になるところです。

あと再帰的に定義されたモノ(オブジェクト)の上の性質は、帰納的な証明と相性が良い。


参考;再帰帰納の違いは?