isPrime函数与TLA+

Question

这个问题是关于TLA+使用工具箱(https://github.com/tlaplus/tlaplus/releases)的，我还没有找到任何关于它的标签。真对不起。这就是为什么我只标记了Primes。如果我错过了什么，请友好地添加更好的标签或创建缺失的标签。

以下是问题所在

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)

谢谢

Answer 1

有很多方法来表达整数是素数的概念，但是你的尝试说，如果在2. n中存在一些整数k，则整数N是素数。N的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)