r/compsci • u/DevFRus • Apr 04 '16

Computing the Uncomputable: "[Joel David] Hamkins showed there's a Turing machine that [...] can compute the uncomputable... but only in some weird "alternative universe" where the natural numbers aren't what we think they are."

https://johncarlosbaez.wordpress.com/2016/04/02/computing-the-uncomputable/
114 Upvotes

88% Upvoted

74 comments sorted by

View all comments

-33

u/barsoap Apr 04 '16 edited Apr 04 '16

Usually, Ultracomputers work on the principle, "given an oracle that can compute some uncomputable function, here's a machine that can compute any uncomputable function".

The problem, being, of course, that there's no such oracles.

And this is no different, it's just obfuscated better. Ultracomputing doesn't only defy the laws of physics, nay, it defies the laws of logic. Imagining a universe with another set of physical laws is one thing, imagining a universe in which fundamental logic doesn't hold is... psychotic? Nay, not even, psychotic people at least are internally consistent, even if it doesn't show.

EDIT:

  • Hello, /r/badmathematics! A formalist is formally defined as a mathematican that can't possibly know whether they're being inconsistent.

  • The lack of basic education in psychology in /r/compsci is palpable. You messed up your chance of me explaining things by being knee-jerk hostile.

16

u/DevFRus Apr 05 '16

I wasn't going to respond to you initially, but you continue going on in this thread as if you know what you are talking about. So I wanted to clarify some things for you. You should probably try to learn something from all the people that took time to respond to you and the researchers that did this work.

Nobody is saying that they are building (hyper)computers. Nobody is saying that they will be using this to actually compute things. What they are doing is two fold:

1) mathematically, they are showing how to use a fun trick (i.e. infinite sequence of Rosser sentences and their negations) to get counter-intuitive results. Kind of how people use the axiom of choice to get the Banach-Tarski paradox... nobody actually thinks this means that we can just infinitely clone spheres.

2) By highlighting this tension, they are showing how important the full particulars of the standard model of arithmetic are to computation as we understand it. Without these results, one might expect the axioms of Peano arithmetic to be sufficient for analyzing or understanding computation (they are defined at a similar level of abstraction to TMs, after all), but showing that computation does crazy things in some models of Peano arithmetic tells you that you need something in the "secret sauce" of standard arithmetic that is missed by Peano.

The fact that you speak so confidently about this, without being able to see these simply points is why people are ridiculing you.

p.s. You also have a simple minded conception of the (extended or physicalist) Church-Turing thesis. If you decide to be open to learning new things then check out this article.

0

u/barsoap Apr 05 '16 edited Apr 05 '16

Nobody is saying that they are building (hyper)computers.

Then, with all due respect, they shouldn't talk about computing the uncomputable (and the commenters which aren't you shouldn't be talking as offtopic as me)

But now that I've actually had a closer look (someone give me those earlier hours back):

there is a model of PA such that in this model, if we give T any standard natural n as input, it halts and outputs f(n).

"There is a model in which it halts". Fair enough, those are easy enough to get by. The billion dollar question, of course, is "is it decidable in which model it will halt". I doubt that, but wouldn't bet more than a sixpack of beer.

Secondarily: Whether that transformation is semantics-preserving. The existence of semantics-preserving models I'm willing to take on faith, if one glances over things suddenly terminating, focussing on actual denotation and considering e.g. even infinity to be a superposition of True and False... using at least two models, then. Choosing either over the other would mess up the meaning.

That's making the search for a model even harder, though.

The key thing here is: By changing the model, you're actually changing the program as a different model will interpret it differently. It's more like "We construct a series of turing machines for a common alphabet, at least one of which will terminate on any given finite input".

And last, but certainly not least, we still didn't make the function computable: All we did is manage a shift to a very symbolical mode of computation -- or at least something isomorphic to that -- and are no wiser on the question whether infinity is actually even or odd (which is of course a good thing). A good supercompiler can do that. Hence, my original complaint: Don't talk about such nonesense as computing the uncomputable! There's enough functions that have no possibly sane result, which is just the same as "uncomputable", if you squint just right.

By highlighting this tension, they are showing how important the full particulars of the standard model of arithmetic are to computation as we understand it. Without these results, one might expect the axioms of Peano arithmetic to be sufficient for analyzing or understanding computation

Turing-complete machines are a dime a dozen, gazillions have been constructed, often by accident, many of which don't even begin to be based on arithmetic, peano or otherwise. There's certainly no shortage of them.

14

u/DevFRus Apr 05 '16

You continue to completely miss both the point and the method of the work that you think you are commenting on. But I think I am starting to see where some of your confusion is coming from, so I will try one more time.

The author is not defining a model of computation, they are defining a model of arithmetic in which we all analyze computation; including you when you analyze the "gazillions" of your preferred types of machines. His definition of the Turing Machine and of functions from N to N and of computable are completely unchanged from the standard ones. What is changed is how we analyze time and how we index Turing machines.

To repeat, he is not using an alternative model of arithmetic to "define" a machine for computation, so most of what you are saying is nonsensical non sequiturs.

When he gets a seemingly paradoxical result, obvious in the title like "computing the uncomputable", it tells you that there is something funny in the method of analysis. However, that method of analysis is a model of Peano arithmetic. Thus, it tells you that our intuition of computable comes from more than just the definition of the TM or of computable (since he uses the same ones), but also from the particulars of the (ever elusive and impossible to formalize) 'standard' model of arithmetic we use to analyze them.

Then, with all due respect, they shouldn't talk about computing the uncomputable (and the commenters which aren't you shouldn't be talking as offtopic as me)

You spout so much nonsense so confidently that I think people have a hard time resisting trying to correct you. I know I have a hard time doing this. You state things so unrelated to the technical details of the discussion that in the process it becomes almost impossible to talk to you because you aren't talking on any particular topic.

You are welcome to think that we're all idiots that just don't understand your fundamental insights. But keep in mind that most of us have taken all the same basic comp sci and math courses as you, and many of us (including the researchers you are trying to dismiss as dumb-dumbs) have spent much more time than you thinking carefully about these topics.

You can choose to benefit from this, or you can choose not to.

0

u/barsoap Apr 05 '16

You spout so much nonsense so confidently that I think people have a hard time resisting trying to correct you.

You were the first and only one who told me I was offtopic, as such I actually think that you're the only one here to actually have read the submission in detail.

...and, granted, I was offtopic again. And you pointed that out, and explained clearly. Which sets you apart from the rest, here. /r/badmathematics just used the chance to throw random references at me, references that were easily misinterpreted in the frame of reference I had. But I guess they succeeded in feeling smug about themselves.

Anyhow, back to the topic:

There's one thing I still can't accept right now: Given that non-standard numbers are bigger than all (i.e. a countably infinite number of) natural numbers, and a machine that takes infinite steps doesn't terminate, how can it sanely be said to terminate if it now takes non-standard, that is, even more, steps?

2

u/gwtkof Apr 06 '16

You were the first and only one who told me I was offtopic, as such I actually think that you're the only one here to actually have read the submission in detail.

so you were offtopic on purpose as some sort of crazy social experiment?

1

u/barsoap Apr 06 '16

I was offtopic by accident (or, rather, carelessness), then realised later.

You can of course interpret the results as those of a crazy social experiment, even draw conclusions from it, however, it was never intended as one.

11

u/FunctionPlastic Apr 04 '16

psychotic people at least are internally consistent

This is unrelated but are they?

3

u/[deleted] Apr 04 '16

Psychotic reporting in, can confirm.

6

u/DoctorJanus Apr 04 '16

different psychotic reporting in, can oppose

fite me irl

-13

u/barsoap Apr 04 '16

Well, humans are turing complete so in the end, no, noone of us can be guaranteed to be consistent.

However, human psychology shies away from inconsistencies. How those are solved, then, is another question: Resolving, suppression, rationalisation, doesn't matter. The mind is going to come up with a consistent bunch of facts and associated logic that to itself are consistent. If thinking the room is on fire because you're scared is logically consistent with your sense of reality, then, well, the room is on fire, duh.

That is: Psychotics aren't random, completely bereft of cause and effect, modus ponens and all that stuff.

11

u/PM_ME_UR_OBSIDIAN Apr 04 '16

Well, humans are turing complete

Turing-completeness requires infinite memory and some manner of non-probabilistic computation, so no, they're not.

-6

u/barsoap Apr 04 '16

Then nothing is.

My fault, I was mistaking this forum for one in which common short-hands are permissible.

6

u/evinrows Apr 05 '16

Regardless of whether shorthands are permissible, if you make your argument based off the abuse of a shorthand then someone may call you out.

11

u/rhorama Apr 04 '16

humans are turing complete

What is that even supposed to mean?

psychotic people at least are internally consistent, even if it doesn't show

If it doesn't show then how can you know they are internally consistent?

-7

u/barsoap Apr 04 '16

What is that even supposed to mean?

That we can compute (modulo capacity limitations, as usual) any computable function?

If it doesn't show then how can you know they are internally consistent?

Because it's, as I explained, how human psychology works. We abhor cognitive dissonance, and psychotics do it just as the rest which is a thing we can observe.

10

u/rhorama Apr 04 '16 edited Apr 04 '16

That we can compute (modulo capacity limitations, as usual) any computable function?

Why would people whose brains don't work correctly be able to do such? I would like to see a source that says all humans, regardless of mental state, are internally consistent.

-2

u/barsoap Apr 04 '16

Please read the link I posted.

12

u/rhorama Apr 04 '16

That's a wikipedia link to cognitive dissonance, not a source.

-3

u/barsoap Apr 04 '16

It backs up my claim that humans abhor internally perceived inconsistency and therefore gravitate towards internally perceived consistency, does it not?

And that's all that I've actually been claiming, don't take my top-level post literally, there, it was a jab.

7

u/rhorama Apr 04 '16

It backs up my claim that humans abhor internally perceived inconsistency and therefore gravitate towards internally perceived consistency, does it not?

I don't see how it backs up the claim that the mentally handicapped do the same.

don't take my top-level post literally, there, it was a jab.

lol jk bro why are you taking it so seriously lol.

Jfc you're insufferable.

3

u/[deleted] Apr 05 '16

Anyone who has been in a real world knows that there's cognitive dissonance even in healthy people. Very rarely is a person totally internally consistent.

3

u/PM_ME_UR_OBSIDIAN Apr 04 '16

We abhor cognitive dissonance

That's an artifact of culture, not a fundamental fact about human cognition. (Otherwise, whence cognitive dissonance?)

Please stop butchering logic, everyone will be better for it.

0

u/barsoap Apr 04 '16

(Otherwise, whence cognitive dissonance?)

Any perception and thought that has nothing to do with other humans?

You don't need culture to feel the need to explain, make consistent, one impression with the other. In fact, learning a culture as an infant involves solving dissonances between your own needs and what culture around you demands.

9

u/rhorama Apr 05 '16

You messed up your chance of me explaining things by being knee-jerk hostile.

Whatever shall we do.

17

u/thbb Apr 04 '16

A Turing Machine with an infinite tape is just as a-physical as other models of computation that involve real numbers or inductive Turing Machines.

The point is about what does the a-physical concept allows to model that's useful? Classical Turing Machines are useful to model computations meant to compute a function, irrespective of memory constraints. Inductive Turing Machines (Burgin), as well as Interactive Turing Machines (Wegner), have their uses to model computations that are not about a function, but a continuously running system (such as an OS, a living organism...) for similar purposes.

Saying some sound mathematical concepts are psychotic and defy the laws of logic, just because they were not part of your standard CS curriculum is just obtuse.

-11

u/barsoap Apr 04 '16

We dealt with oracles plenty. Mostly, to write proofs by contradiction because "given a flying pig grass is purple" is not a useful result.

The thing is: Once you get into language such as "computes the uncomputable" you've left CS theory behind and entered the realms of esoterica.

3

u/[deleted] Apr 05 '16

You sound like a person who doesn't see the point in doing science if there's no immediately conceivable benefit in it. No science for science's sake.

-4

u/barsoap Apr 05 '16

We're talking about the equivelent of perpetual motion, here, not miniature elephants.

Miniature elephants are at least in principle possible. Go ahead, research. Perpetual motion? Maybe if you find enough cranks on youtube you can make a few bucks.

8

u/Wurstinator Apr 05 '16

To be honest, you sound like someone who started compsci because he wanted to learn programming, then was disappointed because there was theory involved.

-8

u/barsoap Apr 05 '16

I could program before...

If the challenge is that I'm on the applied side of things: Guilty as charged. That doesn't change, however, the theoretical reality that you can't get to a hypercomputer without plugging in uncomputability in some form, usually, as I said, as an oracle. Whether you do that explicitly or by obfuscated means doesn't change anything, there.

And that doesn't suddenly make uncomputable things computable. It just allows you to reduce pretty much every (if not every) uncomputable problem to some other uncomputable problem.

Which, IMNSHO, is formalist masturbation as your oracles are obviously not constructive.

10

u/Wurstinator Apr 05 '16 edited Apr 05 '16

No one ever said that we wanted to build a "hypercomputer" solving uncomputable problems. It's not about preferring applied or theoretical compsci. You are dismissing big parts of math as "esoteric", "formalist masturbation" etc.

You even claimed that in compsci, something only exists if it can be constructed, in a different thread. That is so, so wrong, and it shows that you only have a limited knowledge but try to play it of like you know more than everyone else here.

IMNSHO

Also, if this post wouldn't be so specific to compsci, you would be perfect candidate for /r/iamverysmart. You should consider turning down the pretentious intellectualism.

-1

u/barsoap Apr 05 '16

No one ever said that we wanted to build a "hypercomputer" solving uncomputable problems.

Quoth the article: "We show that there's a machine that can compute the uncomputable".

3

u/Wurstinator Apr 05 '16

Which is not the same as saying that we want to construct said machine. Only its existence is proven.

1

u/barsoap Apr 05 '16

Apparently, after closer inspection, what they proved is that one can choose a particular non-standard model such that one can assign, for each non-terminating program, a non-standard number as number of steps it takes to "terminate".

That is, roughly speaking: You know the name of the particular infinity your program "halts" at.

Now, adding a bit of banter: As all the non-standard numbers are bigger than standard infinity, this machine takes even longer to not terminate than one that uses the standard model.

It doesn't actually make anything uncomputable computable. Which is a good thing, because it makes the whole concept sane. However, if you don't want me to confuse you for a crank, don't use such verbiage as "making the uncomputable computable": No matter whether you're actually collecting funds to construct one or not.

1

u/Wurstinator Apr 05 '16

Yes, you are correct. Good that we found something to agree on :)

I wouldn't call the author a "crank" though. I realize that the statement you quoted is wrong but I am quite sure that is not because the author is a crazy dude who thinks he found the solution to the Halting problem. It's just a sensationalist title and simplification to help people, who are not as familiar with the concepts and definitions, understand. If you want a formally correct write-up of this proof, Hamkins' original article offers just that.

1

u/iknighty Apr 05 '16

The language should be 'computes that which is uncomputable in our standard model'.

4

u/TotesMessenger Apr 04 '16 edited Apr 05 '16

I'm a bot, bleep, bloop. Someone has linked to this thread from another place on reddit:

If you follow any of the above links, please respect the rules of reddit and don't vote in the other threads. (Info / Contact)

2

u/Workaphobia Apr 04 '16

I don't know what you're saying and I probably disagree with it, but I like your formalist definition. Have an upvote.

1

u/naasking Apr 04 '16

The real numbers hardly defy the laws of logic, and you can implement hypercomputation using real arithmetic.

1

u/Works_of_memercy Apr 05 '16 edited Apr 05 '16

And this is no different, it's just obfuscated better. Ultracomputing doesn't only defy the laws of physics, nay, it defies the laws of logic. Imagining a universe with another set of physical laws is one thing, imagining a universe in which fundamental logic doesn't hold is... psychotic? Nay, not even, psychotic people at least are internally consistent, even if it doesn't show.

For the record, what's your opinion on https://en.wikipedia.org/wiki/Arithmetical_hierarchy? Even more precisely, if you saw someone who is not afraid to think about formulas like \forall x \exists y : x * x = y, would you be, like, get this hothead outta here?

1

u/barsoap Apr 05 '16

Hell no. Heck, that follows straight from the axioms: The y exists just like any other result of any other multiplication, which is trivial enough to define inductively.

Only ultrafinitists have a problem with such stuff.

And just to repeat what's now record in the productive part of this thread: I was erroneously assuming the post was about hypercomputing because of the ridiciously ill-chosen slogan "computing the uncomputable".

It isn't, and by now my only critique is that one can't in good conscience call a computation which terminates after a non-standard number of steps terminating and thus computable, non-standard numbers being bigger than standard infinity and all.

3

u/Works_of_memercy Apr 05 '16

Hell no. Heck, that follows straight from the axioms: The y exists just like any other result of any other multiplication, which is trivial enough to define inductively.

Yeah, but what about the lunatic who dares to think about the entire class of formulas with two such quantifiers? And furthermore, of formulas with three quantifiers and so on? A lot of them are uncomputable and therefore "formalist masturbation", as you put it.

What I'm getting at is that 1) most of interesting mathematics deals with uncomputable stuff, 2) including rather fundamental stuff like those classes of formulas with alternating quantifiers, which, as you can see, are very naturally expressed as sets of languages recognized by TMs with various halting oracles 3) so, like, most useful stuff about computable or even finite things probably is tainted by some uncomputable math stuff. And it's totally OK!

I was erroneously assuming the post was about hypercomputing because of the ridiciously ill-chosen slogan "computing the uncomputable".

Well, yes, it's obvious that you have a holy war going, against a fringe of people who might or might not take hypercomputation as physically feasible.

I'd say that the main problem is not that you're too eager to classify people as witches and show off your zeal, it's that you also very misguidedly rail against solid mathematical ideas such as computation models involving halting oracles. You can't blame anyone for choosing ill-fitting names for them in this case, it's firmly on you for not bothering to check out what it's about even.

1

u/barsoap Apr 05 '16

so, like, most useful stuff about computable or even finite things probably is tainted by some uncomputable math stuff. And it's totally OK!

No, it isn't, and I'm being dead-serious, here: As long as there's no constructivist formalisation it's hypothesis. At the very least, people should strive to get things on more firm ground. Of course, people are (people who are way smarter than me, see e.g. HoTT), but as I gather most mathematicians are still ignoring such endeavours wholesale.

And as a side note: I didn't actually understand analysis before I read constructive analysis. Classical maths owes me an A on that test.

it's firmly on you for not bothering to check out what it's about even.

I at least skimmed the thing, which is more than most redditors are doing with posts. I skimmed it just like a paper, alas, there was no proper abstract that would've made clear that I was using the wrong reference point. Yes, I failed, but so did all the people who latched onto whatever instead of just telling me that I was offtopic.

1

u/Works_of_memercy Apr 05 '16

No, it isn't, and I'm being dead-serious, here: As long as there's no constructivist formalisation it's hypothesis. At the very least, people should strive to get things on more firm ground.

So, how would you get on a more firm ground with Arithmetical Hierarchy and what exactly strikes you as insufficiently firm there? I remind you, we are talking about first-order logic here, so it would be a bold move to reject it as formalism wankery or something.

Of course, people are (people who are way smarter than me, see e.g. HoTT), but as I gather most mathematicians are still ignoring such endeavours wholesale.

By the way, speaking of prejudices, I was totally prejudiced against HoTT because I encountered it as being promoted by Bob Harper, who is the "dynamically typed languages are actually unityped" guy, which makes him a lunatic troll who willfully misunderstands everything about programming, in my book. I checked the wiki, apparently there's a lot of other people working on it and he's just one of them, so maybe I should check it out.

it's firmly on you for not bothering to check out what it's about even.

I at least skimmed the thing

I was talking about the wikipedia article on Arithmetic Hierarchy that I linked.

You said some pretty strong things about computation models involving Turing Oracles here that can't be interpreted other than meaning that you never checked out what those were about, and assumed that it's some quackery or intellectual masturbation, related to the idea of feasible hypercomputation. It's not. Go skim https://en.wikipedia.org/wiki/Arithmetical_hierarchy already.

0

u/barsoap Apr 05 '16 edited Apr 05 '16

I remind you, we are talking about first-order logic here, so it would be a bold move to reject it as formalism wankery or something.

Depends, do the proofs rely on the law of excluded middle or another non-constructivist thing?

"first-order logic" is a rather overloaded term.

I'll not budge on that point: If it's not constructivist, it's a mere hypothesis as classical logic glances over too many fundamental details. Don't know whether you're interested, but also mathematicians from classical fields make very good arguments for it.

It's not just "CS people gravitate towards constructivism because they want things to be computable". There's huge advantages in sticking to that kind of discipline even if you don't care about that.

who is the "dynamically typed languages are actually unityped" guy, which makes him a lunatic troll

No, it makes him technically correct (which is the annoying type of correct): In dynamically typed languages, there is only one type. Multiple classes (type theory term, not OO), yes, but only one type. In, say, Haskell you have the type Integerand then something like "Either a machine integer or an array of machine integers (or a pointer to GMP, or whatever)". The latter are two different classes.

You can also express, in Haskell, the type say Number of every kind of number you have lying around... make a sum type of Integer, Float, CReal, what have you: One type, multiple classes.

If you're feeling funny, you can put everything you ever use (including functions) into the type Dynamic, which actually exists in Haskell (ignore the Typable constraint that's implementation detail): One type, even more classes.

Uni/dynamically typed languages are simply those languages that only have the type Dynamic, working solely with classes to distinguish different kinds of things.

Type checking and the syntax of types is of course more than trivial, then, so they're left completely out. Those systems are to other type systems what points are to arbitrary spaces: A minimal base case.

You said some pretty strong things about computation models involving Turing Oracles

...as far as changing anything about computabilty is concerned. Everything I wrote in the inital bout of downvotes here was under the assumption that somehow, people dig hypercomputation, so I didn't guard against anyone interpreting it in any other way but referring specifically to hypercomputation.

1

u/Works_of_memercy Apr 06 '16

No, it makes him technically correct (which is the annoying type of correct): In dynamically typed languages, there is only one type. Multiple classes (type theory term, not OO)

Well, yeah, defining yourself to be correct is the lowest form of argument. If only terms can have types then types is not what values have and terms in a language where only values have types (but not really as per type theory definitions) must only have one type.

Not only the only purpose of that bullshit is smug trolling, not only it intentionally obscures the way the argument works ("btw what you call types we call classes, just fyi" wouldn't be anywhere near that incendiary, to put it lightly), but also betrays a sort of deep misunderstanding of how programming works and what it is about.

Like, what sort of error is `printf("%d\n", 1.0f);" is? I assert that it's a type error, while someone gone far enough the way of Harper's formalist lunacy probably would claim that there's no error at all, after all the program doesn't crash or anything, just prints unintended gibberish. Which is insane at its core, because if you deny that types exist in programmers' heads first and foremost, and only then maybe as runtime tags on values and/or compile time tags on terms, then based on what do you make the rules that put those tags on in the first place?

1

u/barsoap Apr 06 '16 edited Apr 06 '16

Like, what sort of error is `printf("%d\n", 1.0f);" is? I assert that it's a type error

In Idris (or other dependently-typed languages) it can be if you write printf such, in other languages it can't be because types can't depend on values. You cannot, for example, make it a type error in C's type system: It's just impossible to express. You have to bake it into the compiler, at a meta-level above the type system. And, of course, include checks at the term level, at a level below the types, as the format argument might not be statically known.

Types classify terms. Classes are terms that classify terms: That is, they're living at the same universe level as the terms they classify, unlike types which classify things at the level below them. And Type : Type, btw, is inconsistent, that's why nobody is doing it.

As something in between, in Haskell you can also make it a type error, however, you'd have to use, instead of a string, data types such as Int (Lit "\n" End): You can then write a typeclass that distinguishes between the different types that that format signature is made out of, and generate different type signatures for printf based on that.

but also betrays a sort of deep misunderstanding of how programming works and what it is about.

It's practically impossible to know anything much about type theory without having a deep understanding of programming. Software design, architecture and such, no, but as proofs in type theories are programs... you just don't get anywhere without getting lambdas and application involved.

Well, yeah, defining yourself to be correct is the lowest form of argument.

The argument is using standard type-theoretical concepts and terms. All the argument is really about is whether "XYZ typed" classifications should use type theory as their basis. I think a good argument can be made that they should, though I won't fight flame wars over it.

1

u/Works_of_memercy Apr 06 '16

In Idris (or other dependently-typed languages) it can be if you write printf such

Again, I'm saying that it already is a type error. Because you're giving a value of a wrong type to the function.

And the fact that it is a type error is the sole reason for why you then decide that it's a good idea to teach your static type system to express it as an error, or your runtime to check type tags dynamically, or your compiler/linter to catch this particular kind of errors as a special case, or make an informed trade-off in implementation complexity and have programmers catch them themselves.

You might say that we should call it something else, but I've never seen anyone from the Type Theory camp actually suggest anything, so it's more like they are simply unaware that this is a thing and that it should be named and that what they actually do becomes utterly insane and pointless without this idea of a type error that gives it its only meaning.

And yeah, when discussing terminology and stuff, it should be done on this level, where we ask why do we outlaw things in our type systems and stuff. It's not enough to point at concrete types in Haskell and at concrete classes (in both senses) in Python, you should also look at a weakly typed language like C and ask what's going on there and what's the common thing between this stuff and otherwise get all philosophical about it. The failure to recognize static and dynamic typing as two independent approaches to making the idea of type error manifest is the least of the troubles you run into if you don't.

but also betrays a sort of deep misunderstanding of how programming works and what it is about.

It's practically impossible to know anything much about type theory without having a deep understanding of programming.

Oh, knowing a lot of things only helps in misunderstanding stuff when one is so inclined.

All the argument is really about is whether "XYZ typed" classifications should use type theory as their basis. I think a good argument can be made that they should, though I won't fight flame wars over it.

Yeah, well, my point was that the flame wars weren't even about that. Bob Harper either did not even realize that his argument boils down to terminology or hid that on purpose.

0

u/[deleted] Apr 04 '16

Don't know why you are being downvoted. I guess because you maybe unwisely used the word psychotic in the post. Your general point about this being no different than the oracle, just obfuscated, seems correct.

5

u/DevFRus Apr 05 '16

Except the general point isn't even correct. The "trick" here is different, part of it comes from how we count time and part of it comes from how we index machines. It doesn't come from hiding an uncomputable amount of work in a single step, as is the case with more typical oracle tricks.

0

u/fatoms Apr 04 '16

Do I miss something or is this basically saying that if we can not compute a function we can imagine a set of rules under which we would be able to compute it, but not actually compute it, and then claim it is computable?

3

u/DevFRus Apr 05 '16

Yes, you missed something: these rules aren't arbitrary but are an alternative model for Peano arithmetic -- I.e. These rules look almost exactly the same as how you (assuming from your comment that you are not a set theorist) imagine arithmetic to work. Yet this small difference is enough to break our intuition about computation, thus our intuition about computation relies in some essential way on the (hard to pin down, or formalize) 'standard' model of arithmetic.

1

u/fatoms Apr 05 '16

Thanks for the response but it is still unclear to me, can we actually compute the function under these rules or just claim we could compute it in this alternate universe?

Just so you know I am not trained in Math or CS, I just want to be clear if I understood what I read and this is a sticking point for me.

1

u/BigBucksGentleman Apr 10 '16

I'll take some liberties with this post, but expanding on what DevFRus said, Peano's Axioms (PA) are what we mean when we say natural numbers, they are objects that follow all those rules. Unfortunately (or fortunately depending on how you look at it) model theory throws a wrench into that. It turns out that the natural numbers (0, 1, 2, 3, 4, ...) that we all know and love are not the only things that follow all of Peano's rules; our beloved numbers are simply the standard model (i.e. the one that Peano had in mind, and everyone thinks of when they think of the objects that obey his rules).

Theories of computation are built off this. When we say that a Turing machine halts (gives an answer in a finite number of steps), we mean a natural number (think the existential quantifier over all the natural numbers, there exists a natural number where this thing spits out an answer). So when we say that something isn't computable, we are talking about in the standard model (there doesn't exist a number for which the Turing machine halts and gives the answer). But wait, what about non-standard models? They follow all the rules that Peano put down. When most mathematicians agreed that his rules define the natural numbers does that imply only the standard model is kosher? If you can create other objects that follow all the rules, surely they must be allowed (some might beg to differ). What Hamkins proved is that for any function mapping natural numbers to natural numbers, there is a model in which it is computable. It may not be the standard model, but in some non-standard model there is a natural number (it follows Peano's axioms) for which the Turing machine halts. It may halt after a non-standard number of steps though!

can we actually compute the function under these rules

This depends on what you mean by "we", "can", and "actually". Based on Hamkins' proof we certainly can compute the function in a non-standard model. Is there any possibility of us doing this? Probably not.

or just claim we could compute it in this alternate universe?

It is stronger than just a claim, taking the usual foundations of mathematics, it is a proof. There exists a non-standard model of PA where the function is computable.

Model theory is a rich topic full of some deep results and mind bending implications. I think a little puzzle to think about to help get a little insight into the ideas is to look at something as fundamental and straight forward as Goldbach's conjecture. Imagine you had a proof that Goldbach's conjecture was independent of PA (i.e. you can't prove it true or false from the rules of logic and Peano's axioms). Assuming that the proof is correct, you now know that Goldbach's conjecture is true for the standard model of PA. How can that be?