event-b:有可能从..生成序列吗..到在一个表达式中通过lambda的素数

Question

我想知道是否有可能在event-b中只生成一个lambda表达式的素数序列。这就是我目前所拥有的：

@axm1 primeSet = {x∣ x ∈ 1‥100 ∧ ¬(∃y·y < x ∧ y > 1 ∧ x mod y = 0)} ∧ finite(primeSet)
@axm2 primeSeq ∈ 1‥card(primeSet) >->> primeSet
@axm3 ∀a,b,c,d·a↦b ∈ primeSeq ∧ c↦d ∈ primeSeq ∧ a↦b ≠ c↦d ⇒ (a < c ⇒ b < d)

@axm1生成一组素数，@axm2定义序列的类型，@axm3将该集合进一步约束为确定性解。我不知道如何用一个lambda表达式来实现这一点，我甚至认为这是不可能的，但我想知道其他人是怎么想的。

Answer 1

我相信这个lambda函数满足了您的请求：

@axm1 primeSeq = {size↦X| size∈ℕ ∧ X⊆ℕ ∧ ∀x·x∈X ⇒ (x∈1‥size ∧ (∀y·y∈1‥x ∧ y≠1 ∧ y≠x ⇒ x mod y ≠ 0))}

Answer 2

我对这个问题的第一次尝试是递归定义的理解集(为了简单起见，我只看素数的无限序列，但很容易添加像i<size这样的附加条件来获得有限序列)：

axm1:  primeSeq1 ∈ ℕ1 --> ℕ1
axm2:  primeSeq1 = { i↦p ∣ i∈ℕ1 ∧ p∈ℕ ∧
( (i=1 ⇒ p=2)
∧ (i>1 ⇒ ( p>primeSeq1(i−1) ∧
∀x·(x∈primeSeq1(i−1)‥p−1 ⇒
∃a,b·(a∈2‥x−1 ∧ a∗b=x)) ∧
¬(∃a,b·(a∈2‥p−1 ∧ a∗b=p))     )))}

换句话说：我们有一个硬编码的基本情况，2是第一个素数。那么对于i>1:p是第i个素数，如果它大于第(i-1)个素数(递归！)，则最后一个素数和p之间的所有数字都不是素数，p本身就是素数。

这个版本仍然需要两个公理，一个只用于类型检查，另一个带有定义。没有axm1，罗丹不会接受。它不是lambda表达式。

现在我们使用一个丑陋的破解：我们使用理解集变量ps作为局部变量来定义递归集，以消除对axm1:的需要

axm3:  primeSeq2 = { j,ps · j∈ℕ1 ∧ ps∈ℕ1→ℕ ∧
ps = { i↦p ∣ i∈ℕ1 ∧ p∈ℕ ∧
( (i=1 ⇒ p=2)
∧ (i>1 ⇒ ( p>ps(i−1) ∧
∀x·(x∈ps(i−1)‥p−1 ⇒
∃a,b·(a∈2‥x−1 ∧ a∗b=x)) ∧
¬(∃a,b·(a∈2‥p−1 ∧ a∗b=p))     )))}
∣ j↦ps(j) }

请注意，我们使用了理解集的另一种语法形式，其中我们为该集的每个元素添加了一个表达式(j↦ps(j))。

所以primeSeq2是通过使用一个表达式来定义的。但它不是lambda表达式。

我们再次使用了一个技巧。我们围绕着一个λ表达式的理解集：

axm4:  primeSeq3 = (λk·k∈ℕ1 ∣ primeSeq2(k))

所以我们有一个lambda表达式。为了将其包含在一个定义中，我们只需将primeSeq2复制到表达式中：

axm5:  primeSeq4 = (λk·k∈ℕ1 ∣ { j,ps · j∈ℕ1 ∧ ps∈ℕ1→ℕ ∧
ps = { i↦p ∣ i∈ℕ1 ∧ p∈ℕ ∧
( (i=1 ⇒ p=2)
∧ (i>1 ⇒ ( p>ps(i−1) ∧
∀x·(x∈ps(i−1)‥p−1 ⇒
∃a,b·(a∈2‥x−1 ∧ a∗b=x)) ∧
¬(∃a,b·(a∈2‥p−1 ∧ a∗b=p))     )))}
∣ j↦ps(j) }(k))

所以，为了回答你的问题：是的，只需要一个lambda表达式就可以定义这样的序列。但结果非常混乱：)

我没有证明(也不打算这么做！)关于上面表达式的任何性质。所以它可能有一些错误。我只是打字检查了一下公式。

Update：在写下上面的解决方案后，我意识到您根本不需要递归。您可以使用primeSet、primeSeq等的原始定义，并将其放入形式的理解集中

primeSeq1 =  (%i . i:NAT1 | ({ primeSet, primeSeq, ... . Definitions | 0|->primeSeq }(0))i)

但是，即使是WD条件也很难证明。