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

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

Отпад! Да, это внушает надежду.

Офф-топ: а вот те AJAX ;-)

[anhinga-anhinga.livejournal.com]

> Отпад! Да, это внушает надежду.

Да, а вот народ вообще чудеса рассказывает..

> AJAX

Насколько это проблематично?

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

народ вообще - год Свиньи, не иначе! Вежливость и покой.

Насколько это - слуш, ну откуда я знаю? Я только сейчас увидела, еще внимательно не читала. Type inference в Джаве, например, циклится на некоторых дженериках. Народ пошумел и успокоился ;-)

[anhinga-anhinga.livejournal.com]

> Type inference в Джаве, например, циклится на некоторых дженериках

Ну циклится и циклится, какое кому дело.. В Standard ML тоже циклится -- это, кажется, принципиальный недостаток подобных полиморфных систем типов..

Попробую что-нибудь узнать про это..

[anhinga-anhinga.livejournal.com]

Циклится -- значит просто надо считать, что если программа слишком долго компилируется, значит она неправильная..

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

Poor man's definition of an incorrect problem. The complete definition is equivalent to the halting problem, ye know.

[anhinga-anhinga.livejournal.com]

"Эквивалентно" в каком смысле?

[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!

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

I mean, of an incorrect program :-)

[anhinga-anhinga.livejournal.com]

> Насколько это - слуш, ну откуда я знаю?

So, the consensus seems to be that if you have your Javascript on in your browser, this creates some potential for serious problems (although in practice we don't seem to observe those problems recently).

This is not AJAX-specific, AJAX does not change the picture, except that you do need to have your Javascript on to use AJAX-based Web sites..

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

Thanks!

I knew it - Javascript is evil! Javascript is a language that was developed with a very little discussion of any sort over a very short time, as I understand. The goal was to beat all the competitors and stick it into every browser before anyone else does (they also used "Java" in their name with no right whatsoever to do it). And there we have it!

For a quickly thrown together language it is actually amazingly reasonable, if one stops being annoyed at the idea that "types are difficult for users to understand, so we'll just sweep them under the rug".

IMHO, IMHO, of course....