[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