"недопустимая функция карты" при определении базового дерева

Question

Я делаю свои первые эксперименты с codatatypeНо я застрял довольно рано. Я начал с этого определения ветвления, возможно, бесконечного дерева:

codatatype (lset: 'a) ltree = Node (lnext : "'a ⇒ 'a ltree option")

и некоторые определения работают нормально:

primcorec lempty :: "'a ltree"
  where "lnext lempty = (λ _ . None)"

primcorec single :: "'a ⇒ 'a ltree"
  where "lnext (single x) = (λ _ . None)(x := Some lempty)"

но это не работает

primcorec many :: "'a ⇒ 'a ltree"
  where "lnext (many x) = (λ _ . None)(x := Some (many x))"

как я получаю сообщение об ошибке

primcorec error:
  Invalid map function in "[x ↦ many x]"

Я мог бы обойти это, написав

primcorec many :: "'a ⇒ 'a ltree"
  where "lnext (many x) = (λ x'. if x' = x then Some (many x) else None)"

что заставляет поверить, что primcorec необходимо "что-то знать" об операторе обновления функции, аналогично тому, как fun потребности fundef_cong леммы и inductive потребности mono Леммы. Но что именно?

Answer 1

Если codatatype рекурсивно проходит через конструкторы других типов, то primcorec ожидает, что рекурсивные вызовы правильно вложены в функции отображения этих конструкторов типов. В этом примере рекурсия проходит через тип функции и тип опции, чьи функции карты op o а также map_option, Следовательно, рекурсивный вызов many должен иметь форму op o (map_option many), Следовательно, работает следующее определение:

primcorec many :: "'a ⇒ 'a ltree"
where "lnext (many x) = map_option many ∘ [x ↦ x]"

Для удобства, primcorec поддерживает еще несколько синтаксических форматов ввода. В частности, функция map для типа функции также может быть написана с использованием лямбда-абстракций. Кроме того, он поддерживает различия в регистре и ifs. Вот почему ваша вторая версия принята. Тем не менее, когда вы смотрите на сгенерированное определение many_def, вы увидите, что это сложнее, чем с явными функциями отображения.

primcorec не поддерживает регистрацию произвольных функций, поэтому вы не можете использовать fun_upd в оригинальном виде. Примитивный corecursion является синтаксическим. Может быть, в будущем будет существенный аналог function,

Функции карты описаны в руководстве по типам данных и в этой статье.