чуть-чуть об алгоритмах (англ.)
Sep. 2nd, 2014 01:39 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avva(может быть интересно читателям со склонностью к математике, компьютерам итп.)
Тьюринг доказал в 1936-м году, что невозможно решить проблему остановки: невозможно написать такую программу, которая сможет, получив на входе описание алгоритма, определить безошибочно, остановится этот алгоритм когда-нибудь, если его запустить, или нет. Эта задача принципиально неразрешима.
В одном обсуждении один из участников написал, что ему не нравится в доказательстве неразрешимости тот факт, что гипотетическая программа, которая может решить проблему остановки, запускает в некотором смысле "сама себя", и противоречие получается от того, что она не может решить проблему остановки для себя самой (или, точнее, немного расширенную версию себя самой). Ведь вообще-то нас интересуют реальные программы; если бы у нас была программа, умеющая решать проблему остановки, мы бы запускали ее на реальных программах, а не на "ней самой"; если бы она вдруг на себе самой не работала, это бы нам и не мешало. Т.е. доказательство верно, конечно, но остается ощущение, что это такая техническая победа, а не настоящая. В ответ я написал нижеследующий длинный комментарий по-английски, о природе алгоритмов и доказательствах неразрешимости проблем.
Algorithms are clever ways to pack up an infinity of data into a finite description.
Say there’s an infinite (here and below “infinite” means “countably infinite”; if you don’t know what that means, ignore this remark) binary string of zeroes and ones, some 010010101101111… Suppose I come up to you and I say: “I am the keeper of this infinite string of data. People come to me and ask: what is at the 13th place in this string, 0 or 1? How about 23523238th place? For any query they ask, I think for a while and then give them the correct answer. But I’ve been doing this for a long time and could use a vacation. Could you take over for me for a while? The job pays well.”
You might reply to me: “I will think about your offer seriously the moment I understand how you propose that I do it. How are you going to teach me your job? If the string were finite, you could just write it on a (possibly very long) piece of paper, and I could keep the piece of paper and consult it. But it’s infinite. No piece of paper will hold it. In fact, I wonder how *you* manage to answer people’s queries truthfully in the first place!”
But what if the string of data, though infinite, actually has some pretty simple and definite structure? Like maybe it’s all alternating 0101010101… to infinity, or maybe it’s the binary representation of the digits of pi. Then it’s easy for me to take over your job. You just write down the way for me to access any part of the string on demand – like “odd places are 0s, even places are 1s”, or “[formula for calculating pi to any desired accuracy]“. These descriptions are finite in length, so they *can* be written down and passed on. Armed with such a recipe, I can answer people’s queries, and you go on vacation. These clever recipes for packing up an infinite string of data in a finite description are algorithms.
There are many many more infinite strings of data than there are finite clever recipes for specifying one particular infinite string. This has to do with the fact that there are different orders of infinity, some larger than others, and the infinity of all the possible infinite strings of data is much much larger than the infinity of all the possible finite descriptions. So in fact, only a tiny minuscule incomprehensibly tiny minority of all infinite strings of data could ever be “teachable”, that is, specified by an algorithm. By any reasonable way of accounting just about all of them aren’t “teachable”. But we don’t know which are and which aren’t.
Say we have a problem. Here I need to be careful because there are many genuine problems (like, I dunno, “Is the Riemann hypothesis provable?”) that have a very short finite description (either “yes” or “no”), but we don’t know what it is. This isn’t the kind of problem I’m talking about. In the context of non-computability we’re talking about problems which have an infinite variety of inputs (“queries”), each of which needs its own separate output (“answer”). Like “given this number, what is the value of pi at this place?”. Or “given this description of an algorithm, does it ever halt?”. So, when we have such a problem, it’s usually a simple matter to represent it as an infinite binary string of 0s and 1s. For example, with binary digits of pi it already has this structure. For the problem "given an algorithm, does it ever halt?" we might use a simple way to enumerate all possible algorithms, and then our string will have 1 at the N-th place if the N-th algorithm halts, and 0 otherwise.
Anyway, whatever the problem is, translating it into "answer queries about this infinite binary string of data" is usually east. And the question then is, is this string one of the “teachable” ones, does there exist a finite clever description for it? Note: not “do we *have* a finite clever description for it?”, but “does there exist one?”. If we have an algorithm, that’s fine, we’re done. If we don’t have one, perhaps we will one day? Maybe our descendants will be much smarter than us and come up with one? Algorithms are clever descriptions, and the cleverness goes up and up and up unbounded. There’re certainly many clever algorithms that are much too complicated for our puny brains. Who’s to say that one of them doesn’t describe our problem?
Because cleverness of algorithms is seemingly unbounded, nobody’s been able to *prove* a particular problem “unteachable” by explicitly considering possible ways to describe it. How would such an attempt look like? Imagine a naive person who learned about pi, and they say: “Clearly it’s impossible to calculate more
than a few digits of pi. How would you even do it? You can draw a circle in the sand, measure its length and diameter, divide… but the accuracy is very limited. Maybe you could blow up a very very accurately round piece of glass, and use a piece of string to measure its diameter very precisely… maybe you’d get 1-2 more digits this way. But that’s it, you’ll never improve on these”. Then you teach them trigonometry, infinite series, and explain painstakingly that here’s a series that sums up to pi and all we need to do to get more digits is to keep calculating. “Oh… I didn’t know that was possible.” But of course, that person’s conviction before you showed them trig was only conviction, not *proof*. Nobody knows how to bar explicitly all unknown clever ways of finding out something, so nobody has been able to prove some infinite string “unteachable” this way.
The only way we have of proving that some infinite string is unteachable is to include information about all the possible algorithms inside the string. This is easier than it sounds, since there’s “only“ an infinity of possible algorithms, and the string is also infinite. So our only method to outsmart all the clever algorithms, including those too clever for our brains, is to say – oh, this problem is so smart that it already knows something about any one of you. This string of data has such a *rich structure* that no clever algorithm will ever describe it, because it knows something about *any* possible algorithm that it can use to defy its attempt to accurately describe it.
This is completely transparent with the Halting Problem, because basically that’s what it is – an infinite string that has “dirt“ on every possible algorithm. But all the other problems that have been proven non-computable are inevitably like this too, it’s just that their *rich structure* is not so obvious and we needed to work hard to uncover it. Maybe there’s a problem in group theory that merely looks hard, but then someone comes along and proves that it has such a rich structure that its infinite string of data actually contains dirt on all possible algorithms, just as the halting problem; you just need to understand how to dress up algorithms as groups in a particularly clever way, so that truths about algorithms become truths about groups that your string has dirt on. All the undecidability results (in this sense of non-computability) have been like this. There’s no other method of getting them.
But what this also means is that while the objection to the Halting Problem undecidability proof, that “P was forced to act on itself, even though it’s sort of a black box”, is understandable, it’s really unavoidable. If we want to *prove* that some infinite string of data is unteachable – not just “be really sure”, but *prove* – we’d better have an argument to applies to any possible finite description and shows that it can’t work. Because there’re descriptions far too clever for our brains, we can only hope to address every possible description by imagining that it exists as a “black box”. But then the only thing we know about it is that it (ostensibly) solves the problem, and at the same time the problem contains “dirt” on it, just as it does on any possible description. Out of these two pieces of information we have to conjure a contradiction; so applying the “black box” to something we construct with the help of the “dirt” on it is just about the only thing we can hope to do. Fortunately, it works.
Тьюринг доказал в 1936-м году, что невозможно решить проблему остановки: невозможно написать такую программу, которая сможет, получив на входе описание алгоритма, определить безошибочно, остановится этот алгоритм когда-нибудь, если его запустить, или нет. Эта задача принципиально неразрешима.
В одном обсуждении один из участников написал, что ему не нравится в доказательстве неразрешимости тот факт, что гипотетическая программа, которая может решить проблему остановки, запускает в некотором смысле "сама себя", и противоречие получается от того, что она не может решить проблему остановки для себя самой (или, точнее, немного расширенную версию себя самой). Ведь вообще-то нас интересуют реальные программы; если бы у нас была программа, умеющая решать проблему остановки, мы бы запускали ее на реальных программах, а не на "ней самой"; если бы она вдруг на себе самой не работала, это бы нам и не мешало. Т.е. доказательство верно, конечно, но остается ощущение, что это такая техническая победа, а не настоящая. В ответ я написал нижеследующий длинный комментарий по-английски, о природе алгоритмов и доказательствах неразрешимости проблем.
Algorithms are clever ways to pack up an infinity of data into a finite description.
Say there’s an infinite (here and below “infinite” means “countably infinite”; if you don’t know what that means, ignore this remark) binary string of zeroes and ones, some 010010101101111… Suppose I come up to you and I say: “I am the keeper of this infinite string of data. People come to me and ask: what is at the 13th place in this string, 0 or 1? How about 23523238th place? For any query they ask, I think for a while and then give them the correct answer. But I’ve been doing this for a long time and could use a vacation. Could you take over for me for a while? The job pays well.”
You might reply to me: “I will think about your offer seriously the moment I understand how you propose that I do it. How are you going to teach me your job? If the string were finite, you could just write it on a (possibly very long) piece of paper, and I could keep the piece of paper and consult it. But it’s infinite. No piece of paper will hold it. In fact, I wonder how *you* manage to answer people’s queries truthfully in the first place!”
But what if the string of data, though infinite, actually has some pretty simple and definite structure? Like maybe it’s all alternating 0101010101… to infinity, or maybe it’s the binary representation of the digits of pi. Then it’s easy for me to take over your job. You just write down the way for me to access any part of the string on demand – like “odd places are 0s, even places are 1s”, or “[formula for calculating pi to any desired accuracy]“. These descriptions are finite in length, so they *can* be written down and passed on. Armed with such a recipe, I can answer people’s queries, and you go on vacation. These clever recipes for packing up an infinite string of data in a finite description are algorithms.
There are many many more infinite strings of data than there are finite clever recipes for specifying one particular infinite string. This has to do with the fact that there are different orders of infinity, some larger than others, and the infinity of all the possible infinite strings of data is much much larger than the infinity of all the possible finite descriptions. So in fact, only a tiny minuscule incomprehensibly tiny minority of all infinite strings of data could ever be “teachable”, that is, specified by an algorithm. By any reasonable way of accounting just about all of them aren’t “teachable”. But we don’t know which are and which aren’t.
Say we have a problem. Here I need to be careful because there are many genuine problems (like, I dunno, “Is the Riemann hypothesis provable?”) that have a very short finite description (either “yes” or “no”), but we don’t know what it is. This isn’t the kind of problem I’m talking about. In the context of non-computability we’re talking about problems which have an infinite variety of inputs (“queries”), each of which needs its own separate output (“answer”). Like “given this number, what is the value of pi at this place?”. Or “given this description of an algorithm, does it ever halt?”. So, when we have such a problem, it’s usually a simple matter to represent it as an infinite binary string of 0s and 1s. For example, with binary digits of pi it already has this structure. For the problem "given an algorithm, does it ever halt?" we might use a simple way to enumerate all possible algorithms, and then our string will have 1 at the N-th place if the N-th algorithm halts, and 0 otherwise.
Anyway, whatever the problem is, translating it into "answer queries about this infinite binary string of data" is usually east. And the question then is, is this string one of the “teachable” ones, does there exist a finite clever description for it? Note: not “do we *have* a finite clever description for it?”, but “does there exist one?”. If we have an algorithm, that’s fine, we’re done. If we don’t have one, perhaps we will one day? Maybe our descendants will be much smarter than us and come up with one? Algorithms are clever descriptions, and the cleverness goes up and up and up unbounded. There’re certainly many clever algorithms that are much too complicated for our puny brains. Who’s to say that one of them doesn’t describe our problem?
Because cleverness of algorithms is seemingly unbounded, nobody’s been able to *prove* a particular problem “unteachable” by explicitly considering possible ways to describe it. How would such an attempt look like? Imagine a naive person who learned about pi, and they say: “Clearly it’s impossible to calculate more
than a few digits of pi. How would you even do it? You can draw a circle in the sand, measure its length and diameter, divide… but the accuracy is very limited. Maybe you could blow up a very very accurately round piece of glass, and use a piece of string to measure its diameter very precisely… maybe you’d get 1-2 more digits this way. But that’s it, you’ll never improve on these”. Then you teach them trigonometry, infinite series, and explain painstakingly that here’s a series that sums up to pi and all we need to do to get more digits is to keep calculating. “Oh… I didn’t know that was possible.” But of course, that person’s conviction before you showed them trig was only conviction, not *proof*. Nobody knows how to bar explicitly all unknown clever ways of finding out something, so nobody has been able to prove some infinite string “unteachable” this way.
The only way we have of proving that some infinite string is unteachable is to include information about all the possible algorithms inside the string. This is easier than it sounds, since there’s “only“ an infinity of possible algorithms, and the string is also infinite. So our only method to outsmart all the clever algorithms, including those too clever for our brains, is to say – oh, this problem is so smart that it already knows something about any one of you. This string of data has such a *rich structure* that no clever algorithm will ever describe it, because it knows something about *any* possible algorithm that it can use to defy its attempt to accurately describe it.
This is completely transparent with the Halting Problem, because basically that’s what it is – an infinite string that has “dirt“ on every possible algorithm. But all the other problems that have been proven non-computable are inevitably like this too, it’s just that their *rich structure* is not so obvious and we needed to work hard to uncover it. Maybe there’s a problem in group theory that merely looks hard, but then someone comes along and proves that it has such a rich structure that its infinite string of data actually contains dirt on all possible algorithms, just as the halting problem; you just need to understand how to dress up algorithms as groups in a particularly clever way, so that truths about algorithms become truths about groups that your string has dirt on. All the undecidability results (in this sense of non-computability) have been like this. There’s no other method of getting them.
But what this also means is that while the objection to the Halting Problem undecidability proof, that “P was forced to act on itself, even though it’s sort of a black box”, is understandable, it’s really unavoidable. If we want to *prove* that some infinite string of data is unteachable – not just “be really sure”, but *prove* – we’d better have an argument to applies to any possible finite description and shows that it can’t work. Because there’re descriptions far too clever for our brains, we can only hope to address every possible description by imagining that it exists as a “black box”. But then the only thing we know about it is that it (ostensibly) solves the problem, and at the same time the problem contains “dirt” on it, just as it does on any possible description. Out of these two pieces of information we have to conjure a contradiction; so applying the “black box” to something we construct with the help of the “dirt” on it is just about the only thing we can hope to do. Fortunately, it works.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2014-09-02 11:01 am (UTC)Обычно иллюстрируют на примере великой теоремы Ферма. Что если можно автоматом определять остановку программы - то значит можно автоматом доказать/опровергнуть великую теорему Ферма о ak + bk = ck
BigInteger n = 2; while (1) { for (BigInteger a = 1; a < n; ++a) { for (BigInteger b = 1; b < n; ++b) for (BigInteger c = 1; c < n; ++c) for (BigInteger k = 3; k < n; ++k) if (Pow(a, k) + Pow(b, k) == Pow(c, k)) { print(a, b, c, k); exit(0); } } n = n + 1; }no subject
Date: 2014-09-02 11:08 am (UTC)no subject
Date: 2014-09-02 11:41 am (UTC)no subject
Date: 2014-09-02 11:58 am (UTC)no subject
Date: 2014-09-02 11:29 am (UTC)Можно. Заставить программу распечатывать доказательство Уайлса, и дело с концом.
no subject
Date: 2014-09-02 11:55 am (UTC)no subject
Date: 2014-09-02 12:02 pm (UTC)Во-вторых, проверка доказательств - штука алгоритмически разрешимая.
no subject
Date: 2014-09-02 12:11 pm (UTC)Или так -- шахматную доску 8x8 нельзя с вырезанными a1 и h8 нельзя, как известно, замостить 31 доминошками. Доказательство состоит в раскрашивании доски в 2 цвета, окажется, что на доске осталось 32 черных и 30 белых, а каждая доминошка занимает один белый и один черный квадрат. Неужели столь красивое и необычное рассуждение можно проверить автоматически?
no subject
Date: 2014-09-02 12:18 pm (UTC)Конечно, если только они записаны полностью.
Доказательства традиционно пишутся обычным языком, с опусканием массы переходов, предполагаемых тривиальными. Разумеется, машина такое понять не может.
Если же доказательство записано абсолютно формально, с полным выписыванием всех тонкостей, то нет проблем. Берёте какую-нибудь Agda2 или Coq, и загоняете туда доказательство.
Собственно, возможность механической проверки доказательства лежит в основе доказательства теоремы Гёделя.
no subject
Date: 2014-09-02 12:29 pm (UTC)no subject
Date: 2014-09-02 12:32 pm (UTC)Не в программу, а в доказательство. Естественно, полностью записанное доказательство должно содержать определение того, что значит "раскрасить в несколько цветов". Которое достаточно тривиально: это просто отображение из множества клеток в множество цветов.
no subject
Date: 2014-09-02 12:24 pm (UTC)no subject
Date: 2014-09-02 03:19 pm (UTC)no subject
Date: 2014-09-02 03:51 pm (UTC)2) Может быть, программа P_N должна быть очень длинной, порядка 2^N (число всех программ длиной меньше N)? На самом деле длину P_N можно сделать порядка N + константа. Дело в том, что среди всех программ длиной меньше N существует программа Q_N, чье время работы конечно, но максимально среди всех таких программ. Т.е. если какая-то другая программа R длиной меньше N работает дольше, чем Q_N, то это означает, что R никогда не остановится. Используя это обстоятельство и зная исходный код Q_N, легко написать P_N.
no subject
Date: 2014-09-03 08:47 am (UTC)no subject
Date: 2014-09-03 10:57 am (UTC)Конечно, такое утверждение может быть недоказуемым в какой-то формальной теории. Например, теорема Гудстейна недоказуема в арифметике Пеано, но доказуема в системе Цермело-Френкеля. Но было бы странно, если бы существование ответа на проблему остановки для данной программы зависело от выбора формальной теории.
Или можно взглянуть на это с другой стороны. Для любой программы P, утверждение "P либо остановится, либо не остановится" доказуемо в арифметике Пеано :-)
тут некоторое недоразумение
Date: 2014-09-04 04:47 pm (UTC)no subject
Date: 2014-09-02 03:55 pm (UTC)no subject
Date: 2014-09-02 11:20 am (UTC)Вы знакомы с теорией тьюринговой сводимости и тьюринговых степеней? Последовательность, соответствующая проблеме остановки, имеет степень, которую часто обозначают 0'. Можно было бы попробовать доказать, что любая невычислимая последовательность (или невычислимое множество A, что то же самое) не менее сложна, чем проблема остановки, то есть что 0' сводится по Тьюрингу к A. Но известно, что это неверно.
no subject
Date: 2014-09-02 11:30 am (UTC)no subject
Date: 2014-09-02 12:22 pm (UTC)no subject
Date: 2014-09-02 03:34 pm (UTC)no subject
Date: 2014-09-02 04:04 pm (UTC)no subject
Date: 2014-09-02 04:11 pm (UTC)no subject
Date: 2014-09-02 04:29 pm (UTC)no subject
Date: 2014-09-02 03:57 pm (UTC)Они большие, сложные, но конечные автоматы. Бесконечной ленты в природе не существует.
Неразрешимость проблемы останова доказана исключительно для машин Тьюринга,
что несколько обесценивает ее применение в реальной жизни по любому возможному поводу.
(Это к вопросу о реальных программах)
no subject
Date: 2014-09-02 04:28 pm (UTC)— Мам, мы в саду сделали машину Тьюринга из бельевой верёвки.
— *выглядывает в окно кухни и видит много верёвок, которые туда-сюда возят простыни и рубашки* Это очень хорошо, дети, скажите только, а когда она остановится? Скоро нужно будет развесить новое бельё.
— *с невинным видом* Откуда бы нам знать?
no subject
Date: 2014-09-02 04:55 pm (UTC)no subject
Date: 2014-09-17 08:07 am (UTC)no subject
Date: 2014-09-17 10:27 pm (UTC)