[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