Fork me on GitHub
Math for the people, by the people.

User login

better than apmxi

Primary tabs

better than apmxi

I'm working on hammering out a better notation for talking about
math with the computer.

Critera:

* I want something better than the notation used by apmxi.

* This time I'd actually like both people and computers to understand what I'm saying.

* I want something "LISP-based" (because I like writing LISP code).

At this point, I'm still just sketching things out.

Here is an example. This is a version of the first proof in djao's
entry about cosets.

http://planetmath.org/encyclopedia/Coset.html

The style for definitions is based on APM-xi (roughly put, everything
in the definition is inside an "and").

Unfortunately, I don't have a very good sense of how to deal with
"mathematical foundations", so we begin with a couple of what seem to
be *particularly* weakly put together definitions.

Comments are welcome. I'd like to know what you think about the
readability of this code,

Joe

<pre>

(defn set (X)
(eq (type X)
set))

(defn elt (x X)
(member x X))

(defn subset (Y X)
(set Y)
(set X)
(forall y :in Y :st (elt y X)))

(defn operation (* X)
(set X)
(forall a b :in X :st (elt (* a b) X)))

(defn associative (* X)
(operation * X)
(forall a b c :in X :st (eq (* a b c)
(* (* a b)
c)
(* a
(* b c)))))

(defn group (G *)
(set G)
(operation * G)
(associative *)
(exists e :in G :st (forall a :in G :st (eq (* e a)
(* a e)
a)))
(forall a :in G :st (exists a' :in G :st (eq (* a a')
(* a' a)
e))))

(defn subgroup (H G)
(group H)
(subset H G))

(defn coset (a H G S)
(group G)
(subgroup H G)
(elt a G)
(eq S (setof (* a h) :st h :in H)))

(defproof two-left-cosets-identical-or-disjoint ()
(coset a H G aH)
(coset b H G bH)
(if (elt c (intersection aH bH))
;; this is the body of the proof
(and
;; rewriting what it means for `c' to be in the intersection of
;; the two cosets
(exists h1 h2 :in H :st (eq c
(* a h1)
(* b h2)))
;; use the last equality to show another equivalent equality
;; first step
(eq (* (inv b) a h1)
h2)
;; second step
(eq (* (inv b) a)
(* h2 (inv h1)))
;; conclude from the last step (and closure of H) -- [0]
(elt (* (inv b) a) H)
;; we now make a big statement about elements of H
(forall h :in H :st (and
;; [1]
(eq (* a
h)
;; introduce `e' in a nice way
(* (* b
(inv b))
a
h)
;; regroup terms
(* b
(* (inv b)
a)
h))
;; from [0] and the definition of bH
;; [2]
(elt (* b
(* (inv b)
a)
h)
bH)
;; just rewrite [2] using [1]
(elt (* a
h)
bH)))
;; shorthand for a variation on the last chain of reasoning
(symmetrically b a
bH aH)
;; summarize the last step
(subset aH bH)
;; using the previous symmetrical argument
(symmetrically bH aH)
(eq aH bH))
;; if there is no element `c' in the intersection
;; the intersection is empty
(eq (intersection S1 S2) nil)))


In case you want to easily download and play this code, I'm posting it on
my webpage too.

http://www.ma.utexas.edu/~jcorneli/j/cosets.lisp

Subscribe to Comments for "better than apmxi"