I'm trying to define binary numbers in agda but agda cant see that ⟦_⇑⟧
is terminating. I really dont want to have to break out accessibility relations. How can I show agda that n gets smaller?
module Binary where
open import Data.Nat using (ℕ; _+_; +-suc)
open ℕ
2* : ℕ → ℕ
2* n = n + n
data Parity : ℕ → Set where
: ∀ k → Parity (2* k)
: ∀ k → Parity (1 + 2* k)
parity : ∀ n → Parity n
parity zero = 0
parity (suc n) with parity n
parity (suc .(k + k)) | k = k
parity (suc .(suc (k + k))) | k rewrite sym (+-suc k k) = (suc k)
data : Set where
:
: →
: →
⟦_⇓⟧ : → ℕ
⟦ ⇓⟧ = 0
⟦ b ⇓⟧ = 2* ⟦ b ⇓⟧
⟦ b ⇓⟧ = 1 + 2* ⟦ b ⇓⟧
⟦_⇑⟧ : ℕ →
⟦ zero ⇑⟧ =
⟦ suc n ⇑⟧ with parity n
⟦ suc .(k + k) ⇑⟧ | k = ⟦ k ⇑⟧
⟦ suc .(suc (k + k)) ⇑⟧ | k = ⟦ k ⇑⟧
Error:
Termination checking failed for the following functions:
⟦_⇑⟧
Problematic calls:
⟦ k ⇑⟧
Termination checking fails for good reasons, since the following function is not structurally recursive over its input:
Agda even tells you what is the problematic call :
⟦ k ⇑⟧
. (in this case, there are two of these ill-formed calls).While I agree it might look that the function is called on a structurally smaller argument it's not the case. To understand why, you have to see that
k
is used as input for a function call,_+_
, and that only the result of this function is structurally smaller thann
, notk
itself. And agda has no way of knowing the following property about_+_
:Should you provide a proof of such lemma, you could use the fact that
_<_
is well founded to make your function structurally recursive overAcc
, but it seems you are reluctant to do so.An easy way to understand why Agda cannot know that this terminates is the following: imagine you replace
suc .(k + k)
bysuc .(a ∸ b)
and recursively call your function overa
. From agda's point of view, both are the same cases, and in this case, it does not usually terminate unlessb
happens to be0
.Here is the module corrected in terms of termination :
I was also skeptical about the correctness of your definitions and it turns out I was right, for instance, considering the following definition:
Agda returns
2
when evaluatingtest
.Considering the definition:
Agda returns
14
when evaluatingtest₁
In order to correct your definitions, you can take inspiration from what is done in the standard library, either in the module Data.Bin (deprecated) or in the module Data.Nat.Binary depending on which version of the stdlib you have.