## Saturday, 20 September 2008

### Accessing Ackermann

`(* The Ackermann function is defined by the equations: * *          n+1             m=0 * A(m,n) = A(m-1,1)        m>0 n=0 *          A(m-1,A(m,n-1)) m>0 n>0 *)(* It's an example of something not structurally recursive, * that means it's going to be a lot of fun to try and define * in type theory. *)(* A simple example to look at first is double: *)Fixpoint double (n : nat) : nat :=  match n with    | O => O    | S m => S (S (double m))  end.(* From the definition you can see that every application of double * is done with m = S n *)Definition nat_struct n m := m = S n.(* This is a well founded relation *)Theorem well_founded_nat_struct : well_founded nat_struct.  unfold well_founded.  (* forall a : nat, Acc nat_struct a *)  Print Acc.  (* Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=         Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x   *)  (* For some relation to be well founded, every element must be     accessable   *)  induction a.  (*     ============================     Acc nat_struct 0          subgoal 2 is:     Acc nat_struct (S a)   *)  apply Acc_intro; intros.  discriminate.    apply Acc_intro; intros.  injection H; intros.  (*     a : nat     IHa : Acc nat_struct a     y : nat     H : nat_struct y (S a)     H0 : a = y     ============================     Acc nat_struct y   *)  rewrite <- H0; assumption.Defined.(* Must used Defined. instead of Qed. here if you want to be * able to use the computational properties of any definition * given by well_founded_induction on nat_struct *)Definition double' : nat -> nat.apply (well_founded_induction well_founded_nat_struct).(*  ============================   forall x : nat, (forall y : nat, nat_struct y x -> nat) -> nat *)intros x double'.refine (match x as x' return x = x' -> nat             (* the trick here ^ is one of many that gives me more                information about the pattern match than I would get                normally *)          with          | O => fun eq => O          | S n => fun eq => S (S (double' n _))                      (* the underscore here ^ is a proof obligation *)        end (refl_equal x)).(* x : nat   double' : forall y : nat, nat_struct y x -> nat   n : nat   eq : x = S n   ============================   nat_struct n x*)unfold nat_struct.(* x : nat   double' : forall y : nat, nat_struct y x -> nat   n : nat   eq : x = S n   ============================   x = S n *)congruence.Defined.Print double'.(*double' = well_founded_induction well_founded_nat_struct (fun _ : nat => nat)  (fun (x : nat) (double' : forall y : nat, nat_struct y x -> nat) =>   match x as x' return (x = x' -> nat) with   | 0 => fun _ : x = 0 => 0   | S n => fun eq : x = S n => S (S (double' n eq))   end (refl_equal x))     : nat -> nat*)Eval compute in (double' 6).(*     = 12       : nat *)Extraction double'.(* let rec double' = function *   | O -> O *   | S n -> S (S (double' n)) *)(* The extraction is very very clean, which is excellent! * It's just that one would like to know -why- the extraction * doesn't have any 'Acc' or 'well_founded_induction' in it. * It's not to do with Prop vs Set or Defined/Qed, the reason is * * Coq/contrib/extraction/mlutil.ml:let manual_inline_list =   let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in   List.map (fun s -> (make_con mp empty_dirpath (mk_label s)))    [ "well_founded_induction_type"; "well_founded_induction";       "Acc_rect"; "Acc_rec" ; "Acc_iter" ; "Fix" ]  * * I wish I knew why this was in here, I can only assume it's * some kind of historical artifact, anyway,Extraction Inline foo bar baz.  * works fine if I were to defined my own Acc type thing. *)(* So now we know _what_ to do, it's just a simple matter of doing it * I must define a relation that is Well Founded (and prove that), * and is suitable for defining the Ackermann function with *)Definition lt_prod_lt : nat * nat -> nat * nat -> Prop :=  fun pq mn =>    let (p,q) := pq in    let (m,n) := mn in         p < m      \/ p = m /\ q < n.Require Import Omega.Theorem well_founded_lt_prod_lt : well_founded lt_prod_lt.  (* ... long ugly proof omitted ... *)Defined.Definition Ackermann : nat -> nat -> nat.intros m n; generalize (m,n); clear m n. (* currying *)apply (well_founded_induction well_founded_lt_prod_lt).destruct x as (m,n).intro Ackermann.refine  (match m as m', n as n' return m = m' -> n = n' -> nat with     | 0,   n   => fun _ _ => S n     | S m, 0   => fun eq eq' => Ackermann (m, 1) _     | S m, S n => fun eq eq' => let x := Ackermann (S m, n) _ in Ackermann (m, x) _   end (refl_equal m) (refl_equal n));  rewrite eq; rewrite eq'; unfold lt_prod_lt; auto with arith.Defined.Eval vm_compute in (Ackermann 3 4).(*     = 125 *     : nat *)Extraction Ackermann.(*let ackermann m n =  let rec f = function    | Pair (m0, n0) ->        (match m0 with           | O -> S n0           | S m1 ->               (match n0 with                  | O -> f (Pair (m1, (S O)))                  | S n1 -> f (Pair (m1, (f (Pair ((S m1), n1)))))))  in f (Pair (m, n))*)(* Lots of fabulous tupling and untupling, * Actually, I don't like that, so I have defined a curried * Acc2 and given similar definitions as the Wf does *)Require Import Acc2.Definition lexi : nat -> nat ->                  nat -> nat ->                  Prop :=  fun p q m n =>       p < m    \/ p = m /\ q < n.Theorem well_founded2_lexi : well_founded2 lexi.  unfold well_founded2; unfold lexi.  induction m.   induction n.    apply Acc2_intro; intros.     elimtype False; omega.    apply Acc2_intro; intros.    destruct H.     inversion H.     destruct H.     destruct (lt_eq_lt_dec q n). destruct s.      destruct IHn.      apply H1.      right; split; auto.      rewrite H; rewrite e; apply IHn.      elimtype False; omega.   induction n.    apply Acc2_intro; intros.    destruct H.     apply Acc2_intro; intros.     destruct H0.      destruct (IHm q).      apply H1.       left; omega.      destruct H0.      rewrite H0.      destruct (IHm q).      apply H2.      destruct (lt_eq_lt_dec p m). destruct s.       left; assumption.       right; split; assumption.       elimtype False; omega.      destruct H.      inversion H0.     apply Acc2_intro; intros.     destruct H.      destruct IHn.      apply H0.      left; assumption.     destruct H.     destruct (lt_eq_lt_dec q n). destruct s.      rewrite H.       destruct IHn.       apply H1.       right; split; auto.      rewrite H; rewrite e; apply IHn.      elimtype False; omega.Defined.Definition Ack2 : nat -> nat -> nat.apply (well_founded2_induction well_founded2_lexi); intros m n Ack2.refine  (match m as m', n as n' return m = m' -> n = n' -> nat with     | 0,   n   => fun eq eq' => S n     | S m, 0   => fun eq eq' => Ack2 m 1 _     | S m, S n => fun eq eq' => let x := Ack2 (S m) n _                                  in Ack2 m x _   end (refl_equal m) (refl_equal n));  unfold lexi; rewrite eq; rewrite eq'.left; auto.right; auto.left; auto.Defined.(* One thing I don't like, is having this let x := .. but I don't know * how to remove that yet, anyway it doesn't matter much *)Extraction Ack2.(*let rec ack2 m n =  match m with    | O -> S n    | S m0 ->        (match n with           | O -> ack2 m0 (S O)           | S n0 -> ack2 m0 (ack2 (S m0) n0))*)Extraction Language Haskell.Extraction Ack2.(*ack2 :: Nat -> Nat -> Natack2 m n =  case m of    O -> S n    S m0 -> (case n of               O -> ack2 m0 (S O)               S n0 -> ack2 m0 (ack2 (S m0) n0))*)`

#### 1 comment: Anonymous said...

(* Ackermann isn't primitive recursive, but it is structurally recursive from a higher-order point of view, with a little help. *)

Fixpoint AckHelp (f:nat -> nat) (n:nat) : nat :=
match n with
| O => 1
| S n' => f (AckHelp f n')
end.
(* Note: AckHelp f == (nat_rec (fun _ => nat) 1 (fun _ => f)) *)

Fixpoint Ack (m:nat) : nat -> nat :=
match m with
| O => S
| S m' => fun n => (AckHelp (Ack m') (S n))
end.