代码之家 › 专栏 › 技术社区 › user1868607

证明Takeuchi函数在Isabelle中终止

termination isabelle

0

user1868607 · 技术社区 · 6 年前

这是我试图证明的 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 )

我怎么修这个?

1 回复 | 直到 6 年前

1

2

Manuel Eberl 6 年前

首先,你的 moore 函数当前不返回三元组,但函数接受两个 int 然后返回 int . 如果是三人组,你就得写 int Ã int Ã int . 此外,元组的构造为 (x, y, z) ,而不是 x y z 就像你一样。

而且,没有理由使用 fun (更不用说) function )定义 穆尔 函数,因为它不是递归的。 definition 工作良好。为了 tk ,另一方面,您需要使用 功能 因为没有明显的辞书终止措施。

另外,在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 终止于值 (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 .