Программы не принадлежат к отдельному узкому классу.
Проблему останова действительно нельзя решить (по крайней мере на устройстве "одного ранга" что ли.. про гипотетические устройства более других "рангов" можно глянуть википедию).
Однако её нельзя решить в общем случае. Для каждого конкретного частного случая её можно попытаться решить. Построенное решение (если удалось его построить, конечно) и есть доказательство завершаемости алгоритма. Те математики которые анализируют алгоритмы, время от времени развлекаются решением проблемы останова (каждый раз в частном случае разумеется). Этим же занимаются и инженеры по формальной верификации.
Чуть более подробно, ситуация такая: для части случаев Coq (и другие подобные системы) может автоматически решать проблему останова. Конкретно Coq определяет что рекурсивный вызов рассматриваемой функции происходит на структурно меньшем аргументе. И если это так, то это значит что алгоритм завершится (поскольку так определяются индуктивные типы в Coq). Но это работает только для примитивно-рекурсивных функций. В общем случае приходится формулировать и доказывать утверждения о завершаемости руками.
Один из подходов к доказательству завершаемости общерекурсивных функций средствами Coq описан у автора в одной из публикаций.
Доказать отсутствие вполне можно. Например, ознакомившись со школьным курсом геометрии, в общем-то по моему вполне можно доказать что нет треугольников с суммой углов больше 180 градусов.
Ну и да, вполне можно доказывать отсутствие ошибок в программах, чем инженеры по формальной верификации и занимаются :).
Унифицирует :) . Можно и в режиме написания кода
eq_symиспользовать в подобном случае (там дальше примеры есть в статье).Я, пожалуй, дополню ответы выше.
Программы не принадлежат к отдельному узкому классу.
Проблему останова действительно нельзя решить (по крайней мере на устройстве "одного ранга" что ли.. про гипотетические устройства более других "рангов" можно глянуть википедию).
Однако её нельзя решить в общем случае. Для каждого конкретного частного случая её можно попытаться решить. Построенное решение (если удалось его построить, конечно) и есть доказательство завершаемости алгоритма. Те математики которые анализируют алгоритмы, время от времени развлекаются решением проблемы останова (каждый раз в частном случае разумеется). Этим же занимаются и инженеры по формальной верификации.
Чуть более подробно, ситуация такая: для части случаев Coq (и другие подобные системы) может автоматически решать проблему останова. Конкретно Coq определяет что рекурсивный вызов рассматриваемой функции происходит на структурно меньшем аргументе. И если это так, то это значит что алгоритм завершится (поскольку так определяются индуктивные типы в Coq). Но это работает только для примитивно-рекурсивных функций. В общем случае приходится формулировать и доказывать утверждения о завершаемости руками.
Один из подходов к доказательству завершаемости общерекурсивных функций средствами Coq описан у автора в одной из публикаций.
Доказать отсутствие вполне можно. Например, ознакомившись со школьным курсом геометрии, в общем-то по моему вполне можно доказать что нет треугольников с суммой углов больше 180 градусов.
Ну и да, вполне можно доказывать отсутствие ошибок в программах, чем инженеры по формальной верификации и занимаются :).