在 Isabelle 中证明 Takeuchi 函数的终止

Question

这是我试图证明Takeuchi function 确实terminate：

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

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

我该如何解决这个问题？

Answer 1

首先，您的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.pinduct 轻松证明tk 函数的部分正确性定理：

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 在值 (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。