Завершаемость определить проще. Для функциональных языков, где единственный источник незавершаемости - это рекурсия, это делается так.
1) Для всех аргументов определена мера. Для числовых аргументов - это обычно просто значение числа. Для строковых - это может быть длина строки или ещё что-то. Для алгебраических типов данных - это обычно количество конструкторов в выражении. Например для "Cons 4 (Cons 2 Nil)" размер может быть равен 3. Аналогично вычисляется размер деревьев (количество узлов) и т.п.
Для таких простых типов мера обычно определяется автоматически. Для более сложных её приходится определять вручную. Например, мне
здесь пришлось определить такую меру:
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
primrec size_type :: "'a type => nat" where
"size_type OclSuper = 0"
| "size_type (Required t) = 0"
| "size_type (Optional t) = 0"
| "size_type (Collection t) = Suc (size_type t)"
| "size_type (Set t) = Suc (size_type t)"
| "size_type (OrderedSet t) = Suc (size_type t)"
| "size_type (Bag t) = Suc (size_type t)"
| "size_type (Sequence t) = Suc (size_type t)"
| "size_type (Tuple t) = Suc (ffold tcf 0 (fset_of_fmap (fmmap size_type t)))"
2) По умолчанию тот же Isabelle HOL пытается найти аргумент или комбинацию аргументов функции, которые с каждым шагом рекурсии уменьшаются. Обычно этого достаточно.
3) Если автоматически не доказывается, то приходится вручную определять меру (которая уменьшается с каждым шагом) и доказывать, что она действительно уменьшается. Например,
здесь я доказывал это так (сама функция и теоремы есть по ссылке):
1.
2.
3.
termination
by (relation "measure (λ(xs, ys). size ys)";
auto simp add: elem_le_ffold' fmran'I)
А
здесь (раздел 4.1) есть хороший пример почему автоматическое доказательство завершаемости может не работать:
1.
2.
function sum :: "nat => nat => nat" where
"sum i N = (if i > N then 0 else i + sum (Suc i) N)"
Эта функция вычисляет сумму 1+2+...+N
Аргумент i с каждым шагом увеличивается на 1, а аргумент N остается неизменным. Поэтому они определяют меру N - i, которая с каждым шагом уменьшается. И ещё добавляют 1, видимо потому, что на последнем вызове рекурсии i > N. При этом N - i будет всё-равно 0, потому что это натуральные числа, а не целые. И если не добавить 1, то на двух последних шагах мера будет 0 - оставаться неизменной, а должна уменьшаться.
1.
2.
3.
4.
termination sum
apply (relation "measure (λ(i,N). N + 1 - i)")
apply auto
done
Для императивных языков доказательство завершаемости должно быть сложнее, потому что там есть переменные, значения которых могут изменяться не только при рекурсивных вызовах, но просто по ходу выполнения алгоритма. Но общая идея там должна быть такая же:
1) Определяем источники незавершаемости. Тут кроме рекурсивных вызовов это могут быть циклы и функции из стандартной библиотеки! Кстати
функции из стандартной библиотеки могут ещё и влиять на сложность алгоритма: поиск в массиве, в хеше и т.п.
2) Определяем простые правила для определения завершаемости (например, один из аргументов или их комбинация всегда уменьшаются или, например, переменная цикла только уменьшается/увеличивается пока не доходит до конечного значения).
3) Для сложных ситуаций всё-равно пользователю придется определять кастомную меру. Кстати, эта мера может быть обязательной частью алгоритма. Чел, который написал алгоритм, пусть прикладывает и меру.
4) Самая жесть - это интегрировать всё это с какой-нибудь системой автоматического доказательства теорем. Обычно это сводится к тому, что нужно реализовать этот язык программирования (на котором пишутся алгоритмы) в Isabelle HOL или ещё какой-то системе. Для Isabelle HOL есть какая-то реализация Java, какие-то примеры простых абстрактных императивных языков. Я, например,
реализовывал язык OCL . Причём, там только абстрактный синтаксис, система типов, правила типизации выражений, без семантики. Для того же C# или другого языка нужно либо искать готовую реализацию, либо это тема для докторской диссертации на несколько лет.
Короче, сделать всё полностью формально очень сложно. Если это требуется, то проще всего, чтобы люди, которые пишут алгоритмы, писали их сразу на нормальном языке типа Isabelle HOL, который поддерживает автоматизированные доказательства теорем. При этом сами и доказывали бы завершаемость, сложность и т.п. Либо можно использовать языки, которые легко интегрируются с такими системами. Для Scala вроде было что-то такое.
Если формальное доказательство не нужно. А просто запускать алгоритм много раз - это слишком тупо. То нужны какие-то эвристики. Например, парсим функцию, получаем её абстрактное синтаксическое дерево (во многих языках это поддерживается). И анализируем циклы, рекурсивные вызовы и т.п. Затем подтверждаем полученную оценку запуском алгоритма на разных входных данных. С практической точки зрения это самое простое и реальное, что можно сделать. На мой взгляд такая штука была бы очень прикольной и востребованной. Например, есть PVS Studio, которая не может формально доказать корректность программы, но в ней заложено много эвристик, которые находят типовые ошибки. С практической точки зрения это уже не плохо. Аналогично и ваша штука могла бы примерно оценивать сложность алгоритмов.
