# [Agda] strange Termination problem

mechvel at scico.botik.ru mechvel at scico.botik.ru
Tue Feb 8 14:51:55 CET 2022

```Please, why does  Agda 2.6.2.1  reports "Termination checking failed"
for the following program?
(not a full code)

------------------------------------------------------
foo :  ∀ {e lev} → e ReducesLevel lev →
sizeHead (reduceLevel e lev) <nn (lSize lev)

foo {e} {d , ps} (d≢0 , any-e-reduces-ps) =
aux d ps d≢0 any-e-reduces-ps
where
aux : (d : ℕ) (ps : Patterns) → d ≢ 0 →
let lev = (d , ps)
in
Any (e Reduces_) ps →
sizeHead (reduceLevel e lev) <nn (lSize lev)

aux 0       _             _     _                  =  anything
aux _       _             _     (there _)          =  anything
aux (suc d) (p ∷ [])      _     (here e-reduces-p) =  anything
aux (suc d) (p ∷ p' ∷ ps) 1+d≢0 (here e-reduces-p) =

aux' (e reduces? p) (any? (e reduces?_) (p' ∷ ps))  -- line 1669
where
1+d = suc d

lev tail : DimLevel
lev  = (1+d , p ∷ p' ∷ ps)
tail = (1+d , p' ∷ ps)

|pp'ps|          = length (p ∷ p' ∷ ps)
redexes          = reduceLevel e lev
tail-redexes     = reduceLevel e tail
sh[tail-redexes] = sizeHead tail-redexes
d₂    = proj₁ sh[tail-redexes]
|ps₂| = proj₂ sh[tail-redexes]

aux' :  Dec (e Reduces p) → Dec (Any (e Reduces_) (p' ∷ ps)) →
sizeHead (reduceLevel e lev) <nn (1+d , |pp'ps|)

aux' (no ¬reduces-p) _  = contradiction e-reduces-p ¬reduces-p
aux' (yes reduces-p) (no ¬e-reduces-any-p'ps) =  anything
aux' (yes reduces-p) (yes e-reduces-any-p'ps) =

aux'' (d₂ <? 1+d) (aux 1+d (p' ∷ ps) 1+d≢0 e-reduces-any-p'ps)  --
line 1691
where
aux'' : Dec (d₂ < 1+d) → sh[tail-redexes] <nn (lSize tail) →
sizeHead redexes <nn (1+d , |pp'ps|)
aux'' _ _ = anything
------------------------------------------------------

It reports
-----------------------------
Termination checking failed for the following functions:
Problematic calls:
aux' (e reduces? p) (any? (_reduces?_ e) (p' ∷ ps))
(at  1669,29-33)

aux (1+d d p p' ps 1+d≢0 e-reduces-p) (p' ∷ ps) 1+d≢0
e-reduces-any-p'ps
(at  1691,34-37)
-----------------------------

The only recursive call is for  aux.
The head call is
aux (suc d) (p ∷ p' ∷ ps) 1+d≢0 (here e-reduces-p).

It calls for
aux' (e reduces? p) (any? (e reduces?_) (p' ∷ ps)).

And this latter calls for
aux'' (d₂ <? 1+d) (aux 1+d (p' ∷ ps) 1+d≢0 e-reduces-any-p'ps)

The latter call for  aux  has  (p' ∷ ps)
among arguments,
while the head call of  aux  had  (p ∷ p' ∷ ps)
for this argument.

{-# OPTIONS --termination-depth=3 #-}  does not help.

Can you, please, give a hint:
why structural recursion does not work here?

Also the report prints  "aux (1+d d p p' ps 1+d≢0 e-reduces-p) ..."
instead of
"aux (1+d (p' ∷ ps) 1+d≢0 e-reduces-p) ...".

It is misleading, because  aux  has four arguments,
while the report prints six arguments.

?

------
Sergei
```

More information about the Agda mailing list