[Agda-dev] Termination
Hans Peter Würmli
wurmli at hispeed.ch
Fri Dec 12 05:40:55 CET 2014
Thank you, Andreas, for your thoughtful lines. As I am an Agda novice I
couldn't see a simpler recursion pattern for the properties I tried to
prove. As an exercise I am trying to prove the various properties of (ℕ,
zero, +, *) and show it's isomorphic to the binary representation.
Learning about the possibilities of Agda, the proofs are not always
turning out elegant therefore. The non-passing of the termination-check
arose with the proof of associativity of addition of strictly positive
binary natural numbers. I copy the sample at the end. It's probably a
fact of mathematics that simple, short and elegant proofs only arise
with mature knowledge, whereas first proofs are often lengthy,
complicated and ugly. A proof assistant might be particularly valuable
for the latter.
Maybe the example below can convince you that a slightly smarter
termination checker might be worth the effort.
Best regards
Hans Peter
------------------------------------------
module Termination2 where
open import Data.Nat
open import Relation.Binary.PropositionalEquality
data Bit : Set where
O : Bit
I : Bit
infixr 5 _∷_
data bℕ : Set where
I : bℕ
_∷_ : Bit → bℕ → bℕ
_+1' : bℕ → bℕ
I +1' = O ∷ I
(O ∷ n) +1' = I ∷ n
(I ∷ n) +1' = O ∷ (n +1')
_b+'_ : bℕ → bℕ → bℕ
I b+' I = O ∷ I
I b+' (O ∷ m) = I ∷ m
I b+' (I ∷ m) = O ∷ I b+' m
(O ∷ n) b+' I = I ∷ n
(O ∷ n) b+' (O ∷ m) = O ∷ n b+' m
(O ∷ n) b+' (I ∷ m) = I ∷ n b+' m
(I ∷ n) b+' I = O ∷ n b+' I
(I ∷ n) b+' (O ∷ m) = I ∷ n b+' m
(I ∷ n) b+' (I ∷ m) = O ∷ ((n b+' m) +1')
open ≡-Reasoning
lemma-I=+1 : (n : bℕ) → (I b+' n) ≡ (n +1')
lemma-I=+1 I = refl
lemma-I=+1 (O ∷ n) = refl
lemma-I=+1 (I ∷ n) = cong (_∷_ O) (lemma-I=+1 n)
lemma-+1'b+' : (n : bℕ) (m : bℕ) → (n +1') b+' m ≡ (n b+' m) +1'
lemma-+1'b+' I I = refl
lemma-+1'b+' I (O ∷ m) =
begin
(I +1') b+' (O ∷ m) ≡⟨ refl ⟩
(O ∷ I) b+' (O ∷ m) ≡⟨ refl ⟩
O ∷ (I b+' m) ≡⟨ refl ⟩
(I b+' (I ∷ m)) ≡⟨ lemma-I=+1 (I ∷ m) ⟩
(I ∷ m) +1' ≡⟨ refl ⟩
(I b+' (O ∷ m)) +1'
∎
lemma-+1'b+' I (I ∷ I) = refl
lemma-+1'b+' I (I ∷ O ∷ m) = refl
lemma-+1'b+' I (I ∷ I ∷ m) = refl
lemma-+1'b+' (O ∷ I) I = refl
lemma-+1'b+' (O ∷ O ∷ n) I = refl
lemma-+1'b+' (O ∷ I ∷ n) I = cong (_∷_ O) (lemma-+1'b+' (O ∷ n) I)
lemma-+1'b+' (O ∷ n) (O ∷ m) = refl
lemma-+1'b+' (O ∷ n) (I ∷ m) = refl
lemma-+1'b+' (I ∷ I) I = refl
lemma-+1'b+' (I ∷ O ∷ n) I = refl
lemma-+1'b+' (I ∷ I ∷ n) I = sym (cong (_∷_ I) (lemma-+1'b+' (O ∷ n) I))
lemma-+1'b+' (I ∷ I) (O ∷ I) = refl
lemma-+1'b+' (I ∷ I) (O ∷ O ∷ m) = cong (_∷_ O) (lemma-+1'b+' I (O ∷ m))
lemma-+1'b+' (I ∷ I) (O ∷ I ∷ m) = refl
lemma-+1'b+' (I ∷ I) (I ∷ I) = refl
lemma-+1'b+' (I ∷ I) (I ∷ O ∷ m) = cong (_∷_ I) (lemma-+1'b+' I (O ∷ m))
lemma-+1'b+' (I ∷ I) (I ∷ I ∷ m) = refl
lemma-+1'b+' (I ∷ O ∷ n) (O ∷ m) = cong (_∷_ O) (lemma-+1'b+' (O ∷ n) m)
lemma-+1'b+' (I ∷ O ∷ n) (I ∷ m) = cong (_∷_ I) (lemma-+1'b+' (O ∷ n) m)
lemma-+1'b+' (I ∷ I ∷ n) (O ∷ m) = cong (_∷_ O) (lemma-+1'b+' (I ∷ n) m)
lemma-+1'b+' (I ∷ I ∷ n) (I ∷ m) = cong (_∷_ I) (lemma-+1'b+' (I ∷ n) m)
lemma-b+'Doubling : (n : bℕ) → O ∷ n ≡ n b+' n
lemma-b+'Doubling I = refl
lemma-b+'Doubling (O ∷ n) = cong (_∷_ O) (lemma-b+'Doubling n)
lemma-b+'Doubling (I ∷ n) =
begin
O ∷ I ∷ n ≡⟨ refl ⟩
O ∷ (I ∷ n) ≡⟨ refl ⟩
O ∷ ((O ∷ n) +1') ≡⟨ cong (_∷_ O) (cong _+1' (lemma-b+'Doubling
n)) ⟩
O ∷ ((n b+' n) +1') ≡⟨ refl ⟩
(I ∷ n) b+' (I ∷ n)
∎
-- {-# NO_TERMINATION_CHECK #-}
assoc-b+' : (x y z : bℕ) → x b+' (y b+' z) ≡ (x b+' y) b+' z
assoc-b+' I y z =
begin
I b+' (y b+' z) ≡⟨ lemma-I=+1 (y b+' z) ⟩
(y b+' z) +1' ≡⟨ sym (lemma-+1'b+' y z) ⟩
y +1' b+' z ≡⟨ sym (cong (λ w → w b+' z) (lemma-I=+1 y)) ⟩
(I b+' y) b+' z
∎
assoc-b+' (O ∷ w) y z =
begin
(O ∷ w) b+' (y b+' z) ≡⟨ cong (λ x₁ → x₁ b+' (y b+' z)) (lemma-b
+'Doubling w) ⟩
(w b+' w) b+' (y b+' z) ≡⟨ sym (assoc-b+' w w (y b+' z)) ⟩
w b+' (w b+' (y b+' z)) ≡⟨ cong (_b+'_ w) (assoc-b+' w y z) ⟩
w b+' ((w b+' y) b+' z) ≡⟨ assoc-b+' w (w b+' y) z ⟩
(w b+' (w b+' y)) b+' z ≡⟨ cong (λ x₁ → x₁ b+' z) (assoc-b+' w w
y) ⟩
((w b+' w) b+' y) b+' z ≡⟨ cong (λ x₁ → (x₁ b+' y) b+' z) (sym
(lemma-b+'Doubling w)) ⟩
((O ∷ w) b+' y) b+' z
∎
assoc-b+' (I ∷ w) y z =
begin
(I ∷ w) b+' (y b+' z) ≡⟨ refl ⟩
(I b+' (O ∷ w)) b+' (y b+' z) ≡⟨ sym (assoc-b+' I (O ∷ w) (y b+'
z)) ⟩
I b+' ((O ∷ w) b+' (y b+' z)) ≡⟨ cong (_b+'_ I) (assoc-b+' (O ∷ w) y
z) ⟩
I b+' (((O ∷ w) b+' y) b+' z) ≡⟨ assoc-b+' I ((O ∷ w) b+' y) z ⟩
(I b+' ((O ∷ w) b+' y)) b+' z ≡⟨ cong (λ t → t b+' z) (assoc-b+' I
(O ∷ w) y) ⟩
((I b+' (O ∷ w)) b+' y) b+' z ≡⟨ refl ⟩
((I ∷ w) b+' y) b+' z
∎
-------------------------------------------
-----Original Message-----
From: Andreas Abel <abela at chalmers.se>
Reply-to: <andreas.abel at gu.se>
To: Hans Peter Würmli <wurmli at hispeed.ch>, agda-dev at lists.chalmers.se
Subject: Re: [Agda-dev] Termination
Date: Thu, 11 Dec 2014 22:22:40 +0100
Yes, the termination analysis is cheap in that respect, it does not see
that the call sequence
stop (I :: n) --> stop (I :: n)
is impossible. Someone (was it Jean-Yves Moyen?) suggested a smarter
static call graph construction, e.g. from
1. stop I = 1
2. stop (O ∷ n) = stop n
3. stop (I ∷ n) = 1 + stop (O ∷ n)
construct the graph
2: stop (O :: n) --> stop n
3: stop (I :: n) --> stop (O :: n)
and observe that 3 has to be followed by 2, so we get only the static
call graph
stop2 --(<)--> stop2
stop2 --(<)--> stop3
stop3 --(=)--> stop2
which we complete by adding another call
stop3 --(<)--> stop3
Now all loops are decreasing (<), and the function passes.
Such an analysis would be much more expensive, I guess. The question is
whether it is worth the effort. As you observe, you can easily rewrite
your program. Often a simpler recursion pattern also helps when you
want to prove properties of your function. I guess I'd need to see more
convincing examples, that not just contain functions that could benefit
from a smarter termination check, but also proofs about these functions
(that possibly also benefit from a smarter termination check).
Cheers,
Andreas
On 11.12.2014 05:47, Hans Peter Würmli wrote:
>
> The following simple program terminates, but the termination checker
> does not pass it:
>
> --------------------------------------------------
>
> module Termination where
>
> open import Data.Nat
>
> data Bit : Set where
> O : Bit
> I : Bit
>
> infixr 5 _∷_
>
> data bℕ : Set where
> I : bℕ
> _∷_ : Bit → bℕ → bℕ
>
> {-# NO_TERMINATION_CHECK #-}
> stop : (n : bℕ) → ℕ
> stop I = 1
> stop (O ∷ n) = stop n
> stop (I ∷ n) = 1 + stop (O ∷ n)
> -- stop (I ∷ n) = 1 + stop (n) -- this would pass the termination
> checker
>
> open import Data.Nat.Show as NShow
> open import Data.String
> open import Data.Unit using (⊤)
> open import IO.Primitive
> open import IO
>
> main : IO.Primitive.IO ⊤
> main = run (IO.putStrLn (NShow.show (stop (I ∷ O ∷ I))))
>
> ---------------------------------------------
>
> It looks like the termination checker expects a lower height in each
> recursive step instead of checking other cases first.
>
> Cheers,
>
> Hans Peter
>
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20141212/24dea642/attachment.html
More information about the Agda-dev
mailing list