Прекращение проверки вызова рекурсивной функции в 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 компилировать код? Есть ли ограничения на определение термина «Агда»?

Answer 1

Agda не предполагает ленивой оценки, такой как Haskell. Вместо этого 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's termination checker проверяет подмножество сильно нормализующих программ: те, которые имеют только структурную рекурсию. Он рассматривает количество и порядок конструкторов, сопоставленных шаблонам в определениях функций, для определения того, используют ли рекурсивные вызовы «меньшие» аргументы. a и b не имеют каких-либо параметров, поэтому проверка завершения проверки видит вложенный вызов от a до a (через b) как тот же «размер», что и сам a.