tag:blogger.com,1999:blog-11295132.post8201342159792013333..comments2015-05-20T17:18:26.607-07:00Comments on A Neighborhood of Infinity: Death to Hydrae (or the operational semantics of ordinals)Dan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger10125tag:blogger.com,1999:blog-11295132.post-61954888850281298212011-02-21T07:27:22.804-08:002011-02-21T07:27:22.804-08:00@Heinrich I should have subtitled this "the o...@Heinrich I should have subtitled this "the operational semantics of ordinal *notation*, including the symbols for successor, limit, addition, multiplication and power" :-)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-3946807367546475042010-08-02T05:57:10.264-07:002010-08-02T05:57:10.264-07:00@thecod
Ah, indeed, the recursion is on the machi...@thecod<br /><br />Ah, indeed, the recursion is on the machines, not the corecursive stream of numbers. That's a convincing argument.Heinrich Apfelmushttp://apfelmus.nfsho.comnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-2001318572368858052010-07-28T06:59:12.840-07:002010-07-28T06:59:12.840-07:00@Heinrich
Actually the use of coinduction here is...@Heinrich<br /><br />Actually the use of coinduction here is perfectly safe, as we are just destructing a coinductive element and recursing on the element of machine (no corecursive element is being built). Anywho, it would be easy to replace the infinite list by a function f:Nat->Nat, and giving an additional Nat parameter to run2.thecodhttp://www.blogger.com/profile/10717993079747767784noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-70201267059707208712010-07-25T03:26:43.331-07:002010-07-25T03:26:43.331-07:00@sigfpe
Well, they are significantly different fr...@sigfpe<br /><br />Well, they are significantly different from an operational perspective: after all, they behave differently for different input. (The argument that one machine can simulate the other breaks down when considering for example <i>2*w</i> vs <i>1+2*w</i>: one machine always prints even while the other always prints odd numbers.)<br /><br />The difference does seem to cease to matter when we're not interested in the full operational behavior, only in whether the machine terminates or not. This corresponds to mapping different machines to the same ordinal number. (Read the other way round, this means ordinal numbers don't necessarily have a unique, canonical machine associated to them, which is a bit at odds with the "promise" of your post). It's this additional step that I'm confused about.Heinrich Apfelmushttp://apfelmus.nfshost.comnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-38275323783627055372010-07-24T09:05:04.744-07:002010-07-24T09:05:04.744-07:00@Heinrich The equalities you point out aren't ...@Heinrich The equalities you point out aren't significant from an operational perspective. For example, consider 2w vs. w. The first is like second except that each time round the first loop you perform 2 inner loops. Inputting N to the first machine takes the same time as inputting 2N to the second machine. So if we're asking questions like "does this terminate for all input N?" the answer is the same.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-24759674306508592952010-07-24T02:48:47.484-07:002010-07-24T02:48:47.484-07:00Thanks for this article, Dan Piponi, the interpret...Thanks for this article, Dan Piponi, the interpretation of ordinals in terms of recursion is fascinating. I finally get around to ponder this, but I still don't quite understand what's going on.<br /><br />One thing that bugs me a lot is that <i>Machine</i> is <b>not</b> an "injective" representation of ordinal numbers! There are many machines with <b>different</b> operational behavior that represent the same ordinal number. For instance, we have <i>3 + w = w</i> or <i>2*w = w</i> as ordinal numbers, but not as machines.<br /><br />The culprit is the limit constructor <i>Input</i>. In terms of ordinal numbers, it represents the supremum of a sequence (:: Natural -> Machine) of ordinal numbers. But many operationally different sequences have the same supremum.<br /><br />Worse, since we are now underestimating the output size for some machines, this might affect the proof that every machine in M terminates. It's probably fine, but still, there's something going on I don't fully understand.<br /><br />@Dan Doel, thecod<br /><br />Wait a moment, it's not clear at all whether this will pass Agda's or Coq's termination checker: the second argument to the <i>run</i> functions is an infinite list, a coinductive thing! Mixing recursion and corecursion recklessly is known to result in nontermination.Heinrich Apfelmushttp://apfelmus.nsfhost.comnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-77585179521597059342010-07-08T07:54:51.783-07:002010-07-08T07:54:51.783-07:00Dan, whereas you are perfectly correct, I'm su...Dan, whereas you are perfectly correct, I'm sure you are aware that the termination of the Agda and Coq systems themselves is proved by appeal to an ordinal construction to justify the correctness of the recursive calls. It is interesting to note that in Coq we traditionally appeal to the First Uncountable Ordinal in what may be the most blatant case of mathematical overkill since Graham's Number!<br /><br />Of course the presence of circular arguments should not be surprising in a discussion about foundations :)thecodhttp://www.blogger.com/profile/10717993079747767784noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-71670918182088674152010-07-05T00:01:42.958-07:002010-07-05T00:01:42.958-07:00Another concrete example of a true unprovable stat...Another concrete example of a true unprovable statement is the Paris-Harrington theorem.speleologichttp://speleologic.livejournal.com/noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-65655102314659925032010-07-04T23:46:42.929-07:002010-07-04T23:46:42.929-07:00Dan Doel said:
> Unfortunately, his stuff seem...Dan Doel said:<br /><br />> Unfortunately, his stuff seems to be <i>inaccessible</i> now.<br /><br /><b>Inaccessible</b>? Waitaminnit, I thought we were talking <i>ordinals</i> here, not <i>cardinals</i> ...<br /><br />(<a href="http://instantrimshot.com/" rel="nofollow">Ba-dump-tshhh</a>)Fritz Ruehrnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-5289840309419458572010-07-04T13:26:56.148-07:002010-07-04T13:26:56.148-07:00Another termination 'proof' is simply that...Another termination 'proof' is simply that all your code, aside from the IO in run1, is (nearly) valid Agda, or easily translatable to Coq, passing their termination checkers. And it pretty clearly doesn't contain any weird fiddling designed to exploit logical inconsistencies you've discovered in their type systems. :)<br /><br />You can even go beyond this simple ordinal definition. If the definition here is O_1, then you can create an O_2 with the same definition, except that the limit constructor takes an O_1 -> O_2. And then you can create an O_3, with O_2 -> O_3. I once found a short paper by someone who'd tied all this up in an inductive-recursive definition in Agda, which roughly contained all of O_N similar to the above for every <i>inductive-recursive ordinal</i> N he could construct, which is pretty mind boggling. Unfortunately, his stuff seems to be inaccessible now.<br /><br />On an unrelated note, is the second incompleteness theorem usually considered contrived (the statement it uses is self-referential in a way)? When viewed through Curry-Howard, it becomes a rather practical concern for computer scientists, at least. Many have interest in languages that are guaranteed to be terminating, but the ability to write a metacircular interpreter is also viewed as desirable. The second incompleteness theorem roughly translates into saying that languages (satisfying its premises) cannot do both.Dan Doelhttp://www.blogger.com/profile/16761291400347369301noreply@blogger.com