## 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 Ack2.
(*
ack2 :: Nat -> Nat -> Nat
ack2 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.