(* 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 -> 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))

*)

## Saturday, 20 September 2008

### Accessing Ackermann

Subscribe to:
Post Comments (Atom)

## 1 comment:

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

Post a Comment