Wikipedia: Algebraic data typeには、 Algebraic data types were introduced in Hope, a small functional programming language developed in the 1970s at the University of Edinburgh. とある。 Hope という言語で導入されたようだ
しかし、Hope を調べても、データ構造のところで algebraic という語は出てこない
では、Haskell からたどるか
では Mirandaか、ということで以下を見ると、これっぽいな
Algebraic data types というのが出てきて、free algebra を宣言する機能とある。 free algebra というのは、law がなく、同じように作られたものだけが等しいということのようだ。 以下のように書いてある。
We call it a free algebra, because there are no associated laws, such as a law equating a tree with its mirror image. Two trees are equal only if they are constructed in exactly the same way.
そして、Unfree algebras というのがその次に出てきて、free algebra に law を追加できるという機能が述べられている。 しかし、An Overview of Miranda によると、 この機能は初期のMirnadaにあったが、あまり使われず消されたとのこと。
代数的データ型というのは ML や Haskell にあるやつで、型があって、コンストラクタがいくつかあって、というものだが、 よく似ているものとして、Coq の 帰納型 (Inductive type) と 余帰納型 (Coinductive type) がある。
帰納型と余帰納型はどちらも、型があって、コンストラクタがいくつかあって、というもので、 代数的データ型と同じなのだが、なにが違うのだろうか。 あるいは同じなのだろうか。
まぁ、帰納型と余帰納型というふたつがあるということで、 それぞれが代数的データ型のサブセットだろう、とは想像がつく
たぶん、帰納型は帰納法が使えるもので、余帰納型は余帰納法が使えるものなんじゃないかな、おそらく。 名前からしても。
帰納型は帰納法を使えるように、Positivity Condition とか条件がついているわけだし。
逆に、Miranda の代数的データ型は、(Miranda は Haskell と同じく lazy なので) big = Node 1 big big みたいな無限構造を作れるため、 帰納法はいつも使えるとは限らない。 (big の例は Miranda: A non-strict functional language with polymorphic types からとってきた)
SSReflect では、Coq の述語 (命題を返す関数) と bool を返す判定関数を相互に変換する small scale reflection が多用される。 そもそも SSReflect という名前がこの機能に由来している。
で、この機能の利点をいろいろな文献がどう説明しているのか調べてみた。 Mathematical Components: Documentation からいろいろな文献がたどれるので、 SSReflect の紹介ぽいところで reflection の利点を述べているところを探してみた。 この機能は SSReflect の目玉機能なので、SSReflect の紹介をするところでなんらかの説明があるのである。
で、以下のような話が見つかった。
ポアンカレ原理というのは、ポアンカレがリーズニングよりも計算を用いるほうが証明が簡略化される、ということを言及していたらしい。 (1902年ということなので、たぶん「科学と仮説」だと思うけれど、確認していない。)
SSReflect では、eqP, andP, leP, ifP とか、名前が P で終わる補題がいろいろ用意されている。 ifPn とか maxn_idPl とか、名前の途中に入っているものもあるが。
この P はなんの略なのか調べてみた。
mathcomp book には、 "The name of a reflection view always ends with a capital P." と書いてあるが、P がなんなのかはわからない。
まぁ、オリジナルを調べるか、ということで、 A computer-checked proof of the Four Color Theorem をみると、 "We prove such properties for all Boolean predicates that have a useful logical counterpart; for a predicate foob, the corresponding lemma is fooP." という記述が見つかった。
(SSReflect は、4色問題の証明を Coq で書く中で作られたライブラリが元になっているので、この論文の中で SSReflect の話が出てくるのである)
この記述からすると、properties の P かなぁ
bool を返す述語 foob に対して、その性質 (properties) を示す補題 fooP があるということですかね。
しかし、bool を返す述語が foob という名前というのは SSReflect ぽくないな。 むしろ、vanilla Coq ぽい
nat の比較関数 (nat -> nat -> bool) は vanilla Coq だと Nat.eqb で、 SSReflect だと eqn となっている。 (そして eqn に対応して eqnP がある)
4色問題の証明は GitHub に公開されているのでちょっとみてみるが、bool な述語が b で終わっている感じではない。 cfcontract.v だと、 contract_ctree に対して contract_ctreeP がある
foob というのは説明で bool を返すニュアンスを出したかったんですかね
[latest]