4

有几个地方说所有的agda 程序都会终止。但是我可以构造一个这样的函数：

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

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

计算stall 0结果的正规形式0。计算结果stall 1会导致 Emacs 挂在看起来很像非终止循环的地方。

这是一个错误吗？或者 Agda 有时可以永远运行吗？还是发生了更微妙的事情？

4

2 回答 2

17

事实上，存在编译错误。agda可执行文件发现错误并将该信息传递到Emacsagda-mode中，然后 Emacs 会突出显示语法以让您知道有错误。我们可以看看如果我们agda直接使用会发生什么。这是我正在使用的文件：

module C1 where

open import Data.Nat

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)

这确实是编译错误。此类错误使我们无法import从其他模块中获取该模块或对其进行编译。例如，如果我们将这些行添加到上面的文件中：

open import IO

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

阳性检查失败：

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 Data.Nat

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（即类型SetisSet本身）并重构罗素悖论：

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

（来源）。我们还可以写出由 AJC Hurkens 简化的 Girard 悖论的变体：

{-# 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术语分成两个有帮助。

于 2013-08-12T14:01:00.700 回答
6

您看到的语法突出显示是编译错误。终止检查器的效果是以一种粉橙色（“鲑鱼”）突出显示非终止函数。您可能会注意到包含此类错误的模块无法从其他模块导入。它也不能编译成 Haskell。

所以是的，Agda 程序总是终止，这不是一个错误。

于 2013-08-12T05:53:28.793 回答