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.


* 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.

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,



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

(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)
(* 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)
(forall a :in G :st (exists a' :in G :st (eq (* a a')
(* a' a)

(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
;; 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)
;; 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
;; introduce `e' in a nice way
(* (* b
(inv b))
;; regroup terms
(* b
(* (inv b)
;; from [0] and the definition of bH
;; [2]
(elt (* b
(* (inv b)
;; just rewrite [2] using [1]
(elt (* a
;; 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.

Subscribe to Comments for "better than apmxi"