Hm... the argument in the 'problematic' line is suc v, and this is what occurs also in the recursive call, <br>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).<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"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></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 "v" 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">
<<a href="mailto:carlos.camarao@gmail.com" target="_blank">carlos.camarao@gmail.com</a> <mailto:<a href="mailto:carlos.camarao@gmail.com" target="_blank">carlos.camarao@gmail.<u></u>com</a>>> wrote:<br>
<br>
>Unfortunately, the termination checker cannot deal well with<br>
tuples. Please try a curried version of mgu1 instead:<br>
> mgu1 : List (T * T) -> N -> N -> N -> Maybe Subs<br>
>Cheers,<br>
>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 "with-expression versus if-then-else" 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') = union (vars t) (vars t')<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') = numConstructors t + numConstructors t'<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') = (apply s t , apply s t')<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 ν') = ⌊ ν' ≟ ν ⌋<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' = 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' = 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' = applyL s pairs_t<br>
c' = numConstructorsLP pairs_t'<br>
k' = num_pairs_tvL pairs_t'<br>
in if occurs v t2 then nothing<br>
else mgu1 pairs_t' v c' k'<br>
<br>
==============================<u></u>==============================<u></u>==========<br>
</div></div></blockquote>
<br><div class="HOEnZb"><div class="h5">
<br>
-- <br>
Andreas Abel <>< 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>