I thought the same thing for a long time, I found s-expressions very elegant. Then I discovered lambda-calculus, with its scary syntax but based on a process I could understand, text-rewriting. So I had the idea to explore the lambda-calculus using s-expressions and patiently rebuilt booleans, pairs, lists, recursion and beyond a real complete Turing language, for instance:
No need for cons, car, cdr and other historical names. We can rebuild everything from scratch, from abstractions and applications. No need for Lisp, Scheme, Common Lisp and other Clojure, even if they remain excellent examples. So in my opinion the Maxwell equations of computation are to be seen more in the lambda-calculus than in LISP and its dialects. We just need to make the syntax a little more human.
I agree that Maxwell’s Equations of Software should be based on lambda calculus,
the binary version of which [1] admits a much more concise 29 byte self-interpreter
I agree with you, but so far I have never been able to get into the logic of de Bruijn's clues. As for example John Tromp knows how to do. (https://tromp.github.io/) But I don't despair of getting there one day...
I was going to say I had heard that this was the intention of Lisp's creators, then I thought I had better check, and immediately found this:
Lisp had assignments and goto before it had recursion, and started as a dialect of Fortran! It was only later that Lisp programmers investigated the benefits of pure functions. Lisp was not based on lambda calculus, but rather Kleene's work on recursive functions. At the time, McCarthy had heard of lambda calculus but had not yet studied it!
The list processing in Lisp was inspired by FLPL: Fortran List Processing Language. This was more like a library of Fortran routines than a language, but in 1958 the term library for routines of code didn't even exist. Making new words of any kind was language development.
FLPL already used the CAR and CDR terminology in its naming, with extra characters: XCARF and XCDRF (and others). The "extract CAR function" and "extract CDR function".
As far as I understand, McCarthy was into Godel, recursive functions, mathematics, and AI in trying to create Lisp to study these, not so much computability and the like. I think that's at least one line of thinking that causes people to say that McCarthy discovered Lisp instead of inventing it.
For the reasons you give, it is perhaps more reasonable to say that Lisp is a Maxwell's Equations of software. But there are several. Forth has another reasonable claim to it, despite unpopularity, and Turing Machines have a claim too, despite their extreme unpopularity as a programming methodology. I don't know array languages well enough to know but I bet they have one too.
There isn't really a unique set of Maxwell's equations in software.
i wasn't able to get a runnable forth to less than a couple of pages written in itself https://github.com/kragen/stoneknifeforth but schönfinkel's ski-combinators are maybe the simplest practical basis
s f g x → f x (g x)
k a b → a
i = s k k (one of many possible definitions)
maybe wolfram knows of a simpler alternative
my favorite is abadi and cardelli's object-calculus on which i based bicicleta. it has two reduction rules rather than the λ-calculus's one. using a hybrid of bicicleta's syntax and abadi and cardelli's
{f = ς(v)b, g = ς(v)c, ...}{f = ς(v)d} → {f = ς(v)d, g = ς(v)c, ...}
{f = ς(v)b, g = ς(v)c, ...}.f → b[{f = ς(v)b, g = ς(v)c, ...}/v]
the first of these derives an inherited object with a new definition for method f. the second one invokes method f on an object, which is evaluated by replacing its self-variable v with the object itself throughout its body, using the standard β-reduction semantics with α-renaming that we're familiar with from the λ-calculus (b[x/y] means b but with x replacing y)
despite the simplicity of the semantics the ς-calculus is enormously more usable for actually writing down functions than the λ-calculus. here's factorial(10) in the notation above (untested)
in particular to be able to define infix operators inside the language, bicicleta rewrites
x * y
as
x.'*'{arg1 = y}.'()'
and analogously for -, <, etc.
they published a bunch of papers and a book on this but they were more interested in static typing than anything else. a paper on one imperative variation of the thing is http://lucacardelli.name/Papers/PrimObjImpSIPL.A4.pdf
you can implement a turing machine in a few lines of c, making it internally simpler than the other alternatives, but as you point out it's unusable except as a compilation target or to prove theorems about
Nice take on lambda calc! It looks like you're making use of beta-reduction for the eval engine.
Shen has a more formal take on lambda calc, and I think it's useful for more advanced constructs like type checking. Shen actually uses K-lambda (a lispish version of lambda calc) as part of it's compiler Sequent-calc->Prolog->Shen->K-lambda->VM:
No need for those pesky variable names that make term rewriting clunk either[1]! The entire hygiene problem just disappears. Your style guide section on naming will also be greatly simplified.
I agree with you, but so far I have never been able to get into the logic of de Bruijn's clues. As for example John Tromp knows how to do. (https://tromp.github.io/) But I don't despair of getting there one day...
The Curry-Howard correspondence suggests the analogy of computation with lambda calculus and logical proof systems. As a non-expert it seems that same analogy extends roughly to lambda calculus and a lisp system
The Curry-Howard Correspondence is about proof systems. You would have a very hard time finding a proof theorist that says it's okay to have an undecidable proof checker or an inconsistent one.
For that reason, only _typed_ lambda calculi have any hope of corresponding to a proof system. You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent.
Perhaps a para-consistent logic might work, but we're getting very exotic here.
>So I had the idea to explore the lambda-calculus using s-expressions and patiently rebuilt booleans, pairs, lists, recursion and beyond a real complete Turing language, for instance:
Syntax is not semantics.
The only thing that s-expressions do that is mathematically interesting is make the abstract syntax tree of expressions explicit in a way that standard notation does not. The whole point of them is that they make string rewriting into tree rewriting which is vastly easier and makes writing your own DSLs a breeze.
From a practical point of view they are also the simplest way to serialize any expression which is why I can type them out in a text only comment as they are. Meanwhile doing the same with a math (or lambda calculus) expression requires a type setting system like latex to be understandable.
Lisp has decided that application is nameless in its syntax which means that things like ((lambda (x) (+ x 1)) 2) work when semantically they mean (apply (lambda (x) (+ x 1)) 2). This makes programming with multivariable functions very clean but partial application incredibly messy, e.g. ((((lambda (x) (lambda (y) (lambda (z) (+ x y z)))) 1) 2) 3). This is not something that can be fixed because the ABS of partial application when thought of as a tree is indeed very messy. The only reason why it works in languages like Haskell as well as it does is that as long as you only have single variable function - goodbye thunks and multivariable functions - you can treat the partial application trees as a list instead.
You can of course do the same in lisp using a DSL:
'(partial
((lambda (x)) (lambda (y)) (lambda (z)) (lambda (w) (+ x y z w)))
(1 2 3 4))
But it doesn't fit very well with the rest of the language and feel quite pointless.
@thrown: This makes programming with multivariable functions very clean but partial application incredibly messy
In lambdatalk the implementation of lambdas does not make them closures (no free variables) but is such that they accept de facto partial application and a number of values higher than the number of arguments. This compensates for the lack of closure. So for instance:
((lambda (x)) (lambda (y)) (lambda (z)) (lambda (w) (+ x y z w))) (1 2 3 4))
is written this way
{{{{{lambda {x y z w} {+ x y z w}} 1} 2} 3} 4}
-> 10
I would change it a bit. Lambda calculus (in Martin-Lof type theory) are Maxwell equations of logic. But, lambda calculus has very little real use in programming. There should be something else here.
Maxwell's Equations are an interesting analogy. As they were originally written, they were cumbersome and hard to understand. Along came Oliver Heaviside, who translated them into the notation of vector calculus, resulting in the form that remains in use today. But even the present form is not without its detractors, and I've read comments in this forum to the effect that a better notation would make them even less forbidding for students.
Algebra has a similar history too. You practically had to be a philosopher to understand algebra as described by Al-Khwarizmi's book -- there are no numerals or equations, just a wall of text. The notation of equations hadn't been invented yet. Today, thanks in part to gradual development of notation, we can teach algebra to schoolchildren.
I think there are probably many developments, where the brilliant invention, and the language that can be understood by the rest of us, had to come from two different people.
Interestingly, the article users the nowadays standard 4-equation form of the Maxwellian concept - but Maxwell himself used 20 equations [1]. The current version is due to Oliver Heaviside (who doesn't get enough respect for this).
As I understand things, Maxwell's work was held in high regard, but only became usable due to Heaviside's reformulation.
Whether that aspect (beautiful but unusable) is true and carries over to Lisp... dunno, I'm insufficiently familiar with Lisp. But the xkcd with brackets [2] comes to mind.
Maxwell's equations address only part of physics. E.g. you can't describe anything nonlinear with it, like transistors.
Also, it is quite difficult to prove that Maxwell's equations have a single solution for different boundary conditions. For lambda calculus it is quite easy, there can only be one solution.
Heaviside promoted Maxwell's equations and created clearer, simpler versions of them. So I think it would be a language that uses list processing and functional concepts as a feature of a syntax that is easier for beginners. Something like Python or JavaScript.
I think a more astute argument would be that Backus-Naur Form is the Maxwells Equations, since that's what the definition of LISP is written in on the 1/2 page screenshot that starts the OP's thesis.
Readit News
- http://lambdaway.free.fr/lambdawalks
- http://lambdaway.free.fr/lambdawalks/?view=lambdacode5
No need for cons, car, cdr and other historical names. We can rebuild everything from scratch, from abstractions and applications. No need for Lisp, Scheme, Common Lisp and other Clojure, even if they remain excellent examples. So in my opinion the Maxwell equations of computation are to be seen more in the lambda-calculus than in LISP and its dialects. We just need to make the syntax a little more human.
Maybe there's an infinite amount of mathematical theories that are turing complete. Why is lambda calculus chosen as the foundational one?
I would argue, the Maxwells equation of software should be MORE foundational. Not some arbitrarily specific turing complete language.
This is what I think it should be (link is a comment in the same thread): https://news.ycombinator.com/item?id=33533321
Lisp had assignments and goto before it had recursion, and started as a dialect of Fortran! It was only later that Lisp programmers investigated the benefits of pure functions. Lisp was not based on lambda calculus, but rather Kleene's work on recursive functions. At the time, McCarthy had heard of lambda calculus but had not yet studied it!
https://crypto.stanford.edu/~blynn/lambda/lisp.html
FLPL already used the CAR and CDR terminology in its naming, with extra characters: XCARF and XCDRF (and others). The "extract CAR function" and "extract CDR function".
There isn't really a unique set of Maxwell's equations in software.
my favorite is abadi and cardelli's object-calculus on which i based bicicleta. it has two reduction rules rather than the λ-calculus's one. using a hybrid of bicicleta's syntax and abadi and cardelli's
the first of these derives an inherited object with a new definition for method f. the second one invokes method f on an object, which is evaluated by replacing its self-variable v with the object itself throughout its body, using the standard β-reduction semantics with α-renaming that we're familiar with from the λ-calculus (b[x/y] means b but with x replacing y)despite the simplicity of the semantics the ς-calculus is enormously more usable for actually writing down functions than the λ-calculus. here's factorial(10) in the notation above (untested)
bicicleta has a lot of syntactic sugar which reduces this to (tested) in particular to be able to define infix operators inside the language, bicicleta rewrites as and analogously for -, <, etc.they published a bunch of papers and a book on this but they were more interested in static typing than anything else. a paper on one imperative variation of the thing is http://lucacardelli.name/Papers/PrimObjImpSIPL.A4.pdf
you can implement a turing machine in a few lines of c, making it internally simpler than the other alternatives, but as you point out it's unusable except as a compilation target or to prove theorems about
https://shenlanguage.org/TBoS/tbos_170.html
[1] https://en.wikipedia.org//wiki/De_Bruijn_index
Deleted Comment
For that reason, only _typed_ lambda calculi have any hope of corresponding to a proof system. You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent.
Perhaps a para-consistent logic might work, but we're getting very exotic here.
Syntax is not semantics.
The only thing that s-expressions do that is mathematically interesting is make the abstract syntax tree of expressions explicit in a way that standard notation does not. The whole point of them is that they make string rewriting into tree rewriting which is vastly easier and makes writing your own DSLs a breeze.
From a practical point of view they are also the simplest way to serialize any expression which is why I can type them out in a text only comment as they are. Meanwhile doing the same with a math (or lambda calculus) expression requires a type setting system like latex to be understandable.
Lisp has decided that application is nameless in its syntax which means that things like ((lambda (x) (+ x 1)) 2) work when semantically they mean (apply (lambda (x) (+ x 1)) 2). This makes programming with multivariable functions very clean but partial application incredibly messy, e.g. ((((lambda (x) (lambda (y) (lambda (z) (+ x y z)))) 1) 2) 3). This is not something that can be fixed because the ABS of partial application when thought of as a tree is indeed very messy. The only reason why it works in languages like Haskell as well as it does is that as long as you only have single variable function - goodbye thunks and multivariable functions - you can treat the partial application trees as a list instead.
You can of course do the same in lisp using a DSL:
But it doesn't fit very well with the rest of the language and feel quite pointless.In lambdatalk the implementation of lambdas does not make them closures (no free variables) but is such that they accept de facto partial application and a number of values higher than the number of arguments. This compensates for the lack of closure. So for instance:
((lambda (x)) (lambda (y)) (lambda (z)) (lambda (w) (+ x y z w))) (1 2 3 4))
is written this way
{{{{{lambda {x y z w} {+ x y z w}} 1} 2} 3} 4} -> 10
and obviously
{{lambda {x y z w} {+ x y z w}} 1 2 3 4} -> 10
Algebra has a similar history too. You practically had to be a philosopher to understand algebra as described by Al-Khwarizmi's book -- there are no numerals or equations, just a wall of text. The notation of equations hadn't been invented yet. Today, thanks in part to gradual development of notation, we can teach algebra to schoolchildren.
I think there are probably many developments, where the brilliant invention, and the language that can be understood by the rest of us, had to come from two different people.
Lisp as the Maxwell’s Equations of Software (2012) - https://news.ycombinator.com/item?id=23687904 - June 2020 (46 comments)
Lisp as the Maxwell’s equations of software (2012) - https://news.ycombinator.com/item?id=9607843 - May 2015 (8 comments)
Lisp as the Maxwell Equations of Software (2012) - https://news.ycombinator.com/item?id=9038505 - Feb 2015 (122 comments)
Lisp as the Maxwell’s equations of software - https://news.ycombinator.com/item?id=3830867 - April 2012 (37 comments)
As I understand things, Maxwell's work was held in high regard, but only became usable due to Heaviside's reformulation.
Whether that aspect (beautiful but unusable) is true and carries over to Lisp... dunno, I'm insufficiently familiar with Lisp. But the xkcd with brackets [2] comes to mind.
[1] https://en.m.wikipedia.org/wiki/History_of_Maxwell%27s_equat...
[2] https://xkcd.com/297/
Also, it is quite difficult to prove that Maxwell's equations have a single solution for different boundary conditions. For lambda calculus it is quite easy, there can only be one solution.
https://en.wikipedia.org/wiki/Oliver_Heaviside
https://www.youtube.com/watch?v=dCuZkaaou0Q