41–50 of 196 posts
> I often see the halting problem misconstrued as "it's impossible to tell if a program will halt before running it." This is wrong. > The halting problem says that we cannot create an algorithm that, when applied to an arbitrary program, tells us whether the program will halt or not. Or more simply: No program can tell whether any program will halt or not.
One of the biggest boost to my SWE career was studying theory of computation and programming languages theory. My major was electronic engineering, so I didn't touch those at the university. But I use some books to at least grasp the introductory knowledge. The boost was how easy it is to find the mechanism to some abstractions. And instead of being those amazing and complex tools that you have to use carefully, they…
As an example, A practical walk through of what a simple CPU is doing was quite useful for getting the idea of what's going on. The concept of a Turing machine, which was originally intended for mathematical proofs, was not.
Earlier quoted context omitted.
Might be hard to approach but my favorite is Pierce's "Types and Programing Languages": https://www.cis.upenn.edu/~bcpierce/tapl/ (known as TAPL). Was grateful to take a graduate level class using it in college.
TAPL is nice, and also very dense. I haven't fully read it, but my current understanding is the follow: Both the Turing Machine and the lambda calculus only describes how to act on data. They don't actually describes what the data is. So you can craft an algorithm that works well, but it can be supplied with the wrong type of data and it will goes haywire. Your only recourse is to trust the user of your algorithm. Wh…
There is a clever way to encode Turing machines into Diophantine equations, so Diophantine equations (linear equations
Earlier quoted context omitted.
Would you have book recommendations / resources to share?
Might be hard to approach but my favorite is Pierce's "Types and Programing Languages": https://www.cis.upenn.edu/~bcpierce/tapl/ (known as TAPL). Was grateful to take a graduate level class using it in college.
https://www.cs.cmu.edu/~rwh/pfpl.html
It’s far more directed than TAPL, so I think it’s easier to read from start to finish. TAPL feels better as a reference.
I'm curious if you could make an analogy to the idea of "underspecified" in FreeCAD. It isn't that the drawing doesn't exist. It is that you still have some freedom in how long certain parts could be. Crucially, not all. It could be that parts of the drawing are indeed fully specified. Same can go with programs. You can constrain parts of it enough that you can answer some pretty specific questions. And similar to ho…
>I'm curious if you could make an analogy to the idea of "underspecified" in FreeCAD. That is just solution theory of a non-linear system of equations. The solution space can have exactly one solution (fully constrained), more than one (under constrained) or zero (over constrained). To be honest I do not really see a connection.
Moving the graphical drawing and constraints over to a symbolic system also helps see how many symbols it can take to cover a simple system.
Of course, the real reason for me thinking on this is that I'm playing with FreeCAD for the first time in a long time. :D
I sometimes wonder if the concept of “intelligence” is going to benefit from a formal model the way “computation” benefited from Turing Machines. Are there classes of intelligence? Are there things that some classes can and cannot do? Is it a spectrum? Is the set of classes countable? Is it finite? Is there a maximum intelligence? One can dream…
Purely intuitively, it seems like there should be a connection between the two (computation and intelligence). But I have not formally studied any relevant fields, I would be interested to hear thoughts from those who have.
If there's a nonphysical aspect to human intelligence and it's not computable, then that means computers can never match human intelligence even in theory.
One of the biggest boost to my SWE career was studying theory of computation and programming languages theory. My major was electronic engineering, so I didn't touch those at the university. But I use some books to at least grasp the introductory knowledge. The boost was how easy it is to find the mechanism to some abstractions. And instead of being those amazing and complex tools that you have to use carefully, they…
I have to vote the opposite direction. I don't think it's ever been relevant. As an example, A practical walk through of what a simple CPU is doing was quite useful for getting the idea of what's going on. The concept of a Turing machine, which was originally intended for mathematical proofs, was not.
Knowing that the actual regular expressions can be recognised by a finite automaton but PCRE and similar "LOL, just whatever neat string matching" extensions cannot means you can clearly draw the line and not accidentally make a product which promises arbitrary computation for $1 per million queries.
I agree that understanding something of how the CPU works is also useful, but it's no substitute for a grounding in theory. The CPU is after all obliged to only do things which are theoretically possible, so it's not even a real difference of kind.
> I often see the halting problem misconstrued as "it's impossible to tell if a program will halt before running it." This is wrong. > The halting problem says that we cannot create an algorithm that, when applied to an arbitrary program, tells us whether the program will halt or not. Or more simply: No program can tell whether any program will halt or not.
I really enjoyed the author’s explanation of undecidability. I found this bit was really helpful: “This to me is a strong "intuitive" argument for why the halting problem is undecidable: a halt detector can be trivially repurposed as a program optimizer / theorem-prover / bcrypt cracker / chess engine. It's too powerful, so we should expect it to be impossible.”
There are at least two meanings of "undecidable". The one, from computer science, is discussed in the blog post. The other, from formal logic, is a synonym to "independent". A proposition (not property) is independent of some axiomatic theory with respect to a proof system, if and only if the proposition can neither be proved nor disproved in that theory. For example, the continuum hypothesis is independent of ZFC. A…
I can't claim to answer this, but you might like to look at A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory[0] which (amongst other interesting things) does discuss the proposition "ZFC is consistent", which is independent from ZFC, in terms of a Turing Machine which enumerates all possible proofs in ZFC and halts when it finds a contradiction (e.g. a proof of 0=1).
But I don't think there's a simple equivalence here, all the same.
The logician's undecidable is always relative to a set of axioms, whereas the question of whether a property of strings can be decided by some TM doesn't place any constraints on the TM, which is to say the deciding TM is not required to, nor prohibited from, implementing any particular axiom set.
(It's tempting to try and show "provable in ZFC" to be a (CS)undecidable property by having a TM enumerate ZFC proofs and halt on finding a proof or disproof of the input string, and imagine the TM running forever when given a statement of the Continuum Hypothesis. But the TM could proceed by other means - for example [1] shows a proof of CH's independence in a theorem prover, so that a TM incorporating this construction could indeed reject CH statements as unprovable in ZFC. Which is not to say "ZFC-provable" *isn't* (CS)undecidable, just that showing this isn't as simple as constructing a ZFC-proof-enumerator and giving it the CH as input.)
Earlier quoted context omitted.
Philosophers have been trying to define what it means to be conscious since forever. I think that is informally what you mean here. If you just mean what problems can it solve, and how quickly, we already have a well developed theory of that in terms of complexity classes - https://complexityzoo.net/Complexity_Zoo
I don't either philosophical conceptions of consciousness or theories of computational complexity count as even "efforts to formalize intelligence". They are each focused on something significantly different. The closest effort I know of as far characterizing intelligence as such is Steven Smale's 18th problem. https://en.wikipedia.org/wiki/Smale%27s_problems
The original paper is better, but still seems to be too vauge to be useful. Where it isn't vauge it seems to point pretty strongly to computability/complexity theory.
Intelligence means many different things to different people. If we just gesture vaugely at it we aren't going to get anywhere, everyone will just talk past each other.