Thursday, 24 May 2007

The type says everything

I've mentioned a number of times that given a sufficiently rich type theory we can use the type to provide a specification for the function, such that the function is correct by construction. I'd like to give a simple example of how this works in the Coq proof assistant.

The following code is an illustration of how the type theory of Coq allows you to fully specify the behaviour of functions. Kragen Sitaker made the comment that there weren't too many reasonable interpretations of the function of the type given to the assoc function:

A -> list (A * B) -> option B 

that is, a function taking an element of type A, a list of pairs of A and B, to the possibility of a B (and possible failure). That got me wondering how hard it would be to tighten the noose so that there was only one way to interpret the type but still possibly many implementations that satisfy the type, all of which will yield the same result.

The following code illustrates that this is indeed possible to do in Coq.

Require Import List. 
Parameter A : Set.
Parameter B : Set. 
Definition assoc_list := list (A * B)%type. 
Parameter eq_dec : forall (x:A) (y:A),{x=y}+{x<>y}.

Theorem assoc : 
  forall (x:A) (l: assoc_list), 
    {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}.
  refine 
    (fix assoc (x:A) (l:assoc_list) {struct l} 
      : {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}
      := match l 
           return {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}
           with 
           | nil => inright _ (fun y => (fun p : In (x,y) nil => _))
           | ((x',y)::t) => 
             match eq_dec x x' with
               | left lft => inleft _ (exist _ y _)
               | right rgt => match assoc x t with 
                                | inleft (exist y p) => inleft _ (exist _ y _)
                                | inright inrgt => inright _ _
                              end
             end
         end) ; clear assoc ; eauto ; subst. constructor. reflexivity.
  firstorder. intros. intro. inversion H ; clear H. firstorder. congruence.
  apply (inrgt y0). assumption.
Defined.

This isn't the most beautiful code but what it lacks in beauty of implementation it makes up for in ease of reading. There are only a couple of lines that you need to understand to be assured that this is in fact the correct implementation.

Theorem assoc : 
  forall (x:A) (l: assoc_list), 
    {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}.

This function has a type that takes an "x" of type "A", a list of pairs and supplies a value "y" of type "B" with a proof that it came from a pair in which the x provided occurs *AND* that that pair exists in the list l. If the function can't find a pair from which to supply a y, it must supply a proof that no such pair exists in the list.

First a bit of the notation so you can read this theorem properly

{ y | P y }

Can be read: "there exists a y such that the property P holds of y".

The notation:

A + {B}

Means that we must supply an A or a proof of B.

The "In" predicate is an inductive predicate which specifies membership in a list and is provided by the Coq library.

With a little practice reading types, we can see that the two lines are correct. We can then run Coq on this code to check that the proof is correct and we can be assured of the correctness of the implementation WITHOUT EVER READING THE CODE! This means we have reduced the problem of correctness to two simple lines of completely declarative statements.

This function is more complicated than a normal assoc function because it carries all of these proof terms along with it. However, because of the clever people involved in writing Coq we have actually mixed two different type universes together. One (called Set) for values and one (called Prop) for proofs. Coq uses this fact to do something very clever. The {y|P y} existential type and the A+{B} type are designed such that the "P y" proof and the {B} proof disappear when we extract (compile) our code. As an illustration of this amazing fact look at the following ocaml code which has been automatically extracted from our definition:

let rec assoc x = function
  | Nil -> Inright
  | Cons (p, t) ->
      let Pair (x', y) = p in
      (match eq_dec x x' with
         | Left -> Inleft y
         | Right -> assoc x t)

Voila! Not only are the proof terms gone, but this is pretty much the code you probably would have written yourself. Notice that "Inright" is a constructor with no information (other than failure), basically implementing the "Nothing" of a Maybe type, and the "Inleft" as the "Just" of a Maybe type.

We have extracted a provably terminating, well specified, totally correct function that runs in ocaml! And to top it off we can also compile to Haskell!!

assoc :: A -> Assoc_list -> Sumor B
assoc x l =
  case l of
    Nil -> Inright
    Cons p t ->
      (case p of
         Pair x' y ->
           (case eq_dec x x' of
              Left -> Inleft y
              Right -> assoc x t))

So it isn't as if this isn't without some cost. There is a huge learning curve on Coq and I'm by no means an expert. The proofs can be arduous, and although this one only took me a couple of minutes, it took far longer than it would have to implement the function directly in ocaml. However as I gain experience with Coq, I increasingly believe the approach will scale better than traditional approaches to software design.

In addition to these caveats there is more than one function that satisfies this type. Namely there is an assoc which starts returning from the end of the list, instead of the beginning. We could get rid of this problem by specifying which of the elements should be returned, returning all of them, or restricting formation of assoc's such that they are mappings. The latter is very elegant, but somewhat more involved than what we have done.

Functional programming reduces the difficulty of writing correct software by reducing the ways in which bugs can occur. However, most functional programming languages are unable to put complex constraints like "this is a sorted list" or "implements an assoc function" into the language. When other functions rely on the behaviour all kinds of funny things can happen.

I recently had a nasty non-termination bug in SML because a function *required* that the input list be sorted or the function wouldn't terminate. My sort routine made use of a bogus less-than-equal predicate over a data-type which I had neglected to write properly. This caused hours of very difficult debugging.

I'm acting on the thesis that I can avoid these problems and I am rewriting a large program in Coq as an experiment. I'll let you know how it goes.

Saturday, 21 April 2007

We don't need no stinking modules!

In my last post I described how unbelievably cool modules are in Coq. Well it turns out that there is some disagreement in the community about whether one should even use them!

Why? Because the type system in Coq is so powerful we hardly even need them. In fact with a bit of syntactic sugar for inductively defined types and the generation of constructors we magically get something like first class modules (first-class meaning modules that are actually values that can be passed around to functions etc...). Enter the Record.

Record MonadBind : Type :=
  { M : forall (A : Type), Type;
    bind : forall (A B : Type), M A -> (A -> M B) -> M B; 
    ret : forall (A : Type), A -> M A; 
    left_unit : forall (A B : Type) (f : A -> M B) (a : A), 
      bind A B (ret A a) f = f a;
    right_unit : forall (A B : Type) (m : M A), 
      bind A A m (ret A) = m;
    bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B), 
      bind B C (bind A B m f) g = bind A C m (fun x => bind B C (f x) g)
  }.

This implements exactly the same strict controls on the instantiation of a Monad that were given with our MONAD signature in the previous post. Each type can rely on previously defined types in the record giving us the full dependent type system needed to specify a proper monad. With a little bit of work we can rewrite our module to be an instantiation of a record.

Look here for the example code

How cool is that!

How a real module system should work

I've been playing with the Coq proof assistant over the past few days, following closely on some frustrations that I've been having with using SML's module system and a bit of toying with type-classes in Haskell.

The gist of the problem is this. Although you can define type-classes and modules such that external users of these modules/type-classes see a uniform interface, consistency is left as an exercise for the implementer. This is not really acceptable in my view. When you are writing software, often times *you* are the implementer. What you really want is for these modules not just to provide a consistent interface to outsiders, but to guarantee the correctness of the implementation! Isn't that the whole point of types? If we can't do that, why are we using types?

Ok, so in Coq I *can* get the properties I've been wanting out of SML's module system. For instance take the following implementation of the Monad signature:

Module Type MONAD.
Set Implicit Arguments. 

Parameter M : forall (A : Type), Type.
Parameter bind : forall (A B : Type), 
  M A -> (A -> M B) -> M B.
Parameter ret : forall (A : Type), 
  A -> M A.

Infix ">>=" := bind (at level 20, left associativity) : monad_scope.
Open Scope monad_scope.

Axiom left_unit : forall (A B : Type) (f : A -> M B) (a : A), 
  (ret a) >>= f = f a.
Axiom right_unit : forall (A B : Type) (m : M A), 
  m >>= (fun a : A => ret a) = m.
Axiom bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B), 
  (m >>= f) >>= g = m >>= (fun x => (f x) >>= g).

End MONAD.

This signature describes something much like the monad that is given by the type-class in haskell. I neglected some stuff like implementing join from bind etc, but we can safely ignore that for now. The point is that users of the MONAD signature can't just fake a monad by supplying an implementation that is nominally the same. i.e. In order to implement this MONAD you actually have to have the right signature for ">>=" *AND* you have to satisfy the monad laws. So what does an implementation look like? Here is an example:

Module ListMonad < : MONAD. 

Require Import List.

Set Implicit Arguments.
 
Definition M := list.

Fixpoint bind (A : Type) (B : Type) (l : M A) (f : A -> M B) {struct l} : M B := 
  match l with 
    | nil => nil 
    | h::t => (f h)++(bind t f)
  end.

Infix ">>=" := bind (at level 20, left associativity) : monad_scope.
Open Scope monad_scope.

Definition ret (A : Type) := fun a : A => a::nil.

Lemma left_unit : forall (A B : Type) (f : A -> M B) (a : A), 
 (ret a) >>= f = f a. 
Proof. 
  intros. simpl. rewrite app_nil_end. reflexivity.
Defined. 

Lemma right_unit : forall (A B : Type) (m : M A), 
  m >>= (fun a : A => ret a) = m.
Proof. 
  simple induction m. 
    simpl. reflexivity. 
    intros. simpl.
    cut (bind l (fun a0 : A => ret a0) = l).
      intros. rewrite H0. reflexivity.
      exact H.
Defined. 

Lemma bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B), 
  (m >>= f) >>= g = m >>= (fun x => (f x) >>= g).
Proof. 
  simple induction m. 
    intros. simpl. reflexivity.
    intros. simpl. 
    cut (l >>= f >>= g = l >>= (fun x0 : A => f x0 >>= g)).
      intros. rewrite < - H0.
      induction (f a). 
        simpl. reflexivity.
        simpl. rewrite IHm0. rewrite app_ass. reflexivity.
      apply H. exact x.
Defined.

End ListMonad.

(* Example *)
Import ListMonad.
Require Import Peano.
Require Import List.

Fixpoint downfrom (n : nat) {struct n} : (list nat) := 
  match n with 
    | 0 => n::nil
    | S m => n::(downfrom m)
  end.

Eval compute in (1::2::3::4::nil) >>= downfrom.
  = 1 :: 0 :: 2 :: 1 :: 0 :: 3 :: 2 :: 1 :: 0 :: 4 :: 3 :: 2 :: 1 :: 0 :: nil
     : M nat

Ok, That took me about an hour to write. I'm not really that good at using Coq, so presumably you could do this more elegantly and in less time. In any case it would be nice if the proofs could be automated a bit more. That aside this is a *much* better situation than we have in SML and Haskell. We have provided a monad that is guaranteed to actually be one!

I'm of the growing opinion that software that is forced to meet specifications will end up being less trouble in the end than the current state of free-wheeling wild-west style implementation.

Coq gives a civilized alternative to the current free-for-all. Coq can help us make good on the promise that "well typed programs can't go wrong".

Thursday, 8 March 2007

Coq

A few months ago I started messing around with The Coq Proof Assistant to figure out what exactly it was, and proceeded to go through the tutorial.

Coq provides a nice interface for doing proofs in an interactive session. It was a lot of fun but didn't seem particularly useful for my research.

As I've been playing with the notion of Total Functional Programming, I ended up reading (and actually doing homework) from a book entitled "Type Theory and Functional Programming". This book is excellent by the way! I highly recommend it to anyone interested in dependent types/proof theory/type theory. It has a very lucid style and makes a lot of complex notions in type theory very easy to understand. I even got to find an error in one of the homework examples (now listed in the errata) which is always fun.

After working through the first 5 chapters I started looking around for a system that would let me apply some of the principles that I had learned.

As it turns out Coq is really a dependently typed functional programming language masquerading as a proof assistant! I've spent quite a lot of time over the past few weeks writing total functional programs in Coq and proving properties about them. I've done a bunch of simple things so far, including a proof of correctness for various properties of insertion sort. I started with merge sort, but stalled when it got too complicated. I'm starting to get a feel for using Coq however and large proofs are getting much easier.

In my research I've been working on the implementation of the distillation algorithm (a form of super-compilation) for logic programming. As it turns out
the distillation algorithm as described by Geoff Hamilton could be a real boon to total functional programming in Coq.

In Coq all functions and other values are terms that represent witnesses of a proof. Inhabitation of types is proved exactly by creating a term of the appropriate type. The "tactic" system in Coq is basically a library that helps you build appropriate terms. Alternately you can supply the proofs directly by writing in the functional programming language that acts as the witness terms of the types.

In order to avoid inconsistency functions are not capable of general recursion or errors or exceptions, as this can immediately lead to proofs of propositions which are not actually inhabited. A simple example (in psuedo-haskell) would be a function with the following structure.

loop :: int -> arbitrary
loop x = loop x

Clearly "int -> arbitrary" is not actually the type of this function. It doesn't terminate and so has type _|_. Types in languages like ML and haskell aren't actually just as they are written, but include the possibilities of non-termination or errors into the type implicitly. This (arguably) works out alright if you expect to run your program, but if you are trying to prove useful properties in your type system it turns out to be pretty worthless.

Syntactic restrictions are therefor necessary to avoid including non-terminating functions in Coq. The method chosen is to accept only structurally recursive functions, which can be checked with simple syntactic criterion. In fact the functions require you to specify *which* argument of a function is structurally recursive. This works out surprisingly well but can occasionally be a real pain (try working out a unification algorithm without using anything but structural recursion).

In Coq 8.1 they include a way to define functions that include a measure function which provably decreases or to use a well-founded relation (in conjunction with a proof) to show that the function terminates.

Distillation likes to take functions from general recursion to structural tail recursion. If you could define functions in Coq such that they were then processed by distillation, it would be very useful!

If you haven't tried Coq yet, you should. And if you haven't tried total functional programming yet, I suggest trying it in Coq.

Wednesday, 28 February 2007

Protected access using lightweight capabilities

The following is some SML code that implements the natural numbers using peano arithmetic in the SML type system. These numbers can be used to protect access to list functions. I haven't yet figured out if addition is possible, but I'm hoping that it is. It could be really handy!

signature SLIST = 
sig
    type 'a nat 
    type Z
    type 'a S
    val S : 'a nat -> 'a S nat
    val P : 'a S nat -> 'a nat
    val Z : unit -> Z nat
    val zerop : 'a nat -> bool
    val toInt : 'a nat -> int 

    type ('elt,'n) slist

    val snil : unit -> ('elt, Z nat) slist
    val scons : 'elt -> ('elt, 'n nat) slist -> ('elt, 'n S nat) slist
    val :+: : 'elt * ('elt, 'n nat) slist -> ('elt, 'n S nat) slist
    val shd : ('elt, 'n S nat) slist -> 'elt
    val stl : ('elt, 'n S nat) slist -> ('elt, 'n nat) slist
    val slen : ('elt, 'n S nat) slist -> int

end

structure SList :> SLIST = 
struct 
    (* encode integer types *) 
    type 'a nat = int
    type Z = unit
    type 'a S = unit
    fun S i = i+1; 
    fun P i = i-1;
    fun Z () = 0 
    fun zerop 0 = true 
      | zerop _ = false
    fun toInt d = d

    type ('elt, 'n) slist = 'elt list * 'n

    fun snil () = ([],0)

    fun scons elt sl =
 let val (l,i) = sl 
 in ((elt::l),S i)
 end    

    infixr :+:
    fun x :+: y = scons x y

    fun shd sl = 
 let val (h::t,i) = sl 
 in h
 end

    fun stl sl  = 
 let val (h::t,i) = sl 
 in (t,P i) 
 end

    fun slen sl = 
 let val (_,i) = sl 
 in i 
 end

end 
 
open SList
infixr :+:

val mylist = 1 :+: 2 :+: 3 :+: snil();
val the_head = shd mylist; 
val the_tail = stl mylist; 
val the_next_head = shd the_tail;
(* 
This doesn't even compile! 
val head_of_nil = shd (snil())
*)

Saturday, 3 February 2007

Automated Deduction and Functional Programming

I just got "ML for the working programmer" in the mail a few days ago,
and worked through it at a breakneck pace since receiving it. It
turns out that a lot of the stuff from the "Total Functional
Programming" book is also in this one. Paulson goes through the use
of structural recursion and extends the results by showing techniques
for proving a large class of programs to be terminating. Work with
co-algebras and bi-simulation didn't quite make it in, except for a
brief mention about co-variant types leading to the possibility of a
type: D := D → D which is the type of programs in the untyped lambda
calculus, and hence liable to lead one into trouble.

I have to say that having finished the book, this is the single most
interesting programming book that I've read since "Paradigms of
Artificial Intelligence Programming" and "Structure and Interpretation
of Computer Programs". In fact, I would rate this one above the other
two, though I think it might be because of my current interests.

The conjunction of "Total Functional Programming" and "ML for the
Working Programmer" have completely changed my world view of automated
deduction. Interestingly, my advisers work looks even more appealing
from this perspective.

The basic crux of the issue is this. Given that we restrict ourselves
to total functional programming, as described in the aforementioned
article, we will have the ability to prove theorems directly by
manipulation of the program source.

My adviser told me about this the first time that I met him. It at
first seemed like a curiosity. It has however, blossomed into a
completely different way of thinking about how proofs should be
performed.

I've spent the last few days converting proofs into program source,
which I then manipulate equationally. I have a few examples of
inductive proofs that can be written quite naturally as structurally
recursive functions.

datatype nat = Z | S of nat

fun lt n m = 
    case m of 
 Z => false
      | (S m') => 
 case n of 
     Z => true 
   | (S n') => lt n' m'

fun divide n d = 
    case n of 
 Z => (Z,Z)
      | (S n') => 
 let val (q',r') = divide n' d in 
     case lt (S r') d of 
  true => (q',S r')
       | false => (S q',Z)
 end

Both of these functions are direct "extractions" of a program from a
proofs that I wrote. The second one is a proof with two existential
variables. The two existential variables present themselves as return
values. In the case of "lt" it simply computes a truth value.

The datatype nat = Z | S of nat defines natural numbers with the
correspondence Z=0, S(Z)=1, S(S(Z))=2 etc...

The proof is a proposition that goes like this:

∀n,d:nat. d>0 ∃q,r:nat. n=dq+r ∧ 0≤r<d

You might notice I dropped the restriction on d in the actual source
code. That can be encoded with an auxiliary function in any case.

The proof proceeds inductively, basically you can turn the divide
function inside out to recover the inductive proof.

The base case is n=0 which gives 0=dq+r which gives r=0 and q=0 (since
d is greater than 0). The first case is exemplified in the case
structure above. (Z,Z) = (q,r) the two existential variables are
returned with a valid result for n=0.

The inductive case is this.

n: ∃q,r. n=dq+r ∧ 0≤r<d
(n+1): ∃q',r'. n+1=dq'+r' ∧ 0≤r'<d
if(r+1)<d
then n+1=dq+r+1

We see that this gives us that r'=r+1, q'=q giving us a solution to r' and q' from r and q (and hence solving the n case, gives us some information about n+1)

else n+1 = d(q+1)+r'

which we can rewrite as: n+1 = d(q+1)+r' = dq+d+r'=dq+r+1 so d+r'=r+1,
but r+1 must be at least d otherwise we wouldn't have failed the test
r+1<d, and r' can be no less than zero, so we must choose r'=0
this results in (finally!)

n+1 = d(q+1) with r'=0,q'=q+1

We have a proof! For the extracted program you can look at the source
and see that in fact it mirrors the proof directly, short of a few
simplifications done by hand. Making use of the r,q in the proof of
r' and q' is the same as my use of r and q in my proof of the n+1 case.

I'm looking forward to a deeper understanding of the correspondences
between proofs and programs with my new found capacity to produce actual functional program proofs by extraction manually. I'm also
curious to try my hand at generating termination proofs directly, and
also at making a syntax that more directly supports total functional
programming.

Friday, 26 January 2007

Total Functional Programming

Recently on Lambda the Ultimate there was a post called "Total Functional Programming".  The title didn't catch my eye particularly, but I tend to read the abstract of any paper that is posted there that doesn't sound terribly boring.  I've found that this is a fairly good strategy since I tend to get very few false positives this way and I'm too busy for false negatives.

The paper touches directly and indirectly on subjects I've posted about here before.  The idea is basically to eschew the current dogma that programming languages should be Turing-complete, and run with the alternative to the end of supplying
"Total Functional Programming"

At first glance this might seem to be a paper aimed at "hair-shirt" wearing functional programming weenies.  My reading was somewhat different.

Most hobbiest mathematicians have some passing familiarity with "Turing's Halting Problem" and the related "Goedel's Incompleteness Theorem".  What this paper is trying to do is say "So what!".  The basic idea is that restriction to a syntacticly restricted language can restrict the semantics in such a way that these problems do not apply.  The resulting (*huge*) class of programs can then solve almost everything that we think is important. 

The "Bazooka" of the paper is a line describing how every program for which we have a complexity upper bound, is in fact inside the restricted language.  This realisation is profound.  It means that all of the algorithms that anyone has bothered to find upper bounds for (a huge class of programs mind you!) is accessible to this technique. 

The paper even deals with infinite data (co-data) in the framework and mechanisms to properly account for streams and other (possibly) infinite structures.

The idea of working in syntactically restricted languages that are sub-Turing (for any number of reasons) is not new.  In fact I think I've mentioned DataLog (wikipedia entry) previously.  In the case of DataLog however, there are serious deficiencies in the expressive power.

Definitely the best paper I've read this year.  I'm not sure how accessible it is to lay-people, but it should be accessible to anyone with a CS B.S. or people who have some familiarity with functional programming.

Saturday, 13 January 2007

Addition in the lambda calculus

I just spent a couple of very cold weeks in Anchorage Alaska.  I went out with a bunch of friends to a bar on the night prior to leaving, where I met up with an old friend (and listened to two other friends play music).  I started describing the lambda calculus to him since it is related to my work and he was curious what I was up to.  In any case I found myself unable to produce addition of the church numerals off the top of my head, which I found pretty disturbing since it shows that I probably didn't quite understand it in the first place.  Therefor I sat down this morning to see if I couldn't reconstruct it from first principles. 

It turns out that it is relatively easy. First, let us start with a bit of notation, and a description of the lambda calculus.  Since wikipedia describes the lambda calculus in detail, I'll just show how one procedes with calculations.  As examples let us start with the church numerals

1 = (λf x.f x)
2 = (λf x.f f x)
3 = (λf x.f f f x)
...
n = (λf x.fn x)

where fn means "f f ... f" n times.

The idea is that each numeral is represented by a lambda term.  The lambda term describes the arguments (f and x in this case) and the "body" in which we substitute the arguments when the are passed in.  An example of an "application" of a lambda term to an argument would be:

1 g = (λf x . f x) g => (λx . g x)

We pass in g, and replace every occurance of f in the body with g, and delete f from the list of variables.  we can continue to apply this term to another term

(λx . g x) y => g y

Which leads us to conclude that

1 g y => g y

Ok, so now that you've seen a few calculations, let us try to construct addition.  The first thing I tried to do is to construct the function +1.  Clearly, we want +1 n => (n+1).  n+1 is (λf x. f(n+1) x) which is also (λf x. f fn x).  Since n = (λf x. fn x) we need to somehow add another f.  The trick is to get the arguments to use the same symbols, and to remove the lambda abstraction.  We can do this by applying the church numeral to the symbols we want to use, in this case f and x.

(λf x. fn x) f x => fn x

So now we know how to get rid of the lambda abstraction.  Now we can add an f on the front, which will get us closer to n+1.

f (λf x. fn x) f x => f fn x

We are almost there.  Now we need to have the λf x part at the beggining so that we look like a church numeral.

(λf x. f (λf x. fn x) f x) => (λf x. f fn x) = (λf x. f(n+1) x)

Looking great so far!  Now we just need to be able to take the whole (λf x. fn x) form as an argument.  This turns out to be really easy, we just put a variable in it's place and add it to the front of the list of lambda arguments.

(λa f x. f a f x) (λf x . fn x) => (λf x. f (λf x. fn x) f x) => (λf x. f fn x)

This shows that (λa f x. f a f x) is the +1 function! 

+1 = (λa f x. f a f x)

Ok, so now that we have +1 can we get a function that takes an n and returns +n?  This would get us a long way towards addition.  We can call this function n->+n.

Ok, so we can guess what +n will look like easily.  It's going to look just like +1 except with n leading f's.

+n = (λa f x. fn a f x)

So we should try to figure out how to take the fn out of a church numeral, and place it there.  Well, we should apply the same trick of applying the church numeral to f and x so that we can extract the body.

(λf x . fn x) f x => fn x

ok, but really we want a to follow, based on +n, so instead of using x, let us apply the form to a.

(λf x . fn x) f a => fn a

Great!  Look how close we are. now we just need to abstract the a,f,x and place f x following it.
(λa f x. (λf x . fn x) f a f x) => (λa f x. fn a f x)

Ok, so now that we know how to take an n, and able to take the entire church numeral n as an a beta reduce it to n+1, let us abstract the n as an argument

(λb a f x. b f a f x)

Let us verify quickly that this function works.

(λb a f x. b f a f x) n =>
(λa f x. n f a f x) =>
(λa f x. (λf x. fn x) f a f x) =>
(λa f x. fn a f x)

Now, we can verify that this works on m, to obtain n+m as the +n function should:

(λa f x. fn a f x) m =>
(λf x. fn (λf x. fm x) f x) =>
(λf x. fn fm x) = (λf x. f(n+m) x) = n+m

Hooray! Not only did we find n->+n, but we have obtained the function "addition" for free.  Since, once we have the +n function we can apply it to m.  So we now have the function:

add = (λb a f x. b f a f x)

I haven't tried multiplication and exponentiation yet, but you are welcome to try!