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