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.
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.
