agda程序是否必然终止？ [英] Do agda programs necessarily terminate?

问题描述

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

  stall：∀n→ℕ
 stall 0 = 0 
摊位x =摊位x 
  

语法荧光笔似乎不喜欢，但没有编译错误

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

这是一个bug吗？还是Agda有时会永远运行？或者是更微妙的事情？

解决方案

其实有编译错误。 agda 可执行文件发现错误，并将该信息传递给Emacs中的 agda-mode ，这反过来又使语法突出显示让你知道有一个错误。我们可以看看如果直接使用 agda 会发生什么。这是我使用的文件：

 模块C1其中
 
打开导入Data.Nat  
 
 loop：ℕ→ℕ
 loop 0 = 0 
循环x =循环x 
  

现在，我们调用 agda -i ../ lib-0.7 / src -i。 C1.agda （不介意 -i 参数，他们只是让可执行文件知道在哪里查找标准库），我们得到错误：

 以下功能的终止检查失败：
 loop 
有问题的电话：
循环x 
（在D：\Agda\tc\C1.agda：7,10-14）
  

这确实是编译错误。这样的错误阻止我们从其他模块中导入 import 来编译该模块。例如，如果我们将这些行添加到上面的文件中：

 打开导入IO  
 
 main = run（putStrLn）
  

使用 Cc Cx Cc ， agda-mode 抱怨：

 您只能编译没有未解析的元变量
或终止检查问题的模块。 
  

---

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

 模块C2其中
 
打开导入 DataBool  
打开导入 Data.Nat  
 
类型错误：ℕ→Bool 
类型错误n = n 
 __________________________ 
 
 D：\Agda\tc\C2.agda：7,16-17 
ℕ！=<当检查表达式n具有类型Bool 
  

时，设置

的Bool失败的积极性检查：

 模块C3其中
 
数据正性：设置在哪里
 bad： （积极性→积极性）→积极性
 __________________________ 
 
 D：\Agda\tc\C3.agda：3,6-16 
积极性不是严格的，因为它发生在
的左边
的构造函数类型在
 Positiveivity的定义中不好。 
  

或未解决的元变量：

 模块C4其中
 
打开导入数据。 Nat  
 
 meta：∀{a}→ℕ
 meta = 0 
 __________________________ 
 
以下位置未解决的元数据：
 D：\Agda\tc\C4.agda：5,11-12 
  

---

现在，您正确地注意到一些错误是死胡同，而其他错误则让您继续编写程序。这是因为一些错误比其他错误更糟糕。例如，如果您获得未解决的元变量，那么可能只需填写缺失的信息，一切都将可行。

关于挂起编译器：检查或编译模块不应该导致 agda 循环。我们试图强制类型检查器循环。我们将在模块中添加更多的内容 C1 ：

  data _ ≡_{a} {A：Set a}（x：A）：A→设置一个地方
 refl：x≡x 
 
 test：loop 1≡1 
 test = refl 
  

现在，检查 refl 是该类型的正确表达式， agda 必须评估循环1 。但是，由于终止检查失败， agda 将不会展开 loop （最终在无限循环中）。 / p>

但是， Cc Cn 真的强制 agda 尝试评估表达式（你基本上告诉它我知道我正在做什么），所以你自然会进入无限循环。

---

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

  { - ＃NO_TERMINATION_CHECK＃ - } 
循环：ℕ→ℕ
循环0 = 0 
循环x =循环x 
 
数据_≡_ {a} {A：设置一个}（x：A）：A→设置一个位置
 refl：x≡x 
 
测试：循环1≡1 
 test = refl 
  

最终结论如下：

 堆栈溢出
  

---

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

  { - ＃选项 - 无积分检查＃ - } 
模块Boom其中
 
数据坏（A：设置）：设置其中
坏：（坏A→A）→坏A 
 
 unBad：{A：设置}→坏A→坏A→A 
 unBad（坏f）= f 
 
 fix：{A：Set}→（A→A）→A 
 fix f =（λx→f（unBad xx））（badλx→f（unBad xx））
 
循环：{A：Set}→A 
 loop = fixλx→x 
  

这一个依赖于不是严格正面的数据类型。或者我们可以强制 agda 接受 Set：Set （即， Set的类型是设置本身），并重建罗素的悖论：

  { - ＃选项 -  type-in​​-type＃ - } 
模块
 
打开导入 Data.Empty  
打开导入 Data.Product  
打开导入Relation.Binary.PropositionalEquality  
 
数据M：设置其中
m :(（ I：Set）→（I→M）→M 
 
_∈_：M→M→Set 
a∈m I f =ΣIλi→a≡fi 
 
_∉_：M→M→Set 
a∉b =（a∈b）→⊥
 
  - 设置不是自己成员的所有集合。 
 R：M 
 R = m（ΣMλa→a∉a）proj 1 
 
  - 如果一个集合属于R，它不包含自身。 
 lem 1：∀{X}→X∈R→X∉X 
 lem 1（（Y，Y∉Y），refl）=Y∉Y
 
  - 如果集合不包含自身，那么它在R. 
 lem 2：∀{X}→X∉X→X∈R 
 lem 2X∉X=（_，X∉X），refl 
 
  -  R不包含自身。 
 lem 3：R∉R 
 lem 3R∈R= lem 1R∈RR∈R
 
  - 但是R也包含自己 - 一个悖论。 
 lem 4：R∈R 
 lem 4 = lem2 lem 3 
 
 loop：{A：Set}→A 
 loop =⊥-elimination（lem 3 lem 4）
  

（source ）。我们还可以写出一个Girard悖论的变体，由AJC Hurkens进行简化：

  { - ＃选项 -  type-in​​-type＃ - } 
模块Boom其中
 
⊥ =∀p→p 
¬_=λA→A→⊥
℘_=λA→A→设定
℘℘_=λ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）→σyp→p（τσy））
Ω=τλ（p：℘U）→∀（x： →σxp→px 
 
 loop：（A：Set）→A 
 loop =（λ（₀：∀（p：℘U）→（∀（x：U）→σ （x：U）（2：σ×Δ）（3：∀（p：℘U）→σ xp→p（τσx））→
（3Δ₂λ（p：℘U）→（3λ（y：U）→p（τσy））））λ（p：℘U）→ 
 0λ（y：U）→p（τσy））λ（p：℘U）（1：∀（x：U）→σxp→px） ：U）→¹（τσx）
  

虽然这是一个真正的混乱。但它有一个很好的属性，它只使用依赖函数。奇怪的是，它甚至没有经过类型检查，导致 agda 循环。将整个循环术语分为两个帮助。

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?

解决方案

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.

这篇关于agda程序是否必然终止？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！