ackermann関数は高階原始帰納的関数なので関数空間を使えば書ける12、というのを幾つか見たので気になって書いた。特に高度なことではなかった。

高階関数を許す原始帰納法で定義される関数を高階原始帰納的関数と呼ぶ3ようです。

right object 1 with ! is
end object;

right object prod(A,B) with pair is
    pi1: prod -> A
    pi2: prod -> B
end object;

right object exp(A,B) with cur is
    ev: prod(exp, A) -> B
end object;

left object nat with pr is
    o: 1 -> nat
    s: nat -> nat
end object;

let swap = pair(pi2,pi1);
let first(f) = prod(f,I);
let second(f) = prod(I,f);
let comp = cur(ev.pair(pi1.pi1,ev.pair(pi2.pi1,pi2)));
let fpow = ev.first(pr(cur(cur(pi2)),cur(comp.pair(ev,pi2)))).swap;
let ack = ev.first(pr(cur(s.pi2),cur(ev.pair(I,s.o.!).fpow.second(s))));