当我写
codatatype inftree = node nat inftree inftree
primcorec one :: inftree and two :: inftree where
"one = node 1 one two"
| "two = node 2 one two"
我明白了
"inftree" 既不与 "inftree" 相互核递归,也不是通过自身嵌套核递归
为什么,我该如何避免呢?
当我写
codatatype inftree = node nat inftree inftree
primcorec one :: inftree and two :: inftree where
"one = node 1 one two"
| "two = node 2 one two"
我明白了
"inftree" 既不与 "inftree" 相互核递归,也不是通过自身嵌套核递归
为什么,我该如何避免呢?
该命令primcorec
仅支持原始 corecursion,因此互 corecursion 仅支持相互 corecursive codatatypes。one
您的两个函数two
并不是原始的核心递归,因此不直接支持。如果更通用的命令corec
支持相互共游,它将落入其片段中,但尚未实现相互共游corec
。因此,您必须找到一个非相互的核心递归定义,然后将one
and定义two
为派生函数。规范的解决方案是使用 abool
作为参数:
primcorec one_two :: "bool => inftree" where
"one_two is_one = Node (if is_one then 1 else 2) (one_two True) (one_two False)"
definition "one = one_two True"
definition "two = one_two False"
此外,在通过共归纳法证明它们之前one
,您two
必须首先概括大多数性质。one_two