agda程序必须终止吗？

Question

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

stall : ? n ? ?
stall 0 = 0
stall x = stall x

语法高亮显示器似乎不喜欢它,但没有编译错误.

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

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

Answer 1

实际上,存在编译错误.该agda可执行文件中发现了错误,并传递这些信息agda-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(即,类型Set是Set本身)和重建罗素悖论:

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

(来源).我们还可以编写一个Girard悖论的变体,由AJC 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术语拆分为两个有助于.

Answer 2

您看到的语法突出显示是编译错误.终止检查器的作用是突出显示一种粉红橙色("鲑鱼")的非终止功能.您可能会注意到无法从其他模块导入包含此类错误的模块.它也不能编译成Haskell.

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