[Agda] Termination checking, if-then-else X with
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Jul 5 17:11:40 CEST 2013
Note: if you use 'with', what you see is not what you get.
'with' creates an auxiliary function that abstracts over the pattern
variables of the clause it was spawned from.
This is why mgu1-with below has pattern "v" and not "suc v", so a call
to mgu1 with "suc v" is actually an increase.
--termination-depth
was added to address this situation.
Cheers,
Andreas
On 04.07.2013 17:22, Carlos Camarao wrote:
> Hm... the argument in the 'problematic' line is suc v, and this is what
> occurs also in the recursive call,
> so I see no "increase" (non-decrease, yes); but the main issue/question
> was the fact that the code with if-then-else works but with
> with-expression does not, which seems undesirable (surprising).
>
> Thanks.
>
> Carlos
>
> On Thu, Jul 4, 2013 at 3:01 AM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
> 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>
> <mailto: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 <mailto:andreas.abel at ifi.lmu.de>
> http://www2.tcs.ifi.lmu.de/~__abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
>
--
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