Agda程序一定会终止吗？

Question

Agda程序一定会终止吗？

4

有几个地方提到所有Agda程序都会终止。然而，我可以构造一个类似这样的函数：

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

语法高亮似乎不喜欢它，但没有编译错误。

计算 stall 0 的正常形式结果为 0。计算 stall 1 的结果会导致 Emacs 僵在一个看起来非常像非终止循环的地方。

这是一个 bug 吗？还是 Agda 有时会永远运行？还是正在发生更微妙的事情？

- user833970

2个回答

6

您所看到的语法高亮是编译错误。终止检查器的作用是以一种粉橙色（“鲑鱼色”）突出显示非终止函数。您可能会注意到，包含此类错误的模块无法从其他模块导入。它也无法编译为Haskell。因此，是的，Agda程序始终终止，这不是错误。

- Dominique Devriese

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Vitus · Accepted Answer

实际上，存在编译错误。 agda 可执行文件发现错误并将该信息传递给 Emacs 中的 agda-mode，后者会进行语法高亮以让您知道出现了错误。我们可以看一下如果直接使用 agda 会发生什么。这是我正在使用的文件：

module C1 where

open import <a href="http://vituscze.github.io/agda-stdlib-html/Data.Nat.html">Data.Nat</a>

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

现在，我们执行agda -i../lib-0.7/src -i. C1.agda命令（不要介意-i参数，它们只是让可执行文件知道标准库的位置），然后我们会收到以下错误信息：

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

这确实是编译错误。这种错误会阻止我们从其他模块中导入该模块或编译它。例如，如果我们将以下行添加到上面的文件中：

open import <a href="http://vituscze.github.io/agda-stdlib-html/IO.html">IO</a>

main = run (putStrLn "")

使用C-c C-x C-c编译模块时，agda-mode会报错：

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

其他类型的编译错误包括类型检查问题：

module C2 where

open import <a href="http://vituscze.github.io/agda-stdlib-html/Data.Bool.html">Data.Bool</a>
open import <a href="http://vituscze.github.io/agda-stdlib-html/Data.Nat.html">Data.Nat</a>

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

阳性检查失败：

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.

或未解决的元变量：

module C4 where

open import <a href="http://vituscze.github.io/agda-stdlib-html/Data.Nat.html">Data.Nat</a>

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

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

现在，您正确地注意到有些错误是“死胡同”，而其他错误则让您继续编写程序。这是因为一些错误比其他错误更糟糕。例如，如果您遇到未解决的元变量，那么您很可能只需填写缺少的信息，一切就会没问题。

至于使编译器挂起：检查或编译模块不应导致agda陷入循环。让我们尝试强制类型检查器进入循环。我们将向模块C1中添加更多内容：

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

test : loop 1 ≡ 1
test = refl

现在，为了检查refl是否是该类型的正确表达式，agda必须评估loop 1。然而，由于终止检查失败，agda将不会展开loop（并最终进入无限循环）。

然而，C-c C-n真正地强制agda尝试评估表达式（您基本上告诉它“我知道我在做什么”），因此您自然会陷入无限循环。

顺便说一下，如果禁用终止检查，您可以使agda进入循环。

{-# 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

这将最终导致：

stack overflow

作为一条经验法则：如果您可以在不使用任何编译器指示的情况下检查（或编译）一个模块而使agda陷入循环，那么这确实是一个错误，并且应该在错误跟踪器上报告。话虽如此，如果您愿意使用编译器指示，有几种方法可以制造非终止程序。我们已经看到了{-# NO_TERMINATION_CHECK #-}，这里还有一些其他的方法：

{-# 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

这个问题涉及到一个不严格为正的数据类型。或者我们可以强制agda接受Set : Set（也就是说，Set的类型是Set本身），并重构罗素悖论：

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

open import <a href="http://vituscze.github.io/agda-stdlib-html/Data.Empty.html">Data.Empty</a>
open import <a href="http://vituscze.github.io/agda-stdlib-html/Data.Product.html">Data.Product</a>
open import <a href="http://vituscze.github.io/agda-stdlib-html/Relation.Binary.PropositionalEquality.html">Relation.Binary.PropositionalEquality</a>

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₄)

(来源). 我们还可以写一个Girard悖论的变体，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)

这是一个真正的混乱，但它有一个好处，它只使用依赖函数。奇怪的是，它甚至无法通过类型检查，并导致agda循环。将整个loop术语分成两部分有所帮助。