`[<<][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)
where
add k Zero a = a
add k One Zero = One
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 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
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][>>][..]`