时间戳

首页 > 解决方案 > 使用 zip、ma​​p 和 products 终止递归函数的问题

isabelle - 使用 zip、ma​​p 和 products 终止递归函数的问题

问题描述

我在尝试定义使用 map over zip 的递归函数时遇到了问题。

这是我的代码的简化版本，第一个可以使用

datatype bar = Bar "bar list"

function (sequential) bar_lub :: "[bar,bar] ⇒ bar" ("_⊔b_" [30,60] 60)
  where
    "(Bar ts) ⊔b (Bar us) = Bar (map (λ(t1,t2). t1 ⊔b t2) (zip ts us))"
  by pat_completeness auto

这很好，并导致终止目标

1. ⋀ts us a b. (a, b) ∈ set (zip ts us) ⟹ P (a, b) ~ P (Bar ts, Bar us)

这很容易证明给定一个适当的P和~。

当我将列表更改为对列表时，我的问题就来了，如下

数据类型 'a foo = Foo "('a foo × 'a) 列表"

function (sequential) foo_lub1 :: "['a foo, 'a foo] ⇒ 'a foo" ("_⊔_" [30,60] 60)
  where
    "(Foo ts) ⊔ (Foo us) = Foo (map (λ((t1,_), (t2,_)). (t1 ⊔ t2, undefined)) (zip ts us))"
  by pat_completeness auto

现在，我们得到终止目标

1. ⋀ts us t1 b1 t2 b2 xc. ((t1, b1), t2, b2) ∈ set (zip ts us) ⟹ P (t1, xc) ~ P (Foo ts, Foo us)

变量xc已经出现，并且与任何事物无关。理想情况下，我希望有这个假设xc = t2，并且证明会很简单。

有谁知道为什么会发生这种情况，以及任何解决方法？

标签： isabelletermination

解决方案

这些function包使用一致性规则来确定递归调用的上下文。不幸的是，全等规则不能捕获所有类型的上下文，元组上的深度模式匹配就是这样一种失败的情况。幸运的是，有一个简单的解决方法：使用投影fst而snd不是元组抽象：

function (sequential) foo_lub1 :: "['a foo, 'a foo] ⇒ 'a foo" ("_⊔_" [30,60] 60)
  where
    "(Foo ts) ⊔ (Foo us) = Foo (map (λx. (fst (fst x) ⊔ fst (snd x), undefined)) (zip ts us))"

推荐阅读