[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