10 LISP primitives analogous to 5 axioms of Euclidean geometry?

Up vote 3 down vote favorite share g+ share fb share tw.

LISP can be built from ten primitives: The primitives are: atom, quote, eq, car, cdr, cons, cond, lambda, label, apply. Apparently these are equivalent to the 5 axioms of Euclidean geometry. hyperpolyglot.wikidot.com/lisp Can anyone explain how they are equivalent?

Lisp geometry primitive axiom link|improve this question asked Jul 11 '10 at 10:47hawkeye2,2041344 85% accept rate.

It only says: The primitives are analogous to the 5 axioms of Euclidean plane geometry. Which doesn't express equivalence. As far as I can tell the author just draws an analogy and wants to say that LISP is constructed from its ten atoms, just like Euclid's plane geometry is constructed from its five axioms.

Poor analogy though.

You don't need all those primitives. Much can be done with LAMBDA alone, like integer numerics, ... In real life Lisps have more primitives.

Well, the only thing I can think of is that all of Euclidean geometry can be derived starting from those 5 axioms (e.g. See The Elements), just like how apparently all of LISP can be built from those ten primitives. For the lazily curious, here is one phrasing of Euclid's five axioms, from Wikipedia: To draw a straight line from any point to any point. To produce extend a finite straight line continuously in a straight line.

To describe a circle with any center and distance radius. That all right angles are equal to one another. The parallel postulate: That, if a straight line falling on two straight lines make the interior angles on the same side less than two right angles, the two straight lines, if produced indefinitely, meet on that side on which are the angles less than the two right angles.

They are comparable in that they are sufficient to implement all of Lisp, just as you can derive all of planar geometry from these axioms. But they have nothing to do with geometry particularly. So that's not equivalence, just a general similarity.

(A more interesting property of the Euclidian axioms is that you can negate one of them and get a different system, which is nevertheless very useful (non-planar gemometry). But I'm not sure whether the same holds for Lisp primitives, and I doubt the author had this in mind. ).

The claim is NOT that theorems in plane geometry can be proven using Lisp primitives. To think that is to miss the analogy. I rewrote the sentence to hopefully discourage people from thinking that.

The correct analogy is not new; Graham's paper opens with the observation that McCarthy "did for programming something like what Euclid did for geometry. " Systems of mathematical reasoning were on McCarthy's mind when he was designing Lisp. In his 1979 retrospective on the history of Lisp, he notes that "it is now easier to prove that pure Lisp programs meet their specifications than it is for any other programming language in extensive use.

" And this is because Lisp primitives have referential transparency, a property they share with mathematical notation. Any program which can be implemented by the primitives shares the property. Mathematical neatness pays dividends when you have to reason about your program.

The concept that "a proof is a program" is made precise by the Curry-Howard correspondence. References: McCarthy on "mathematical neatness" the Curry-Howard Correspondence (wikipedia) The Roots of Lisp, Paul Graham Referential Transparency (wikipdia).