CODEWITHSUNDEEP
agda
rampion
rampion

Reputation: 89053

How to convince the Agda compiler that an expression terminates?

I'm learning Agda using Philip Wadler's Programming Language Foundations In Agda, and I can't figure out how to convince the compiler that a computation terminates.

I've got types for unary and binary naturals:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

And I wrote a function to convert between the two representations (using some helpers):

-- try to count to a given power of two
--
-- to-count m t f n =
--    t (n - 2^m)     if n >= 2^m
--    (f * 2^m) + n   otherwise
to-count : ℕ → (ℕ → Bin) → Bin → ℕ → Bin
to-count zero    t f zero    = f
to-count zero    t f (suc n) = t n
to-count (suc m) t f n       = to-count m (to-count m t (f I)) (f O) n

-- keep trying to count bigger and bigger powers of two
to-next : ℕ → ℕ → Bin
to-next m = to-count m (to-next (suc m)) (⟨⟩ I)

to : ℕ → Bin
to = to-count zero (to-next zero) ⟨⟩

Later, when trying to prove that my conversion is faithful:

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

_ : to zero ≡ ⟨⟩
_ = refl

_ : to (suc zero) ≡ ⟨⟩ I
_ = refl

The compiler complains that termination checking failed:

Checking Naturals (Naturals.agda).
Naturals.agda:23,1-24,48
Termination checking failed for the following functions:
  to-next
Problematic calls:
  to-next (suc m)
    (at Naturals.agda:24,25-32)
Naturals.agda:37,5-9
to-next zero zero != ⟨⟩ I of type Bin
when checking that the expression refl has type
to (suc zero) ≡ (⟨⟩ I)

What are some strategies I can use to help convince the compiler that it terminates?

Upvotes: 1

Views: 395

Answers (2)

Sassa NF
Sassa NF

Reputation: 5406

Using pragma is not how you need to convince the compiler that the function terminates.

The compiler indicated the problematic call: to-next (suc m) cannot be seen as unused in the cases you think, and obviously it creates a structurally bigger value than on input.

A way to deal with this problem is express the construction of Bin from ℕ differently.

inc-bin : Bin -> Bin
inc-bin ⟨⟩ = ⟨⟩ I
inc-bin (bb O) = bb I
inc-bin (bb I) = (inc-bin bb) O

to-bin-daft : ℕ -> Bin
to-bin-daft zero = b O
to-bin-daft (suc m) = inc-bin (to-bin-daft m)

This is "daft", as it literally increments Bin by one at a time, for every suc, but more complex algorithms involving, say, division by 2, require evidence that the result of division is smaller than the input.

Upvotes: 2

rampion
rampion

Reputation: 89053

Not sure if this is the most idiomatic solution, but I got it working using the TERMINATING pragma:

{-# TERMINATING #-}
to-next : ℕ → ℕ → Bin
to-next m = to-count m (to-next (suc m)) (⟨⟩ I)

Upvotes: 1

Related Questions