41–50 of 101 posts
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…
Earlier quoted context omitted.
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?
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 im…
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?
Earlier quoted context omitted.
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 co…
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 algor…
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.
Earlier quoted context omitted.
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 co…
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 tha…
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.
Earlier quoted context omitted.
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…
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 wh…
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.
Earlier quoted context omitted.
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…
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 wh…
It's not; here it is quoted from [1]:
(λ 1 1) (λ λ λ 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)))
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...
Earlier quoted context omitted.
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 wh…
> 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.
Make that a few dozen...
Earlier quoted context omitted.
There is. Using the Mogensen–Scott encoding, a self-interpreter can be written in lambda calculus as (λf.ff)(λf.λt.t(λx.x)(λm.λn.ffm(ffn))(λm.λv.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)…
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…
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 λ 1, and output the blc encoding of the nil-terminated list of 4 booleans that represents that bitstring:
01000101100000110010110000011001011000001001011000001100101100000100000100000000101101110110