art with code

2009-06-10

A wee bit of algebra

Am currently in the process of writing a game of algebra in Haskell. The gameplay consists of coaxing group axioms to equality or, in the case of the neutral element and the inverse function, a binding. The base act of equation munging is accomplished through one's big bag of previously proven lemmas and given axioms, which one then applies to matching parts of the equation in the feeble hope of achieving enlightenment.

For example, let us step through the process of proving associativity for a o b = (a x b) x 1, given the abelian group x. The | x in the following denotes applying the rule x at the emboldened position in the equation (why yes, it is an AST internally):

a o (b o c) = (a o b) o c | a o b = (a x b) x 1
(a x (b o c)) x 1 = (a o b) o c | a o b = (a x b) x 1
(a x ((b x c) x 1)) x 1 = (a o b) o c | (a x b) x c = a x (b x c)
(a x (b x (c x 1))) x 1 = (a o b) o c | (a x b) x c = a x (b x c)
((a x b) x (c x 1)) x 1 = (a o b) o c | a x b = b x a
((a x b) x (1 x c)) x 1 = (a o b) o c | (a x b) x c = a x (b x c)
(((a x b) x 1) x c) x 1 = (a o b) o c | a o b = (a x b) x 1
((a o b) x c) x 1 = (a o b) o c | a o b = (a x b) x 1
(a o b) o c = (a o b) o c

Oh, have the neutral element as well:

a o e(o) = a | a o b = a x b x 1
(a x e(o)) x 1 = a | (a = b) = ((a x inv(x,1)) = (b x inv(x,1)))
((a x e(o)) x 1) x inv(x,1) = a x inv(x,1) | (a x b) x c = a x (b x c)
(a x e(o)) x (1 x inv(x,1)) = a x inv(x,1) | a x inv(x,a) = e(x)
(a x e(o)) x e(x) = a x inv(x,1) | a x e(x) = a
a x e(o) = a x inv(x,1) | (a = b) = ((inv(x,c) x a) = (inv(x,c) x a))
inv(x,a) x (a x e(o)) = inv(x,a) x (a x inv(x,1)) | (a x b) x c = a x (b x c)
(inv(x,a) x a) x e(o) = inv(x,a) x (a x inv(x,1)) | inv(x,a) x a = e(x)
e(x) x e(o) = inv(x,a) x (a x inv(x,1)) | (a x b) x c = a x (b x c)
e(x) x e(o) = (inv(x,a) x a) x inv(x,1) | inv(x,a) x a = e(x)
e(x) x e(o) = e(x) x inv(x,1) | e(x) x a = a
e(x) x e(o) = inv(x,1) | e(x) x a = a
e(o) = inv(x,1)

As you might imagine, it is not a very exciting game in its current form. One might imagine replacing the typographical symbols with mushrooms and small furry animals, and the addition of fireworks and showers of colourful jewels on the successful completion of one's proof obligations. Maybe even a fountain of money.

Roam the countryside and befriend local wildlife with your awesome powers of axiomatic rigor! Bring down the castle drawbridge with a well-placed induction! Banish ghosts with the radiant aura of reductio ad absurdum!

Reducing the rest of mathematics to gameplay mechanics remains an open question.

Codewise, what I'm doing looks like this (leaving out all the hairy bits):

type Op = String
data Expr = Expr (Op, Expr, Expr)
| A | B | C
| Inv (Op, Expr)
| Neutral Op
| Literal Int

type Pattern = Expr
type Substitution = Expr

data Rule = Rule (Pattern, Substitution)

type CheckableRule = ((Rule -> Bool), Rule)


isTrue :: Rule -> Bool
isTrue (Rule (a,b)) = a == b

isBinding :: Expr -> Rule -> Bool
isBinding e (Rule (a,b)) = e == a || e == b

opf :: Op -> Expr -> Expr -> Expr
opf op a b = Expr (op, a, b)


{-
Group axioms main stage:

Stability: a o b exists in G for all a, b in G
Magma!

Associativity: a o (b o c) = (a o b) o c
Semigroup!

Neutral element: a o 0 = 0 o a = a
Monoid!

Inverse element: a o a_inv = a_inv o a = 0
Group! Enter Abelian bonus stage!
-}
type CheckableRule = ((Rule -> Bool), Rule)

checkCheckableRule :: CheckableRule -> Bool
checkCheckableRule (p, rule) = p rule

associativity :: Op -> CheckableRule
associativity op = (isTrue, (A `o` (B `o` C)) `eq` ((A `o` B) `o` C))
where o = opf op

rightNeutral :: Op -> CheckableRule
rightNeutral op = (isBinding (Neutral op), (A `o` Neutral op) `eq` A)
where o = opf op

leftNeutral :: Op -> CheckableRule
leftNeutral op = (isBinding (Neutral op), (Neutral op `o` A) `eq` A)
where o = opf op

rightInverse :: Op -> CheckableRule
rightInverse op = (isBinding (Inv (op, A)), (A `o` Inv (op, A)) `eq` Neutral op)
where o = opf op

leftInverse :: Op -> CheckableRule
leftInverse op = (isBinding (Inv (op, A)), (Inv (op, A) `o` A) `eq` Neutral op)
where o = opf op

{-
Abelian bonus stage:

Commutativity: a o b = b o a
Abelian group! Enter ring bonus stage!
-}

commutativity :: Op -> CheckableRule
commutativity op = (isTrue, (A `o` B) `eq` (B `o` A))
where o = opf op

magma op = [] -- FIXME?
semiGroup op = magma op ++ [associativity op]
monoid op = semiGroup op ++ [rightNeutral op, leftNeutral op]
group op = monoid op ++ [rightInverse op, leftInverse op]
abelianGroup op = group op ++ [commutativity op]

{-
Ring bonus stage:

Show bonus function to be a semigroup!

Distributivity of x over o:
a x (b o c) = (a x b) o (a x c)
(a o b) x c = (a x c) o (b x c)
Pseudo-ring!
-}

leftDistributivity :: Op -> Op -> CheckableRule
leftDistributivity opO opX = (isTrue, (A `x` (B `o` C)) `eq` ((A `x` B) `o` (B `x` C)))
where o = opf opO
x = opf opX

rightDistributivity :: Op -> Op -> CheckableRule
rightDistributivity opO opX = (isTrue, (A `x` (B `o` C)) `eq` ((A `x` B) `o` (B `x` C)))
where o = opf opO
x = opf opX
{-
Neutral element for x: a x 1 = 1 x a = a
Ring!

Commutativity for x: a x b = b x a
Commutative ring! Enter field bonus stage!

Field bonus stage:

Inverse element for x in G: a x a_inv = a_inv x a = 1
Field! Superior! Shower of jewels!
-}

pseudoRing o x = abelianGroup o ++ semiGroup x ++
[leftDistributivity o x, rightDistributivity o x]
ring o x = pseudoRing o x ++ [rightNeutral x, leftNeutral x]
commutativeRing o x = ring o x ++ [commutativity x]
field o x = commutativeRing o x ++ [rightInverse x, leftInverse x]

1 comment:

Anonymous said...

I think that is awesome. Let us know when it's playable.

Blog Archive