<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.25in 1.0in 1.25in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">Is Patterns nonempty list? If so, that’s the reason. Two <span style="font-family:"Cambria Math",serif">
∷ are different constructors.</span></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason Hu<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a><br>
<b>Sent: </b>Tuesday, February 8, 2022 8:51 AM<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>
<b>Subject: </b>[Agda] strange Termination problem</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Please, why does Agda 2.6.2.1 reports "Termination checking failed"<br>
for the following program?<br>
(not a full code)<br>
<br>
------------------------------------------------------<br>
foo : <span style="font-family:"Cambria Math",serif">∀</span> {e lev} → e ReducesLevel lev →<br>
sizeHead (reduceLevel e lev) <nn (lSize lev)<br>
<br>
foo {e} {d , ps} (d<span style="font-family:"Cambria Math",serif">≢</span>0 , any-e-reduces-ps) =<br>
aux d ps d<span style="font-family:"Cambria Math",serif">≢</span>0 any-e-reduces-ps<br>
where<br>
aux : (d : <span style="font-family:"Cambria Math",serif">ℕ</span>) (ps : Patterns) → d
<span style="font-family:"Cambria Math",serif">≢</span> 0 →<br>
let lev = (d , ps)<br>
in<br>
Any (e Reduces_) ps →<br>
sizeHead (reduceLevel e lev) <nn (lSize lev)<br>
<br>
aux 0 _ _ _ = anything<br>
aux _ _ _ (there _) = anything<br>
aux (suc d) (p <span style="font-family:"Cambria Math",serif">∷</span> []) _ (here e-reduces-p) = anything<br>
aux (suc d) (p <span style="font-family:"Cambria Math",serif">∷</span> p' <span style="font-family:"Cambria Math",serif">
∷</span> ps) 1+d<span style="font-family:"Cambria Math",serif">≢</span>0 (here e-reduces-p) =<br>
<br>
aux' (e reduces? p) (any? (e reduces?_) (p' <span style="font-family:"Cambria Math",serif">
∷</span> ps)) -- line 1669<br>
where<br>
1+d = suc d<br>
<br>
lev tail : DimLevel<br>
lev = (1+d , p <span style="font-family:"Cambria Math",serif">∷</span> p' <span style="font-family:"Cambria Math",serif">
∷</span> ps)<br>
tail = (1+d , p' <span style="font-family:"Cambria Math",serif">∷</span> ps)<br>
<br>
|pp'ps| = length (p <span style="font-family:"Cambria Math",serif">
∷</span> p' <span style="font-family:"Cambria Math",serif">∷</span> ps)<br>
redexes = reduceLevel e lev<br>
tail-redexes = reduceLevel e tail<br>
sh[tail-redexes] = sizeHead tail-redexes<br>
d₂ = proj₁ sh[tail-redexes]<br>
|ps₂| = proj₂ sh[tail-redexes]<br>
<br>
aux' : Dec (e Reduces p) → Dec (Any (e Reduces_) (p' <span style="font-family:"Cambria Math",serif">
∷</span> ps)) →<br>
sizeHead (reduceLevel e lev) <nn (1+d , |pp'ps|)<br>
<br>
aux' (no ¬reduces-p) _ = contradiction e-reduces-p ¬reduces-p<br>
aux' (yes reduces-p) (no ¬e-reduces-any-p'ps) = anything<br>
aux' (yes reduces-p) (yes e-reduces-any-p'ps) =<br>
<br>
aux'' (d₂ <? 1+d) (aux 1+d (p' <span style="font-family:"Cambria Math",serif">
∷</span> ps) 1+d<span style="font-family:"Cambria Math",serif">≢</span>0 e-reduces-any-p'ps) --
<br>
line 1691<br>
where<br>
aux'' : Dec (d₂ < 1+d) → sh[tail-redexes] <nn (lSize tail) →<br>
sizeHead redexes <nn (1+d , |pp'ps|)<br>
aux'' _ _ = anything<br>
------------------------------------------------------<br>
<br>
<br>
It reports<br>
-----------------------------<br>
Termination checking failed for the following functions:<br>
Problematic calls:<br>
aux' (e reduces? p) (any? (_reduces?_ e) (p' <span style="font-family:"Cambria Math",serif">
∷</span> ps))<br>
(at 1669,29-33)<br>
<br>
aux (1+d d p p' ps 1+d<span style="font-family:"Cambria Math",serif">≢</span>0 e-reduces-p) (p'
<span style="font-family:"Cambria Math",serif">∷</span> ps) 1+d<span style="font-family:"Cambria Math",serif">≢</span>0
<br>
e-reduces-any-p'ps<br>
(at 1691,34-37)<br>
-----------------------------<br>
<br>
The only recursive call is for aux.<br>
The head call is<br>
aux (suc d) (p <span style="font-family:"Cambria Math",serif">∷</span> p' <span style="font-family:"Cambria Math",serif">
∷</span> ps) 1+d<span style="font-family:"Cambria Math",serif">≢</span>0 (here e-reduces-p).<br>
<br>
It calls for<br>
aux' (e reduces? p) (any? (e reduces?_) (p' <span style="font-family:"Cambria Math",serif">
∷</span> ps)).<br>
<br>
And this latter calls for<br>
aux'' (d₂ <? 1+d) (aux 1+d (p' <span style="font-family:"Cambria Math",serif">
∷</span> ps) 1+d<span style="font-family:"Cambria Math",serif">≢</span>0 e-reduces-any-p'ps)<br>
<br>
The latter call for aux has (p' <span style="font-family:"Cambria Math",serif">
∷</span> ps)<br>
among arguments,<br>
while the head call of aux had (p <span style="font-family:"Cambria Math",serif">
∷</span> p' <span style="font-family:"Cambria Math",serif">∷</span> ps)<br>
for this argument.<br>
<br>
{-# OPTIONS --termination-depth=3 #-} does not help.<br>
<br>
Can you, please, give a hint:<br>
why structural recursion does not work here?<br>
<br>
<br>
Also the report prints "aux (1+d d p p' ps 1+d<span style="font-family:"Cambria Math",serif">≢</span>0 e-reduces-p) ..."<br>
instead of<br>
"aux (1+d (p' <span style="font-family:"Cambria Math",serif">∷</span> ps) 1+d<span style="font-family:"Cambria Math",serif">≢</span>0 e-reduces-p) ...".<br>
<br>
It is misleading, because aux has four arguments,<br>
while the report prints six arguments.<br>
<br>
?<br>
<br>
------<br>
Sergei<br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>