时间戳

首页 > 解决方案 > 在 Isabelle 中证明 Takeuchi 函数的终止

isabelle - 在 Isabelle 中证明 Takeuchi 函数的终止

问题描述

这是我证明Takeuchi 函数确实终止的尝试：

function moore :: "(int ⇒ int ⇒ int) ⇒ (int ⇒ int ⇒ int)" where
"moore x y z = ((if (x ≤ y) then 0  else 1) (max(x,y,z) - min(x,y,z)) (x - min(x,y,z)))"


fun tk :: "int ⇒ int ⇒ int ⇒ int" where
"tk x y z = ( if x ≤ y then y else tk (tk (x-1) y z) (tk (y-1) z x) (tk (z-1) x y) )"

这里有几个问题。首先我应该在函数 moore 中返回一个三元组。现在，系统正在抱怨错误：

类型统一失败：类型“int”和“_ ⇒ _”的冲突

应用程序中的类型错误：不兼容的操作数类型

运算符：op ≤ x :: (int ⇒ int ⇒ int) ⇒ bool 操作数：y :: int

那么，终止证明当然不会成功，因为我没有应用上面的终止函数（实现方式应该类似于这里）。

我怎样才能解决这个问题？

标签： isabelletermination

解决方案

首先，您的moore函数当前不返回三元组，而是一个接受两个ints 并返回一个的函数int。对于三元组，您必须编写int × int × int. 此外，元组的构造为(x, y, z)，而不是x y z像您所做的那样。

此外，没有理由使用fun（更不用说function）来定义moore函数，因为它不是递归的。definition工作正常。tk另一方面，因为没有明显的词典终止措施，您将需要使用function。

此外，返回三元组的函数在 Isabelle 中处理起来通常有点难看。定义三个单独的函数更有意义。将所有这些放在一起，您可以像这样定义您的函数：

definition m1 where "m1 = (λ(x,y,z). if x ≤ y then 0 else 1)"
definition m2 where "m2 = (λ(x,y,z). nat (Max {x, y, z} - Min {x, y, z}))"
definition m3 where "m3 = (λ(x,y,z). nat (x - Min {x, y, z}))"

function tk :: "int ⇒ int ⇒ int ⇒ int" where
  "tk x y z = ( if x ≤ y then y else tk (tk (x-1) y z) (tk (y-1) z x) (tk (z-1) x y))"
  by auto

tk然后，您可以使用部分归纳规则轻松证明函数的部分正确性定理tk.pinduct：

lemma tk_altdef:
  assumes "tk_dom (x, y, z)"
  shows   "tk x y z = (if x ≤ y then y else if y ≤ z then z else x)"
  using assms by (induction rule: tk.pinduct) (simp_all add: tk.psimps)

tk_dom (x, y, z)假设说tk终止于values (x, y, z)。

现在，如果我正确阅读了您链接的论文，终止证明的模板如下所示：

termination proof (relation "m1 <*mlex*> m2 <*mlex*> m3 <*mlex*> {}", goal_cases)
  case 1
  show "wf (m1 <*mlex*> m2 <*mlex*> m3 <*mlex*> {})"
    by (auto intro: wf_mlex)
next
  case (2 x y z)
  thus ?case sorry
next
  case (3 x y z)
  thus ?case sorry
next
  case (4 x y z)
  thus ?case sorry
next
  case (5 x y z)
  thus ?case sorry
qed

在此处的最后四种情况下，您将必须进行实际工作来显示度量减少。运算符将<*mlex*>几个度量组合成一个字典度量。显示某物包含在该度量中的相关规则是mlex_less和mlex_le。

推荐阅读