arithmoi-0.4.1.3: Efficient basic number-theoretic functions. Primes, powers, integer logarithms.

Copyright (c) 2011 Daniel Fischer MIT Daniel Fischer Provisional Non-portable (GHC extensions) None Haskell2010

Math.NumberTheory.Primes.Testing.Certificates

Description

Certificates for primality or compositeness.

Synopsis

# Certificates

A certificate of either compositeness or primality of an `Integer`. Only numbers `> 1` can be certified, trying to create a certificate for other numbers raises an error.

Constructors

 Composite !CompositenessProof Prime !PrimalityProof

Instances

 Show Certificate

A proof of compositeness of a positive number. The type is abstract to ensure the validity of proofs.

Instances

 Show CompositenessProof

The number whose compositeness is proved.

A proof of primality of a positive number. The type is abstract to ensure the validity of proofs.

Instances

 Show PrimalityProof

The number whose primality is proved.

# Arguments

An argument for compositeness of a number (which must be `> 1`). `CompositenessProof`s translate directly to `CompositenessArguments`, correct arguments can be transformed into proofs. This type allows the manipulation of proofs while maintaining their correctness. The only way to access components of a `CompositenessProof` except the composite is through this type.

Constructors

 Divisors `compo == firstDiv*secondDiv`, where all are `> 1` Fieldscompo :: Integer firstDivisor :: Integer secondDivisor :: Integer Fermat `compo` fails the strong Fermat test for `fermatBase` Fieldscompo :: Integer fermatBase :: Integer Lucas `compo` fails the Lucas-Selfridge test Fieldscompo :: Integer Belief No particular reason given Fieldscompo :: Integer

An argument for primality of a number (which must be `> 1`). `PrimalityProof`s translate directly to `PrimalityArguments`, correct arguments can be transformed into proofs. This type allows the manipulation of proofs while maintaining their correctness. The only way to access components of a `PrimalityProof` except the prime is through this type.

Constructors

 Pock A suggested Pocklington certificate Fieldsaprime :: Integer largeFactor :: Integer smallFactor :: Integer factorList :: [(Integer, Int, Integer, PrimalityArgument)] Division Primality should be provable by trial division to `alimit` Fieldsaprime :: Integer alimit :: Integer Obvious `aprime` is said to be obviously prime, that holds for primes `< 30` Fieldsaprime :: Integer Assumption Primality assumed Fieldsaprime :: Integer

## Weaken proofs to arguments

`arguePrimality` transforms a proof of primality into an argument for primality.

`argueCompositeness` transforms a proof of compositeness into an argument for compositeness.

## Prove valid arguments

`verifyPrimalityArgument` checks the given argument and constructs a proof from it, if it is valid. For the explicit arguments, this is simple and resonably fast, for an `Assumption`, the verification uses `certify` and hence may take a long time.

`verifyCompositenessArgument` checks the given argument and constructs a proof from it, if it is valid. For the explicit arguments, this is simple and resonably fast, for a `Belief`, the verification uses `certify` and hence may take a long time.

# Determine and prove whether a number is prime or composite

`certify n` constructs, for `n > 1`, a proof of either primality or compositeness of `n`. This may take a very long time if the number has no small(ish) prime divisors

## Checks for the paranoid

Check the validity of a `Certificate`. Since it should be impossible to construct invalid certificates by the public interface, this should never return `False`.

Check the validity of a `CompositenessProof`. Since it should be impossible to create invalid proofs by the public interface, this should never return `False`.

Check the validity of a `PrimalityProof`. Since it should be impossible to create invalid proofs by the public interface, this should never return `False`.