[Agda] how to use monoid solver and how to derive a concept monoid if assume we do not know monoid

[Mandy Martino]

Hi  Sergei , 
i   find this  method  from book  polynomials  completion  book, mention  fst and  snd  for  And  and  Or
then edit code of all combinations of tree with  fst and snd, then  it can generate all valid relations
for transitive axiomeval (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))
then  i guess the criteria for valid axiom may be eval x > eval y
i believe the book so i guess this will work well, if this is wrong, please verify it.
now, you know that how i can try all combinations of equivalence relations by replacing transitive with new relation.
:l trees.hslet allparams = replicateM 3 [1.0, 2.0]let alltrees = [getAllTrees c | x <- allparams, c <- [x]]eval(alltrees!!1!!1) == eval(alltrees!!1!!1)let alltrees1 = forM_ [0..(sizeoflist alltrees)] $ \i -> forM_ [0..(sizeoflist (alltrees!!i))] $ \j -> [(alltrees!!i!!j, eval(alltrees!!i!!j)== eval(alltrees!!i!!j))]--let bb = filter (\n -> if n != () then snd n == True) alltrees1
allexprs :: [ Mree Double ]let allexprs = concat alltrees   -- a list of all the Mrees in alterslet alltrees2 = [ ((x,y), eval x > eval y) | x <- allexprs, y <- allexprs]let bb = [ (x,y) | ((x,y), True) <- alltrees2 ]
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))

trees.hs
import Data.Listimport Control.Monadimport Math.Combinatimport System.IO
data Operation  = And  | Or  | MA  | MB  | Impl    deriving Show
data Mree x = Meaf x | Mode (Mree x) Operation (Mree x)   deriving Show
splits :: [a] -> [([a], [a])]splits xs = zip (inits xs) (tails xs)
getAllTrees :: [a] -> [Mree a]getAllTrees [] = []getAllTrees [x] = return $ Meaf xgetAllTrees xs = do  (left, right) <- splits xs  guard $ not (null left) && not (null right)  leftT <- getAllTrees left  rightT <- getAllTrees right  op <- [And, Or]  return $ Mode leftT op rightT
eval :: Mree Double -> Doubleeval (Meaf x) = xeval (Mode l And r) = eval leval (Mode l Or r) = eval r
peval :: Mree Double -> Stringpeval (Meaf x) = show x :: Stringpeval (Mode l And r) = "(" ++ peval l ++ "^" ++ peval r ++ ")"peval (Mode l Or r) = "(" ++ peval l ++ "V" ++ peval r ++ ")"

sizeoflist :: [a] -> Intsizeoflist = length
eeval1 :: Mree Float -> Floateeval1 (Meaf x) = xeeval1 (Mode l And r) = eeval1 l * eeval1 reeval1 (Mode l Or r) = eeval1 l + eeval1 reeval1 (Mode l MA r) = eeval1 l + eeval1 reeval1 (Mode l MB r) = eeval1 l + eeval1 r
eeval2 :: Mree Float -> Floateeval2 (Meaf x) = xeeval2 (Mode l And r) = eeval2 l * eeval2 reeval2 (Mode l Or r) = eeval2 l + eeval2 reeval2 (Mode l MA r) = eeval2 l + eeval2 reeval2 (Mode l MB r) = eeval2 l * eeval2 r
eeval3 :: Mree Float -> Floateeval3 (Meaf x) = xeeval3 (Mode l And r) = eeval3 l * eeval3 reeval3 (Mode l Or r) = eeval3 l + eeval3 reeval3 (Mode l MA r) = eeval3 l * eeval3 reeval3 (Mode l MB r) = eeval3 l + eeval3 r
eeval4 :: Mree Float -> Floateeval4 (Meaf x) = xeeval4 (Mode l And r) = eeval4 l * eeval4 reeval4 (Mode l Or r) = eeval4 l + eeval4 reeval4 (Mode l MA r) = eeval4 l * eeval4 reeval4 (Mode l MB r) = eeval4 l * eeval4 r
mulVV :: Num a => [a] -> [a] -> amulVV u v = sum $ zipWith (*) u v
mulMV :: Num a => [[a]] -> [a] -> [a]mulMV m v = map (mulVV v) m
mulMM :: Num a => [[a]] -> [[a]] -> [[a]]mulMM m n = transpose $ map (mulMV m) $ transpose $ n
msize :: [[Float]] -> Intmsize = length
mapMatrix :: (Float -> Float) -> [[Float]] -> [[Float]]mapMatrix f = map (map f)
coords :: [[Float]] -> [[(Int, Int)]]coords = zipWith (map . (,)) [0..] . map (zipWith const [0..])
delmatrix :: Int -> Int -> [[Float]] -> [[Float]]delmatrix i j = dellist i . map (dellist j)  where    dellist i xs = take i xs ++ drop (i + 1) xs
determinant :: [[Float]] -> Floatdeterminant m    | msize m == 1 = head (head m)    | otherwise    = sum $ zipWith addition [0..] m  where    addition i (x:_) =  x * cofactor i 0 m
cofactor :: Int -> Int -> [[Float]] -> Floatcofactor i j m = ((-1.0) ** fromIntegral (i + j)) * determinant (delmatrix i j m)
cofactorM :: [[Float]] -> [[Float]]cofactorM m = map (map (\(i,j) -> cofactor j i m)) $ coords m
inversem :: [[Float]] -> [[Float]]inversem m = mapMatrix (* recip det) $ cofactorM m  where    det = determinant m


Regards,
Martin 

> Subject: Re: [Agda] how to use monoid solver and how to derive a concept monoid if assume we do not know monoid
> From: mechvel at botik.ru
> To: tesleft at hotmail.com
> CC: agda at lists.chalmers.se
> Date: Tue, 15 Dec 2015 00:29:32 +0400
> 
> On Mon, 2015-12-14 at 19:21 +0800, Mandy Martino wrote:
> 
> > Hi ,
> > i find many places  define  identity, symmetric and  transitive,   how
> > to  use  monoid  solve and  which  can  it  solve?
> >
> >
> > i would like  to define a new  set  of  equivalence relations,  is  
> > there  a  light  weight  version of  monoid?
> 
> See in Wikipedia what is a monoid.
> Monoid  in Standard library is adequate, it cannot be any more
> "light weight".
> 
> Monid has the axioms of
> (1) associativity for _∙_,   (2) identity (ε).
> 
> 
> > how to use  monoid  solve and  which  can  it  solve?
> 
> Earlier I tried  SemiringSolver  for  Nat.
> And I guess that  MonoidSolver  uses a similar principle of reduction to
> a normal form
> (let people correct me, if I mistake).
> 
> For monoid:
> having expressions        e1  and  e2,
> a proof for the equality
>                           e1 ≈ e2    (E)
> 
> can be searched by applying the  `solve'  function.
> `solve' brings  e1  and  e2  to their certain normal forms  e1' and e2'.
> This is done by moving parentheses (by using the associativity law),
> and canceling  ε  by using the identity law.
> Then, if  e1'  and  e2'  coincide
> (are equal by  Equivalence.refl  contained in the setoid),
> then the result of `solve'  is a proof for  (E).
> Otherwise, some other proof may exist or not.
> 
> In various instances of Monoid there may exist many equations or
> statements which can be proved but are not proved by  MonoidSolver.
> 
> Example of a proof:
> I expect that `solve' will bring  e1 =  (x ∙ (e ∙ x)) ∙ (y ∙ e)
> and                               e2 =  (e ∙ (x ∙ x)) ∙ y
> 
> by using the laws of  associativity and identity to the same expression
> 
>                              x ∙ (x ∙ y).
> And this proves the equality
> 
>                 (x ∙ (e ∙ x)) ∙ (y ∙ e)  ≈  (e ∙ (x ∙ x)) ∙ y
> 
> for any Monoid.
> 
> I do not know how precisely MonoidSolver is used.
> But I have an example of using  SemiringSolver,  and I expect that
> MonoidSolver has a similar usage.
> 
> For  Nat (n : Nat) :
> 
>   open import Data.Nat.Properties using (module SemiringSolver)
> 
>   open SemiringSolver using (solve; _:=_; con; _:+_; _:*_)
> 
>   e :  suc (suc (n + n)) ≡ 2 * suc n
>   e =  solve 1 (\n →  con 1 :+ (con 1 :+ (n :+ n))  :=
>                       (con 2) :* (con 1 :+ n)
>                )
>                PE.refl n
> 
> I guess that `solve' does the following. It has
> 
>   e1 =  1 + (1 + (n + n))
>   e2 =  (1 + (1 + 0)) * (1 + n),
> 
> and it brings both terms to this normal form:
>                                               1 + (1 + (n + n)).
> 
> It is done only by using the axioms of an arbitrary (commutative) ring.
> 
> I have arranged this by looking into the source of Standard library,
> where it uses SemiringSolver, I just mimic the usage.
> 
> I guess that under this `solve',
> `con' is a tag for a constant,  `:' is a tag for an operator,
> all other items (in this case it is `n') are variables in a term.
> 
> I expect that  MonoidSolver  has a similar usage.
> 
> 
> > assume we do not know monoid,  how to build  a concept such as  
> > monoid  based  on  custom  equivalence  relations?
> 
> I do not know what is a  custom equivalence relation.
> So I cannot tell.
> 
> Regards,
> 
> ------
> Sergei
> 
> 
> 
> 
> 
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151215/03a93ce3/attachment-0001.html