[Agda] Termination checking, if-then-else X with

Andreas Abel andreas.abel at ifi.lmu.de
Wed Jul 3 08:19:27 CEST 2013


Unfortunately, the termination checker cannot deal well with tuples. 
Please try a curried version of mgu1 instead:

   mgu1 : List (T * T) -> N -> N -> N -> Maybe Subs

Cheers,
Andreas

On 02.07.2013 16:35, Carlos Camarao wrote:
> Hi. Is the following ok, or a bug?
>
> With line I (with an if-then-else expression) uncommented, module Unif
> compiles ok (no error detected), but
> commenting line I and uncommenting lines W1, W2, W3 (using a
> with-expression instead of if-then-else),
> the termination checker complains (mgu1 becomes colored in light salmon).
>
> I am using agda version 2.3.0.1, on Ubuntu 12.04 LTS.
>
> Cheers,
>
> Carlos
>
> ===============================================
> module Unif where
>
> open import Relation.Nullary.Decidable using (⌊_⌋)
> open import Data.Bool                  using (Bool; false; _∨_;
> if_then_else_)
> open import Data.Nat                   using (ℕ; suc; _+_; _≟_; zero)
> open import Data.Maybe.Core       using (Maybe; nothing; just)
> open import Data.Product             using (_×_; _,_; proj₁)
> open import Data.List                   using (List; []; [_]; _∷_; map;
> sum; length; concat; filter)
> open import Function                   using (_∘_)
> open import Relation.Nullary.Core using (yes; no)
> open import Relation.Binary.Core  using (Decidable; _≡_; refl)
>
> {- ========= was Ty.agda ==============-}
>
> 𝕍ar  : Set
> 𝕍ar = ℕ
>
> 𝕍ars : Set
> 𝕍ars = List ℕ
>
> mem : ℕ → 𝕍ars → Bool
> mem _ []      = false
> mem a (b ∷ x) = ⌊ a ≟ b ⌋ ∨ mem a x
>
> union : 𝕍ars → 𝕍ars → 𝕍ars
> union []      y = y
> union (a ∷ x) y = if mem a y then union x y else a ∷ union x y
>
> data 𝕋 : Set where
>   Con : ℕ → 𝕋     {- type constructor -}
>   Var : ℕ → 𝕋     {- type variable -}
>   _⇒_ : 𝕋 → 𝕋 → 𝕋 {- function type -}
>
> vars : 𝕋 → 𝕍ars
> vars (Con _)   = []
> vars (Var v)   = [ v ]
> vars (ta ⇒ tb) = union (vars ta) (vars tb)
>
> varsP : 𝕋 × 𝕋 → 𝕍ars
> varsP (t , t') = union (vars t) (vars t')
>
> numVarsL : List (𝕋 × 𝕋) → ℕ
> numVarsL = length ∘ concat ∘ map varsP
>
> numVars : 𝕋 → ℕ
> numVars = length ∘ vars
>
> numConstructors : 𝕋 → ℕ
> numConstructors (Con _)   = 1
> numConstructors (Var _)   = 0
> numConstructors (ta ⇒ tb) = 1 + numConstructors ta + numConstructors tb
>
> numConstructorsP : (𝕋 × 𝕋) → ℕ
> numConstructorsP (t , t') = numConstructors t + numConstructors t'
>
> numConstructorsLP : List (𝕋 × 𝕋) → ℕ
> numConstructorsLP = sum ∘ map numConstructorsP
>
> {- ========== end of Ty.agda ================== -}
>
> {- =========== was Subst.agda ================ -}
> Mapping : Set
> Mapping = 𝕍ar × 𝕋
>
> Subs : Set
> Subs = List Mapping
>
> emptySubs : Subs
> emptySubs = []
>
> insert : 𝕍ar → 𝕋 → Subs → Subs
> insert v st s = (v , st) ∷ s
>
> find : 𝕍ar → Subs → Maybe 𝕋
> find v s with filter (λ vt → ⌊ proj₁ vt ≟ v ⌋)  s
> ... | []          = nothing
> ... | (_ , t) ∷ _ = just t
>
> apply : Subs → 𝕋 → 𝕋
> apply s (Var v) with find v s
> ... | just t       = t
> ... | nothing      = Var v
> apply s (Con c)    = Con c
> apply s (ta ⇒ tb)  = (apply s ta) ⇒ (apply s tb)
>
> applyP : Subs → (𝕋 × 𝕋) → (𝕋 × 𝕋)
> applyP s (t , t') = (apply s t , apply s t')
>
> applyL : Subs → List (𝕋 × 𝕋) → List (𝕋 × 𝕋)
> applyL s l = map (applyP s) l
>
> {- ============= end of Subst.agda ================ -}
>
> num_pairs_tv : 𝕋 × 𝕋 → ℕ
> num_pairs_tv (Var _ , _)         = 0
> num_pairs_tv (_ , Var _)         = 1
> num_pairs_tv (ta ⇒ tb , tc ⇒ td) = num_pairs_tv (ta , tc) + num_pairs_tv
> (tb , td)
> num_pairs_tv _                   = 0
>
> num_pairs_tvL : List (𝕋 × 𝕋) → ℕ
> num_pairs_tvL = sum ∘ map num_pairs_tv
>
> occurs : 𝕍ar → 𝕋 → Bool
> occurs ν (Var ν')  = ⌊ ν' ≟ ν ⌋
> occurs _ (Con _)   = false
> occurs ν (ta ⇒ tb) = (occurs ν ta) ∨ (occurs ν tb)
>
> TerminationTriple : Set
> TerminationTriple = ℕ × ℕ × ℕ
>
> mgu1 : (List (𝕋 × 𝕋) × TerminationTriple) → Maybe Subs
> mgu1 ([]                        ,         _         )       = just
> emptySubs
> mgu1 (((Con _ , _) ∷ _)         ,        (_ , 0 , _))       = nothing --
> impossible
> mgu1 (((Con n1 , Con n2) ∷ pairs_t) , (v , suc c , k))      = if ⌊ n1 ≟
> n2 ⌋ then mgu1 (pairs_t , (v , c , k)) else nothing  -- line I
>
> -- mgu1 (((Con n1 , Con n2) ∷ pairs_t)   ,    (v , suc c , k))   with n1
> ≟ n2                                        -- line W1
> -- mgu1 (((Con n1 , Con .n1) ∷ pairs_t)  ,    (v , suc c , k))   | yes
> refl = mgu1 (pairs_t , (v , c , k) )   -- line W2
> -- mgu1 (((Con n1 , Con n2) ∷ pairs_t)   ,    (v , suc c , k))   | no
> _     = nothing                               -- line W3
>
> mgu1 (((Con _ , _ ⇒ _) ∷ _)           ,  _                ) = nothing
> mgu1 (((Con _ , Var _) ∷ pairs_t)     ,    (v , c , 0)    ) = nothing --
> impossible
> mgu1 (((Con c1 , Var v2) ∷ pairs_t)   ,    (v , c , suc k)) = mgu1
> (((Var v2 , Con c1) ∷ pairs_t) , (v , c , k))
>
> mgu1 (((_ ⇒ _ , _) ∷ pairs_t)         ,    (_ , 0 , _)    ) = nothing --
> impossible
> mgu1 (((_ ⇒ _ , Con _) ∷ _)           ,  _                ) = nothing
> mgu1 (((_ ⇒ _ , Var v2) ∷ pairs_t)    ,  (_ , _ , 0)      ) = nothing --
> impossible
> mgu1 (((ta ⇒ tb , Var v2) ∷ pairs_t)  ,  (v , c , suc k)  ) = mgu1
> (((Var v2 , ta ⇒ tb) ∷ pairs_t) , (v , c , k))
> mgu1 (((_ ⇒ _ , _ ⇒ _) ∷ _)           ,  (_ , suc 0 , _)  ) = nothing --
> impossible
> mgu1 (((ta ⇒ tb , tc ⇒ td) ∷ pairs_t) , (v , suc (suc c) , k)) = mgu1
> (((ta , tc) ∷ (tb , td) ∷ pairs_t) , (v , c , k))
>
> mgu1 (((Var _ , _)   ∷ _ )            ,   (0 , _ , _)     ) = nothing --
> impossible
> mgu1 (((Var v1 , Var v2) ∷ pairs_t)   ,   (suc v , c , k) ) = let
> s        = insert v1 (Var v2) emptySubs
>
> pairs_t' = applyL s pairs_t
>                                                                 in if ⌊
> v1 ≟ v2 ⌋ then mgu1 (pairs_t , (suc v , c , k))
>                                                                                   else mgu1 (pairs_t , (v , c , k))
> mgu1 (((Var v1 , t2) ∷ pairs_t)       ,   (suc v , c , k) ) = let
> s        = insert v1 t2 emptySubs
>
> pairs_t' = applyL s pairs_t
>
> c'       = numConstructorsLP pairs_t'
>
> k'       = num_pairs_tvL pairs_t'
>                                                                 in if
> occurs v t2 then nothing
>                                                                                   else mgu1 (pairs_t' , (v , c' , k'))
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
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/


More information about the Agda mailing list