Исправление fmdw, (текущая версия) :
Анонiмус открыл для себя проблему останова?
Agda может определять только некоторые случаи, когда остановка точно произойдёт, для этого используются алгоритм, использованный в Foetus. Этот алгоритм очень ограничен, например такой случай он забракует (я уже крепко забыл её синтаксис, так что пусть будет haskell):
f :: Nat -> Nat
f x | x == 0 = 0
| even x = f $ x + 1
| True = f $ x - 2
Хотя очевидно, что эта ф-ция завершается, обо
f (f x) | x == 0 = 0
| even x = f (x + 1 - 2) -> f $ (x - 1)
| True = f $ x - 4
(Когда-то я проверял этот пример, вроде не вру)
Был ещё язык MiniAgda, использующий sized-типы (т.е. типы, параметризуемые максимальной глубиной терма). Критерием остановки в этом случае будет просто уменьшающийся размер терма. Вроде сейчас их запилили и в Agda.
Но вообще, я не понимаю, что мешало набрать в поисковике «agda termination checker» и прочитать всё там, не прибегая к помощи лорчан с дырявой памятью.
Исходная версия fmdw, :
Анонiмус открыл для себя проблему останова?
Agda может определять только некоторые случаи, когда остановка точно произойдёт, для этого используются алгоритм, использованный в Foetus. Этот алгоритм очень ограничен, например такой случай он забракует (я уже крепко забыл её синтаксис, так что пусть будет haskell):
f :: Nat -> Nat
f x | x == 0 = 0
| even x = f $ x + 1
| True = f $ x - 2
Хотя очевидно, что эта ф-ция завершается, обо
f (f x) | x == 0 = 0
| even x = f (x + 1 - 2) -> f $ (x - 1)
| True = f $ x - 4
(Когда-то я проверял этот пример, вроде не вру)
Был ещё язык MiniAgda, использующий sized-типы (т.е. типы, параметризуемые максимальной глубиной терма). Критерием остановки в этом случае будет просто уменьшающийся размер терма. Вроде сейчас их запилили и в Agda.