Функция isPrime с TLA + - PullRequest
Новая
       42

Функция isPrime с TLA +

0 голосов
/ 18 ноября 2018

Этот вопрос касается TLA + с использованием панели инструментов (https://github.com/tlaplus/tlaplus/releases) Я не смог найти какой-либо тег об этом. Извини за это. Вот почему я помечен только с помощью простых чисел. Если я что-то упустил, пожалуйста, добавьте лучшие теги или создайте недостающие.

Вот вопрос

Существует хорошо известная функция и алгоритм для GCD. Вот оно. 

------------------ MODULE Euclid -------------------------------
EXTENDS Naturals, TLC
CONSTANT K
Divides(i,j) == \E k \in 0..j: j = i * k
IsGCD(i,j,k) ==
    Divides(i,j)
    /\ Divides(i,k)
    /\ \A r \in 0..j \cup 0..k :
        (Divides(r,j ) /\ Divides(r,k)) => Divides(r,i)
    (* --algorithm EuclidSedgewick
    {
        variables m \in 1..K, n \in 1..m, u = m, v = n;
        {
            L1: while (u # 0) {
            if (u < v) { u := v || v := u };
            L2: u := u - v
            };
            assert IsGCD(v, m, n)
        }
    }
    *)

Это хорошо известное решение, которое работает.

Я сейчас пытаюсь написать функцию isPrime, используя эту. Но я думаю, что я делаю неправильно. Я хотел бы знать, если у вас есть идея. 

isPrime(nb) ==
        \E k \in 2..nb: isGCD(nb,k,1) \/ isGCD(nb,k,nb)

Спасибо

1 Ответ

0 голосов
/ 18 ноября 2018

Существует множество способов выразить идею, что целое число является простым, однако ваша попытка сказать, что целое число N является простым, если в 2..N существует какое-то целое число k, для которого gcd (k, n) = 1 илиgcd (k, n) = n.Легко видеть, что это неверно, поскольку 4 явно составная, но gcd (3,4) = 1. И, конечно, для каждого простого числа N или нет, gcd (N, N) = N.

Я не уверен насчет правил для TLA +, но я быстро прочитал некоторую документацию, и вот моя попытка на IsPrime 

isPrime(nb) == \A k in 2..nb-1: ~Divides(k, nb)

или 

isPrime(nb) == \A k in 1..nb: Divides(k, nb) => ( (k = 1) \/ (k=nb) )

или, если вы действительнопо какой-то причине хочу работать там с IsGCD 

isPrime(nb) == \A k in 1..nb: IsGCD(k, nb, d) => ( (d = 1) \/ (d = nb) )

или 

isPrime(nb) == \A k in 2..nb-1: IsGCD(k, nb, d) => (d = 1)
...