<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
I now have a concrete program illustrating the issue: <a href="https://github.com/agda/agda/issues/5646" id="LPlnkOWALinkPreview">
https://github.com/agda/agda/issues/5646</a><br>
</div>
<div class="_Entity _EType_OWALinkPreview _EId_OWALinkPreview _EReadonly_1">
<div id="LPBorder_GTaHR0cHM6Ly9naXRodWIuY29tL2FnZGEvYWdkYS9pc3N1ZXMvNTY0Ng.." class="LPBorder351244" style="width: 100%; margin-top: 16px; margin-bottom: 16px; position: relative; max-width: 800px; min-width: 424px;">
<table id="LPContainer351244" role="presentation" style="padding: 12px 36px 12px 12px; width: 100%; border-width: 1px; border-style: solid; border-color: rgb(200, 200, 200); border-radius: 2px;">
<tbody>
<tr style="border-spacing: 0px;" valign="top">
<td>
<div id="LPImageContainer351244" style="position: relative; margin-right: 12px; height: 120px; overflow: hidden; width: 240px;">
<a target="_blank" id="LPImageAnchor351244" href="https://github.com/agda/agda/issues/5646"><img id="LPThumbnailImageId351244" alt="" style="display: block;" width="240" height="120" src="https://opengraph.githubassets.com/c20a4be1cb39340e55f4c7a4df0e371714690cf798325b6b8c494b381deaa1d9/agda/agda/issues/5646"></a></div>
</td>
<td style="width: 100%;">
<div id="LPTitle351244" style="font-size: 21px; font-weight: 300; margin-right: 8px; font-family: "wf_segoe-ui_light", "Segoe UI Light", "Segoe WP Light", "Segoe UI", "Segoe WP", Tahoma, Arial, sans-serif; margin-bottom: 12px;">
<a target="_blank" id="LPUrlAnchor351244" href="https://github.com/agda/agda/issues/5646" style="text-decoration: none; color: var(--themePrimary);">Termination checker rejects mutual functions on induction-recursion definition · Issue #5646 · agda/agda</a></div>
<div id="LPDescription351244" style="font-size: 14px; max-height: 100px; color: rgb(102, 102, 102); font-family: "wf_segoe-ui_normal", "Segoe UI", "Segoe WP", Tahoma, Arial, sans-serif; margin-bottom: 12px; margin-right: 8px; overflow: hidden;">
I am running agda 2.6.2 and here is an example: {-# OPTIONS --without-K --safe #-} open import Data.Nat data Exp : Set where mutual Env : Set Env = ℕ → D data D : Set where Π : D → (t : Exp) → (ρ :...</div>
<div id="LPMetadata351244" style="font-size: 14px; font-weight: 400; color: rgb(166, 166, 166); font-family: "wf_segoe-ui_normal", "Segoe UI", "Segoe WP", Tahoma, Arial, sans-serif;">
github.com</div>
</td>
</tr>
</tbody>
</table>
</div>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
Any help with me understanding the termination checking strategy will be appreciated.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<span style="font-family: "Courier New", monospace;">{-# OPTIONS --without-K --safe #-}</span>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">open import Data.Nat</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">data Exp : Set where</span></div>
<div><br>
</div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">mutual</span></div>
<div><span style="font-family: "Courier New", monospace;"> Env : Set</span></div>
<div><span style="font-family: "Courier New", monospace;"> Env = ℕ → D</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> data D : Set where</span></div>
<div><span style="font-family: "Courier New", monospace;"> Π : D → (t : Exp) → (ρ : Env) → D</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">variable</span></div>
<div><span style="font-family: "Courier New", monospace;"> T T′ : Exp</span></div>
<div><span style="font-family: "Courier New", monospace;"> A A′ : D</span></div>
<div><span style="font-family: "Courier New", monospace;"> B B′ : D</span></div>
<div><span style="font-family: "Courier New", monospace;"> a a′ : D</span></div>
<div><span style="font-family: "Courier New", monospace;"> b b′ : D</span></div>
<div><span style="font-family: "Courier New", monospace;"> ρ ρ′ : Env</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">_↦_ : Env → D → Env</span></div>
<div><span style="font-family: "Courier New", monospace;">(ρ ↦ d) zero = d</span></div>
<div><span style="font-family: "Courier New", monospace;">(ρ ↦ d) (suc x) = ρ x</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">data ⟦_⟧_↘_ : Exp → Env → D → Set where</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">data _∙_↘_ : D → D → D → Set where</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">record ΠRT T ρ T′ ρ′ (R : D → D → Set) : Set where</span></div>
<div><span style="font-family: "Courier New", monospace;"> field</span></div>
<div><span style="font-family: "Courier New", monospace;"> ⟦T⟧ : D</span></div>
<div><span style="font-family: "Courier New", monospace;"> ⟦T′⟧ : D</span></div>
<div><span style="font-family: "Courier New", monospace;"> ↘⟦T⟧ : ⟦ T ⟧ ρ ↘ ⟦T⟧</span></div>
<div><span style="font-family: "Courier New", monospace;"> ↘⟦T′⟧ : ⟦ T′ ⟧ ρ′ ↘ ⟦T′⟧</span></div>
<div><span style="font-family: "Courier New", monospace;"> T≈T′ : R ⟦T⟧ ⟦T′⟧</span></div>
<div><br>
</div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">record Π̂ (f a f′ a′ : D) (R : D → D → Set) : Set where</span></div>
<div><span style="font-family: "Courier New", monospace;"> field</span></div>
<div><span style="font-family: "Courier New", monospace;"> fa : D</span></div>
<div><span style="font-family: "Courier New", monospace;"> fa′ : D</span></div>
<div><span style="font-family: "Courier New", monospace;"> ↘fa : f ∙ a ↘ fa</span></div>
<div><span style="font-family: "Courier New", monospace;"> ↘fa′ : f′ ∙ a′ ↘ fa′</span></div>
<div><span style="font-family: "Courier New", monospace;"> fa≈fa′ : R fa fa′</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">mutual</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> data 𝕌 : D → D → Set where</span></div>
<div><span style="font-family: "Courier New", monospace;"> Π : (A≈A′ : 𝕌 A A′) →</span></div>
<div><span style="font-family: "Courier New", monospace;"> (∀ {a a′} →</span></div>
<div><span style="font-family: "Courier New", monospace;"> El A≈A′ a a′ →</span></div>
<div><span style="font-family: "Courier New", monospace;"> ΠRT T (ρ ↦ a) T′ (ρ′ ↦ a′) 𝕌) →</span></div>
<div><span style="font-family: "Courier New", monospace;"> -------------------------</span></div>
<div><span style="font-family: "Courier New", monospace;"> 𝕌 (Π A T ρ) (Π A′ T′ ρ′)</span></div>
<div><br>
</div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> El : 𝕌 A B → D → D → Set</span></div>
<div><span style="font-family: "Courier New", monospace;"> El (Π A≈A′ RT) = λ f f′ → ∀ {a b} (inp : El A≈A′ a b) → Π̂ f a f′ b (El (ΠRT.T≈T′ (RT inp)))</span></div>
<div><br>
</div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">mutual</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> 𝕌-sym : 𝕌 A B → 𝕌 B A</span></div>
<div><span style="font-family: "Courier New", monospace;"> 𝕌-sym (Π {_} {_} {T} {ρ} {T′} {ρ′} A≈A′ RT) = Π (𝕌-sym A≈A′) helper</span></div>
<div><span style="font-family: "Courier New", monospace;"> where helper : El (𝕌-sym A≈A′) a a′ → ΠRT T′ (ρ′ ↦ a) T (ρ ↦ a′) 𝕌</span></div>
<div><span style="font-family: "Courier New", monospace;"> helper a≈a′ = record</span></div>
<div><span style="font-family: "Courier New", monospace;"> { ⟦T⟧ = ⟦T′⟧</span></div>
<div><span style="font-family: "Courier New", monospace;"> ; ⟦T′⟧ = ⟦T⟧</span></div>
<div><span style="font-family: "Courier New", monospace;"> ; ↘⟦T⟧ = ↘⟦T′⟧</span></div>
<div><span style="font-family: "Courier New", monospace;"> ; ↘⟦T′⟧ = ↘⟦T⟧</span></div>
<div><span style="font-family: "Courier New", monospace;"> ; T≈T′ = 𝕌-sym T≈T′</span></div>
<div><span style="font-family: "Courier New", monospace;"> }</span></div>
<div><span style="font-family: "Courier New", monospace;"> where open ΠRT (RT (El-sym (𝕌-sym A≈A′) A≈A′ a≈a′))</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> El-sym : ∀ (A≈B : 𝕌 A B) (B≈A : 𝕌 B A) → El A≈B a b → El B≈A b a</span></div>
<div><span style="font-family: "Courier New", monospace;"> El-sym (Π A≈B RT) (Π B≈A RT′) f≈f′ a≈a′</span></div>
<div><span style="font-family: "Courier New", monospace;"> with 𝕌-sym A≈B</span></div>
<span style="font-family: "Courier New", monospace;"> ... | x = {!!}</span><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div>
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color: rgb(69, 129, 142);"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>
</div>
</div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Jason Hu<br>
<b>Sent:</b> November 9, 2021 2:47 PM<br>
<b>To:</b> agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Subject:</b> Terminating checking for functions on induction-recursion</font>
<div> </div>
</div>
<style type="text/css" style="display:none">
<!--
p
{margin-top:0;
margin-bottom:0}
-->
</style>
<div dir="ltr">
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Hi all,</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
I am hitting a case where termination checker is unhappy with two mutual functions on my induction-recursion definitions. I am still trying to nail down a smaller reproduction but at least I would like to have an understanding of how things work.</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Essentially I have a PER model for dependently typed languages, where I define a PER U and another PER on U:</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
U A B : means A and B are two values related by U. That is A and B are two types.</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Given (AB : U A B), El AB a b: means a and b are two values related by El AB, where El AB computes the PER generated by the type A (or equivalently B).</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Now I shall move on to prove symmetry. I have</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<span style="font-family:"Courier New",monospace">mutual</span></div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<span style="font-family:"Courier New",monospace"> U-sym : U A B -> U B A</span></div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<span style="font-family:"Courier New",monospace"> U-sym AB = ...</span></div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<span style="font-family:"Courier New",monospace"><br>
</span></div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<span style="font-family:"Courier New",monospace"> El-sym : (AB : U A B) <span>(BA : U B A)</span> -> El AB a b -> El BA b a</span></div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<span style="font-family:"Courier New",monospace"> El-sym AB BA = ...</span></div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
Now, U-sym proceeds by pattern matching on AB and El-sym proceeds by pattern matching on AB
<b>and</b> BA. In U-sym, I can call U-sym and El-sym on smaller structure. However, for some reason, in El-sym, I can only El-sym on smaller structure. Any call of U-sym on smaller structure in El-sym will (almost) cause a termination checking error*.<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
I cannot possibly figure out why calling U-sym in El-sym is forbidden. How exactly termination checking with induction-recursion definitions work in Agda? Could anyone give some insights about what could go wrong if U-sym can be called in El-sym, if Agda is
doing the right thing?<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
* almost means I have counterexample but I cannot summarize the pattern<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div id="x_Signature">
<div>
<div></div>
<div id="x_divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font size="3" style="font-size:12pt"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>
</div>
</div>
</div>
</div>
</body>
</html>