[Agda] Compositional termination
Karn Kallio
tierpluspluslists at gmail.com
Tue Sep 25 18:50:49 CEST 2012
My first encounter with noncompositional termination was while writing some
parser combinators while threading a termination counter so as to escape from
proof obligations. Looking at the resulting definitions along the lines of
loop₁ : Char → ℕ → Maybe Char
loop₁ x zero = nothing
loop₁ x (suc n) = loop₁ x n
zig : Char → ℕ → Maybe Char
zag : Char → ℕ → Maybe Char
zig x zero = nothing
zig x (suc n) = zag x n
zag x zero = nothing
zag x (suc n) = zig x n
I wanted to have a termination counter weak or quasi monad (the left and right
unit laws fail, so not a monad)
M : Set → Set
M A = ℕ → Maybe A
q-return : ∀ {A} → A → M A
q-return x = λ n → just x
_q->>=_ : ∀ {A B} → M A → (A → M B) → M B
_q->>=_ m f zero = nothing
_q->>=_ m f (suc n) = m n >>= λ x → f x n
where open RawMonad monad
But then the termination checker does not "see through" applications of
quasibind, so [loop] below does not terminate:
loop : Char → M Char
loop x = q-return x q->>= loop
so I was stuck with expanding out quasibind manually.
More information about the Agda
mailing list