I will never understand how people think like that. Sure, there are things computers cannot compute, but that's because those things are _uncomputable_ in general
It's obvious to you because of people like Church and Turing. Until their work on the Entscheidungsproblem was published, it was not only common, but mainstream to believe that nothing was inherently incomputable. They not only demonstrated that there were things that weren't, they did so by proving that the set of everything computable was the same set of things their approaches could compute and that certain proble…
What Computers Cannot Do: The Consequences of Turing-Completeness
51–60 of 61 posts
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#52I love this. I’m in appsec and bring up the halting problem all the time to developers to get them to think about the security landscape. The halting problem is why security is a unsolvable problem at its core. The real world consequences of this problem are something we have become desensitized to. I didn’t quite understand the impact of the halting problem until I started working in security, specifically for a com…
If you haven't already, read "Gödel, Escher, Bach". It sounds like you would enjoy it. For me its more of a "pick it up somewhere in the middle and get inspired" than "front-to-back" title but iirc it considers the halting problem and the incompleteness theorem to be two sides of the same coin. ISBN is 3423300175.
I really appreciate your comment. That book has been sitting behind me on my bookshelf for years blending into background. I just pulled it off the shelf.
I just graduated a few weeks ago after working on my BS for 10 years. The fact that you brought this book up, the piece that inspired me to go back to school in the first place… is something Hofstadter would probably refer as my minds I recursive loop of existence. Something of that sentiment at least
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#53I love this. I’m in appsec and bring up the halting problem all the time to developers to get them to think about the security landscape. The halting problem is why security is a unsolvable problem at its core. The real world consequences of this problem are something we have become desensitized to. I didn’t quite understand the impact of the halting problem until I started working in security, specifically for a com…
I think you misunderstand the halting problem. An algorithm that can prove any program halts or doesn't is impossible. But it's possible to prove it for some programs. This is relevant for security, because entire operating systems have been formally proven to adhere to their specification/free of all bugs: https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#54Earlier quoted context omitted.
I'm confused by your 'additively optimal' definition. Suppose that the objects we want to describe are strings of bits, and the description method D is just "listing the bits out in a sequence". Then surely no BLC term can describe the same sequence of bits with only a constant amount of overhead.
Then D is just identity, or λ 1, using only 4 bits of overhead?!
Regardless, I'd still consider your 'additively optimal' to be a strange definition, given that BLT programs get to have their input bits pre-expanded as a valid sequence of boolean terms for free. If all it means is that the input format accepted by D is a subset of the input format accepted by U, then many existing small UTMs could easily meet it just by restricting D's input format.
[0] https://doi.org/10.1016/j.tcs.2006.06.002
[1] https://mural.maynoothuniversity.ie/12416/1/Woods_FourSmall_...
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#55Earlier quoted context omitted.
Does the following terminate for all n? def foo(n): if n
Collatz is not "theoretically undecidable" because of a paradox, it's "practically undecidable" because it has an infinite domain, so "is_halting" implemented via simulation would take infinite time to try every number. Would you give an engineer an infinitely large project, criticize them for being unable to complete it, and use their 'failure' to support cancellation of a finite, smaller project with potential bene…
Or, how about this one:
def foo(n):
if n
I can trivially prove this halts for all n. Can your code?Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#56Earlier quoted context omitted.
Then D is just identity, or λ 1, using only 4 bits of overhead?!
If a 'description' of an 'object' is defined to always be a valid term or program that operates on provided input, then I don't see why Turing machines wouldn't nearly as easily be 'additively optimal' in your sense. For most universal Turing machines that represent an input bit as a constant-sized word (such as Neary & Woods' 8-state 4-symbol UTM [0], which represents each input bit as two symbols, or even their 15-…
Could you construct a 2-symbol UTM whose own encoding is under, say, 10,000 bits in size? If it takes 10,000 bits then it would not seem as easy as the 232 bit universal lambda machine.
> you could add a few states extra to expand new input on the fly, shifting any existing data to the left as necessary.
That would be more than "a few" states, and could easily add thousands of bits to the UTM size.
> given that BLT programs get to have their input bits pre-expanded as a valid sequence of boolean terms for free.
I guess you mean BLC programs. That criticism seems unfair, since the lambda machine model has no primitive notion of bits. Thus there is no expansion, only representation of bits in the lambda calculus.
> If all it means is that the input format accepted by D is a subset of the input format accepted by U
The input format for D can be all binary strings, e.g. if D is identity (assuming the delimited input model).
> many existing small UTMs could easily meet it just by restricting D's input format.
I don't know what this means. A UTM should parse the description of a TM from its input, and simulate that TM on the remainder of input. If it does that, then it would be additively optimal. It cannot assume any restriction on that remainder of input.
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#57I will never understand how people think like that. Sure, there are things computers cannot compute, but that's because those things are _uncomputable_ in general
It's obvious to you because of people like Church and Turing. Until their work on the Entscheidungsproblem was published, it was not only common, but mainstream to believe that nothing was inherently incomputable. They not only demonstrated that there were things that weren't, they did so by proving that the set of everything computable was the same set of things their approaches could compute and that certain proble…
Einstein, Gödel, and a few others verified work means the majority of us are coloring within the lines they drew until we die.
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#58Earlier quoted context omitted.
1. Unfortunately the set of "some" programs is unknown and most probably really small. 2. Even proving anything about finite state machines is NP hard so the problem is harder than just using weaker model of computation. 3. Proofs are not reuable: proving something about one program does not tell us anything about other programs. See excellent https://pron.github.io/posts/correctness-and-complexity for more details.
I don't think your reply is particularly effective when you are replying to a comment that exhibits a formally verified microkernel. > 1. Unfortunately the set of "some" programs is unknown and most probably really small. Many useful algorithms can be proven to terminate. Compare against the situation in mathematics: many theorems are not be provable, but that does not stop us from trying to prove useful theorems, or…
I would say that one small piece of software (Sel4 is only 9,400 SLOC!) always cited as an example is actually a very small set of programs that can be formally verified. I haven't heard of a formally verified web browser...
> Many useful algorithms can be proven to terminate.
Proving that a program terminates is not that much interesting. Lack of security vulnerabilities would be much better.
> But it is clear for example that if, say a program is recognized by inspection as the concatenation (splicing the final states and initial states together) of two programs that terminate, then this program terminates
But it does not tell us anything about real programs? We don't compose software by concatenating their state machines.
> Even the link you provide gives optimism and claims that
This is a call for empiricism (aka testing) and ad-hoc heuristics exactly because the problem is not solvable in general using formal methods.
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#59Earlier quoted context omitted.
If a 'description' of an 'object' is defined to always be a valid term or program that operates on provided input, then I don't see why Turing machines wouldn't nearly as easily be 'additively optimal' in your sense. For most universal Turing machines that represent an input bit as a constant-sized word (such as Neary & Woods' 8-state 4-symbol UTM [0], which represents each input bit as two symbols, or even their 15-…
> I don't see why Turing machines wouldn't nearly as easily be 'additively optimal' in your sense. Could you construct a 2-symbol UTM whose own encoding is under, say, 10,000 bits in size? If it takes 10,000 bits then it would not seem as easy as the 232 bit universal lambda machine. > you could add a few states extra to expand new input on the fly, shifting any existing data to the left as necessary. That would be m…
Ah, if you're specifically talking about self-encoding size as a yardstick, then you've got me: I spent yesterday afternoon adapting an existing UTM construction to take a look at this. While I managed to get most of the way there within ~40 states, it would take ~4 megabits to encode itself, by my estimation. Though it's difficult to tell just what the lower bound is, since the more states you allow in the UTM, the shorter you can make the encoding. I still suspect that 5 kilobits should be more than enough for someone actually good at TM golfing.
> That criticism seems unfair, since the lambda machine model has no primitive notion of bits. Thus there is no expansion, only representation of bits in the lambda calculus.
> The input format for D can be all binary strings, e.g. if D is identity (assuming the delimited input model).
> A UTM should parse the description of a TM from its input, and simulate that TM on the remainder of input. If it does that, then it would be additively optimal. It cannot assume any restriction on that remainder of input.
Having played with the UTM problem, I have a better understanding of the point I was trying to make. Consider a thought experiment, where you try to construct a UTM by making a TM that simply evaluates a BLC term on the tape. This TM by itself would still not be 'additively optimal' by your rules! It would also need an incremental input encoder to convert packed bits into BLC terms, as well as a lazy evaluation model to trigger it only when needed.
Thus, I think your UTM rules are a bit unfairly strict. A UTM that abides by those rules, as well as being additively optimal, must further be 'concatenatively optimal', in that for any description D, bit string s, and bit stream t, there must exist an encoding , no longer than + s, such that + t is equivalent to + s + t. (That is, adding a fixed prefix before the input cannot extend the encoding by more than the length of the prefix.)
But by itself, the language of BLC programs is not and cannot be concatenatively optimal! This is the expansion I was talking about: a given bitstring can't be represented as efficiently inside the BLC encoding as it can outside the encoding. To get a concatenatively optimal language, you'd have to formulate it as a (term, input) pair, where the input is a raw binary string that must be encoded before feeding it into the actual program. (This isn't an issue entirely unique to BLC: a TM model mandating an empty initial tape also couldn't be concatenatively optimal.)
So then, one might ask, where is the implementation of this input encoding within your 232-bit BLC term? Nowhere! Its only task is to 'interrogate' the first several input bits (as already encoded) to parse the description D. And when it finishes constructing the term corresponding to D, its job is done, since the remaining input bits are already encoded in a form it can use. So if we try to trace the point where the encoding actually happens, we can only conclude that it occurs wholly outside the lambda calculus. But the encoding step is entirely necessary for concatenative optimality to hold.
That is all to say, self-encoding size is an easily gameable metric (in the trivial case, you could make a universal machine that's also a quine, so that it can encode itself in 1 bit), and your idea of additive optimality is tied very closely to the power of the input model defined outside the system. (The input model can also be easily gamed: imagine that each cons term of the input, alongside the head and tail, also supplied a universal program. Under that input model, the program within the system would be trivial.) By saying that a UTM only gets 2 symbols and has to accept dense input, you mandate a very weak input model, so of course it will be tough to get it to accept arbitrary data.
---
But in the bigger picture, I'd like to note that I'm not trying to dunk on BLC here, nor on the lambda calculus in general: clearly, it's very efficient at representing and simulating itself, and no simple TM model can simulate itself nearly as easily. And that's all well and good if you want a model where you can treat code as data and do other stuff like that. But I maintain that this self-representation doesn't make it more universal, or otherwise more fundamental, than the TM model, which aims to use as simple a rule as possible for transitioning from one configuration to the next, at the cost of having heterogeneous code and data. (Imperatively speaking, lambda-calculus reductions would seem closer in power to a random-access machine, or perhaps a TM on a branching tape.) So being generous, I'd say that both are equally as fundamental, they're just trying to excel at two different goals.
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#60Earlier quoted context omitted.
> I don't see why Turing machines wouldn't nearly as easily be 'additively optimal' in your sense. Could you construct a 2-symbol UTM whose own encoding is under, say, 10,000 bits in size? If it takes 10,000 bits then it would not seem as easy as the 232 bit universal lambda machine. > you could add a few states extra to expand new input on the fly, shifting any existing data to the left as necessary. That would be m…
> Could you construct a 2-symbol UTM whose own encoding is under, say, 10,000 bits in size? If it takes 10,000 bits then it would not seem as easy as the 232 bit universal lambda machine. Ah, if you're specifically talking about self-encoding size as a yardstick, then you've got me: I spent yesterday afternoon adapting an existing UTM construction to take a look at this. While I managed to get most of the way there w…
Coincidentally, that is about the size of Penrose's UTM [1] which takes 5495 bits in its own encoding. I suspect that one is only linearly optimal, so it might take another few thousand bits to make it additively optimal.
> Consider a thought experiment, where you try to construct a UTM by making a TM that simply evaluates a BLC term on the tape. This TM by itself would still not be 'additively optimal' by your rules! It would also need an incremental input encoder to convert packed bits into BLC terms, as well as a lazy evaluation model to trigger it only when needed.
Yes; that's what it means to evaluate BLC programs. If the UTM does that, then it's additively optimal. It would be a TM implementation of the Universal Lambda Machine [2]. Most implementations you find there also have subroutines doing the conversion from bits to terms and back.
> for any description D, bit string s, and bit stream t, there must exist an encoding , no longer than + s, such that + t is equivalent to + s + t. (That is, adding a fixed prefix before the input cannot extend the encoding by more than the length of the prefix.)
I'm not quite understanding this. In my write-up, D is not a description but a description method, i.e. a computable mapping from binary strings (descriptions) to outputs (some set that includes binary strings). What is your D and what does mean?
> a given bitstring can't be represented as efficiently inside the BLC encoding as it can outside the encoding
By "inside the BLC encoding", do you mean as part of the lambda term encoding prefix of the BLC program? Indeed, that is why we equip BLC programs with pure binary input so that k bits of data only add k bits to program length. Which is what allows additive optimality.
> where is the implementation of this input encoding within your 232-bit BLC term?
It's part of the BLC machine model, i.e. of the description method. We can agree that BLC is a computable mapping from bitstrings to outputs including bitstrings.
> Its only task is to 'interrogate' the first several input bits (as already encoded) to parse the description D.
If by D you mean an encoded lambda term, then the 232 bits definitely include the parser of that binary encoding.
[1] R. Penrose, The Emperor's New Mind, Oxford University press, 1989.