[Agda] Termination checking regression (Matrix-shaped orders?)

Dominique Devriese dominique.devriese at cs.kuleuven.be
Thu Mar 7 13:56:09 CET 2013

```All,

I have some code that used to termination check, but which no longer
does with the Darcs version of Agda, perhaps due to the 18-2-2013
change titled "Disabled matrix-shaped orders in the termination
checker."?

The problem seems to be that (suc n, t) is no longer considered
smaller than (n, lambda s t).  Defining SomeExpr as an inductive data
type instead of a record does not seem to help, so it does not appear
to be caused by the record eliminator translation...

Can anyone suggest an alternative way to make this termination check
with the current Agda? Note: I would like to keep using the Induction
stuff, although the reason I need it is not shown in this simplified
example.

Thanks
Dominique

module Test where

open import Data.Unit
open import Data.Nat
open import Data.Fin
open import Data.Product

-- simplified from Induction (standard lib)
RecStruct : Set → Set₁
RecStruct A = (A → Set) → (A → Set)

RecursorBuilder : {A : Set} → RecStruct A → Set₁
RecursorBuilder Rec = ∀ P → (∀ x → Rec P x → P x) → ∀ x → Rec P x

data Expr (n : ℕ) : Set where
var      : (x : Fin n) → Expr n
lambda   : (s : Expr n) → (t : Expr (suc n)) → Expr n
appl     : (f : Expr n) → (val : Expr n) → Expr n

SomeExpr : Set
SomeExpr = ∃ Expr

SyntacticInductionStruct : RecStruct SomeExpr
SyntacticInductionStruct P (n , var x) = ⊤
SyntacticInductionStruct P (n , lambda s t) = P (n , s) × P (suc n , t)
SyntacticInductionStruct P (n , appl f val) = P (n , f) × P (n , val)

rec-builder : RecursorBuilder SyntacticInductionStruct
rec-builder P f (n , var x) = tt
rec-builder P f (n , lambda s t) =
f (n , s) (rec-builder P f (n , s)) , f (suc n , t) (rec-builder P
f (suc n , t))
rec-builder P f (n , appl f′ val) =
f (n , f′) (rec-builder P f (n , f′)) , f (n , val) (rec-builder P
f (n , val))
```