Some sums

1 − 1 + 1 − 1 + ... = 1/2

1 + 1 + 1 + 1 + ... = -1/2

1 + 2 + 3 + 4 + ... = -1/12

1 + 2 + 4 + 8 + ... = -1

1 − 2 + 4 − 8 + ... = 1/3

1 * 2 * 3 * 4 * ... = sqrt(2*pi)

2 * 3 * 5 * 7 * ... = 4*pi^2

Why is the derivative of a type a zipper

Why is the derivative of a regular type its type of one-hole contexts?

Let us define a function that counts the elements of a type, |()| = 1, |Void| = 0, |Either x y| = |x|+|y|, |(x,y)|=|x|*|y|, |List A| = 0 + |A| + |A|^2 + |A|^3 + ... (because lists can be [], [a], [a,b], and so on)

In general the 'size' of any type can be written as a power series (like an infinite polynomial), now for the type |k|*|x|^3, if we punch a hole in it, we get |k|*|x|^2 but we could have picked one of 3 different places to put it so we need to say which one, this gives 3*|k|*|x|^2, and this should be done to every term of a power series.

Since the derivative of a type = the derivative of its powerseries* this explains why we can 'differentiate' a type and get a zipper. (At least it sort of makes sense).

(* why is this true?)

Algebra System

I have made a start on this already, al-jabr. Really what I am doing here is just getting my toes wet - What I want to do is:

• Algebra hierarchy -- build up monoids, groups, fields etc and develop the basic theory of these structures also give concrete implementations of things like integers, reals (isomorphisms with efficient representations would be nice too!)


• Algebraic algorithms -- produce algorithms that can be used to help me do mathematics (e.g. factoring, transformations, solving classes of equations)


• Wiki -- Dependently typed programming in the large has already been done, they came up with FTA and FTC -- this is a constructive proof that it works!

There are some projects already working on this kind of thing, http://c-corn.cs.ru.nl/, http://github.com/Eelis/new-alg-hierarchy, http://www.lix.polytechnique.fr/coq/contribs/Algebra.html, http://hlombardi.free.fr/liens/constr.html, http://www.lix.polytechnique.fr/~assia/rech-eng.html, help make this list bigger!.

Ignoring these would be so dammed stupid I am not even going to think about it, but I want to point out that unless we make the most use of these projects as is possible then anything we create will be an anti-social library that nobody can use except me -- that is not desirable.

I think the only way to get this done is by collaborating with other people in a formally checked wiki (http://www.vdash.org/, http://code.google.com/p/hol-online/, http://prover.cs.ru.nl/login.php, http://www.cs.ru.nl/~herman/afstud.html, more?). These projects are all 'beta' that don't let everyone get involved so that's not very useful. Lets write it in Ur perhaps, using Coq as a subprocess. The directory structure of the Coq libraries would reflect that of the wiki. Edits will be accepted if they are checked and correct. I think once you have a spinal chord implemented, people will be able to add on parts quite easily.

I see no reason why someone with a bit of time wouldn't pick up Disquisitiones Arithmeticae or whatever and fold it into the wiki. With a bit of work getting everything set up correctly I think we could make a useful (basic) algebra system.

LU Decomposition in Prolog

:- use_module(library(clpr)).

// various obvious bits of matrix machinary.

lu_decompose(M, L*U) :-
 dimensions(M,N*N),
 dimensions(L,N*N),
 dimensions(U,N*N),
 lower(L),
 upper(U),
 matrix_multiply(L,U,M).

ZFC's probably inconsistent

Now stop worrying and enjoy your life.

Nice books

Cantors Diagonalization Proof in Coq

Axiom b : (nat -> nat) -> nat.
Axiom b' : nat -> (nat -> nat).

Axiom bijection : forall f, b' (b f) = f.
Axiom bijection' : forall x, b (b' x) = x.

Definition Stream A := nat -> A.
Definition Map {A B} (f : A -> B) : Stream A -> Stream B :=
  fun sa =>
    fun i =>
      f (sa i).

Definition l : Stream (nat -> nat) -> Stream nat :=
  Map b.
Definition l' : Stream nat -> Stream (nat -> nat) :=
  Map b'.

Definition isnt x :=
  match x with
    | O => S O
    | S _ => O
  end.

Theorem isn't_isnt {x} : isnt x <> x.
  destruct x; discriminate.
Qed.

Definition Diagonal {A} (s : Stream (Stream A)) : Stream A:=
  fun i => s i i.

Definition Diagonalization (sequences : Stream (nat -> nat)) : Stream nat :=
  Map isnt (Diagonal sequences).

Theorem isn't_in {sequences} : forall i, Diagonalization sequences <> sequences i.
intros; intro.
pose (f_equal (fun f => f i) H) as H'.
unfold Diagonalization in H'.
unfold Diagonal in H'.
unfold Map in H'.
revert H'.
apply isn't_isnt.
Qed.

Definition pink_elephant : Stream nat := fun i => i.

Definition sequence_enumeration : Stream (nat -> nat) := l' pink_elephant.

Theorem every_sequence : forall s, exists i, s = sequence_enumeration i.
intro s; exists (b s).
unfold sequence_enumeration.
unfold pink_elephant.
unfold l'.
unfold Map.
rewrite bijection.
reflexivity.
Qed.

Theorem Cantor : False.
destruct (every_sequence (Diagonalization sequence_enumeration)) as [i iPrf].
pose (@isn't_in sequence_enumeration i).
contradiction.
Qed.