Termination check of a recursive function call in agda

Question

The following code is perfectly ok in Haskell:

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

Similiar code in Agda wouldn't compile (termination check fails):

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)

The definition of a uses a which is not structurally smaller, hence the loop. It seems that the termination checker wouldn't look inside the definition of dh.

I've tried using coinduction, setting option --termination-depth=4 -- doesn't help. Inserting {-# NO_TERMINATION_CHECK #-} within the mutual block helps but it looks like a cheat.

Is there a clean way to make Agda compile the code? Does Agda's termination checker have some fundamental limitations?

Answer 1

Agda doesn't assume lazy evaluation like Haskell does. Instead, Agda requires that all expressions be strongly normalizing. That means you should get the same answer regardless of the order in which you evaluate subexpressions. The definitions you give are not strongly normalizing, because there is an evaluation order that don't terminate:

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

In particular, Agda's JavaScript backend would generate code that doesn't terminate for a and b, because JavaScript is strictly evaluated.

Agda's termination checker checks for a subset of strongly normalizing programs: those that have only structural recursion. It looks at the number and order of constructors pattern-matched in function definitions to determine whether recursive calls use "smaller" arguments. a and b don't have any parameters, so the termination checker sees the nested call from a to a (via b) as being the same "size" as a itself.