[<<][meta][>>][..]
Sun Feb 14 17:52:57 CET 2010

Ai and nesting types

  - How to perform AI (normal forms from ainum.hs) on the Term type?  

  - How to nest number types, i.e. construct complex math / matrix
    math in terms of real base types.

It's a royal pain to write down the algebraic transformation rules in
terms of AST pattern matching.  Without syntactic abstraction of
binding forms (pattern matching) they cannot be abstracted over
easily.

Alternatives?

  - Use richer datatypes + perform evaluation on these before
    compilation to Term.

  - Find a way to express matching rules as combinators so they can be
    abstracted over.


I.e. the following is a concrete evaluator for performing addition on
terms in normal form, producing a normal form.

termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
termAdd = add (add Add)
    where
      add k Zero a = a
      add k One Zero = One
      add k One a = add k (Lit 1) a
      add k (Lit a) (Lit b) = Lit (a + b)                                  -- e
      add k (Lit a) (Negate (Lit b)) = Lit (a - b)
      add k (Lit a) (Add (Lit b) c) = Add (Lit (a + b)) c                  -- ae
      add k (Add (Lit a) b) (Add (Lit c) d) = Add (Lit (a + c)) (Add b d)  -- aec
      add k a (Add b@(Lit _) c) = Add b (Add a c)                          -- an
      add k a@(Lit _) b = Add a b                                          -- n  
      add k a b = k b a                                                    -- c



Using operators doesn't really make this more readable:

termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
termAdd = try (try (:<+>:)) where
    try flipAdd = (<+>) where
      L 0 <+> a = a
      L a <+> L b = L (a + b)                                            -- e
      L a <+> Negate (L b) = L (a - b)
      L a <+> ((L b) :<+>: c) = L (a + b) :<+>: c                        -- ae
      ((L a) :<+>: b) <+> ((L c) :<+>: d) = L (a + c) :<+>: (b :<+>: d)  -- aec
      a <+> (b@(L _) :<+>: c) = b :<+>: (a :<+>: c)                      -- an
      a@(L _) <+> b = a :<+>: b                                          -- n  
      a <+> b = b `flipAdd` a  


So... let's convert to intermediate form, and perform simplificiation
on that.

EDIT: finaly it stabilized at this:


-- Commuative reduction is able to propagate ``literal bubbles to the
-- surface'' by keeping semi-literal terms in a (L a :<*>: b) normal form.

data CT l t = U                        -- unit
            | Z                        -- zero
            | L l                      -- literal
            | T t                      -- opaque term
            | (CT l t) :<*>: (CT l t)  -- op
              deriving Show

ctOp :: (Num l) => (l -> l -> l) -> CT l t -> CT l t -> CT l t
ctOp binop = (<*>) where
    (*) = binop

    -- unit and zero
    Z <*> a = Z ;  a <*> Z = Z
    U <*> a = a ;  a <*> U = a

    -- reduce literals/semi-literals: (L a) or (L a :<*>: _)
    L a <*> L b = L (a * b)
    L a <*> (L b :<*>: c) = L (a * b) :<*>: c
    (L a :<*>: b) <*> L c = L (a * c) :<*>: b
    (L a :<*>: b) <*> (L c :<*>: d) = L (a * c) :<*>: (b :<*>: d)

    -- no reduction -> enforce normalized semi-literal form
    a <*> (L b :<*>: c) = L b :<*>: (a :<*>: c)
    (L a :<*>: b) <*> c = L a :<*>: (b :<*>: c)

    -- catch-all 
    a <*> b = a :<*>: b







[Reply][About]
[<<][meta][>>][..]