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

[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_/]

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!