1

我正在做我的第一次实验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引理。但究竟是什么？

4

1 回答 1

2

如果 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支持更多的语法输入格式。特别是，函数类型的映射函数也可以使用 lambda 抽象来编写。此外，它还支持大小写区分和ifs. 这就是为什么您的第二个版本被接受的原因。但是，当您查看生成的定义many_def时，您会发现它比使用显式映射函数更复杂。

primcorec不支持注册任意函数，所以不能fun_upd以原始形式使用。原始的 corecursion 是句法的。也许将来会有一个核心的对应物function.

映射函数在数据类型教程和本文中进行了解释。

于 2014-11-12T10:26:25.727 回答