Do agda programs necessarily terminate?

Question

It has been stated a few places that all agda programs terminate. However I can construct a function like this:

stall : ∀ n → ℕ
stall 0 = 0
stall x = stall x

The syntax highlighter doesn't seem to like it, but there are no compilation errors.

Computing the normal form of stall 0 results in 0. Computing the result of stall 1 causes Emacs to hang in what looks a lot like a non-terminating loop.

Is this a bug? Or can Agda sometimes run forever? Or is something more subtle going on?

Answer 1

In fact, there are compilation errors. The agda executable finds an error and passes that information to agda-mode in Emacs, which in turn does the syntax highlighting to let you know there was an error. We can take a look at what happens if we use agda directly. Here's the file I'm using:

module C1 where

open import Data.Nat

loop : ℕ → ℕ
loop 0 = 0
loop x = loop x

Now, we call agda -i../lib-0.7/src -i. C1.agda (don't mind the -i parameters, they just let the executable know where to look for the standard library) and we get the error:

Termination checking failed for the following functions:
  loop
Problematic calls:
  loop x
    (at D:\Agda\tc\C1.agda:7,10-14)

This is indeed compilation error. Such errors prevent us from importing this module from other modules or compiling it. For example, if we add these lines to the file above:

open import IO

main = run (putStrLn "")

And compile the module using C-c C-x C-c, agda-mode complains:

You can only compile modules without unsolved metavariables
or termination checking problems.

---

Other kinds of compilation errors include type checking problems:

module C2 where

open import Data.Bool
open import Data.Nat

type-error : ℕ → Bool
type-error n = n
__________________________

D:\Agda\tc\C2.agda:7,16-17
ℕ !=< Bool of type Set

when checking that the expression n has type Bool

Failed positivity check:

module C3 where

data Positivity : Set where
  bad : (Positivity → Positivity) → Positivity
__________________________

D:\Agda\tc\C3.agda:3,6-16
Positivity is not strictly positive, because it occurs to the left
of an arrow in the type of the constructor bad in the definition of
Positivity.

Or unsolved metavariables:

module C4 where

open import Data.Nat

meta : ∀ {a} → ℕ
meta = 0
__________________________

Unsolved metas at the following locations:
  D:\Agda\tc\C4.agda:5,11-12

---

Now, you rightly noticed that some errors are "dead ends", while others let you carry on writing your program. That's because some errors are worse than others. For example, if you get unsolved metavariable, chances are that you'll be able to just fill in the missing information and everything will be okay.

As for hanging the compiler: checking or compiling a module shouldn't cause agda to loop. Let's try to force the type checker to loop. We'll add more stuff into the module C1:

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

test : loop 1 ≡ 1
test = refl

Now, to check that refl is correct expression of that type, agda has to evaluate loop 1. However, since the termination check failed, agda will not unroll loop (and end up in an infinite loop).

However, C-c C-n really forces agda to try to evaluate the expression (you basically tell it "I know what I'm doing"), so naturally you get into an infinite loop.

---

Incidentally, you can make agda loop if you disable the termination check:

{-# NO_TERMINATION_CHECK #-}
loop : ℕ → ℕ
loop 0 = 0
loop x = loop x

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

test : loop 1 ≡ 1
test = refl

Which ends up in:

stack overflow

---

As a rule of thumb: if you can make agda loop by checking (or compiling) a module without using any compiler pragmas, then this is indeed a bug and should be reported on the bug tracker. That being said, there are few ways to make non-terminating program if you are willing to use compiler pragmas. We've already seen {-# NO_TERMINATION_CHECK #-}, here are some other ways:

{-# OPTIONS --no-positivity-check #-}
module Boom where

data Bad (A : Set) : Set where
  bad : (Bad A → A) → Bad A

unBad : {A : Set} → Bad A → Bad A → A
unBad (bad f) = f

fix : {A : Set} → (A → A) → A
fix f = (λ x → f (unBad x x)) (bad λ x → f (unBad x x))

loop : {A : Set} → A
loop = fix λ x → x

This one relies on a data type which is not strictly positive. Or we could force agda to accept Set : Set (that is, the type of Set is Set itself) and reconstruct Russell's paradox:

{-# OPTIONS --type-in-type #-}
module Boom where

open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality

data M : Set where
  m : (I : Set) → (I → M) → M

_∈_ : M → M → Set
a ∈ m I f = Σ I λ i → a ≡ f i

_∉_ : M → M → Set
a ∉ b = (a ∈ b) → ⊥

-- Set of all sets that are not members of themselves.
R : M
R = m (Σ M λ a → a ∉ a) proj₁

-- If a set belongs to R, it does not contain itself.
lem₁ : ∀ {X} → X ∈ R → X ∉ X
lem₁ ((Y , Y∉Y) , refl) = Y∉Y

-- If a set does not contain itself, then it is in R.
lem₂ : ∀ {X} → X ∉ X → X ∈ R
lem₂ X∉X = (_ , X∉X) , refl

-- R does not contain itself.
lem₃ : R ∉ R
lem₃ R∈R = lem₁ R∈R R∈R

-- But R also contains itself - a paradox.
lem₄ : R ∈ R
lem₄ = lem₂ lem₃

loop : {A : Set} → A
loop = ⊥-elim (lem₃ lem₄)

(source). We could also write a variant of Girard's paradox, simplified by A.J.C. Hurkens:

{-# OPTIONS --type-in-type #-}
module Boom where

⊥   = ∀ p → p
¬_  = λ A → A → ⊥
℘_  = λ A → A → Set
℘℘_ = λ A → ℘ ℘ A

U = (X : Set) → (℘℘ X → X) → ℘℘ X

τ : ℘℘ U → U
τ t = λ (X : Set) (f : ℘℘ X → X) (p : ℘ X) → t λ (x : U) → p (f (x X f))

σ : U → ℘℘ U
σ s = s U λ (t : ℘℘ U) → τ t

τσ : U → U
τσ x = τ (σ x)

Δ = λ (y : U) → ¬ (∀ (p : ℘ U) → σ y p → p (τσ y))
Ω = τ λ (p : ℘ U) → ∀ (x : U) → σ x p → p x

loop : (A : Set) → A
loop = (λ (₀ : ∀ (p : ℘ U) → (∀ (x : U) → σ x p → p x) → p Ω) →
  (₀ Δ λ (x : U) (₂ : σ x Δ) (₃ : ∀ (p : ℘ U) → σ x p → p (τσ x)) →
  (₃ Δ ₂ λ (p : ℘ U) → (₃ λ (y : U) → p (τσ y)))) λ (p : ℘ U) →
  ₀ λ (y : U) → p (τσ y)) λ (p : ℘ U) (₁ : ∀ (x : U) → σ x p → p x) →
  ₁ Ω λ (x : U) → ₁ (τσ x)

This one is a real mess, though. But it has a nice property that it uses only dependent functions. Strangely, it doesn't even get past type checking and causes agda to loop. Splitting the whole loop term into two helps.