[HN Gopher] Lisp as the Maxwell's Equations of Software (2012)
___________________________________________________________________
Lisp as the Maxwell's Equations of Software (2012)
Author : graderjs
Score : 108 points
Date : 2022-11-08 06:21 UTC (1 days ago)
(HTM) web link (michaelnielsen.org)
(TXT) w3m dump (michaelnielsen.org)
| amelius wrote:
| 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.
| sbf501 wrote:
| 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.
| nerpderp82 wrote:
| Guy Steele talk on Metanotation [1]
|
| https://www.youtube.com/watch?v=dCuZkaaou0Q
| Beldin wrote:
| 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.
|
| [1]
| https://en.m.wikipedia.org/wiki/History_of_Maxwell%27s_equat...
|
| [2] https://xkcd.com/297/
| tim_hutton wrote:
| If this is true then Haskell's type system is Noether's Theorem.
| sitkack wrote:
| If Lisp is the Maxwell's Equations, what is the Heaviside
| language?
|
| https://en.wikipedia.org/wiki/Oliver_Heaviside
| protonfish wrote:
| 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.
| deltasevennine wrote:
| A lot of people don't agree. But I feel category theory is the
| Maxwells Equation for software.
|
| 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.
| martyalain wrote:
| Every time I try to understand what category theory is, I hit
| an impassable wall, I don't understand it. Alexander
| Grothendieck is much too intelligent for me. But I don't
| despair of getting there one day...
| deltasevennine wrote:
| I'm not an math expert. I hated math. I learned it off of
| very informal material:
|
| 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.
| ..
| martyalain wrote:
| Thank you so much for these links, a lot to learn ...
| adamddev1 wrote:
| I've found Bartosz Milewski's lectures on category theory for
| programmers to be very understandable and enlightening. (And
| I'm weak on math) He explains it really well in plain terms.
|
| 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.
| gaze wrote:
| It's the idea that most structures in math can be put upon a
| foundation of a structure consisting of objects and the
| relationships between those objects.
| justinhj wrote:
| Eugenia Cheng has a couple of very accessible books on
| Category Theory
| austern wrote:
| I was going to make the same recommendation. In particular
| I'd recommend her new book, _The Joy of Abstraction_. It's
| a real textbook that goes up through the Yoneda Lemma, but
| it isn't too scary and it doesn't assume that the reader
| already knows any theoretical math.
| deltasevennine wrote:
| I read the first couple chapters. It's a bit too watered
| down in the beginning IMO. I couldn't get past the first
| part especially when she tries to relate category theory
| to feminism. Might come back to it later.
|
| As a non-math expert and programmer I highly highly
| recommend Bartosz stuff I linked it in another branch
| under my original comment.
| justinhj wrote:
| Bartosz's material is great but it has a practical
| programming focus, so Cheng's books which focus more on
| teach Category Theory as mathematics, make a good
| complement.
| justinhj wrote:
| Yes, that book in particular. I have Emily Riehl's
| Category Theory in Context which was not immediately
| accessible to me at all. Joy of Abstraction aims to be an
| on-ramp to that.
| sicp-enjoyer wrote:
| I do not agree with this (however, I only have one grad
| category theory course). I think category theory is a fine tool
| for formalizing computation and thinking about type systems,
| but wouldn't approach it as a program design tool.
| deltasevennine wrote:
| All of computation is related to types.
|
| 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.
| sicp-enjoyer wrote:
| I have studied haskell from this perspective. Like I said,
| you learn how to model computation and how the haskell
| language works, you don't learn how to design programs. I
| actually have gotten much more program design ideas from
| traditional branches of math (analysis, algebra, etc).
| deltasevennine wrote:
| Then your comment doesn't make sense to me. If you
| designed programs in haskell then you designed them using
| concepts from category theory.
|
| 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.
| hither_shores wrote:
| > Haskell is basically a category theory framework.
|
| 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.
| sicp-enjoyer wrote:
| > If you designed programs in haskell then you designed
| them using concepts from category theory.
|
| 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.
| martyalain wrote:
| 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:
|
| - 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.
| alexisread wrote:
| 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:
|
| https://shenlanguage.org/TBoS/tbos_170.html
| mattgreenrocks wrote:
| This is really cool, thanks for linking that.
| martyalain wrote:
| My first goal was to write in a wiki using a light and
| extended HTML. I then discovered LISP and lambda-calculus.
| I built an "inverted" evaluator working directly on
| s-expressions (without AST), ignoring words (which
| therefore did not have to be protected by apostrophes and
| quotation marks), like in basic HTML. I can thus write wiki
| pages that are lambdatalk programs, mixing pure text and
| code effortlessly. It's my all-purpose tool.
| voxl wrote:
| How is beta reduction not "formal"???
| alexisread wrote:
| Sorry I wasn't clear - beta-reduction is formal, I was
| trying to refer to the extension of the formal treatment of
| lambdas to cover proofs, formal logic and typechecking.
| Shen does this for typechecking.
| solomatov wrote:
| 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.
| tromp wrote:
| 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
| (l11)(lll1(llll3(l5(3(l2(3(ll3(l1 2 3)))(4(l4(l3 1(2
| 1))))))(1(2(l1 2))(l4(l4(l2(1 4)))5))))(3 3)2)(l1((l1 1)(l1
| 1)))
|
| [1] https://tromp.github.io/cl/Binary_lambda_calculus.html
| martyalain wrote:
| 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...
| lisper wrote:
| Note that the person you were responding to is John Tromp.
| :-)
| SkyMarshal wrote:
| _> As for example John Tromp knows how to do._
|
| You might not have noticed the userid of the person you're
| replying to ;)
| martyalain wrote:
| yes, I hadn't noticed that. I wish I could understand him
| better.
| qsort wrote:
| A picture is worth a thousand words: https://en.wikipedia.o
| rg/wiki/De_Bruijn_index#/media/File:De...
|
| 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.
| pierrebai wrote:
| Syntax and layout ware worth yet a few more orders of
| magnitude of words. But that argument has slipped past
| LISPers forever. I'll just let them keep scratching their
| heads why Python got so popular when LISP was around for
| so long and is /clearly/ superior.
| [deleted]
| lispm wrote:
| I don't think LISPers are scratching their head about
| this. Lisp syntax is optimized towards meta-programming.
| Generating and processing code is built-in and supported
| with central mechanisms: READ, EVAL, PRINT,
| s-expressions, macros, ...
|
| Python is optimized towards simple pseudo-code like
| imperative OOP. That's easier for most programmers.
| thrown_22 wrote:
| Python is popular because the majority of programs are
| extremely simple.
|
| Look at how ugly decorators are in python when in lisp
| you get them for free and they don't even need a name.
| deltasevennine wrote:
| lambda calculus is turing complete. But so are turing
| machines. So why not have turing machines be the Maxwells
| equations of software.
|
| 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
| tromp wrote:
| Because Turing machines are so cumbersome compared to
| lambda calculus that a universal Turing machine takes
| thousands of bits [1].
|
| [1] http://www.verostko.com/tur-
| doc.html#B0,%20Universal%20Turin...
| [deleted]
| mejutoco wrote:
| I find Lambda calculus and term rewriting much more elegant
| and easy to understand. I don't think there is a simpler
| Turing-complete language (maybe Game of Life?).
|
| For Turing machines I recommend the book "The annotated
| Turing".
| deltasevennine wrote:
| Well if game of life is simpler, why not game of life?
|
| 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
| d0mine wrote:
| > What does it mean to be Maxwells Equations?
|
| In a word: elegant.
| sfpotter wrote:
| It means much more than just being 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.
| kragen wrote:
| what it means to say maxwell's equations have 'predictive
| power' is that we can
|
| 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 very close to the ones 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 l-calculus and predict what a lisp
| interpreter can do, you can model the l-calculus in a
| turing machine and predict what l-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
|
| 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
| deltasevennine wrote:
| elegance is a human attribute. Opinionated and open to
| interpretation. So Maxwells equations are an opinionated
| choice? I don't think so.
| thrown_22 wrote:
| >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.
| martyalain wrote:
| @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
|
| and obviously
|
| {{lambda {x y z w} {+ x y z w}} 1 2 3 4} -> 10
| jerf wrote:
| 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.
| kragen wrote:
| 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 schonfinkel'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
| l-calculus's one. using a hybrid of bicicleta's syntax and
| abadi and cardelli's {f = s(v)b, g = s(v)c,
| ...}{f = s(v)d} - {f = s(v)d, g = s(v)c, ...} {f =
| s(v)b, g = s(v)c, ...}.f - b[{f = s(v)b, g = s(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 b-reduction semantics with a-renaming that we're
| familiar with from the l-calculus (b[x/y] means b but with x
| replacing y)
|
| despite the simplicity of the semantics the s-calculus is
| enormously more usable for actually writing down functions
| than the l-calculus. here's factorial(10) in the notation
| above (untested) {fac = s(env){
| n = s(_)3, return = s(o) (o.n <
| 2).if_true{ then = s(_)1
| else = s(_)o.n * env.fac{n = s(_)o.n - 1}.return
| }.return } }.fac{n = s(10)}.return
|
| bicicleta has a lot of syntactic sugar which reduces this to
| (tested) {env: fac = {fac: arg1
| = 3 '()' = (fac.arg1 < 2).if_true(
| then = 1 else = fac.arg1 * env.fac(fac.arg1 -
| 1) ) }}.fac(10)
|
| 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
| gradschool wrote:
| > maybe wolfram knows of a simpler alternative
|
| Wolfram on combinators:
|
| https://writings.stephenwolfram.com/2020/12/combinators-a-
| ce...
|
| not any simpler, but maybe these are:
|
| https://en.wikipedia.org/wiki/Iota_and_Jot
| kragen wrote:
| oh yeah, how could I forget iota and jot, that was stupid
| of me
| Gordonjcp wrote:
| > but schonfinkel's ski-combinators are maybe the simplest
| practical basis
|
| Okay, but how much code goes into creating those operators?
| kragen wrote:
| it depends on what you're implementing them in, but in a
| term-rewriting language all you need is the two lines
| above. in js you need to implement some kind of term-
| rewriting. in 02006 i wrote a compiler from l-calculus
| (using \ for l, so you can write for example \x.\y.x for
| lx.ly.x, which is equivalent to the k combinator) to an
| augmented sk-combinator language in js that's at
| http://canonical.org/~kragen/tmp/sk.html
|
| 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) }],
|
| which are used as templates for matching by the 33-line-
| long sk_reduce function, which i'll spare you here
|
| the l-calculus parser, the compiler from l-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
|
| but that is depending on the js interpreter to do the
| actual evaluation
|
| 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
| justinhj wrote:
| 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
| voxl wrote:
| 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.
| justinhj wrote:
| Interesting, thanks
| hither_shores wrote:
| > You could rephrase Lisp as a Unityped system, but I
| seriously doubt it would be consistent.
|
| It's not. (x -> x) is always inhabited, so if you have a
| fixed point combinator (x -> x) -> x then every theorem is
| true.
| mannykannot wrote:
| 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!_
|
| https://crypto.stanford.edu/~blynn/lambda/lisp.html
| kazinator wrote:
| 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".
| bmitc wrote:
| 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.
| User23 wrote:
| 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.
|
| [1] https://en.wikipedia.org//wiki/De_Bruijn_index
| martyalain wrote:
| 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...
| [deleted]
| phoe-krk wrote:
| Also related, _An Intuition for Lisp Syntax (2020)_ -
| https://news.ycombinator.com/item?id=32630675#32635785
| dang wrote:
| Related:
|
| _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)
| [deleted]
___________________________________________________________________
(page generated 2022-11-09 23:01 UTC)