모든 agda 프로그램이 종료되는 곳이 몇 곳 있습니다. 그러나 다음과 같은 함수를 만들 수 있습니다 :agda 프로그램이 반드시 종료 되나요?
stall : ∀ n → ℕ
stall 0 = 0
stall x = stall x
구문 형광펜은 좋아하지 않지만 컴파일 오류가 없습니다.
stall 0의 정규형을 계산하면 0이됩니다. stall 1의 결과를 계산하면 Emacs가 멈추지 않는 루프처럼 보입니다.
이것은 버그입니까? 아니면 Agda가 때로는 영원히 달릴 수 있습니까? 아니면 좀 더 미묘한가?
실제로 컴파일 오류가 있습니다. agda 실행 파일은 오류를 찾고이 정보를 Emacs의 agda-mode으로 전달합니다.이 정보는 오류가 있음을 알려주는 구문 강조 표시입니다. 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)
이것은 실제로 컴파일 오류입니다. 이러한 오류로 인해 다른 모듈에서이 모듈을 컴파일하거나 컴파일 할 수 없습니다. 우리는 위의 파일에 다음 줄을 추가 예를 들어, :
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.
또는 미해결 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
지금, 당신은 바로, 약간의 오류가 "막 다른 골목"이있는 것으로 나타났습니다. 일부 오류는 다른 오류보다 더 나빠기 때문입니다. 예를 들어 메타베이스를 미해결로 만들면 누락 된 정보를 모두 채우면 모든 것이 정상이됩니다.
컴파일러 걸기 : 모듈을 검사하거나 컴파일하면 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을 언 롤링하지 않으며 무한 루프로 끝납니다.
그러나 실제로는이 표시됩니다. (기본적으로 "내가하는 일을 알고"라고 말하면서) 무한 루프가 발생합니다.
{-# 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 루프를 할 수있는 경우 컴파일러 pragma를 사용하지 않고 모듈을 검사 (또는 컴파일)하여 agda 루프를 만들 수 있습니다. 이것은 실제로 버그이며 bug tracker에보고해야합니다. 즉, 컴파일러 pragma를 사용하고자한다면 비 종결 프로그램을 만드는 방법은 거의 없습니다. 우리는 이미 몇 가지 다른 방법을 여기 {-# 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
이 사람은 엄격하게 긍정적되지 않는 데이터 유형에 의존한다. 아니면 Set : Set을 받아 agda을 강제로 (즉, Set의 유형 Set 자체이다)과 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을). 하지만,
{-# 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)
이 사람이 진짜 엉망입니다 : 우리는 또한 지라의 역설의 변형, simplified by A.J.C. Hurkens을 작성할 수 있습니다. 그러나 종속 함수 만 사용하는 좋은 속성이 있습니다. 이상하게도 과거 유형 검사를받지 않아서 agda이 반복됩니다. 전체 loop 용어를 두 가지로 나눕니다.
표시되는 구문 강조는 컴파일 오류입니다. 종료 검사기의 효과는 일종의 핑크 - 오렌지 색상 ("연어")으로 비 종결 기능을 강조 표시하는 것입니다. 이러한 오류가있는 모듈은 다른 모듈에서 가져올 수 없습니다. 하스켈에게 컴파일 될 수 없습니다.
그렇습니다. Agda 프로그램은 항상 종료되며 이는 버그가 아닙니다.