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:
I think that is awesome. Let us know when it's playable.
Post a Comment