event-b: Ist es möglich, eine Folge von ... bis ... von Primzahlen über Lambda in einem Ausdruck zu erzeugen?

Question

Ich frage mich, ob es möglich ist, eine Sequenz von Primzahlen mit nur einem lambda Ausdruck in event-b zu generieren. Dies ist das, was ich bisher:

@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 einen Satz von Primzahlen erzeugt, @axm2 definiert die Art der Sequenz und @axm3 schränkt diese gesetzt weiter auf eine deterministische Lösung. Ich habe keine Ahnung, wie man das mit einem Lambda-Ausdruck macht, und ich glaube nicht, dass es überhaupt möglich ist, aber ich möchte wissen, was andere denken.

Answer 1

Ich glaube, das Lambda-Funktion Ihre Anfrage erfüllt:

@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

Mein erster Versuch, das Problem würde ein Verständnis Satz sein, die rekursiv (der Einfachheit halber definiert ist, ich auf die unendliche Folge von Primzahlen suchen gerade, aber es wäre leicht, eine zusätzliche Bedingung wie i<size hinzufügen, um eine endliche Folge zu erhalten):

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)) )))} 

In Worten: Wir haben einen hartcodierte Basisfall, dass 2 ist die erste Primzahl. Dann gilt für i> 1: p ist die i-te Primzahl, wenn sie größer ist als die (i-1) -te Primzahl (Rekursion!), Alle Zahlen zwischen der letzten Primzahl und p sind Primzahlen und p selbst ist eine Primzahl.

Diese Version benötigt noch zwei Axiome, eines nur für die Typprüfung, das andere mit der Definition. Rodin akzeptiert es nicht ohne axm1. Und es ist kein Lambda-Ausdruck.

Jetzt verwenden wir eine hässliche Hack: Wir verwenden ein Verständnis Variable ps als lokale Variable die rekursive Satz definieren die Notwendigkeit axm1 zu beseitigen:

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) } 

Bitte beachten Sie, dass wir eine andere syntaktische Form verwendet eines Verständnissatzes, in dem wir für jedes Element des Satzes einen Ausdruck (j↦ps(j)) hinzugefügt haben.

So wird primeSeq2 mit nur einem Ausdruck definiert. Aber es ist kein Lambda-Ausdruck.

Wieder verwenden wir einen Trick. Wir umgeben das Verständnis von einem Lambda-Ausdruck gesetzt:

So haben wir einen Lambda-Ausdruck. Um es in einer Definition zu haben, kopieren wir nur primeSeq2 in den Ausdruck:

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)) 

Also, um Ihre Frage zu beantworten: Ja, es möglich ist, mit nur einem Lambda-Ausdruck eine solche Sequenz zu definieren. Aber das Ergebnis ist extrem chaotisch :)

Ich habe keine Eigenschaften über die oben genannten Ausdrücke (und nicht planen, es zu tun!) Zu beweisen. Es könnte also einige Fehler geben. Ich tippte einfach die Formeln ein.

Update: Nachdem ich die Lösung oben notiert hatte, erkannte ich, dass Sie die Rekursion überhaupt nicht benötigen. Sie können Ihre ursprünglichen Definitionen von primeSet, primeSeq usw. verwenden.und setzen Sie es in ein Verständnis Set des Formulars

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

Aber immer noch, auch die WD Bedingungen wäre sehr schwer zu beweisen.