<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:新細明體
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><font size="3" style="font-size:12pt;" color="#000000">Hi Sergei , </font><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">i find this method from book polynomials completion book, mention fst and snd for And and Or</font></div><div><div style="background-color: rgb(255, 255, 255);"><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><br></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;">then edit code of all combinations of tree with fst and snd, </p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;">then it can generate all valid relations</p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><br></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;">for transitive axiom</p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eval (Mode (Mode (Meaf 1.0) And (Meaf 2.0)) Or (Mode (Meaf 2.0) And (Meaf 3.0))) > eval (Mode (Meaf 1.0) And (Meaf 3.0))</font></p><div><font color="#222222" face="Times New Roman, serif"><br></font></div><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;">then i guess the criteria for valid axiom may be <span style="font-size: 12pt;">eval x > eval y</span></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><span style="font-size: 12pt;"><br></span></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><span style="font-size: 12pt;">i believe the book so i guess this will work well, if this is wrong, please verify it.</span></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><span style="font-size: 12pt;"><br></span></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><span style="font-size: 12pt;">now, you know that how i can try all combinations of equivalence relations by replacing transitive with new relation.</span></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><br></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">:l trees.hs</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">let allparams = replicateM 3 [1.0, 2.0]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">let alltrees = [getAllTrees c | x <- allparams, c <- [x]]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eval(alltrees!!1!!1) == eval(alltrees!!1!!1)</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">let alltrees1 = forM_ [0..(sizeoflist alltrees)] $ \i -> forM_ [0..(sizeoflist (alltrees!!i))] $ \j -> [(alltrees!!i!!j, eval(alltrees!!i!!j)== eval(alltrees!!i!!j))]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">--let bb = filter (\n -> if n != () then snd n == True) alltrees1</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">allexprs :: [ Mree Double ]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">let allexprs = concat alltrees -- a list of all the Mrees in alters</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">let alltrees2 = [ ((x,y), eval x > eval y) | x <- allexprs, y <- allexprs]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">let bb = [ (x,y) | ((x,y), True) <- alltrees2 ]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eval (Mode (Mode (Meaf 1.0) And (Meaf 2.0)) Or (Mode (Meaf 2.0) And (Meaf 3.0))) > eval (Mode (Meaf 1.0) And (Meaf 3.0))</font></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><br></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><br></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;">trees.hs</p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><br></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">import Data.List</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">import Control.Monad</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">import Math.Combinat</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">import System.IO</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">data Operation</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> = And</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> | Or</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> | MA</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> | MB</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> | Impl</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> deriving Show</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">data Mree x</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> = Meaf x</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> | Mode (Mree x) Operation (Mree x)</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> deriving Show</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">splits :: [a] -> [([a], [a])]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">splits xs = zip (inits xs) (tails xs)</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">getAllTrees :: [a] -> [Mree a]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">getAllTrees [] = []</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">getAllTrees [x] = return $ Meaf x</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">getAllTrees xs = do</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> (left, right) <- splits xs</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> guard $ not (null left) && not (null right)</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> leftT <- getAllTrees left</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> rightT <- getAllTrees right</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> op <- [And, Or]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> return $ Mode leftT op rightT</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eval :: Mree Double -> Double</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eval (Meaf x) = x</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eval (Mode l And r) = eval l</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eval (Mode l Or r) = eval r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">peval :: Mree Double -> String</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">peval (Meaf x) = show x :: String</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">peval (Mode l And r) = "(" ++ peval l ++ "^" ++ peval r ++ ")"</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">peval (Mode l Or r) = "(" ++ peval l ++ "V" ++ peval r ++ ")"</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">sizeoflist :: [a] -> Int</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">sizeoflist = length</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval1 :: Mree Float -> Float</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval1 (Meaf x) = x</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval1 (Mode l And r) = eeval1 l * eeval1 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval1 (Mode l Or r) = eeval1 l + eeval1 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval1 (Mode l MA r) = eeval1 l + eeval1 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval1 (Mode l MB r) = eeval1 l + eeval1 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval2 :: Mree Float -> Float</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval2 (Meaf x) = x</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval2 (Mode l And r) = eeval2 l * eeval2 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval2 (Mode l Or r) = eeval2 l + eeval2 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval2 (Mode l MA r) = eeval2 l + eeval2 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval2 (Mode l MB r) = eeval2 l * eeval2 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval3 :: Mree Float -> Float</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval3 (Meaf x) = x</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval3 (Mode l And r) = eeval3 l * eeval3 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval3 (Mode l Or r) = eeval3 l + eeval3 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval3 (Mode l MA r) = eeval3 l * eeval3 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval3 (Mode l MB r) = eeval3 l + eeval3 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval4 :: Mree Float -> Float</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval4 (Meaf x) = x</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval4 (Mode l And r) = eeval4 l * eeval4 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval4 (Mode l Or r) = eeval4 l + eeval4 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval4 (Mode l MA r) = eeval4 l * eeval4 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">eeval4 (Mode l MB r) = eeval4 l * eeval4 r</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">mulVV :: Num a => [a] -> [a] -> a</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">mulVV u v = sum $ zipWith (*) u v</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">mulMV :: Num a => [[a]] -> [a] -> [a]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">mulMV m v = map (mulVV v) m</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">mulMM :: Num a => [[a]] -> [[a]] -> [[a]]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">mulMM m n = transpose $ map (mulMV m) $ transpose $ n</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">msize :: [[Float]] -> Int</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">msize = length</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">mapMatrix :: (Float -> Float) -> [[Float]] -> [[Float]]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">mapMatrix f = map (map f)</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">coords :: [[Float]] -> [[(Int, Int)]]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">coords = zipWith (map . (,)) [0..] . map (zipWith const [0..])</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">delmatrix :: Int -> Int -> [[Float]] -> [[Float]]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">delmatrix i j = dellist i . map (dellist j)</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> where</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> dellist i xs = take i xs ++ drop (i + 1) xs</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">determinant :: [[Float]] -> Float</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">determinant m</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> | msize m == 1 = head (head m)</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> | otherwise = sum $ zipWith addition [0..] m</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> where</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> addition i (x:_) = x * cofactor i 0 m</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">cofactor :: Int -> Int -> [[Float]] -> Float</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">cofactor i j m = ((-1.0) ** fromIntegral (i + j)) * determinant (delmatrix i j m)</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">cofactorM :: [[Float]] -> [[Float]]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">cofactorM m = map (map (\(i,j) -> cofactor j i m)) $ coords m</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"><br></font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">inversem :: [[Float]] -> [[Float]]</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif">inversem m = mapMatrix (* recip det) $ cofactorM m</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> where</font></p><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt;"><font color="#222222" face="Times New Roman, serif"> det = determinant m</font></p><p class="MsoNormal" style="color: rgb(34, 34, 34); font-family: 'Times New Roman', serif; font-size: 12pt; margin: 0cm 0cm 0.0001pt;"><br></p></div></div><div><br><br><div>Regards,</div><div><br></div><div>Martin </div><br><br><div>> Subject: Re: [Agda] how to use monoid solver and how to derive a concept monoid if assume we do not know monoid<br>> From: mechvel@botik.ru<br>> To: tesleft@hotmail.com<br>> CC: agda@lists.chalmers.se<br>> Date: Tue, 15 Dec 2015 00:29:32 +0400<br>> <br>> On Mon, 2015-12-14 at 19:21 +0800, Mandy Martino wrote:<br>> <br>> > Hi ,<br>> > i find many places define identity, symmetric and transitive, how<br>> > to use monoid solve and which can it solve?<br>> ><br>> ><br>> > i would like to define a new set of equivalence relations, is <br>> > there a light weight version of monoid?<br>> <br>> See in Wikipedia what is a monoid.<br>> Monoid in Standard library is adequate, it cannot be any more<br>> "light weight".<br>> <br>> Monid has the axioms of<br>> (1) associativity for _∙_, (2) identity (ε).<br>> <br>> <br>> > how to use monoid solve and which can it solve?<br>> <br>> Earlier I tried SemiringSolver for Nat.<br>> And I guess that MonoidSolver uses a similar principle of reduction to<br>> a normal form<br>> (let people correct me, if I mistake).<br>> <br>> For monoid:<br>> having expressions e1 and e2,<br>> a proof for the equality<br>> e1 ≈ e2 (E)<br>> <br>> can be searched by applying the `solve' function.<br>> `solve' brings e1 and e2 to their certain normal forms e1' and e2'.<br>> This is done by moving parentheses (by using the associativity law),<br>> and canceling ε by using the identity law.<br>> Then, if e1' and e2' coincide<br>> (are equal by Equivalence.refl contained in the setoid),<br>> then the result of `solve' is a proof for (E).<br>> Otherwise, some other proof may exist or not.<br>> <br>> In various instances of Monoid there may exist many equations or<br>> statements which can be proved but are not proved by MonoidSolver.<br>> <br>> Example of a proof:<br>> I expect that `solve' will bring e1 = (x ∙ (e ∙ x)) ∙ (y ∙ e)<br>> and e2 = (e ∙ (x ∙ x)) ∙ y<br>> <br>> by using the laws of associativity and identity to the same expression<br>> <br>> x ∙ (x ∙ y).<br>> And this proves the equality<br>> <br>> (x ∙ (e ∙ x)) ∙ (y ∙ e) ≈ (e ∙ (x ∙ x)) ∙ y<br>> <br>> for any Monoid.<br>> <br>> I do not know how precisely MonoidSolver is used.<br>> But I have an example of using SemiringSolver, and I expect that<br>> MonoidSolver has a similar usage.<br>> <br>> For Nat (n : Nat) :<br>> <br>> open import Data.Nat.Properties using (module SemiringSolver)<br>> <br>> open SemiringSolver using (solve; _:=_; con; _:+_; _:*_)<br>> <br>> e : suc (suc (n + n)) ≡ 2 * suc n<br>> e = solve 1 (\n → con 1 :+ (con 1 :+ (n :+ n)) :=<br>> (con 2) :* (con 1 :+ n)<br>> )<br>> PE.refl n<br>> <br>> I guess that `solve' does the following. It has<br>> <br>> e1 = 1 + (1 + (n + n))<br>> e2 = (1 + (1 + 0)) * (1 + n),<br>> <br>> and it brings both terms to this normal form:<br>> 1 + (1 + (n + n)).<br>> <br>> It is done only by using the axioms of an arbitrary (commutative) ring.<br>> <br>> I have arranged this by looking into the source of Standard library,<br>> where it uses SemiringSolver, I just mimic the usage.<br>> <br>> I guess that under this `solve',<br>> `con' is a tag for a constant, `:' is a tag for an operator,<br>> all other items (in this case it is `n') are variables in a term.<br>> <br>> I expect that MonoidSolver has a similar usage.<br>> <br>> <br>> > assume we do not know monoid, how to build a concept such as <br>> > monoid based on custom equivalence relations?<br>> <br>> I do not know what is a custom equivalence relation.<br>> So I cannot tell.<br>> <br>> Regards,<br>> <br>> ------<br>> Sergei<br>> <br>> <br>> <br>> <br>> <br></div></div> </div></body>
</html>