<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>