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

Andreas Abel andreas.abel at ifi.lmu.de
Thu Jul 4 08:01:27 CEST 2013


The problematic line is

mgu1 ((Var v1 , Var .v1) ∷ pairs_t)   (suc v) c k | yes refl
   = mgu1 pairs_t (suc v) c k

You are calling

   mgu1 ... (suc v) ...

from a with-generated function

   mgu1-with ... v ...

so, the argument "v" is increased.  In this case, since we are dealing 
with natural numbers, the problem is fixed by setting

   {-# OPTIONS --termination-depth=2 #-}

so that Agda counts increase/decrease farther.

Cheers,
Andreas

On 03.07.2013 19:07, Carlos Camarao wrote:
>
> On Wed, Jul 3, 2013 at 12:09 PM, Carlos Camarao
> <carlos.camarao at gmail.com <mailto:carlos.camarao at gmail.com>> wrote:
>
>      >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
>
>     Thanks Andreas! Surprisingly (for me), changing to a curried version
>     did work! (Surprising for me because I think making the termination
>     checker work with tuples also should not be difficult).
>
>     The curried version of mgu1 is below; it compiles ok also with a
>     with-expression (i.e. it also compiles ok by uncommenting lines
>     W1,W2,W3 and commenting line I).  ...
>
>
> Unfortunately, the problem "with-expression versus if-then-else" appears
> again, in the following curried version of mgu1: the code below compiles
> ok but mgu1 becomes colored in light salmon if if-then-else is replaced
> by a with-expression (i.e. if lines I1 to I4 are commented and lines W1
> to W5 are uncommented).
>
> 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)
>
> {- ===================== 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 ========================================== -}
>
> {- ===========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)
>
> mgu1 : List (𝕋 × 𝕋) → ℕ → ℕ → ℕ → Maybe Subs
> --   v = number of variables
> --   c = number of constructors
> --   k = sum of number of pairs (t,v) where v is (and t is not) a variable;
> -- k is the decreasing measure in rec. calls where t1 is not and t2 is a
> var, first arg = ((t1,t2) ∷ _).
> mgu1 [] _ _ _
>       = just emptySubs
> mgu1 ((Con _ , _) ∷ _) _ 0 _                                           =
> nothing -- impossible
> mgu1 ((Con n1 , Con n2) ∷ pairs_t)   v (suc c) k  with n1 ≟ n2
> mgu1 ((Con n1 , Con .n1) ∷ pairs_t)  v (suc c) k  | yes refl = mgu1
> pairs_t  v c k
> mgu1 ((Con n1 , Con n2) ∷ pairs_t)   v (suc c) k  | no _     = nothing
> 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        -- line I1
>                                                                                             pairs_t' = applyL s pairs_t                          -- line I2
>                                                                                          in if ⌊ v1 ≟ v2 ⌋ then mgu1 pairs_t (suc v) c k -- line I3
>                                                                                             else mgu1 pairs_t v c k                             -- line I4
> {-
> mgu1 ((Var v1 , Var v2) ∷ pairs_t)   (suc v) c k with v1 ≟
> v2                                                             -- line W1
> mgu1 ((Var v1 , Var .v1) ∷ pairs_t)   (suc v) c k | yes refl = mgu1
> pairs_t (suc v) c k                          -- line W2
> mgu1 ((Var v1 , Var v2) ∷ pairs_t)   (suc v) c k  | no _      = let
> s        = insert v1 (Var v2) emptySubs -- line W3
>                                                                                            pairs_t' = applyL s pairs_t                    -- line W4
>                                                                                         in mgu1 pairs_t v c k                              -- line W5
> -}
> 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'
>
> ======================================================================


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