5

表达式生成一系列素数。这是我到目前为止所拥有的：

@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 表达式来做到这一点，我认为这甚至不可能，但我想知道其他人的想法。

4

2 回答 2

2

我相信这个 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))}
于 2014-04-12T18:41:29.887 回答
0

我对这个问题的第一次尝试是一个递归定义的理解集（为简单起见，我只看素数的无限序列，但很容易添加一个额外的条件，比如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-1) 个素数（递归！），则 p 是第 i 个素数，最后一个素数和 p 之间的所有数字都不是素数，p 本身是素数。

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

现在我们使用一个丑陋的 hack：我们使用一个理解集变量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)为集合的每个元素添加了一个表达式 ( )。

SoprimeSeq2是通过仅使用一个表达式来定义的。但它不是 lambda 表达式。

我们再次使用一个技巧。我们用 lamda 表达式包围理解集：

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 表达式来定义这样的序列。但结果非常混乱:)

我没有证明（也不打算这样做！）关于上述表达式的任何属性。因此，其中可能存在一些错误。我只是输入检查了公式。

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

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

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

于 2014-05-21T13:13:05.640 回答