1

这个问题是关于 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)

谢谢

4

1 回答 1

1

有很多方法可以表达整数是素数的概念，但是您的尝试说整数 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)
于 2018-11-18T02:36:24.853 回答