伊莎贝尔列表提升和压缩

Question

需要从 Isabelle 的两个集合中创建第三个列表，其中的元素形式为 (a, b)，其中 a 来自第一个集合，b 在第二个集合中。此外，最后一组中的元素必须按某些条件进行过滤。

代码：

theory Scratch
imports Main Nat
begin 
  value "let a = {(1::int), 2, 3, 4} in (let b = {(6::int),7,8,9} in 
    ((1::int), 6) ∈ set (filter (λ el . (snd el) < 8) [(n,m). n ∈ a ∧ m ∈ b]))"
end

我预期的结果是对还是错。结果是：

"(1, 6)
 ∈ set [u←if (1 = n ∨ 2 = n ∨ 3 = n ∨ 4 = n) ∧ 
             (6 = m ∨ 7 = m ∨ 8 = m ∨ 9 = m) 
          then [(n, m)] else [] . snd u < 8]"
  :: "bool"

为什么结果不等于 True/False 值？
是否可以编写在集合而不是列表上计算过滤器函数的代码？

Answer 1

首先，您不能将集合转换为列表。列表具有特定的元素顺序；集没有。

问题 1

这是因为您在其中有自由变量：n 和 m。表达式 [(n,m). n ∈ a ∧ m ∈ b] 基本上意味着 if n ∈ a ∧ m ∈ b then [(n,m)] else []。这不是你想要的。

如果 a 和 b 是列表，您可以使用列表理解语法 [(n,m). n ← a, m ← b]。然而，由于 a 和 b 是集合，这不可能工作，因为结果将是一个具有特定顺序的列表，而该顺序必须来自某处 – 但是 a 和 b 作为集合没有这样的顺序。

问题 2

在形式化中，最好的方法是首先抽象地定义事物，而不使用过于具体的数据结构。如果您不需要维护值的特定顺序，请使用集合，而不是列表。然后您可以稍后将其从集合优化为列表以获得可执行（和高效）代码。

伊莎贝尔code generation manual中有一节是关于提炼的。我推荐你看看。

也就是说，对使用集生成代码的支持有限。然后集合在内部表示为列表，并且大多数基本操作都有效，但代码生成有时可能会失败——一般来说，并非所有集合上的操作都是可计算的。有一个函数 Set.filter，它是可执行的，并且基本上与常规 filter 函数对列表所做的相同。

但是，由于排序错误，以下操作将失败：

value "let a = {(1::int), 2, 3, 4} in (let b = {(6::int),7,8,9} in 
    ((1::int), (6 :: int)) ∈ Set.filter (λ el . (snd el) < 8) {x. fst x ∈ a ∧ snd x ∈ b})"

这是因为集合推导（即 {x. … }）通常是不可计算的。您必须将此 {x. fst x ∈ a ∧ snd x ∈ b} 替换为代码生成器可以为其生成代码的内容。在这种情况下，这很容易，因为这个操作只是笛卡尔积。你可以这样写：

value "let a = {(1::int), 2, 3, 4} in (let b = {(6::int),7,8,9} in 
    ((1::int), (6 :: int)) ∈ Set.filter (λ el . (snd el) < 8) (a × b))"

你会得到你期望的结果。

伊莎贝尔列表提升和压缩

Isabelle list lifter and compression

isabelle

问题 1

问题 2