Проверка завершения рекурсивного вызова функции в agda

Question

Следующий код отлично подходит для Haskell:

dh :: Int -> Int -> (Int, Int)
dh d q = (2^d, q^d)
a = dh 2 (fst b)
b = dh 3 (fst a)

Подобный код в Agda не будет компилироваться (проверка завершения не пройдена):

infixl 9 _^_
_^_ : ℕ → ℕ → ℕ
x ^ zero = 1
x ^ suc n = x * (x ^ n)

dh : ℕ -> ℕ -> ℕ × ℕ
dh d q = 2 ^ d , q ^ d

mutual
  a = dh 2 (proj₁ b)
  b = dh 3 (proj₁ a)

Определение a использования a который структурно не меньше, следовательно, петля. Кажется, что проверка завершения не заглянет внутрь определения dh,

Я пытался использовать Coinduction, параметр настройки --termination-depth=4 - не помогает Вставка {-# NO_TERMINATION_CHECK #-} в пределах mutual Блок помогает, но это похоже на чит.

Есть ли чистый способ заставить Agda компилировать код? Есть ли у проверки завершения Agda некоторые фундаментальные ограничения?

Answer 1

Агда не принимает ленивых оценок, как Хаскелл. Вместо этого Agda требует, чтобы все выражения были строго нормализованы. Это означает, что вы должны получить один и тот же ответ независимо от порядка, в котором вы оцениваете подвыражения. Определения, которые вы даете, не сильно нормализуются, потому что есть порядок оценки, который не заканчивается:

a
-->
dh 2 (proj₁ b)
-->
dh 2 (proj₁ (dh 3 (proj₁ a))
-->
dh 2 (proj₁ (dh 3 (proj₁ (dh 2 (proj₁ b)))))

В частности, JavaScript-код Agda будет генерировать код, который не завершается для a а также bпотому что JavaScript строго оценен.

Средство проверки завершения Agda проверяет подмножество сильно нормализующихся программ: тех, которые имеют только структурную рекурсию. Он определяет количество и порядок сопоставления шаблонов в определениях функций, чтобы определить, используют ли рекурсивные вызовы "меньшие" аргументы. a а также b не имеет никаких параметров, поэтому проверка завершения видит вложенный вызов из a в a (с помощью b) так же, как "размер" a сам.