Hm... the argument in the &#39;problematic&#39; line is suc v, and this is what occurs also in the recursive call, <br>so I see no &quot;increase&quot; (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).<br>
<br>Thanks. <br><br>Carlos   <br><br><div class="gmail_quote">On Thu, Jul 4, 2013 at 3:01 AM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">The problematic line is<div class="im"><br>
<br>
mgu1 ((Var v1 , Var .v1) ∷ pairs_t)   (suc v) c k | yes refl<br>
  = mgu1 pairs_t (suc v) c k<br>
<br></div>
You are calling<br>
<br>
  mgu1 ... (suc v) ...<br>
<br>
from a with-generated function<br>
<br>
  mgu1-with ... v ...<br>
<br>
so, the argument &quot;v&quot; is increased.  In this case, since we are dealing with natural numbers, the problem is fixed by setting<br>
<br>
  {-# OPTIONS --termination-depth=2 #-}<br>
<br>
so that Agda counts increase/decrease farther.<br>
<br>
Cheers,<br>
Andreas<div class="im"><br>
<br>
On 03.07.2013 19:07, Carlos Camarao wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
<br>
On Wed, Jul 3, 2013 at 12:09 PM, Carlos Camarao<br></div><div><div class="h5">
&lt;<a href="mailto:carlos.camarao@gmail.com" target="_blank">carlos.camarao@gmail.com</a> &lt;mailto:<a href="mailto:carlos.camarao@gmail.com" target="_blank">carlos.camarao@gmail.<u></u>com</a>&gt;&gt; wrote:<br>
<br>
     &gt;Unfortunately, the termination checker cannot deal well with<br>
    tuples. Please try a curried version of mgu1 instead:<br>
     &gt;  mgu1 : List (T * T) -&gt; N -&gt; N -&gt; N -&gt; Maybe Subs<br>
     &gt;Cheers,<br>
     &gt;Andreas<br>
<br>
    Thanks Andreas! Surprisingly (for me), changing to a curried version<br>
    did work! (Surprising for me because I think making the termination<br>
    checker work with tuples also should not be difficult).<br>
<br>
    The curried version of mgu1 is below; it compiles ok also with a<br>
    with-expression (i.e. it also compiles ok by uncommenting lines<br>
    W1,W2,W3 and commenting line I).  ...<br>
<br>
<br>
Unfortunately, the problem &quot;with-expression versus if-then-else&quot; appears<br>
again, in the following curried version of mgu1: the code below compiles<br>
ok but mgu1 becomes colored in light salmon if if-then-else is replaced<br>
by a with-expression (i.e. if lines I1 to I4 are commented and lines W1<br>
to W5 are uncommented).<br>
<br>
Cheers,<br>
<br>
Carlos<br>
<br>
==============================<u></u>==============================<u></u>=====<br>
module Unif where<br>
<br>
open import Relation.Nullary.Decidable using (⌊_⌋)<br>
open import Data.Bool                  using (Bool; false; _∨_;<br>
if_then_else_)<br>
open import Data.Nat                   using (ℕ; suc; _+_; _≟_; zero)<br>
open import Data.Maybe.Core            using (Maybe; nothing; just)<br>
open import Data.Product               using (_×_; _,_; proj₁)<br>
open import Data.List                  using (List; []; [_]; _∷_; map;<br>
sum; length; concat; filter)<br>
open import Function                   using (_∘_)<br>
open import Relation.Nullary.Core      using (yes; no)<br>
open import Relation.Binary.Core       using (Decidable; _≡_; refl)<br>
<br>
{- ===================== Ty.agda ==============================<u></u>=====-}<br>
<br>
𝕍ar  : Set<br>
𝕍ar = ℕ<br>
<br>
𝕍ars : Set<br>
𝕍ars = List ℕ<br>
<br>
mem : ℕ → 𝕍ars → Bool<br>
mem _ []      = false<br>
mem a (b ∷ x) = ⌊ a ≟ b ⌋ ∨ mem a x<br>
<br>
union : 𝕍ars → 𝕍ars → 𝕍ars<br>
union []      y = y<br>
union (a ∷ x) y = if mem a y then union x y else a ∷ union x y<br>
<br>
data 𝕋 : Set where<br>
  Con : ℕ → 𝕋     {- type constructor -}<br>
  Var : ℕ → 𝕋     {- type variable -}<br>
  _⇒_ : 𝕋 → 𝕋 → 𝕋 {- function type -}<br>
<br>
vars : 𝕋 → 𝕍ars<br>
vars (Con _)   = []<br>
vars (Var v)   = [ v ]<br>
vars (ta ⇒ tb) = union (vars ta) (vars tb)<br>
<br>
varsP : 𝕋 × 𝕋 → 𝕍ars<br>
varsP (t , t&#39;) = union (vars t) (vars t&#39;)<br>
<br>
numVarsL : List (𝕋 × 𝕋) → ℕ<br>
numVarsL = length ∘ concat ∘ map varsP<br>
<br>
numVars : 𝕋 → ℕ<br>
numVars = length ∘ vars<br>
<br>
numConstructors : 𝕋 → ℕ<br>
numConstructors (Con _)   = 1<br>
numConstructors (Var _)   = 0<br>
numConstructors (ta ⇒ tb) = 1 + numConstructors ta + numConstructors tb<br>
<br>
numConstructorsP : (𝕋 × 𝕋) → ℕ<br>
numConstructorsP (t , t&#39;) = numConstructors t + numConstructors t&#39;<br>
<br>
numConstructorsLP : List (𝕋 × 𝕋) → ℕ<br>
numConstructorsLP = sum ∘ map numConstructorsP<br>
<br>
{- ===========end of Ty.agda ==============================<u></u>============ -}<br>
<br>
{- ===========Subst.agda ==============================<u></u>============ -}<br>
Mapping : Set<br>
Mapping = 𝕍ar × 𝕋<br>
<br>
Subs : Set<br>
Subs = List Mapping<br>
<br>
emptySubs : Subs<br>
emptySubs = []<br>
<br>
insert : 𝕍ar → 𝕋 → Subs → Subs<br>
insert v st s = (v , st) ∷ s<br>
<br>
find : 𝕍ar → Subs → Maybe 𝕋<br>
find v s with filter (λ vt → ⌊ proj₁ vt ≟ v ⌋)  s<br>
... | []          = nothing<br>
... | (_ , t) ∷ _ = just t<br>
<br>
apply : Subs → 𝕋 → 𝕋<br>
apply s (Var v) with find v s<br>
... | just t       = t<br>
... | nothing      = Var v<br>
apply s (Con c)    = Con c<br>
apply s (ta ⇒ tb)  = (apply s ta) ⇒ (apply s tb)<br>
<br>
applyP : Subs → (𝕋 × 𝕋) → (𝕋 × 𝕋)<br>
applyP s (t , t&#39;) = (apply s t , apply s t&#39;)<br>
<br>
applyL : Subs → List (𝕋 × 𝕋) → List (𝕋 × 𝕋)<br>
applyL s l = map (applyP s) l<br>
<br>
{- =============end of Subst.agda<br>
==============================<u></u>================= -}<br>
<br>
num_pairs_tv : 𝕋 × 𝕋 → ℕ<br>
num_pairs_tv (Var _ , _)         = 0<br>
num_pairs_tv (_ , Var _)         = 1<br>
num_pairs_tv (ta ⇒ tb , tc ⇒ td) = num_pairs_tv (ta , tc) + num_pairs_tv<br>
(tb , td)<br>
num_pairs_tv _                   = 0<br>
<br>
num_pairs_tvL : List (𝕋 × 𝕋) → ℕ<br>
num_pairs_tvL = sum ∘ map num_pairs_tv<br>
<br>
occurs : 𝕍ar → 𝕋 → Bool<br>
occurs ν (Var ν&#39;)  = ⌊ ν&#39; ≟ ν ⌋<br>
occurs _ (Con _)   = false<br>
occurs ν (ta ⇒ tb) = (occurs ν ta) ∨ (occurs ν tb)<br>
<br>
mgu1 : List (𝕋 × 𝕋) → ℕ → ℕ → ℕ → Maybe Subs<br>
--   v = number of variables<br>
--   c = number of constructors<br>
--   k = sum of number of pairs (t,v) where v is (and t is not) a variable;<br>
-- k is the decreasing measure in rec. calls where t1 is not and t2 is a<br>
var, first arg = ((t1,t2) ∷ _).<br>
mgu1 [] _ _ _<br>
      = just emptySubs<br>
mgu1 ((Con _ , _) ∷ _) _ 0 _                                           =<br>
nothing -- impossible<br>
mgu1 ((Con n1 , Con n2) ∷ pairs_t)   v (suc c) k  with n1 ≟ n2<br>
mgu1 ((Con n1 , Con .n1) ∷ pairs_t)  v (suc c) k  | yes refl = mgu1<br>
pairs_t  v c k<br>
mgu1 ((Con n1 , Con n2) ∷ pairs_t)   v (suc c) k  | no _     = nothing<br>
mgu1 ((Con _ , _ ⇒ _) ∷ _)  _ _ _                                    =<br>
nothing<br>
mgu1 ((Con _ , Var _) ∷ pairs_t)     v  c 0                         =<br>
nothing -- impossible<br>
mgu1 ((Con c1 , Var v2) ∷ pairs_t)   v  c (suc k)               = mgu1<br>
((Var v2 , Con c1) ∷ pairs_t) v c k<br>
<br>
mgu1 ((_ ⇒ _ , _) ∷ pairs_t)         _  0 _                           =<br>
nothing -- impossible<br>
mgu1 ((_ ⇒ _ , Con _) ∷ _)           _  _ _                          =<br>
nothing<br>
mgu1 ((_ ⇒ _ , Var v2) ∷ pairs_t)    _ _ 0                         =<br>
nothing -- impossible<br>
mgu1 ((ta ⇒ tb , Var v2) ∷ pairs_t)  v c (suc k)                 = mgu1<br>
((Var v2 , ta ⇒ tb) ∷ pairs_t) v c k<br>
mgu1 ((_ ⇒ _ , _ ⇒ _) ∷ _)           _ (suc 0) _                   =<br>
nothing -- impossible<br>
mgu1 ((ta ⇒ tb , tc ⇒ td) ∷ pairs_t) v (suc (suc c)) k        = mgu1<br>
((ta , tc) ∷ (tb , td) ∷ pairs_t) v c k<br>
<br>
mgu1 ((Var _ , _)   ∷ _ )            0 _ _<br>
= nothing -- impossible<br>
mgu1 ((Var v1 , Var v2) ∷ pairs_t)   (suc v) c k                = let<br>
s        = insert v1 (Var v2) emptySubs        -- line I1<br>
                                                                                            pairs_t&#39; = applyL s pairs_t                          -- line I2<br>
                                                                                         in if ⌊ v1 ≟ v2 ⌋ then mgu1 pairs_t (suc v) c k -- line I3<br>
                                                                                            else mgu1 pairs_t v c k                             -- line I4<br>
{-<br>
mgu1 ((Var v1 , Var v2) ∷ pairs_t)   (suc v) c k with v1 ≟<br>
v2                                                             -- line W1<br>
mgu1 ((Var v1 , Var .v1) ∷ pairs_t)   (suc v) c k | yes refl = mgu1<br>
pairs_t (suc v) c k                          -- line W2<br>
mgu1 ((Var v1 , Var v2) ∷ pairs_t)   (suc v) c k  | no _      = let<br>
s        = insert v1 (Var v2) emptySubs -- line W3<br>
                                                                                           pairs_t&#39; = applyL s pairs_t                    -- line W4<br>
                                                                                        in mgu1 pairs_t v c k                              -- line W5<br>
-}<br>
mgu1 ((Var v1 , t2) ∷ pairs_t)       (suc v) c k            = let s<br>
        = insert v1 t2 emptySubs<br>
                                                                                      pairs_t&#39; = applyL s pairs_t<br>
                                                                                      c&#39;         = numConstructorsLP pairs_t&#39;<br>
                                                                                      k&#39;         = num_pairs_tvL pairs_t&#39;<br>
                                                                                  in if occurs v t2 then nothing<br>
                                                                                  else mgu1 pairs_t&#39; v c&#39; k&#39;<br>
<br>
==============================<u></u>==============================<u></u>==========<br>
</div></div></blockquote>
<br><div class="HOEnZb"><div class="h5">
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</div></div></blockquote></div><br>