LISP может быть построен из десяти примитивов: Примитивами являются: атом, котировка, эквалайзер, автомобиль, cdr, cons, cond, lambda, label, apply.10 примитивов LISP, аналогичных 5 аксиомам евклидовой геометрии?
По-видимому, они эквивалентны 5 аксиомам евклидовой геометрии. http://hyperpolyglot.wikidot.com/lisp
Может ли кто-нибудь объяснить, насколько они эквивалентны?
Он только говорит:
Примитивы аналогичны 5 аксиом евклидовой планиметрии.
Который не выражает эквивалентности. Насколько я могу судить, автор просто рисует аналогию и хочет сказать, что LISP построен из своих десяти атомов, точно так же, как плоская геометрия Евклида построена из пяти ее аксиом.
Плохая аналогия.
Действительно? Единственное, о чем я могу думать, это то, что всю евклидову геометрию можно получить, исходя из этих 5 аксиом (например, см. The Elements), точно так же, как очевидно, что все LISP можно построить из этих десяти примитивов.
Для лениво любопытно, вот одна формулировки Евклида пяти аксиом, из Wikipedia:
Они сопоставимы с тем, что их достаточно для реализации всех Lisp, так же, как вы можете получить всю плоскую геометрию из этих аксиом. Но они не имеют ничего общего с геометрией. Так что это не эквивалентность, просто общее сходство.
(Более интересное свойство аксиом Евклида состоит в том, что вы можете свести на нет одну из них и получить другую систему, которая, тем не менее, очень полезна (непланарная гемометрия). Но я не уверен, Lisp, и я сомневаюсь, что автор имел это в виду.)
Вам не нужны все эти примитивы. Многое можно сделать только с помощью LAMBDA, например, целочисленных чисел, ...
В реальной жизни у Lisps больше примитивов.
Утверждение не является то, что теоремы в плоской геометрии могут быть доказаны с использованием примитивов Lisp. Думать, что это пропустить аналогию. Я переписал предложение, надеясь, что это не позволит людям думать об этом. Правильная аналогия не нова; Статья Грэма открывается замечанием, что Маккарти «сделал для программирования что-то вроде того, что сделал Евклид для геометрии.«
Системы математического мышления были умом Маккарти, когда он разрабатывал Lisp. В своей ретроспективе 1979 года по истории Лиспа он отмечает, что« теперь легче доказать, что чистые программы Lisp соответствуют их спецификациям, чем для любой другой язык программирования в широком использовании ». И это потому, что примитивы Lisp имеют ссылочную прозрачность, свойство, которое они разделяют с математической нотацией. Любая программа, которая может быть реализована примитивами, разделяет свойство. Математическая аккуратность выплачивает дивиденды, когда вы должны рассуждать о ваша программа.
понятие, что «доказательство программа» сделано точное соответствие Карри-Говард.
Ссылки:
McCarthy on "mathematical neatness"
Карри-Говарда Переписка (википедия)
Корни Лиспе, Пол Грэм
ссылочной прозрачности (wikipdia)
Алан Кей ставит это хорошо: Уравнения Максвелла программного обеспечения!
»... это было большим откровением для меня, когда я был в аспирантуре школьного, когда я, наконец, понял, что половина страницы кода на внизу страницы 13 Лиспа 1.5 руководства был Лисп в Эти были «уравнениями Максвелла программного обеспечения!» Это целый мир программирования в нескольких строках, которые я могу передать ».