Forgotten Computer Proofs

When I was working on my masters thesis I got really interested in using computers to prove things.

An important part of my thesis hinged on discovering a super-commutative ring that did not have a super divided power structure. In my thesis I present a whole class of rings that have that property, one ring for each prime number. However, before I figured out the proof that it worked for every prime, I used a computer to prove that it worked for the number 3. That work has never been published. Until today.

Super Duper Example

In order to do that, I built a mini-algebra system using the Miranda programming language.

p = 3
monomial ::= Mon (num,[char]) ||A monomial is a number followed by a (possibly empty) list of variables represented by characters
 ||A polynomial is just a list of monomials

highcount :: [*] -> num ||finds the number of the most plentiful element in a list
highcount [] = 0
highcount (a:x) = (1 + #[b | b <- x; b = a]), if ((1 + #[b | b <- x; b = a]) >= highcount (x -- [b | b <- x; b = a]))
 = highcount (x -- [b | b <- x; b = a]), otherwise

fact :: num -> num ||input n -> output n factorial
fact 0 = 1
fact (n+1) = ((n+1)*(fact n))

clt :: [monomial] -> [monomial] ||takes a sorted polynomial and "collects like terms"
clt [] = [] ||If polynomial is 0 (an empty list), return 0
clt (a:[]) = (a:[]) ||If polynomial is a monomial return it
clt ((Mon(a, astr)):(Mon(b, astr)):x) = clt ((Mon((a+b) mod p, astr)):clt (x))
 ||If the first two monomials in the polynomial have the same variables
 ||add them together by adding their coefficiants. (You see why "sorted" is important)
clt (a:x) = a:(clt x) ||If they don't have the same variables then move on to the rest of the list

remo :: [monomial] -> [monomial] ||removes zeros to clean up polynomials
remo [] = []
remo (Mon(a, astr):x) = remo x, if ((a=0) \/ ((highcount astr) >= p)) || KILL ALL POWERS OF P! (powers of p are zero)
remo (Mon(a, astr):x) = (Mon(a, astr)):(remo x), otherwise

monsort :: [monomial] -> [monomial] ||puts polynomials in alphabetical order, so collecting like terms is easier.
monsort [] = []
monsort (Mon(a,astr):x) = monsort [ Mon(b,bstr) | Mon(b,bstr) <- x; bstr <= astr ]
 ++ [Mon(a,astr)] ++
 monsort [ Mon(b,bstr) | Mon(b,bstr) <- x; bstr > astr ]

polysan :: [monomial] -> [monomial] ||sanitises polynomials
polysan x = remo(clt(monsort(x)))

mult :: monomial -> monomial -> monomial ||multiplies monomials
mult (Mon (a, astr)) (Mon (b, bstr)) = (Mon ( (a*b) mod p, (sort(astr++bstr))))

scalmult :: num -> monomial -> monomial ||multiplies monomials and scalars
scalmult n (Mon(a, astr)) = (Mon((n*a) mod p, astr))

polyscalmult :: num -> [monomial] -> [monomial] ||multiply polynomials by scalars
polyscalmult n x = (map (scalmult n) x)

polyadd :: [monomial] -> [monomial] -> [monomial] ||adds polynomials. note: 0 = []
polyadd x y = polysan (x++y)

polymul :: [monomial] -> [monomial] -> [monomial] ||multiply polynomials. note 1 = Mon (1,[])
polymul x [] = []
polymul [] y = []
polymul (a:x) y = (polyadd (map (mult a) y) (polymul x y))

power :: ([monomial], num) -> [monomial] ||exponetiates polynomials
power (x,0) = [Mon (1,[])]
power (x,1) = x
power (x,n+1) = (polymul x (power (x, n)))

repeater :: num -> * -> [*] ||outputs a list of the input repeated a bunch of times
repeater 0 x = []
repeater 1 x = [x]
repeater k x = (x:(repeater (k-1) (x)))

gammamon :: num -> monomial -> monomial ||gamma on a monomial
gammamon 0 x = Mon (1, []) ||Rule 1
gammamon 1 x = x ||Rule 1
gammamon k (Mon (l, a:[])) = Mon (l^k * ((fact k)^(p-2) mod p) mod p, repeater k a) ||What gamma does on the generators.
gammamon k (Mon (l, a:x)) = mult (Mon (1,repeater k a)) (gammamon k (Mon (l, x))) ||Rule 3


sigma :: (num, num) -> ( num -> [monomial]) -> [monomial] ||adds incremental functions (used to implement rule 2.)
sigma (i, k) func = [Mon(0,[])] , if i > k
sigma (i, k) func = polysan ((func i) ++ (sigma (i+1,k) func)) 

gamma :: num -> [monomial] -> [monomial]
gamma 0 x = [Mon (1,[])] ||Rule 1
gamma 1 x = x ||Rule 1
gamma k [] = [] ||gamma(0) is 0
gamma k (x:[]) = polysan [gammamon k x] ||gamma of a monomial goes to gammamon
gamma k (x:y) = polysan (sigma (0, k) (gammaprod [x] y k)) ||Rule 2

||Things to test.

|| Rule 4
test1 i j x = (polysan (polymul (gamma i x) (gamma j x)) = polysan (polyscalmult (((fact (i+j)) div ((fact i)*(fact j))) mod p) (gamma (i+j) x)))

|| Rule 5
test2 i q x = (polysan (gamma i (gamma q x)) = polysan (polyscalmult (((fact (i*q)) div ((fact i)*(fact q)^i)) mod p) (gamma (i*q) x)))

test i j x = (test1 i j x) & (test2 i j x)

gammaprod :: [monomial] -> [monomial] -> num -> num -> [monomial] || used to implement rule 2.
gammaprod x y k 0 = gamma k y ||gamma 0 x = 1
gammaprod x y k k = gamma k x ||gamma 0 y = 1
gammaprod [] y k i = [] ||0*stuff = 0
gammaprod x [] k i = [] ||stuff*0 = 0
gammaprod x y k i = polymul (gamma i x) (gamma (k-i) y)

write :: [monomial] -> [char] ||outputs polynomials so they can be read by other programs
write [] = "0\n"
write (Mon(a,astr):[]) = (show a) ++ "*" ++ (condence(astr)) ++ ['\n']
write (Mon(a,astr):rest) = (show a) ++ "*" ++ (condence(astr)) ++ " + " ++ (write rest)

stars :: [char] -> [char]
stars [] = []
stars (a:[]) = (a:[])
stars (a:rest) = [a] ++ "*" ++ (stars(rest))

condence :: [char] -> [char] ||takes a string and writes it in exponent form, ex: "aaabb"-> "a^3*b^2"
condence [] = []
condence (a:[]) = (a:[])
condence (a:rest) = a:'*':(condence rest), if ([ b | b <- rest; b=a] = [])
 = [a] ++ "^" ++ (show (1 + #[ b | b <- rest; b=a])) ++ "*" ++ (condence (rest -- [ b | b <- (rest); b=a])), 
 if ~((rest -- [ b | b <- (rest); b=a])= [])
 = [a] ++ "^" ++ (show (1 + #[ b | b <- rest; b=a])), otherwise

||some variables

a = [Mon (1, "a")]
b = [Mon (1, "b")]
c = [Mon (1, "c")]
d = [Mon (1, "d")]
f = [Mon (1, "f")]
g = [Mon (1, "g")]
rel = [Mon (1,"ab"),Mon (1, "cd"),Mon (1, "ef")]
rel1 = [Mon (-1,"ab")]
rel2 = [Mon (1, "cd"),Mon (1, "ef")]
rel3 = [Mon (1, "cd"),Mon (1, "ef"), Mon (1, "gh")]

When I tried to run the problem for the number 5 it crashed my laptop.

 

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s