Hacker News Reader

Comment by JadeNB | Hacker News Reader

I'm confused by this. It seems to be promising a normal form for all expressions in a Turing-complete language—but that's equivalent to guaranteeing termination, isn't it? Moreover, it promises to produce equal results for equivalent programs, which would allow a solution of the halting problem, wouldn't it?

I suspect that I've got some bad conceptual misunderstanding here; but, on the other hand, I also have a hard time believing that, if beta- and eta-reduction alone were sufficient to express such powerful optimisations, it would have taken this long to discover that.

View on HN

Simple—it's not Turing complete. The whole premise is to eliminate recursive structure. Replacing them are measured folds and unfolds of data and codata respectively. These allow you to get as close to infinity as needed on both sides without going over (for some moderate syntactic and semantic penalties).

Within a language like the Calculus of Coinductive Constructions like Morte appears to implement it's not such a strange idea to have normalization.

So, no infinite loops means no Halting Problem means no completeness.

The upside is a larger set of easy-to-perform optimizations, much greater mathematical elegance. The downside is that you cannot directly write an interpreter for a complete language. Though you could write one which halts every N steps and requires user input to continue. In practice, that isn't the worst idea for a repl anyway.

How will be Morte used to do "real work"? Would it always have to be called from a larger language that can do effectful things like IO?

I have no idea what Gabriel is intending here; I'm just talking from general knowledge about consistent languages like the CIC.

There are a number of general examples, though.

1. You can leave termination guarantees in foreign code up to the programmer using an "unsafe" marker.

2. You can model effects using a monad

3. You can model the whole program as codata which is "driven" by the runtime

4. You can write a compiler of an embedded language in CIC and execute complete programs in, say, C

>Moreover, it promises to produce equal results for equivalent programs, which would allow a solution of the halting problem, wouldn't it?

I believe this is the case. So the article's promise (as I read it) can not hold true in the general case.

On a similar note, just write a program that runs the collatz conjecture and prints the result and a program that prints 1. Run them through Morte. If they compile to the same code, then boom, you've solved the Collatz conjecture :)

You can't encode the Collatz Conjecture (in that way) in Morte. It would require an infinite amount of computation and infinite loops have been disallowed. You would have to get a little bit more creative with the dependently typed parts of CIC and then finding a program which matches the needed type is as of today an unsolved task.

Equivalent in the sense he's talking about means "I can take any declaration a = b and replace a with b in the scope of that definition". This is substantially weaker than "if the two programs produce the same output", which would obviously violate Rice's Theorem.

Did the author claim Morte was Turing-complete? I don't think I saw that claim, but I'm a newcomer to all this computer science theory stuff. I think these Wikipedia links answer your question:

http://en.wikipedia.org/wiki/Calculus_of_constructions (What morte is based on)

and

http://en.wikipedia.org/wiki/Normalization_property_(abstrac...

answers the point on Turing completeness.

I had assumed that it must be Turing complete because otherwise its utility as an intermediate language seems dramatically reduced (despite its power, no one is compiling to Coq!); but, now that you point it out, I agree that there is no such claim. I originally thought that general recursion followed from folds and unfolds (http://lambda-the-ultimate.org/node/4290), but Ross Angle points out at http://lambda-the-ultimate.org/node/5045#comment-82340 that that's only when they are mixed, which is apparently not the case here.

I don't know how useful it will be in the end. The idea of targeting a powerful (proper) subset of turing completeness to produce fast executables makes a lot of sense to me, and furthermore for reasons that you have already brought up this is the only way it is possible if we truly desire a mechanized solution to this problem.

My concern on the practicality point is that the superoptimizer here really isn't "superoptimizing" so much as super-simplifying. There's a reason modern compilers don't aggressively inline every single function called if they have access to the source code, and for the same reasons they don't aggressively unroll every loop they come across if the loop bounds are known compile time.The tradeoffs of such optimizations are very complicated and hard to reason about because processors are very complicated and hard to reason about.

In a reddit discussion, the author indicates that, indeed, it is explicitly not Turing complete: http://www.reddit.com/r/haskell/comments/2g6wsx/haskell_for_....

I don't think this will allow solving the halting problem, its been mathematically proved to be impossible to solve [1].

Nothing prevents a turing complete program from entering an infinite loop. A GUI program for example is terminated only when the user decides to, which is impossible to predict.

1. http://en.wikipedia.org/wiki/Rice%27s_theorem

> I don't think this will allow solving the halting problem, its been mathematically proved to be impossible to solve [1].

Yes, this is my point: the proposed super-optimiser would, it seems to me, en passant be solving the halting problem, which means that it can't actually exist (or, at least, can't actually satisfy the stated guarantee).

> Nothing prevents a turing complete program from entering an infinite loop. A GUI program for example is terminated only when the user decides to, which is impossible to predict.

On the level of the lambda-calculus, this is reflected in the corresponding term's having no normal form, in which case the algorithm described (which relies on reducing everything to a normal form) cannot do anything with it.

The halting problem forbids the existence of oracles which can decide with certainty in some finite time that an arbitrary program will halt. Loosen any of these qualifiers and the problem is not necessarily undecidable. Loosening the "arbitrary program" restriction, the problem of analyzing the termination of a subset of programs which doesn't encode looping or recursion constructs ( i.e. simply typed lambda calculus ) is trivially decidable. A totality checker like in Agda can decide whether some programs halt given a set of restrictions on the program.

Reply on news.ycombinator.com