Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: Andy.Gordon@uk.ac.cam.cl
Message-Id: <9205141012.AA25702@oxley>
Date: 14 May 1992 1110-WET (Thursday)
To: toal@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: Ackermann's function
In-Reply-To: Message of Wed, 13 May 92 17:08:42 PDT from toal@edu.ucla.cs <9205140008.AA15050@ewa.cs.ucla.edu>

Ackermann's function is a curried function A:num->num->num that satisfies the 
predicate:

    "!m n.
        (A 0 n = SUC n) /\
        (A (SUC m) 0 = A m 1) /\
        (A (SUC m) (SUC n) = A m (A (SUC m) n))"

We can define such an A using primitive recursion in HOL as follows:

    new_theory `ackermann`;;

    let G =
        new_prim_rec_definition
        (`G`,
         "(G Am 0 = Am 1) /\
          (G Am (SUC n) = Am (G Am n))");;

    let A =
        new_prim_rec_definition
        (`A`,
         "(A 0 n = SUC n) /\
          (A (SUC m) n = G (A m) n)");;

    let Intuition =
        prove(
        "!m. G (A m) = A (SUC m)",
        GEN_TAC THEN
        CONV_TAC FUN_EQ_CONV THEN
        REWRITE_TAC [A]);;
    
    let Ackermann =
        prove(
        "!m n.
            (A 0 n = SUC n) /\
            (A (SUC m) 0 = A m 1) /\
            (A (SUC m) (SUC n) = A m (A (SUC m) n))",
        INDUCT_TAC THEN
        REWRITE_TAC [G;A]);;

    close_theory();;

The trick here is the higher-order function G: (num->num)->num->num,
with the property (that I've proved as Intuition above):

    G (A m) = A (SUC m)

This way of defining Ackermann's function depends on your logic being able 
to define the higher-order function G by primitive recursion; typically 
a first-order logic wouldn't let you do this.

Andy.