[Agda] Terminating checking for functions on induction-recursion

[Jason Hu]

I now have a concrete program illustrating the issue: https://github.com/agda/agda/issues/5646
[https://opengraph.githubassets.com/c20a4be1cb39340e55f4c7a4df0e371714690cf798325b6b8c494b381deaa1d9/agda/agda/issues/5646]<https://github.com/agda/agda/issues/5646>
Termination checker rejects mutual functions on induction-recursion definition · Issue #5646 · agda/agda<https://github.com/agda/agda/issues/5646>
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) → (ρ :...
github.com

Any help with me understanding the termination checking strategy will be appreciated.

{-# OPTIONS --without-K --safe #-}

open import Data.Nat

data Exp : Set where


mutual
  Env : Set
  Env = ℕ → D

  data D : Set where
    Π   : D → (t : Exp) → (ρ : Env) → D

variable
  T T′ : Exp
  A A′ : D
  B B′ : D
  a a′ : D
  b b′ : D
  ρ ρ′ : Env

_↦_ : Env → D → Env
(ρ ↦ d) zero    = d
(ρ ↦ d) (suc x) = ρ x

data ⟦_⟧_↘_ : Exp → Env → D → Set where

data _∙_↘_ : D → D → D → Set where

record ΠRT T ρ T′ ρ′ (R : D → D → Set) : Set where
  field
    ⟦T⟧   : D
    ⟦T′⟧  : D
    ↘⟦T⟧  : ⟦ T ⟧ ρ ↘ ⟦T⟧
    ↘⟦T′⟧ : ⟦ T′ ⟧ ρ′ ↘ ⟦T′⟧
    T≈T′  : R ⟦T⟧ ⟦T′⟧


record Π̂ (f a f′ a′ : D) (R : D → D → Set) : Set where
  field
    fa     : D
    fa′    : D
    ↘fa    : f ∙ a ↘ fa
    ↘fa′   : f′ ∙ a′ ↘ fa′
    fa≈fa′ : R fa fa′

mutual

  data 𝕌 : D → D → Set where
    Π  : (A≈A′ : 𝕌 A A′) →
         (∀ {a a′} →
            El A≈A′ a a′ →
            ΠRT T (ρ ↦ a) T′ (ρ′ ↦ a′) 𝕌) →
         -------------------------
         𝕌 (Π A T ρ) (Π A′ T′ ρ′)


  El : 𝕌 A B → D → D → Set
  El (Π A≈A′ RT)  = λ f f′ → ∀ {a b} (inp : El A≈A′ a b) → Π̂ f a f′ b (El (ΠRT.T≈T′ (RT inp)))


mutual

  𝕌-sym : 𝕌 A B → 𝕌 B A
  𝕌-sym (Π {_} {_} {T} {ρ} {T′} {ρ′} A≈A′ RT) = Π (𝕌-sym A≈A′) helper
    where helper : El (𝕌-sym A≈A′) a a′ → ΠRT T′ (ρ′ ↦ a) T (ρ ↦ a′) 𝕌
          helper a≈a′ = record
            { ⟦T⟧   = ⟦T′⟧
            ; ⟦T′⟧  = ⟦T⟧
            ; ↘⟦T⟧  = ↘⟦T′⟧
            ; ↘⟦T′⟧ = ↘⟦T⟧
            ; T≈T′  = 𝕌-sym T≈T′
            }
            where open ΠRT (RT (El-sym (𝕌-sym A≈A′) A≈A′ a≈a′))

  El-sym : ∀ (A≈B : 𝕌 A B) (B≈A : 𝕌 B A) → El A≈B a b → El B≈A b a
  El-sym (Π A≈B RT) (Π B≈A RT′) f≈f′ a≈a′
    with 𝕌-sym A≈B
  ...  | x = {!!}


Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Jason Hu
Sent: November 9, 2021 2:47 PM
To: agda at lists.chalmers.se <agda at lists.chalmers.se>
Subject: Terminating checking for functions on induction-recursion

Hi all,

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.

Essentially I have a PER model for dependently typed languages, where I define a PER U and another PER on U:

U A B : means A and B are two values related by U. That is A and B are two types.
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).

Now I shall move on to prove symmetry. I have

​mutual
  U-sym : U A B -> U B A
  U-sym AB = ...

  El-sym : (AB : U A B) (BA : U B A) -> El AB a b -> El BA b a
  El-sym AB BA = ...

Now,  U-sym  proceeds by pattern matching on AB and El-sym proceeds by pattern matching on AB and 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*.

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?

* almost means I have counterexample but I cannot summarize the pattern

Thanks,
Jason Hu
https://hustmphrrr.github.io/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211111/2cb3a0ef/attachment-0001.html>