[HN Gopher] Show HN: LambdaLisp - A Lisp interpreter that runs o...
___________________________________________________________________
Show HN: LambdaLisp - A Lisp interpreter that runs on lambda
calculus
Author : woodrush
Score : 171 points
Date : 2022-09-17 18:17 UTC (1 days ago)
(HTM) web link (woodrush.github.io)
(TXT) w3m dump (woodrush.github.io)
| lisper wrote:
| This is one of the most mind-blowing things I have ever seen.
| Words fail me, so I'll appropriate some of the author's:
|
| "Lisp has been described by Alan Kay as the Maxwell's equations
| of software. In the same sense, I believe that lambda calculus is
| the particle physics of computation. LambdaLisp may therefore be
| a gigantic electromagnetic Lagrangian that connects the realm of
| human-friendly programming to the origins of the notion of
| computation itself."
|
| BTW, if you have no idea what is going on here, eight years ago I
| took a whack at writing a gentle introduction to this same sort
| of thing, but done in a more half-assed way, and with a much less
| ambitious scope:
|
| https://flownet.com/ron/lambda-calculus.html
| eointierney wrote:
| Delightful, thank you
| bobbylarrybobby wrote:
| Fantastic read, thanks.
| haskellandchill wrote:
| Then what is System F?
| actually_a_dog wrote:
| This is undoubtedly cool, but I'd be really impressed if it
| wasn't stupidly slow. (I'm not saying it _is_ stupidly slow,
| because I haven 't had a chance to run it, just that I'd be
| impressed if it wasn't.)
| woodrush wrote:
| Thanks for your feedback, I forgot to mention the execution
| speed in the post. The number guessing game example (44 lines
| long) in the Usage section actually runs with an instantaneous
| response time on the terminal. I added some remarks on the
| execution speed.
| lisper wrote:
| I haven't tried it either, but I would not bet my life savings
| on it being slow. I tried something similar to this a few years
| ago (see my top-level comment for a pointer) and was amazed at
| how fast it turned out to be.
| quickthrower2 wrote:
| It has to be slow. Multiplication will be O(N^2)!
| sudosysgen wrote:
| Multiplication is generally done in O(n^2) of the number of
| bits so I'm not sure what you mean to say. Do you mean O(n^2)
| of the size of the operands?
| quickthrower2 wrote:
| In Lambda calculus, numbers are encoded using 0 and
| successor. So 3 = S(S(S(0)))
|
| Adding these would be O(N+M) where N and M are the numbers,
| not the number of bits.
|
| Multiplying is O(N*M) where again it is the numbers.
|
| 1000*1000 would require a million operations at least. It
| takes a million operations just to store/read the number
| million!
|
| See: https://en.wikipedia.org/wiki/Church_encoding
|
| Unless this HN submitted implementation doesn't use church
| encoding. In which case I am wrong.
| wrbs wrote:
| There's nothing about the lambda calculus which forces
| you to use the church encoding of natural numbers.
|
| You could also come up with an encoding based on booleans
| as bits: {true} = \t f. t {false} =
| \t f. f
|
| then bytes: {0b00001111} = \f. f [false]
| [false] [false] [false] [true] [true] [true] [true]
|
| which you could merge up into larger integers just like
| real computers.
|
| or for one less based on the 8-bits and to keep the
| infinite range you could just represent integers as lists
| of binary numbers: {[]} = \c n. n
| {x::y} = \c n. c x y {0} = [] {1} =
| [true] {2} = [false, true] (i.e. reversed 0b10)
| {3} = [true, true] {4} = [false, false, true]
|
| which you could imagine using to implement a way more
| efficient shift-and-add multiply, O(log M * log N)
| tromp wrote:
| > {[]} = \c n. n
|
| > {x::y} = \c n. c x y
|
| Note that Binary Lambda Calculus uses the simpler {x::y}
| = \c. c x y, which allows you to operate on a list l with
| l (\head \tail \dummy. non_null_case) null_case
| atennapel wrote:
| The page mentions that the implementation has 32 bit
| signed integers, plus it uses Scott encodings and not
| Church.
| tromp wrote:
| As author of the Binary Lambda Calculus (BLC), I find this quite
| fascinating. It implements LISP in 163,654 bits of BLC. For
| comparison, minimal esoteric languages like BLC itself can be
| implemented in 232 bits of BLC, and Brainfuck in 893 bits.
|
| I'm still reading the document, but one thing that caught my eye
| is the List encoding with cons and nil, which is claimed to be a
| Mogensen-Scott one.
|
| Rather, cons \x\y\c. c x y is the Scott encoding of infinite
| lists that have no nil terminator (also known as streams) and
| thus only one constructor, while nil is the Scott encoding in
| nil-terminated lists with 2 constructors.
|
| Thus the given encoding is some non-standard hybrid of streams
| and lists that helps BLC achieve its conciseness. In Wikipedia
| [1] it's described as
|
| > Alternatively, with NIL := FALSE, the construct l
| (lh.lt.lz.deal_with_head_h_and_tail_t) (deal_with_nil) obviates
| the need for an explicit NULL test
|
| [1] https://en.wikipedia.org/wiki/Lambda_calculus#Pairs
| lisper wrote:
| > It implements LISP in 163,654 bits of BLC. For comparison,
| minimal esoteric languages like BLC itself can be implemented
| in 232 bits of BLC, and Brainfuck in 893 bits.
|
| That's hardly a fair comparison. LambdaLisp includes a ton of
| features that BLC and BF do not.
| keithalewis wrote:
| Slap yourself and reread the rest of the post.
| lisper wrote:
| Sorry, I'm going to need you to give me a little more of a
| clue what you are talking about.
| keithalewis wrote:
| You missed the substantive portion of the post.
| tromp wrote:
| > Writing in continuation-passing style also helps the lambda
| calculus interpreter to prevent re-evaluating the same term
| multiple times. This is very, very important and critical when
| writing programs for the 521-byte binary lambda calculus
| interpreters Blc, tromp and uni, since it seems that they lack
| a memoization feature, although they readily have a garbage
| collection feature.
|
| Note that Melvin Zhang added a memoization feature (call-by-
| need evaluation with result sharing) in his refactoring [1] of
| my BLC interepreter.
|
| [1] https://github.com/melvinzhang/binary-lambda-calculus
| tromp wrote:
| > The pattern \lambda a. \lambda b. \lambda w. \lambda x.
| \lambda y. yla.lb.lw.lx.ly.y is noticable in many places in
| lambdalisp.pdf, since isnil is used a lot of times in
| LambdaLisp.
|
| Sadly, this heavy use of the isnil operator derived in section
| [1] adds a lot of unnecessary verbosity, since instead of
| writing isnil list result1
| (let { head = car list, tail = cdr list} in result2)
|
| one can simply write list (\head
| \tail \_ . result2) result1
|
| [1] https://woodrush.github.io/blog/lambdalisp.html#deriving-
| isn...
| ducktective wrote:
| Page 32 of the pdf...omg the legends were true!
|
| https://woodrush.github.io/lambdalisp.pdf
| somewhereoutth wrote:
| Lambda calculus is mathematically foundational in a way that Lisp
| of course isn't.
|
| The question is what does Lisp give us as an interpretation of
| those foundations? Or does it admit issues that might be
| unhelpful? (Are macros a good thing?)
| lisper wrote:
| Let's not sell Lisp short here. LC might be _mathematically_
| foundational, but I think it 's fair to say that Lisp is
| _computationally_ foundational. Mathematics and computation are
| related, of course, but they are not identical. Computation is
| the study of _mechanical processes_ for doing math. As such,
| Lisp 's identification of CONS/CAR/CDR/COND as a sufficient set
| of primitives for a universal Turing machine is important
| because it's obvious (or at least it was obvious by 1958) how
| those primitives can be implemented as a mechanical process.
| Implementing LAMBDA in all its generality is far less obvious,
| which is why it took 20 years of further research to go from
| Lisp 1 to Scheme.
| kazinator wrote:
| LC is only computationally foundational; it describes
| recursive functions. It's just another universal turing
| machine.
|
| LC has a great disadvantage: it's difficult to write a LC
| interpreter in LC. This project shows exactly what that
| means. To write an LC interpreter, you need a data structure
| for representing expressions. You need a symbolic data type.
|
| LC does not know what a LC expression is. Papers about LC
| know what that is, but they are not executable.
|
| In Lisp we can say, okay, lambda calculus can be represented
| sort of like this: (lambda (x) x)
|
| and so on. That's a nested list. It contains symbols. We can
| use an assoc list to associate symbols with the terms that
| are their values. And so on ...
|
| Lisp has the programmatic vocabulary to talk about lambda
| calculus formally, in a way that is executable.
|
| I don't suspect there is a significantly easier way for LC to
| interpret LC than to use the 42 page expression to create a
| Lisp, and then write the interpreter in that lisp.
| lisper wrote:
| > it's difficult to write a LC interpreter in LC.
|
| Why? It's pretty easy to write Lisp in LC (a simple Lisp,
| not the feature-full version described in TFA) and it's
| pretty easy to write an LC interpreter in Lisp. I'll bet
| that an LC interpreter in LC could be done in only a few
| hundred lambda terms.
| tromp wrote:
| > an LC interpreter in LC could be done in only a few
| hundred lambda terms.
|
| Make that a few dozen...
| haskellandchill wrote:
| lisper and kazinator need to put down the keyboard and
| spare some time for reflection. thanks tromp for your
| tireless efforts at education. big fan of your work!
| lisper wrote:
| Yeah, I should have realized that. In fact, I had seen
| your BLC interpreter some time ago but for some reason it
| didn't come to mind as I was writing that. I must be
| getting old.
| kazinator wrote:
| Good point; a minimal Lisp needed for processing LC
| doesn't require the 42 page formula. That has features
| like mutable global variables.
| tromp wrote:
| > LC has a great disadvantage: it's difficult to write a LC
| interpreter in LC.
|
| It's not; here it is quoted from [1]: (l
| 1 1) (l l l 1 (l l l l 3 (l 5 (3 (l 2 (3 (l l 3 (l 1 2 3)))
| (4 (l 4 (l 3 1 (2 1)))))) (1 (2 (l 1 2)) (l 4 (l 4 (l 2 (1
| 4))) 5)))) (3 3) 2) (l 1 ((l 1 1) (l 1 1)))
|
| > LC does not know what a LC expression is.
|
| Again, it's trivial to encode LC terms as bitstrings [1],
| which are trivially decoded back into lambda terms. That is
| exactly what the above lambda expression does.
| Alternatively, you can encode LC terms with Mogensen's
| encoding, but that one doesn't give you a textual
| representation like a bitstring.
|
| [1] https://tromp.github.io/cl/Binary_lambda_calculus.html#
| Lambd...
| kazinator wrote:
| > _BLC requires translating bitstrings into lambda terms,
| to which the machine (itself a lambda term) can be
| readily applied._
|
| I.e. a man behind the curtain is required to complete the
| "interpreter".
| bidirectional wrote:
| Can you explain at a high level what you think a valid
| LC-in-LC interpreter looks like then? Because it's very
| hard to understand what your objection is to the examples
| in this thread.
| kazinator wrote:
| A LC interpreter (whether in LC or anything else) has to
| process the actual syntax with the lambdas and symbols
| (or integer literals, in the case of De Bruin).
|
| If it is necessary to translate that representation to
| something else, the interpreter must do that itself.
|
| You can take a LC expression and write some other LC
| expression which encodes it; but if that is done outside
| of LC in some meta-language, then that has to be counted
| as part of the interpreter's implementation, which means
| that it's not in LC any more.
|
| Based on that, I think it's not actually possible without
| extensions to LC.
|
| You need to be able to read the syntax with the lambda
| symbols and names (or integer constants in the case of De
| Bruin), so I/O is needed. Or else, if that is
| unacceptable, you need to be able to embed the
| representation of the code as a quoted literal.
|
| Without I/O or quoting, you have no way to express the
| test cases.
| woodrush wrote:
| The basic tools required for implementing a LC
| interpreter in LC is demonstrated in LambdaLisp. Although
| LambdaLisp implements Lisp, the same tools can be used to
| implement a LC interpreter in LC.
|
| The largest concern in question here may be how I/O is
| done. I/O can be done by viewing a lambda term as a
| function that takes a string as an input and outputs a
| string. Here, a "string" can be expressed as a "list" of
| "characters", where lists can be encoded using the Scott
| encoding, and characters can be encoded as a list of
| bits, and "bits" can be encoded as 0=\x.\y.x, 1=\x.\y.y.
| This I/O strategy is used in LambdaLisp as well, and is
| explained in my post in [1].
|
| How Lisp terms are encoded as lambda terms in LambaLisp
| is explained in [2].
|
| To implement a LC interpreter instead of a Lisp
| interpreter in LC, it then remains to somehow encode and
| quote a lambda calculus term into a lambda calculus term.
| The function described by tromp's reply in this thread,
| called the Universal Machine, does this - it does so by
| using an encoding called the binary lambda calculus (BLC)
| notation for encoding lambda terms into lambda terms. In
| this notation, an arbitrary lambda term in the usual
| plaintext notation such as \x.\y.\z.(x y z) can be
| encoded into a bitstream. The converse is also always
| possible. The Universal Machine uses the BLC notation for
| expressing lambda terms, with the same 0/1 bit encoding
| and list encoding mentioned earlier, and outputs a
| bitstream (encoded as lambda terms) representing the
| evaluation result. The BLC notation is described in my
| post in [3].
|
| [1]
| https://woodrush.github.io/blog/lambdalisp.html#handling-
| io-...
|
| [2]
| https://woodrush.github.io/blog/lambdalisp.html#basic-
| data-s...
|
| [3] https://woodrush.github.io/blog/lambdalisp.html#the-
| binary-l...
| heavenlyblue wrote:
| The objection to them is that they are trivial and lead
| to none of the profound truth that is usually implied by
| their presentation.
| somewhereoutth wrote:
| Perhaps LC is telling us that maybe macros weren't such a
| good idea after all??
| anderskaseorg wrote:
| There is. Using the Mogensen-Scott encoding, a self-
| interpreter can be written in lambda calculus as
|
| (lf.ff)(lf.lt.t(lx.x)(lm.ln.ffm(ffn))(lm.lv.ff(mv))),
|
| which is a direct translation of the equivalent Haskell
| code data Term t = Var t | App (Term t)
| (Term t) | Abs (t -> Term t) newtype Function =
| Function {apply :: Function -> Function}
| interpret :: Term Function -> Function interpret
| (Var x) = x interpret (App m n) = apply (interpret
| m) (interpret n) interpret (Abs m) = Function (\v
| -> interpret (m v))
|
| https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encodi
| n...
| kazinator wrote:
| I don't see what in the interpreter converts the lambda
| calculus into the Morgensen-Scott encoding.
|
| The Wikipedia page describes a "mse" function that is in
| some meta-language which is not lambda calculus. So first
| wee need a Lambda Calculus based interpreter for the
| meta-language, which can run this "mse" function.
|
| It looks like mse[x] is supposed to match a variable
| term, and mse[M N] matches a function application and so
| on. There are no such concepts and representations in
| lambda calculus, not to mention shape matching on them.
|
| The meta language might as well just be a paragraph of
| English: instructions on how to hand-compile the lambda
| calculus into a bunch of thunks which the interpreter can
| just invoke in certain ways to bring about the
| evaluation.
| tromp wrote:
| You're claiming that LC cannot implement a quoting
| operator. Which is quite wrong.
|
| What you misunderstand is that a LC quote would not work
| on arbitrary lambda terms.
|
| A Mogensen quote operator would take a Mogensen encoding,
| and output a Mogensen encoding of that Mogensen encoding.
|
| Or a BLC quote operator would take a bitstring like 0010
| which encodes the identity function l 1, and output the
| blc encoding of the nil-terminated list of 4 booleans
| that represents that bitstring:
|
| 010001011000001100101100000110010110000010010110000011001
| 01100000100000100000000101101110110
| kazinator wrote:
| > _would take a Mogensen encoding_
|
| obtained where?
|
| > _output a Mogensen encoding of that Mogensen encoding_
|
| That's not what a quote operator does; it does precisely
| nothing, yielding the argument formula without evaluating
| it. No encoding-of-encoding. Just the encoding.
|
| > _output the blc encoding of the nil-terminated list of
| 4 booleans that represents that bitstring_
|
| Where/how does that become l 1 again?
| tromp wrote:
| > That's not what a quote operator does; it does
| precisely nothing,
|
| This is what gives Lisp murky semantics; you need
| something (quote) to do nothing, while having nothing (no
| quote) does something (evaluate).
|
| Lisp lacks referential transparency, even without the use
| of variables. An evaluated term can be evaluated again,
| yielding something different.
|
| > Where/how does that become l 1 again?
|
| By decoding it, which is what mostly what the LC self-
| interpreter does, as detailed on pages 6,7 of [1].
|
| [1] https://tromp.github.io/cl/LC.pdf
| kazinator wrote:
| > _An evaluated term can be evaluated again, yielding
| something different._
|
| Yes, and a Mogensen-Scott encoding can be Mogensen-Scott-
| encoded again, requiring two rounds of decoding, and so
| on.
|
| Multiple rounds of encoding and evaluation seem
| inescapable of you have the entanglement of
| homoiconicity.
|
| The quote operator in Lisp is designed exactly right.
|
| In mathematics there are literals like the number 3 or
| the set {}. These objects stand for themselves and are
| not understood as requiring any calculation: they just
| are.
|
| Symbols like x do not stand for themselves. If you want
| to talk about x literally as the symbol object, it is
| inescapable that there is some quoting operator to
| indicate that the usual semantics of _x_ denoting
| something else do not apply. (Oxford 's _A Dictionary of
| Computer Science_ has a definition of _literal_ which
| acknowledges this very issue.)
|
| Literals being constants, it means that when they are
| concretely implemented in a computer, in the best
| possible way, they do nothing other than trivially
| reproduce a canned value that already exists before the
| program starts.
| kazinator wrote:
| A quote operator that doesn't work on arbitrary lambda
| terms is not correct. It doesn't meet the definition of
| quoting.
| anderskaseorg wrote:
| The situation with Lisp is exactly the same. To run a
| Lisp self-interpreter, we don't pass it a Lisp function:
| (interpret (lambda (x) x))
|
| but rather an encoded version of that Lisp function's
| code: (interpret (cons 'lambda (cons
| (cons 'x nil) (cons 'x nil)))
|
| Of course, Lisp gives us a more convenient syntax for the
| latter, in the form of the quote macro:
| (interpret (quote (lambda (x) x)))
| (interpret '(lambda (x) x))
|
| But the quote macro is not a function; it's just syntax.
| If it were a function, you'd expect this to be
| equivalent: (interpret (let
| ((f (lambda (x) x))) (quote f)))
|
| which of course it is not.
|
| Although the quote macro is an important part of what
| makes Lisp Lisp, it's not a fundamental part of what
| makes Lisp a programming language. We could write any
| Lisp program without it (assuming we were still given a
| way to build a primitive 'symbol).
| kazinator wrote:
| > _The situation with Lisp is exactly the same._
|
| No it isn't, because the Lisp code is already understood
| to have an encoding. So we don't have to play any Godel-
| numbering-like games to get the code to be able to talk
| about code. That battery is included.
|
| > _gives us a more convenient syntax for the latter, in
| the form of the quote macro_
|
| The ' in (cons 'lambda ...) is an instance of quote!
|
| You must write (cons (intern "lambda") ...) to remove
| quote. Oops, now you're using a different kind of quote:
| a string literal quote. If you remove that, you will have
| character literals to otherwise build the symbol name.
|
| I agree that quote is not essential: take out quote and
| you can still do useful symbolic processing. Just doing
| interactive testing and writing unit tests will be
| inconvenient, mainly.
|
| The requirement for quote has a different effect. If we
| have quote, we can make the additional step in the
| documentation that all code has the representation
| produced by quote, even when quote is not being used.
| When _lambda_ is seen in code, that is actually the same
| thing that _(quote lambda)_ produces or that _(intern
| "lambda")_ produces.
|
| The above is almost inescapable if user-defined macros
| are supported. When code is read, it is not determined at
| read time what is a macro and what isn't. Therefore it is
| not known what parts of the form may need to be passed to
| a user-defined expander function without having been
| evaluated (and thus in the quote representation). The
| whole thing is in the quoted encoding, so that quote
| doesn't have to do anything other than pass through its
| interior.
| anderskaseorg wrote:
| Yes, I was clear above that I know ' means quote. My
| experiment is to compare Lisp to a restriction of Lisp
| where quote only works on symbols. This restriction
| doesn't make it any harder to write a self-interpreter.
|
| > _If we have quote, we can make the additional step in
| the documentation that all code has the representation
| produced by quote, even when quote is not being used.
| When lambda is seen in code, that is actually the same
| thing that (quote lambda) produces or that (intern
| "lambda") produces._
|
| I'm not sure what you're suggesting here. Certainly the
| number (+ 2 2) must be distinguishable from the list '(+
| 2 2). Even lambda expressions must be distinguishable
| from their quoted encodings, because otherwise lexical
| scoping breaks. If you make (lambda () x) equivalent to
| '(lambda () x), then this breaks: (let
| ((x 1)) (funcall (let ((x 2)) (lambda () x))))
|
| and if you make (lambda () x) equivalent to `(lambda ()
| ',x), then this breaks: (let ((x 1))
| (funcall (lambda () (let ((x 2)) x))))
|
| Macros expand at compile time, not runtime. Macros are
| also cool, but not fundamental, and don't contribute to
| the ease of writing a self-interpreter.
| kazinator wrote:
| If we don't have quote for expressions but only for
| symbols, we can still write the interpreter function, and
| give it a test case by writing an expression which
| calculates the code that we want to interpret. Even
| without quote the language has given us a representation
| of the syntax that we can rely on.
|
| We have it as a given that (list 'lambda (list 'x) 'x)
| produces (lambda (x) x).
|
| We do not have such a thing in lambda calculus. We could
| create an extended lambda calculus which has it.
| anderskaseorg wrote:
| The sense in which the Lisp code (list 'lambda (list 'x)
| x) evaluates to the data representation of (lambda (x) x)
| is exactly the same as the sense in which the lambda
| calculus code la. lb. lc. c (lx. la. lb. lc. a x)
| evaluates to the data representation of lx. x.
|
| What makes Lisp special is that this particular
| correspondence is made visible to the programmer via
| quote and other macros. Again, very cool, but not
| fundamental to this particular discussion.
| pmcjones wrote:
| > which is why it took 20 years of further research to go
| from Lisp 1 to Scheme.
|
| Actually it only took Peter Landin a few years. For example
| see:
|
| P. J. Landin, The Mechanical Evaluation of Expressions, The
| Computer Journal, Volume 6, Issue 4, January 1964, Pages
| 308-320, https://doi.org/10.1093/comjnl/6.4.308
| lisper wrote:
| Thanks for that link! TIL.
| pmcjones wrote:
| Also: MIT's PAL (1968 -- Art Evans, Martin Richards, and
| others) and John Reynolds' GEDANKEN (1969):
|
| https://www.softwarepreservation.org/projects/PAL/
|
| https://www.softwarepreservation.org/projects/GEDANKEN/
| somewhereoutth wrote:
| I'd say that _all_ foundations are mathematical (at least for
| 'concrete' stuff, and more besides). If lisp was
| foundationaly interesting presumably mathematicians would
| have given it more study? (perhaps they did?)
|
| I would disagree that computation is process for doing math -
| it _is_ math in its own right, specifically that for
| operating over a discrete state space (urgh help needed to
| tighten this statement up)
|
| LC is basically a rewrite engine, so I'm not sure it would be
| so hard to implement? Probably some plastic bags, in two
| colours, paper scraps, and a marker pen would do it? (Edit -
| one colour bag would need 2 ordered compartments - or if you
| really have lots of spare time you could build it all with
| just plain bags and some set theory) However as you say
| perhaps Lisp is a better abstraction over the Turing tape
| (yuck).
| lisper wrote:
| > I would disagree that computation is process for doing
| math
|
| Sorry, but you are mistaken. This is not a matter of
| opinion, it is a matter of historical fact. There is a
| reason that the title of McCarthy's original Lisp paper
| ends with "and Their Computation _by Machine_. " The
| opening paragraph of Turing's 1936 paper ends with the
| sentence, "According to my definition, a number is
| computable if its decimal can be written down _by a
| machine_. "
|
| > specifically that for operating over a discrete state
| space.
|
| Sorry, but you are mistaken about that too. Analog
| computers and quantum computers are computers but they do
| not operate over discrete state spaces. They are, however,
| machines.
| somewhereoutth wrote:
| I think I meant computation in the _mathematical_ sense.
| In other words that 'computation' is a mathematical
| object worthy of study in its own right.
|
| Per analog and quantum, indeed, and they are also
| mathematics.
|
| I think that is my point - (very nearly) everything
| proceeds from mathematics, there is no other foundation.
| lisper wrote:
| What can I say? You are mistaken. Computation is as much
| about physics as it is about math. It is the study of
| what can actually be done in this universe with real
| hardware (including human brains). If you doubt this,
| read the opening paragraph of this paper:
|
| https://www.scottaaronson.com/papers/pnp.pdf
|
| The only reason that P=NP? matters _at all_ (let alone
| why it is a foundational question) is because the theory
| of computation concerns itself with what can be done with
| actual physical hardware in actual physical time.
|
| > Per analog and quantum, indeed, and they are also
| mathematics.
|
| No, they aren't. Analog computers are _machines_. Quantum
| computers are _machines_ (or at least they will be if we
| ever actually manage to build one). We can describe the
| behavior of these machines mathematically, but that is
| not why they matter. They matter because _we can actually
| build them_.
| somewhereoutth wrote:
| I agree that much of the _motivation_ comes from real
| world imperatives, but, for example, P=NP is of deep
| mathematical interest in its own right, and if /when
| mathematicians solve it, they will move on and let us
| sort out the details.
|
| We can actually build stuff (beyond some somewhat blessed
| prototypes) often only when we've understood the
| mathematics behind it - edit: or is that the other way
| around??
|
| I'm not sure that _any_ rigorous discipline can consider
| itself outside or unbound by mathematics.
| lisper wrote:
| > P=NP is of deep mathematical interest in its own right
|
| Sure. Computation and math are closely related, but they
| are not identical. Physics is described almost
| exclusively by differential equations, but differential
| equations and physics are nonetheless two distinct fields
| of study.
| lioeters wrote:
| Opening paragraphs of the linked paper:
|
| > In 1900, David Hilbert challenged mathematicians to
| design a "purely mechanical procedure" to determine the
| truth or falsehood of any mathematical statement. That
| goal turned out to be impossible. But the question --
| does such a procedure exist, and why or why not? --
| helped launch two related revolutions that shaped the
| twentieth century: one in science and philosophy, as the
| results of G odel, Church, Turing, and Post made the
| limits of reasoning itself a subject of mathematical
| analysis; and the other in technology, as the electronic
| computer achieved, not all of Hilbert's dream, but enough
| of it to change the daily experience of most people on
| earth.
|
| > Although there's no "purely mechanical procedure" to
| determine if a mathematical statement S is true or false,
| there is a mechanical procedure to determine if S has a
| proof of some bounded length n: simply enumerate over all
| proofs of length at most n, and check if any of them
| prove S. This method, however, takes exponential time.
| The P ?= NP problem asks whether there's a _fast_
| algorithm to find such a proof (or to report that no
| proof of length at most n exists), for a suitable meaning
| of the word "fast." One can think of P ?= NP as a modern
| refinement of Hilbert's 1900 question. The problem was
| explicitly posed in the early 1970s in the works of Cook
| and Levin, though versions were stated earlier--including
| by G odel in 1956, and as we see above, by John Nash in
| 1955.
|
| > Think of a large jigsaw puzzle with (say) 101000
| possible ways of arranging the pieces, or an encrypted
| message with a similarly huge number of possible
| decrypts, or an airline with astronomically many ways of
| scheduling its flights, or a neural network with millions
| of weights that can be set independently. All of these
| examples share two key features:
|
| > (1) a finite but exponentially-large space of possible
| solutions; and
|
| > (2) a fast, mechanical way to check whether any claimed
| solution is "valid."
| kazinator wrote:
| The complexity topic from which we have P = NP is not
| actually about time, but number of steps.
|
| Of course that matters physically because if you only
| have a machine that performs one step at a time (or a
| somewhat better one that performs N steps at a time, for
| some fixed N), then the number of steps does translate to
| amount of time.
|
| If you have access to unlimited parallelism, then, for
| instance, some recursive algorithms that completely
| process a tree structure can drop from linear time to
| logarithmic.
| lisper wrote:
| > Of course that matters physically because if you only
| have a machine that performs one step at a time (or a
| somewhat better one that performs N steps at a time, for
| some fixed N), then the number of steps does translate to
| amount of time.
|
| It's much more fundamental than that. If you have _any_
| finite machine then the amount of time it takes to
| perform N steps will be proportional to N for
| sufficiently large N.
|
| > If you have access to unlimited parallelism...
|
| And if you had some magic pixie dust...
|
| Sorry to be the one to break this to you but you live in
| a finite universe.
| medo-bear wrote:
| > Sorry to be the one to break this to you but you live
| in a finite universe
|
| i don't think cosmologists make that claim in such a
| strong way. its mainly worded something along the lines
| of, "given our current understanding, its most likely to
| be finite"
| lisper wrote:
| "You live in a finite universe" is not the same as "the
| universe is finite". You live in a light cone, and unless
| you are immortal that light cone comprises a finite
| amount of space-time.
| kazinator wrote:
| For sufficiently large N, all computation that isn't O(1)
| takes infinite time.
|
| Complexity analysis goes out to infinity, but the way we
| use it as a _tool_ is to inform us about what happens
| with our practical, finite inputs.
|
| We know that something requires a non-polynomial number
| of steps, it quickly becomes untractable for small
| inputs. (So if we code that in a practical program, we
| need some justification that either the inputs won't
| occur, or we actively guard against them.)
|
| Whether the entire universe is actually finite is not
| known, and not really relevant because that subset of it
| which is available to us as resources is vastly tiny.
|
| The universe is vast, and vastly parallel: things are
| happening all over it at once, with more objects than
| have ever been crammed into any of our computing
| machines.
| openfuture wrote:
| Lisp is called the dyck language or the catalan numbers
| depending on what kind of mathematician you are talking to.
| tromp wrote:
| Lambda Calculus is computationally foundational. Lisp carries
| a lot of non-foundational baggage, some of which (like number
| primitives) makes it far more efficient for running on actual
| hardware.
|
| > As such, Lisp's identification of CONS/CAR/CDR/COND as a
| sufficient set of primitives for a universal Turing machine
|
| You don't need any of those for universality. They are
| trivially expressible in Lambda Calculus. LAMBDA is really
| the only necessary primitive.
| lisper wrote:
| Yes, that is why I said _sufficient_ and not _necessary_.
| The reason CONS /CAR/CDR/COND matter is not because they
| are necessary. That they are not necessary was known long
| before 1958. The reason they matter is that they are a
| better impedance match to human cognition than LC. People
| can actually write useful programs in Lisp. Very few people
| can write useful code in LC. Lisp matters because it is a
| local maximum on the ratio of real-world utility to the
| size of the formalism.
|
| [UPDATE] One idea I've been kicking around for a long time
| but have not yet acted on is to explore using abstract
| associative maps as a primitive and see how far that gets
| you. I suspect this would be a significant win in terms of
| comprehensibility of code. The foundational axiom would be
| something like:
|
| ((amap k1 v2 k2 v2 ... kn vn ...) kn) == vn
|
| So IF, for example, can be written as (amap true [then]
| false [else]), CONS is (amap car [left] cdr [right]), etc.
|
| Or something like that.
|
| Oh, yeah, Lisp also introduced symbols as first-class
| entities. That's a big win.
| armchairhacker wrote:
| Lisp is more expressive: I can write any program in LC but I'd
| much rather use Lisp.
|
| Similarly someone could write C or JavaScript or Swift or
| Haskell in LC. Although I'd argue Lisp is a bit better as it's
| one of the first languages, one of the first to involve
| functional concepts like code-as-data, and itself is based on
| really simple concepts like LC.
| tromp wrote:
| Haskell is more expressive. I can write any program in LISP
| but I'd much rather use Haskell. Btw, Haskell is much closer
| in spirit to LC than LISP is.
| somewhereoutth wrote:
| Yes expressiveness is a crucial quality.
|
| I'd suggest that code-as-data is in fact _not_ a functional
| concept, and indeed may not necessarily be as helpful as we
| might like to think.
|
| Lisp strayed from the path somewhat when it embarked on
| runtime enclosure (if my understanding is correct), and
| anyway it was never going to be as elegant as a true rewrite
| system.
| kazinator wrote:
| Lisp gives you a programming language in which you don't have
| to write a cryptic 42 page one-liner to have an implementation
| of lambda calculus.
|
| Lisp gives you a way to talk _about_ lambda calculus, in a way
| that executes. For instance, papers about lambda calculus may
| talk about "beta reduction" and things of that nature. Those
| concepts are not _in_ lambda calculus; they are _about_ lambda
| calculus.
|
| In lambda calculus examples you have terms like \x x and
| whatnot. But lambda calculus doesn't explain what x is; x is an
| identifier and that is part of the description of lambda
| calculus, and not in lambda calculus.
|
| Lisp has the batteries included for describing languages, such
| as lambda calculus. It has an answer for what is x: it's a
| symbol, available as a data type. It has an answer for what is
| "beta reduction"; it's a function you can write, and execute on
| some piece of lambda calculus.
|
| Lisp closes the circle; the stuff you talk about in a paper can
| become code, and code which is not far from what the paper
| talks about.
| tromp wrote:
| > Lisp gives you a programming language in which you don't
| have to write a cryptic 42 page one-liner to have an
| implementation of lambda calculus.
|
| You totally misunderstood what the 42 pages are. They are not
| an implementation of LC, but an implementation of LISP in LC.
|
| > Lisp gives you a way to talk about lambda calculus, in a
| way that executes.
|
| LC gives you that too; it allows you to encode lambda terms
| as bitstrings, which can be represented as lambda terms
| themselves.
|
| > But lambda calculus doesn't explain what x is
|
| In the binary encoding, x is a de-Bruijn index: a natural
| number indicating the nesting level of the binding lambda.
|
| > Lisp closes the circle
|
| So does Binary Lambda Calculus.
| kazinator wrote:
| > _You totally misunderstood what the 42 pages are._
|
| There is a deliberate reversal of roles in my sentence that
| may not be obvious at a glance.
| somewhereoutth wrote:
| Beta reduction is in fact the _essence_ of LC - without it
| all you 'd have is a nice tree.
|
| The beauty and generality of LC is that x doesn't _need_ an
| explanation, it is just a placeholder, yet that is enough to
| define interesting (perhaps all) things.
|
| Lisp is an abstraction, that per article can be built upon
| the deeper abstraction of LC - question is, what does it give
| us in terms of expressiveness and understanding?
| smitty1e wrote:
| > Here is a PDF showing its entire lambda term, which is 42 pages
| long:
|
| Elsewhere, Douglas Adams smiles.
| zentr1c wrote:
| This
| lisper wrote:
| Hm, I wonder if the authors fine-tuned the feature set (and
| font size!) to achieve this outcome :-)
| zentr1c wrote:
| did he know the question to finetune too?
| somewhereoutth wrote:
| Ah but this is where it becomes interesting! Because we can
| then guage how much work this abstraction is doing for us - and
| indeed whether or not it might stray from the 'one true path'
| (whatever that might be)
| zentr1c wrote:
| Maybe I am stupid but what's the point in reimplementing lisp in
| lambda? Just to prove how beautiful simple lambda calculus is?
| The lambda functionality is allready in lisp. And lisp is
| beautiful simple!
|
| () is nothing and (is something) What does the implementation
| show more beautiful than that?
| tromp wrote:
| Binary Lambda Calculus is indeed beautifully simple [1]. LISP
| is rather complex by comparison, but then it's full-fledged
| non-esoteric programming language.
|
| [1] https://www.ioccc.org/2012/tromp/hint.html
| jart wrote:
| We do what we must because we can.
| contravariant wrote:
| Here I was wondering what a lambda expression implementing lisp
| would look like.
|
| Page 33:
|
| >((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((
| (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((
| ((((...
|
| Yeah that seems about right.
| somewhereoutth wrote:
| Yes but isn't it beautiful? But seriously, instead of seeing
| lots of brackets, see the whole as a texture, a texture that
| has some importance (per Lisp advocates). See it in context
| with other textures, indeed _all possible_ textures.
___________________________________________________________________
(page generated 2022-09-18 23:01 UTC)