Live data from Hacker News

Lisp is not based on the Lambda Calculus

danielsz.github.io

131–138 of 138 posts

Re: Lisp is not based on the Lambda Calculus

#131
post #129

Earlier quoted context omitted.

Could you elaborate? A bit searching throws up some very interesting stuff but AFAICS a transducer is roughly comparable to a partial function, which doesn't relate to my request for manual expression manipulation support. If I'm missing something, please say.

I'm referring to transducers as in clojure. You can compose 2 'map' transducers, and that results in a single 'map' of the composed mapping-functions. That's to say that the two expressions you wrote would result in the same computations if you expressed them in terms of transducers.

5 mins looking at https://stackoverflow.com/questions/26317325/can-someone-exp... I think I'm getting it. Ops accumulated and composed until they actually have to be evaluated. That's very interesting indeed, thanks, and I'll spend a couple of hours on it.

However, I was using my my example exactly as an example; I was after a symbolic manips app.

The issue of the cost of naively compiled functional languages matters to me as bad performance will kill a good thing.

Re: Lisp is not based on the Lambda Calculus

#132
post #128

Earlier quoted context omitted.

The Actor (which cannot be implemented by a nondeterministic TM) sends the 'stop' message to itself. However, just as there can be an arbitrarily long amount of time between two steps of a computation, there can be a arbitrarily long amount of time for a message to be delivered.

> The Actor (which cannot be implemented by a nondeterministic TM) As you now describe it, it cannot be implemented (physically realized) at all. Or, conversely, any physically implementable refinement of it (which will not exhibit the entire range of behaviors) will be simulatable by a TM. There are many abstract machines that cannot be implemented by TMs -- e.g. various oracle TMs. There is nothing special, surpris…

Digital arbiters can theoretically take an arbitrary amount of time to settle although statistically they tend to settle soon rather than later. Also, if an Actor sends itself a 'stop' message over the Internet via Timbuktu, it can take an arbitrary amount of time to be received back. Also, an Actor can take an arbitrary amount of time to process a message.

In the above models of computation, arbitrary means absolutely arbitrary, i.e., there is no a priori bound on the amount of time that it can take.

Your trouble may be with Plotkin's proof, which shows that state machine models of nondeterministic computation are inadequate.

Re: Lisp is not based on the Lambda Calculus

#133

Earlier quoted context omitted.

Object orientation derived from Simula-67 which was lexically scoped and preceded Sch3me by many years.

So Lisp 1, Lisp 2, Sch3me?

Sorry for the typo, HN on Android didn't enable me to fix it :-(

Re: Lisp is not based on the Lambda Calculus

#134
post #128

Earlier quoted context omitted.

> The Actor (which cannot be implemented by a nondeterministic TM) As you now describe it, it cannot be implemented (physically realized) at all. Or, conversely, any physically implementable refinement of it (which will not exhibit the entire range of behaviors) will be simulatable by a TM. There are many abstract machines that cannot be implemented by TMs -- e.g. various oracle TMs. There is nothing special, surpris…

Digital arbiters can theoretically take an arbitrary amount of time to settle although statistically they tend to settle soon rather than later. Also, if an Actor sends itself a 'stop' message over the Internet via Timbuktu, it can take an arbitrary amount of time to be received back. Also, an Actor can take an arbitrary amount of time to process a message. In the above models of computation, arbitrary means absolute…

I have no problem with the proof. It's easy to come up with non-computable abstractions. All of calculus is one (in fact, Turing himself pointed it out in "On Computable Numbers", and he invented and used others when he found them useful), yet it's commonly used to model natural systems without anyone considering it a proof against Church-Turing. So the fact that an abstraction is non-computable is unsurprising and has nothing to do with the thesis. The Turing thesis is relevant when you're talking about a physical realization, and you have not provided any proof that you've found one that's not Turing-computable.

Every physical object does have an a priori bound on the amount of time it can take to do something, unless that time could possibly be infinite. The reason is that it needs some sort of a counter, so it needs some state, and there's only so much state storable in the universe to store a counter.

Re: Lisp is not based on the Lambda Calculus

#135
post #50

Earlier quoted context omitted.

> general recursion using the y combinator isn't actually implementable in lisps I think the 'typed' bit is key. You can't implement Y in plain old Haskell because it would need to recurse infinitely during type-checking.

There is a strongly-typed definition of Y here: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

Some enterprising hacker should research who should be credited for the strongly-typed recursive def of Y.

Re: Lisp is not based on the Lambda Calculus

#137
post #71
post #62

Earlier quoted context omitted.

> this contributes to the notion that LISP/Schema/Lambda Calculus were "discovered", not that Lambda calculus has an explicit pedigree. That notion is wrong (at least with a very high likelihood), and it's usually stated by people who fetishize the lambda calculus but know little of its long evolution. It's just your ordinary case (of hubris) where people aesthetically drawn to something describe it as inevitable or…

Wow, that is an impressive survey --- thanks for putting that together!

Ron presented this at Curry On 2018

Ron Pressler - Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra

https://www.youtube.com/watch?v=2oNmR0q1uA0

Re: Lisp is not based on the Lambda Calculus

#138
post #28

Earlier quoted context omitted.

Don't forget Gödel!

In his famous 1936 article, Turing correctly noted that proof of the computational undecidabilty of halting problem does not involve the same fixed point as the one used by Gödel. See the following: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

Wow. Thanks for sharing this.
Post reply on HN