[Agda] Agda Termination Checker Implements Size-Change Termination?

[Reuben Rowe]

Dear Agda List,

Apologies if the answer to my question is by now folklore, but I could
not find it through searching online, or by asking some colleagues who
are Agda users.

Q: Does the Agda termination checker in fact implement the check for
size-change termination? [1]

When I look at the Agda documentation for information about the
termination checker, it points me towards Andreas' original technical
report [2]. I have also looked at the subsequent formally published
description, written with Thorsten [3].

Certainly, one can identify the call matrices of [2,3] with the
size-change graphs of [1]. However, there is a difference between the
lexicographic and termination orders of Defs 3.14 and 3.15 of [3], and
the size-change termination property (Thm 4) of [1].

In particular, consider the following Agda function, 2-hydra-total, that
encodes the standard cyclic proof of the totality of Berardi and
Tatsuta's 2-hydra predicate [4].

open import Data.Nat using (ℕ; zero; suc)

-- The 2-Hydra predicate
data 2-hydra : ℕ → ℕ → Set where
   base₁ : 2-hydra 0 0
   base₂ : 2-hydra 1 0
   base₃ : ∀{n} → 2-hydra n 1
   step₁ : ∀{n m} → 2-hydra n m → 2-hydra (suc n) (suc (suc m))
   step₂ : ∀{n} → 2-hydra (suc n) n → 2-hydra 0 (suc (suc n))
   step₃ : ∀{n} → 2-hydra (suc n) n → 2-hydra (suc (suc n)) 0

-- Totality of 2-hydra
2-hydra-total : ∀(n m : ℕ) → 2-hydra n m
2-hydra-total zero zero             = base₁
2-hydra-total (suc zero) zero       = base₂
2-hydra-total (suc (suc n)) zero    = step₃ (2-hydra-total (suc n) n)
2-hydra-total n (suc zero)          = base₃
2-hydra-total zero (suc (suc m))    = step₂ (2-hydra-total (suc m) m)
2-hydra-total (suc n) (suc (suc m)) = step₁ (2-hydra-total n m)

This does *not* have a termination ordering according to Def. 3.15 of
[3]. The "recursion behaviour" of 2-hydra-total is the set B = {(<,<),
(<,?), (?,<)}, and so there is no way to pick a permutation π of the
input parameters such that for all r ∈ B, r_π(0) ≠ ? (as required by
Def. 3.14 of [3]).

However, 2-hydra-total *does* satisfy the size-change termination
condition (infinite descent in cyclic proofs is equivalent to the
size-change termination property). Moreover, Agda happily reports that
2-hydra-total terminates.

I did find a blog post (from 2018) discussing the termination checker
[5], which demonstrates debug output from Agda talking about "Idempotent
call matrices". This also suggests to me that the termination checker
may be implementing size-change termination since, as formulated in [1],
this requires checking properties of idempotent size-change graphs.

(I wanted to reproduce this debug output in the version of Agda I am
running - 2.6.3 - but the commands used in the blog post do not seem to
produce this output anymore. Is there still a way to get Agda to output
the call matrices produced by the termination checker?).

Is there a more up-to-date published account of what Agda currently
implements in the termination checker? I'd be very interested to know
about this.

Thanks,

Reuben  Rowe

[1] Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram: The Size-change
Principle for Program Termination. In Proceedings of the 28th ACM
SIGPLAN-SIGACT symposium on Principles of programming languages (POPL
'01). Association for Computing Machinery, New York, NY, USA, 81–92.
(2001). https://doi.org/10.1145/360204.360210
[2] Andreas Abel: foetus - Termination Checker for Simple Functional
Programs. https://www.cse.chalmers.se/~abela/foetus.pdf
[3] Andreas Abel,Thorsten Altenkirch: A Predicative Analysis of
Structural Recursion. Journal of Functional Programming.
2002;12(1):1–41. https://doi.org/10.1017/S0956796801004191
[4] Stefano Berardi, Makoto Tatsuta: Classical System of Martin-Lof's
Inductive Definitions is not Equivalent to Cyclic Proofs. Log. Methods
Comput. Sci. 15(3) (2019). https://doi.org/10.23638/LMCS-15(3:10)2019
[5] Oleg Grenrus: Notes on Agda's Termination Checker.
https://oleg.fi/gists/posts/2018-08-29-agda-termination-checker.html

This email, its contents and any attachments are intended solely for the addressee and may contain confidential information. In certain circumstances, it may also be subject to legal privilege. Any unauthorised use, disclosure, or copying is not permitted. If you have received this email in error, please notify us and immediately and permanently delete it. Any views or opinions expressed in personal emails are solely those of the author and do not necessarily represent those of Royal Holloway, University of London. It is your responsibility to ensure that this email and any attachments are virus free.