LISPは、10個のプリミティブから構築できます。プリミティブは、atom、quote、eq、car、cdr、cons、cond、lambda、label、applyです。
どうやらこれらはユークリッド幾何学の5つの公理に相当します。 http://hyperpolyglot.wikidot.com/lisp
誰かがそれらがどのように同等であるかを説明できますか?
LISPは、10個のプリミティブから構築できます。プリミティブは、atom、quote、eq、car、cdr、cons、cond、lambda、label、applyです。
どうやらこれらはユークリッド幾何学の5つの公理に相当します。 http://hyperpolyglot.wikidot.com/lisp
誰かがそれらがどのように同等であるかを説明できますか?
それは言うだけです:
プリミティブは、ユークリッド平面幾何学の5つの公理に類似しています。
これは同等性を表していない。私が知る限り、著者は類推を描いており、Euclidの平面幾何学が5つの公理から構築されているのと同じように、LISPは10個の原子から構築されていると言いたい。
しかし、アナロジーは貧弱です。
これらすべてのプリミティブは必要ありません。整数の数値のように、LAMBDAだけで多くのことができます...
実生活では、Lispにはより多くのプリミティブがあります。
本当に?さて、私が考えることができる唯一のことは、すべてのLISPがこれらの10個のプリミティブから構築できるように、すべてのユークリッド幾何学がこれらの5つの公理から導出できることです(たとえば、The Elementsを参照)。
怠惰な好奇心のために、ウィキペディアからのユークリッドの5つの公理の1つの言い回しがあります:
これらの公理からすべての平面ジオメトリを導出できるのと同じように、これらはすべてのLispを実装するのに十分であるという点で同等です。しかし、それらは特に幾何学とは何の関係もありません。つまり、これは同等ではなく、一般的な類似性にすぎません。
(ユークリッド公理のより興味深い特性は、それらの1つを否定して別のシステムを取得できることですが、それでも非常に便利です(非平面ジェモメトリー)。しかし、同じことがLispプリミティブにも当てはまるかどうかはわかりません。著者がこれを念頭に置いていたとは思えません。)
主張は、平面幾何学の定理がLispプリミティブを使用して証明できるということではありません。それを考えることは、アナロジーを見逃すことです。うまくいけば人々がそれを考えるのを思いとどまらせるために、私は文を書き直しました。正しいアナロジーは新しいものではありません。グラハムの論文は、マッカーシーが「ユークリッドが幾何学に対して行ったようなものをプログラミングするために行った」という観察から始まります。
マッカーシーがLispを設計していたとき、数学的な推論のシステムが頭に浮かびました。Lispの歴史に関する1979年の回顧展で、彼は「純粋なLispプログラムが、広く使用されている他のプログラミング言語よりも仕様を満たしていることを証明するのが簡単になりました」と述べています。これは、Lispプリミティブが参照透過性を持っているためです。これは、数学表記と共有するプロパティです。プリミティブによって実装できるすべてのプログラムは、プロパティを共有します。あなたがあなたのプログラムについて推論しなければならないとき、数学的なきちんとしたことは利益をもたらします。
「証明はプログラムである」という概念は、カリー・ハワード同盟によって正確に作られています。
参照:
カリーハワード通信(ウィキペディア)
Lispのルーツ、ポール・グレアム
参照透過性(wikipdia)
アランケイはそれをうまく言います:マクスウェルのソフトウェア方程式!
「...それは私が大学院にいたときの大きな啓示でした。Lisp1.5マニュアルの13ページの下部にあるコードの半分のページがそれ自体がLispであることがようやくわかったときです。これらは「マクスウェルの方程式ソフトウェア!" これは、私が手渡すことができる数行のプログラミングの全世界です。」