[Agda] a termination problem

[Andreas Abel]

Hello Ramana,

On 29.11.11 11:38 PM, Ramana Kumar wrote:
> Apart from the feeling that "there must be a better way", I also have
> a real problem to do with termination.
> In particular, I define a recursive function that passes itself to
> Relation.Binary.List.StrictLex.transitive.
> How can I convince Agda that transitive will only apply it to smaller
> arguments, or how can I avoid having to try?

This is the typical situation where you would use sized types for 
termination checking.  Unfortunately, the support for sized types is 
rudimentary in Agda at the moment.

However, your example works!  I attach a version of your agda code with 
a sized definition of data type _<_.  [I removed Name since it was not 
available to me, but this is inessential.]

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
{-# OPTIONS --sized-types #-}
module Type where

open import Data.Nat using (ℕ) renaming (_<_ to _N<_)
open import Data.Nat.Properties using () renaming (<-trans to N<-trans)
open import Data.Vec using (Vec;_∷_;[_];[]) renaming (toList to Vec→List;fromList to List→Vec)
open import Data.Product using (_,_;_×_)
open import Data.List.Properties using (∷-injective)
open import Data.String
import Data.List
open import Function using (_on_)
open import Function.Injection using (Injective)
open import Relation.Binary using (Rel;StrictTotalOrder;Transitive;Trichotomous;tri<;tri≈;tri>)
open import Relation.Binary.Product.StrictLex using (×-Lex;×-transitive;×-compare)
open import Relation.Binary.Product.Pointwise using (_×-Rel_;×-Rel↔≡)
open import Relation.Binary.List.StrictLex using (Lex-<;<-compare) renaming (transitive to Lex<-trans)
import Relation.Binary.List.Pointwise as Pointwise
import Relation.Binary.On as On
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_;refl)
open import Relation.Nullary using (¬_)
open import Level using (_⊔_)
open import Size

postulate 
  _S<_      : String -> String -> Set
  S<-trans : Transitive _S<_

record TypeOperator : Set where
  constructor op[_,_]
  field name  : String
        arity : ℕ

data Type : Set where
  TyVar : String → Type
  TyApp : (op : TypeOperator) → Vec Type (TypeOperator.arity op) → Type

-- convert type operators to pairs enabling lexicographic comparison
op→pair : TypeOperator →  String × ℕ
op→pair op[ name , arity ] = name , arity

infix 4 _op<_
_op<_ : Rel TypeOperator _
_op<_ = ×-Lex _≡_ _S<_ _N<_ on op→pair

op<-trans : Transitive _op<_
op<-trans = On.transitive op→pair (×-Lex _≡_ _S<_ _N<_) (×-transitive PropEq.isEquivalence (PropEq.resp₂ _S<_) S<-trans {_≤₂_ = _N<_} N<-trans)

-- a "natural" ordering on types
-- can such a thing not be defined automatically?
-- maybe should define the order on vectors separately?
infix 4 _<_
data _<_ : {size : Size} → Type → Type → Set where
  TyVar<TyVar : ∀ {size} {s₁} {s₂} → 
                (s₁<s₂ : s₁ S< s₂) → _<_ {↑ size} (TyVar s₁) (TyVar s₂)
  TyVar<TyApp : ∀ {size} {s} {op} {as} → _<_ {↑ size} (TyVar s) (TyApp op as)
  TyApp<TyApp : ∀ {size} {op₁} {as₁} {op₂} {as₂} → ×-Lex _≡_ _op<_ (Lex-< _≡_ (_<_ {size})) (op₁ , Vec→List as₁) (op₂ , Vec→List as₂) → _<_ {↑ size} (TyApp op₁ as₁) (TyApp op₂ as₂)

-- the ordering is transitive
-- but this definition fails the termination check
-- what's the best way to prove this? prove it (using WfRec or something)? or restructure the above?
<-trans : {size : Size} → Transitive (_<_ {size})
<-trans (TyVar<TyVar p) (TyVar<TyVar q) = TyVar<TyVar (S<-trans p q)
<-trans (TyVar<TyVar _) TyVar<TyApp = TyVar<TyApp
<-trans TyVar<TyApp (TyApp<TyApp _) = TyVar<TyApp
<-trans (TyApp<TyApp p) (TyApp<TyApp q) = TyApp<TyApp (×-transitive PropEq.isEquivalence (PropEq.resp₂ _op<_) op<-trans {_≤₂_ = Lex-< _≡_ _<_ } (Lex<-trans PropEq.isEquivalence (PropEq.resp₂ _<_) <-trans) p q)