[Agda] Termination checking, if-then-else X with
Carlos Camarao
carlos.camarao at gmail.com
Thu Jul 4 16:22:31 CEST 2013
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>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<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/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130704/b0a8dda1/attachment-0001.html
More information about the Agda
mailing list