Программы agda обязательно заканчиваются?
В нескольких местах было указано, что все программы agda завершаются. Однако я могу построить такую функцию:
stall : ∀ n → ℕ
stall 0 = 0
stall x = stall x
Подсветка синтаксиса, кажется, не нравится, но нет ошибок компиляции.
Вычисление нормальной формы stall 0 результаты в 0, Вычисление результата stall 1 заставляет Emacs зависать во внешнем цикле.
Это ошибка? Или Агда иногда бежит вечно? Или происходит что-то более тонкое?
2 ответа
На самом деле, есть ошибки компиляции. 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₄)
( источник). Мы могли бы также написать вариант парадокса Жирара, упрощенный 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 Термин на две подсказки.
Подсветка синтаксиса, которую вы видите, является ошибкой компиляции. Эффект проверки завершения заключается в выделении не завершающих функций в виде розово-оранжевого цвета ("лосось"). Вы можете заметить, что модуль, содержащий такую ошибку, не может быть импортирован из других модулей. Он также не может быть скомпилирован в Haskell.
Так что да, программы Agda всегда завершаются, и это не ошибка.