找不到字典终止顺序

Question

type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"
fun LTS_is_reachable :: "('q, 'a) LTS  \<Rightarrow> 'q \<Rightarrow> 'a list \<Rightarrow> 'q \<Rightarrow> bool" where
   "LTS_is_reachable \<Delta> q [] q' = (q = q')"|
   "LTS_is_reachable \<Delta> q (a # w) q' = 
      (\<exists>q''. (if (q,{},q'') \<in> \<Delta> then LTS_is_reachable \<Delta> q'' (a # w) q' else (\<exists> \<sigma>. (a \<in> \<sigma> \<and> (q, \<sigma>, q'') \<in> \<Delta> \<and> LTS_is_reachable \<Delta> q'' w q'))))"

在这里，我只想定义一个带有三元组、初始状态、列表和最终状态的转换标记系统。函数LTS_is_reachable是检查是否存在从初态到终态的路径。三元组中的元素可以是 (q,{a,b},p) 这意味着如果我们可以得到 a 或 b，状态 a 将转换为状态 b。另外 (q,{},p) 意味着我们不需要任何操作，状态 a 将自动转换为状态 b。我的问题在于如何定义后面的转换。这对我来说听起来很难。

Isabelle 中的上述定义警告无法找到词典终止顺序。任何帮助将不胜感激。

Answer 1

要定义一个递归函数，它必须是终止的。你得到的错误意味着 Isabelle 无法自动证明你的函数正在终止。

确实，LTS_is_reachable \<Delta> q (a # w) q' 调用了 LTS_is_reachable \<Delta> q'' (a # w) q'。实际上（伊莎贝尔和我）都不清楚这是否会终止。

一般情况下有以下几种解决方法：

函数确实被 Isabelle 终止，无法自动找到它。请参阅功能文档。
它不会终止，但您不需要该函数可执行。您可以使用归纳谓词。
它不会终止，但您需要函数可执行。您可以使用燃料的概念：您运行 up-to 燃料步骤。然后，如果您将燃料设置得足够高，一切都会顺利进行。这很少是最好的方法，但有时是必需的。

在您的情况下，归纳谓词听起来是个不错的方法。

Answer 2

这个概念绝对应该形式化为归纳谓词。然后，在假设涉及 LTS_is_reachable.

的情况下，您将拥有用于证明 LTS_is_reachable 实例的工具，并反过来通过归纳法证明事实

而且不需要证明终止。

找不到字典终止顺序

Could not find lexicographic termination order

isabelle