Lisp as the Maxwell’s Equations of Software (2012)
michaelnielsen.org
michaelnielsen.org
- 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.
There isn't really a unique set of Maxwell's equations in software.
s f g x → f x (g x)
k a b → a
i = s k k (one of many possible definitions)
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]
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)
{fac = ς(env){
n = ς(_)3,
return = ς(o)
(o.n < 2).if_true{
then = ς(_)1
else = ς(_)o.n * env.fac{n = ς(_)o.n - 1}.return
}.return
}
}.fac{n = ς(10)}.return
{env: fac = {fac:
arg1 = 3
'()' = (fac.arg1 < 2).if_true(
then = 1
else = fac.arg1 * env.fac(fac.arg1 - 1)
)
}}.fac(10)
x * y
x.'*'{arg1 = y}.'()'
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
Wolfram on combinators:
https://writings.stephenwolfram.com/2020/12/combinators-a-ce...
not any simpler, but maybe these are:
Okay, but how much code goes into creating those operators?
the definitions of s and k in it are
S: [3, function(f, g, x) { return App(App(f, x), App(g, x)) }],
K: [2, function(k, _) { return Ind(k) }],
the λ-calculus parser, the compiler from λ-calculus to sk-combinators, the sk-combinator parser, and the sk-combinator evaluator together are 391 lines of js
if you just want to define the s and k combinators in js they look like this
s = f => g => x => f(x)(g(x))
k = a => b => a
more recently i implemented a term-rewriting language in i386 assembly, it's about 800 bytes and 400 instructions: http://canonical.org/~kragen/sw/dev3/qfitzah.s but i haven't quite figured out how to handle arithmetic, i/o, and variadic lists
i think you could probably implement sk combinatory logic in about half a page of c if you were okay with leaking memory, you don't really need the flexibility of variadic lists and arbitrary identifiers in the sk-combinator language. every term is either a function application (of one function to one argument), s, or k
Okay, so what do I type those two lines into to implement that? How many lines of code does that involve?
> more recently i implemented a term-rewriting language in i386 assembly, it's about 800 bytes and 400 instructions: http://canonical.org/~kragen/sw/dev3/qfitzah.s but i haven't quite figured out how to handle arithmetic, i/o, and variadic lists
Have you considered having a parameter stack that arithmetic operators pull their arguments from and push their results onto? Oh wait... ;-)
i just answered that in the comment you are replying to
> Have you considered having a parameter stack
this is a remarkably bad answer to my explanation of how much code i needed to write a self-compiling forth that generates machine code
what is wrong with you
i am sad now
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!
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".
(λ11)(λλλ1(λλλλ3(λ5(3(λ2(3(λλ3(λ1 2 3)))(4(λ4(λ3 1(2 1))))))(1(2(λ1 2))(λ4(λ4(λ2(1 4)))5))))(3 3)2)(λ1((λ1 1)(λ1 1)))
It's literally just notation:
- It doesn't matter how you name variables. (if you want to sound cool: "lambda terms are invariant under alpha-conversion")
- Each new variable introduces a scope.
- Therefore, how scopes are nested defines the entire expression.
- Instead of the usual way, we represent scopes with numbers, with the index representing "how nested the scope is". Imagine it's python, and you're pressing tab that many times.
Look at how ugly decorators are in python when in lisp you get them for free and they don't even need a name.
Python is optimized towards simple pseudo-code like imperative OOP. That's easier for most programmers.
You might not have noticed the userid of the person you're replying to ;)
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
[1] http://www.verostko.com/tur-doc.html#B0,%20Universal%20Turin...
For Turing machines I recommend the book "The annotated Turing".
What does it mean to be Maxwells Equations? Does it mean absolutely most fundamental? Most practical? What?
Maybe there's something more fundamental then turing. Thanks for the book recommendation
In a word: elegant.
Maxwell’s equations are arguably the most successful existing physical theory. They are incredibly accurate over a huge range of scales. They are used in essentially unaltered form all over modern day engineering and have astonishing predictive power.
On top of this, they are a useful tool without modification! They are the working tool for all electrical engineers. They’re not some lower-level substrate that exists in the background. They are used directly to model and generate other, simpler approximate theories (such as geometric and physical optics) which are powerful and elegant in their own right.
I don’t think Lisp, lambda calculus, Turing machines, or similar can make this kind of claim.
1. take a situation observed or designed in the contingent universe,
2. translate it into the abstract entities maxwell's equations talk about,
3. deduce consequences in the world of abstract entities,
4. translate those consequences back into the contingent universe, and then
5. find that the consequences in the contingent universe are within narrow uncertainty bounds we translated from the abstract world of ideas
the meaning of turing universality is precisely that any turing-complete programmable system can be used to model any other logical or mathematical system, including other turing-complete systems, in exactly the same way that maxwell's equations model electromagnetism
for example, you can model risc-v execution in lisp and predict what a risc-v processor will do, you can model lisp execution in the λ-calculus and predict what a lisp interpreter will do, you can model the λ-calculus in a turing machine and predict what λ-reduction will do, and you can model a turing machine in a risc-v processor and predict what the turing machine will do
there is a significant sense in which this sort of modeling is much more perfect than the kind done with maxwell's equations
when we apply maxwell's equations, we are subject to measurement error in steps 1 and 5; our measurements are never complete and correct, and heisenberg's uncertainty principle strongly suggests that they never can be. and in step 3, because maxwell's equations are continuous-time continuous-space differential equations, we often also introduce numerical error in our calculations as well, because we usually have to integrate them numerically rather than algebraically
on the other hand, in the case of computational universality all the entities being discussed are discrete, algebraic, mathematically abstract entities, so our simulations are absolutely perfect unless we run out of memory or suffer a rare hardware error
obviously these universal machines are not limited to modeling other universal machines; we can also use lisp or turing machines or risc-v processors to model things like gravitation, taxation, or maxwell's equations. and they are obviously also the main working tool for all electrical engineers today, having displaced slide rules and load lines generations ago
ultimately, though, we are also using maxwell's equations (and other equations describing electromagnetism, like the ebers-moll transistor model) to design our electronic computers which we use to simulate lisp
Maxwell's equations are "the Maxwell's equations" of physics because they are "the most successful" physical theory: i.e., incredible accuracy, wide applicability, and concision. This is relative to other physical theories. (I guess you could debate whether this is actually the case---obviously this is all subjective, and not everyone agrees. Maybe someone thinks Einstein's field equations should really be "the Maxwell's equations" of physics.)
To say that the lambda calculus or anything else are "the Maxwell's equations" of computer science is to say that they have the same set of properties relative to other let's theoretical constructs in computer science. But is this actually the case? It seems like Turing machines, lambda calculus, etc. are all similar in terms of relative modeling utility and concision. I disagree that they are widely applicable---in practice, just about any commonly used programming language is far more widely applicable than anything of these. And as you pointed out, by Turing universality, they're all logically equivalent---so the question of difference in modeling "power" is not relevant here.
I guess I just don't think it makes much sense to talk about anything in CS being "the Maxwell's equations" of CS. In physics, a wide variety of disparate physical phenomena are being modeled, with individual models having a quite varied range of power and applicability. In CS, things are much different.
Incidentally, even if you simulate Maxwell's equations on a computer using Lisp, a Turing machine, or whatever else, you will not go far if you insist on algebraically exact computations. :-) As you say yourself, you must integrate them numerically, which means numerical error introduced through your discretization. But I honestly can't say I understand your point including this information above.
similarly there are lots of equivalent formulations of universal computation. lisp and the λ-calculus are analogous to the geometric-algebra formulation above and the more commonly used form in terms of vector field derivatives: they look very different, and they make different problems easy, but ultimately they all model the same thing, just like the various formulations of maxwell's equations
maxwell's equations are the maxwell's equations of classical electrodynamics, not of physics. without a lot of extra assumptions they won't get you very far in understanding why solid things are solid (which depends on the pauli exclusion principle) or why some nuclei break down or how transistors work or how stars can burn or why mercury's orbit precesses or why hot things go from red to orange to yellow when you heat them further
my point about modeling maxwell's equations in lisp (etc.) is that lisp (etc.) can model maxwell's equations (at least, as well as any other effective means of calculation we know of can model them — discretization and rounding error also happen when you numerically integrate with pencil and paper), so if we're looking for incredible accuracy, wide applicability, and concision, lisp (etc.) would seem to trump maxwell's equations — but good luck trying to build a computer without electromagnetism, maybe you can in some sense do it on a neutron star but not with atoms
So, yes, since I've used the lc in these ways I believe the same claim can be made regarding the lambda calculus.
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.
It's not. (x -> x) is always inhabited, so if you have a fixed point combinator (x -> x) -> x then every theorem is true.
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))
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...
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.
For example:
Turing Machines and the Halting Problem
Queueing Theory
Shannon Entropy
The CAP Theorem
What is the shortest distances between two points? A straight line. I calculate the solution to that problem. I don't design it. What's the best way to travel between two points? Do I take a car or plane? Which is cheaper, faster, or more comfortable? I can't calculate a solution because the problem is to complex. Instead I design the solution to the problem. That is the fundamental difference between design and calculation.
Whenever you use the word "design" you are operating in a zone where humans have no foundational optimization theory. You are guessing, using your instincts, your common sense and your gut to find solutions for the problem. It's unlikely you'll hit the most optimal solution, but you can very likely arrive at a "good" solution.
If you squint, Category theory looks to fill this gap for designing programs. Depending on how you look at it, category theory looks like a fundamental theory on how to organize code. It can be thought of as a fundamental theory on abstraction or a fundamental theory on interfaces.
Maybe another way to put it is that the concept of interfaces are the maxwells equations of software..
Even turing machines/lambda caculus seem oddly specific let alone lisp. If we want something fundamental and general I think Category theory is it.
My guess is, if the advancement of computer science was allowed to play out for centuries and we got rid of all the historical baggage, some form of category theory would lie at the heart of it all.
https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
and his associated youtube videos (which are EVEN better):
https://youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa...
As a non-math expert and programmer I highly highly recommend Bartosz stuff I linked it in another branch under my original comment.
It's mostly the beginning chapters don't even get into the meat of CT quick enough. Instead it spends a lot of time justifying things. I feel It's written for people who hated math even more then I did.
https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI...
He also has a series of blog posts on it, but I found the lectures especially helpful.
You are taking Type A and converting it to Type B. That is the entire point of computation. All else is abstractions on top of that and algorithms below.
Category theory is what lives on top. Haskell is a programming language and style that borrows very very heavily from category theory. Getting a certain level of mastery in haskell well help you see how programming is related to CT.
Category theory isn't just about how haskell works. You use it to design your programs. Haskell is basically a category theory framework.
I would say you didn't get very far then if you didn't come out of learning haskell with the realization of how you design programs with CT.
It's the level of abstraction and focus. Category theory can describe "mapping over promises" it doesn't give a lot of insight into how to design an internet communication protocol with low latency (for example).
> I would say you didn't get very far then
Sounds like you put a lot of value in your experience with this topic and I am unlikely to convince you.
I would say it's more of a better theory for optimal organization and reuse of code. It's a theory of interfaces. If programming is all about abstraction then CT is the theory of design and abstraction.
I agree that detail and speed and execution are important in computer science but these things maybe aren't general enough as the efficiency of speed also relies on which turing complete language (out of an unlimited set of languages) that is used to drive the computation.
We also do have a general theory for optimizing speed. Computational Complexity theory. Which is based on Knuth's little assembly language. This theory can literally help you converge onto the best possible solution. Not by calculation but it can quantify the speed of an algorithm for definitive comparisons.
But then would complexity theory be the Maxwell's equations of programming? I think there's a good argument for that route but I don't think that's what the OP is thinking about in his article.
The op is thinking about design because Lisp is definitely a design philosophy. Lisp won't help you design an internet communication protocol for low latency either.
Maybe you did study category theory deeply but your thinking about it from an angle of computational cost. This is certainly valid. Apologies for that comment, Haskell and CT like any other design pattern out there is usually not targeted specifically at optimizing speed, but more for optimizing code reuse and increasing modularity. It's for dealing with technical debt and how to handle the complexity of programming through abstraction.
If you're thinking about it from that angle then I think the universe already has your answer. Computational Complexity theory is the Maxwell's equations of software. It's not a very complete theory but it's much more concrete then all the other "design" stuff in computer science.
Haskell probably draws more from category theory than any other mainstream language, but in absolute terms that's still not very much. It's okayish for modelling cartesian closed categories, but if you want any more structure than that things get quite painful. Even something as simple as a category with finitely many objects requires stupid amounts of type-level boilerplate.
However if foundational theory was what justified the title, I believe CT is more foundational then lambda calculus.