event-b: возможно ли сгенерировать последовательность из... в... простых чисел через лямбду в одном выражении?

Question

Интересно, возможно ли сгенерировать последовательность простых чисел с одним лямбда- выражением в событии b? Это то, что я до сих пор:

@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 ограничивает этот набор в дальнейшем детерминированным решением. Я понятия не имею, как сделать это с одним лямбда-выражением, и я не думаю, что это даже возможно, но я хочу знать, что думают другие.

Answer 1

Я считаю, что эта лямбда-функция удовлетворяет ваш запрос:

@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. И это не лямбда-выражение.

Теперь мы используем некрасивый хак: мы используем переменную набора понимания 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 определяется с помощью только одного выражения. Но это не лямбда-выражение.

Мы снова используем трюк. Мы окружаем понимание, заданное лямда-выражением:

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

Итак, у нас есть лямбда-выражение. Чтобы иметь это в одном определении, мы просто копируем 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))

Итак, чтобы ответить на ваш вопрос: Да, такую ​​последовательность можно определить только одним лямбда-выражением. Но результат крайне грязный:)

Я не доказывал (и не планирую делать это!) Никаких свойств в отношении приведенных выше выражений. Так что в этом могут быть некоторые ошибки. Я просто напечатал проверенные формулы.

Обновление: записав решение выше, я понял, что рекурсия вам вообще не нужна. Вы можете использовать ваши оригинальные определения primeSet, primeSeqи т. д. и положить его в набор для понимания формы

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

Но все же, даже условия WD было бы очень трудно доказать.