С оговорками, скрывающими прекращение действия

Я пытаюсь определить двоичные числа в agda, но agda не видит, что ⟦_⇑⟧ завершается. Я действительно не хочу разрывать отношения доступности. Как я могу показать agda, что n становится меньше?

module Binary where

open import Data.Nat using (ℕ; _+_; +-suc)
open ℕ

2* : ℕ → ℕ
2* n = n + n

data Parity : ℕ → Set where
  ???? : ∀ k → Parity (2* k)
  ???? : ∀ k → Parity (1 + 2* k)

parity : ∀ n → Parity n
parity zero = ???? 0
parity (suc n) with parity n
parity (suc .(k + k)) | ???? k = ???? k
parity (suc .(suc (k + k))) | ???? k rewrite sym (+-suc k k) = ???? (suc k)

data ???? : Set where
  ???? : ????
  ???? : ???? → ????
  ???? : ???? → ????

⟦_⇓⟧ : ???? → ℕ
⟦ ???? ⇓⟧ = 0
⟦ ???? b ⇓⟧ = 2* ⟦ b ⇓⟧
⟦ ???? b ⇓⟧ = 1 + 2* ⟦ b ⇓⟧

⟦_⇑⟧ : ℕ → ????
⟦ zero ⇑⟧ = ????
⟦ suc n ⇑⟧ with parity n
⟦ suc .(k + k) ⇑⟧ | ???? k = ???? ⟦ k ⇑⟧
⟦ suc .(suc (k + k)) ⇑⟧ | ???? k = ???? ⟦ k ⇑⟧

Ошибка:

Termination checking failed for the following functions:
  ⟦_⇑⟧
Problematic calls:
  ⟦ k ⇑⟧

agda non-termination
person Kyle McKean    schedule 11.11.2019    source источник
comment
Что значит не хочешь разорвать прочные отношения? Вы имеете в виду, что не хотите их использовать или не хотите учиться? Поскольку в вашем конкретном случае, поскольку ваш рекурсивный вызов не выполняется на аргументе структурно меньшего размера, у вас нет другого выбора, кроме как использовать их. К счастью, они есть в стандартной библиотеке. Я могу показать вам, как их использовать, при условии, что вы этого хотите. Теперь, когда я подумал об этом, есть еще одно решение, которое состоит в том, чтобы отключить проверку завершения для этого определения с помощью связанной прагмы, но я настоятельно рекомендую вам не использовать этот вариант.   -  person MrO    schedule 13.11.2019
comment
Я умею использовать хорошо выстроенные отношения. id просто хотелось бы, чтобы их не заставляли использовать все время. мне кажется, что он структурно убывает, но agda этого не видит. он разворачивает по крайней мере один успех за каждый вызов функции.   -  person Kyle McKean    schedule 13.11.2019
comment
Это определенно не структурно рекурсивно. Позвольте мне дать ответ, а не комментарий, чтобы объяснить вам, почему.   -  person MrO    schedule 13.11.2019

Ответы (1)


arrow_upward
3
arrow_downward

Проверка завершения не выполняется по уважительным причинам, поскольку следующая функция не является структурно рекурсивной при вводе:

⟦_⇑⟧ : ℕ → ????
⟦ zero ⇑⟧ = ????
⟦ suc n ⇑⟧ with parity n
⟦ suc .(k + k) ⇑⟧ | ???? k = ???? ⟦ k ⇑⟧
⟦ suc .(suc (k + k)) ⇑⟧ | ???? k = ???? ⟦ k ⇑⟧

Agda даже сообщает вам, в чем проблема: ⟦ k ⇑⟧. (в данном случае таких некорректных вызовов два).

Хотя я согласен, может выглядеть, что функция вызывается для аргумента структурно меньшего размера, но это не так. Чтобы понять почему, вы должны увидеть, что k используется в качестве входных данных для вызова функции _+_, и что только результат этой функции структурно меньше n, а не сам k. И у agda нет возможности узнать следующее свойство о _+_:

∀ {n} → n < suc (n + n)

Если вы предоставите доказательство такой леммы, вы можете использовать тот факт, что _<_ хорошо обоснован, чтобы сделать вашу функцию структурно рекурсивной по сравнению с Acc, но, похоже, вы не хотите этого делать.

Простой способ понять, почему Agda не может узнать об этом, заключается в следующем: представьте, что вы заменяете suc .(k + k) на suc .(a ∸ b) и рекурсивно вызываете свою функцию поверх a. С точки зрения agda, оба случая являются одними и теми же, и в этом случае он обычно не завершается, если b не совпадает с 0.

Вот модуль, исправленный в части прекращения действия:

module Binary where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Induction.Nat
open import Induction.WellFounded

2* : ℕ → ℕ
2* n = n + n

data Parity : ℕ → Set where
  ???? : ∀ k → Parity (2* k)
  ???? : ∀ k → Parity (1 + 2* k)

parity : ∀ n → Parity n
parity zero = ???? 0
parity (suc n) with parity n
parity (suc .(k + k)) | ???? k = ???? k
parity (suc .(suc (k + k))) | ???? k rewrite sym (+-suc k k) = ???? (suc k)

data ???? : Set where
  ???? : ????
  ???? : ???? → ????
  ???? : ???? → ????

⟦_⇓⟧ : ???? → ℕ
⟦ ???? ⇓⟧ = 0
⟦ ???? b ⇓⟧ = 2* ⟦ b ⇓⟧
⟦ ???? b ⇓⟧ = 1 + 2* ⟦ b ⇓⟧

decr : ∀ {n} → n < suc (n + n)
decr {n} = s≤s (m≤m+n n n) 

helper : (n : ℕ) → Acc _<_ n → ????
helper zero a = ????
helper (suc n) a with parity n
helper (suc .(k + k)) (acc rs) | ???? k = ???? (helper k (rs _ decr))
helper (suc .(suc (k + k))) (acc rs) | ???? k = ???? (helper k (rs _ (s≤s (<⇒≤ decr))))

⟦_⇑⟧ : ℕ → ????
⟦ n ⇑⟧ = helper n (<-wellFounded n)

Я тоже скептически относился к правильности ваших определений и оказался прав, например, учитывая следующее определение:

test : ℕ
test = ⟦ ⟦ 124 ⇑⟧ ⇓⟧

Agda возвращает 2 при оценке test.

Учитывая определение:

test₁ : ℕ
test₁ = ⟦ ⟦ 16 ⇑⟧ ⇓⟧

Agda возвращает 14 при оценке test₁

Чтобы исправить свои определения, вы можете вдохновиться тем, что сделано в стандартной библиотеке, либо в модуле Data.Bin (не рекомендуется), либо в модуле Data.Nat.Binary, в зависимости от того, какая версия stdlib у вас установлена.

person MrO    schedule 13.11.2019
comment
Связанный вопрос: stackoverflow.com/questions/58846127/ - person Sassa NF; 14.11.2019