Раменское, однако..

[anhinga_anhinga]

people say it really looks like this:
http://boooms.livejournal.com/30095.html

a large collection of these photos (traffic):
http://sturman.livejournal.com/271320.html?thread=1433560#t1433560

В середине 2000-х годов в Раменском был реализован проект по художественному оформлению группы типовых жилых домов, весьма необычный для России. В центре города было установлено много разнообразных скульптур, некоторые из них созданы по мотивам советских мультфильмов.

Comments

[http://users.livejournal.com/_rowan_tree_/]

You need to determine whether the compiler halts on a program.

[anhinga-anhinga.livejournal.com]

In order to do what? :-)

What's the complete statement you are trying to make? :-)

[cema.livejournal.com]

In order to fix the compiler, of course! ;-)

[anhinga-anhinga.livejournal.com]

In Standard ML the problem is decidable, it's just that the worst case is that the derived type is exponential in the length of the program (as a directed acyclic graph, and double exponential as linear output).

So one needs a bit less than Turing oracle to fix the compiler, at least for Standard ML ;-) Some other type systems are actually undecidable.

But at the same time, I am not sure that Turing oracle by itself can be used to reduce the complexity of the computation involved to make it fit a real computer -- I am just not familiar enough with the theory of computations with such oracles.. For example, if one uses such an oracle in a straightforward way, as applied to this problem, the oracle always says "yes" (a large enough computer will always complete type inference of a Standard ML program given enough time), and this does not help us to reduce the resources needed to figure out the outcome of the type inference process.

[anhinga-anhinga.livejournal.com]

Actually, it is possible to use the Turing oracle to determine whether the outcome of a program is a particular value: one just modifies the program to loop after any other outcome, and applies the oracle..

[http://users.livejournal.com/_rowan_tree_/]

Slowly from the beginning: in order to determine whether a program compiles correctly you need to determine whether the compiler halts on that program which is undecidable.

[anhinga-anhinga.livejournal.com]

OK :-)

So what I wrote in my answer to Cema, is that

1) It depends on the particular type system, for some of them (Standard ML) it is decidable, but the compiter does not terminate in any practically reasonable time/space, so it still "loops" in practice;

2) It is not clear whether one can covert a magic instant solver of the halting problem (a "Turing oracle") into a practical solver for the actual outcome of the type inference (since the termination can be of two types: "validated" and "error found").

***************************************

There is also the third type of possible eqiuvalence here, which is also not clear. The question is, given an oracle solving system F, can we obtain the solution of halting problem (without specific complexity constraints)? I don't know the answer to that either..

[anhinga-anhinga.livejournal.com]

I don't remember enough of the proof for system F to say whether halting problem reduces to it, although usually the proofs are made in such a fashion that it would, and then, in the third sense, we would have an equivalence..

BTW, if we know that type inference for a program in system F nonterminates, does this tell us anything about the program?

[anhinga-anhinga.livejournal.com]

> 2) It is not clear whether one can covert a magic instant solver of the halting problem (a "Turing oracle") into a practical solver for the actual outcome of the type inference (since the termination can be of two types: "validated" and "error found").

Actually, this is doable -- one just considers a modified program: which loops, if the original one gave the "error found" answer, or, alternatively, which loops, if the original one gave the "validated" answer, and apply the oracle to those.. Cool!