Блог

Я провел несколько экспериментов со «старыми» и «новыми» способами работы с коиндукцией в Agda, но я думаю, что мне все еще не хватает некоторых важных фактов о поведении проверки завершения сорекурсивных функций Agda, когда Size они не используются.

В качестве примера рассмотрим следующие определения Stream и repeat :

 data    Stream (A : Set) : Set
record ∞Stream (A : Set) : Set where
  coinductive
  field force : Stream A
open ∞Stream

data Stream A where
  cons : A -> ∞Stream A -> Stream A

repeat : ∀{A} -> A -> ∞Stream A
force (repeat x) = cons x (repeat x)
 

Грубо говоря, коиндуктивный тип записи ∞Stream является специализированным Thunk для потоков. Я видел похожие определения во многих формализациях Agda, хотя обычно они уточняются Size для большей точности. В любом случае, приведенное выше определение repeat принимается Agda без каких-либо Size аннотаций.

Проблема заключается в том, что я пытаюсь разложить ∞Stream запись на a Thunk , чтобы я мог повторно Thunk использовать ее в другом месте для определения других потенциально бесконечных типов данных:

 record Thunk (A : Set) : Set where
  coinductive
  field force : A
open Thunk

data Stream (A : Set) : Set where
  cons : A -> Thunk (Stream A) -> Stream A

repeat : ∀{A} -> A -> Thunk (Stream A)
force (repeat x) = cons x (repeat x)
 

Обратите внимание, что:

• код для repeat точно такой же в двух случаях,
• в каждом случае рекурсивный вызов repeat находится непосредственно под конструктором cons ,
• в каждом случае repeat генерируется значение типа записи с одновременным вводом,

и все же Agda принимает первое определение repeat , но отклоняет второе (проверка завершения не удалась для следующих функций: repeat ).

Я знаю, что при использовании размера Thunk в стандартной библиотеке вторая версия может быть изменена таким образом, чтобы она была принята Agda. Тем не менее, я хотел бы понять, что делает первую версию выше настолько отличной от второй, что она проходит проверку завершения. Для меня они выглядят в основном одинаково.

Спасибо!