Ackermann関数は二変数の関数\(\mathord {\textnormal {\textsf {ack}}}:\mathbb {N}\to \mathbb {N}\to \mathbb {N}\)で、次のように定義される。

• -\(\mathord {\textnormal {\textsf {ack}}}(0,n)\equiv \mathord {\textnormal {\textsf {succ}}}(n)\)
• -\(\mathord {\textnormal {\textsf {ack}}}(\mathord {\textnormal {\textsf {succ}}}(m),0)\equiv \mathord {\textnormal {\textsf {ack}}}(m,\mathord {\textnormal {\textsf {succ}}}(0))\)
• -\(\mathord {\textnormal {\textsf {ack}}}(\mathord {\textnormal {\textsf {succ}}}(m),\mathord {\textnormal {\textsf {succ}}}(n))\equiv \mathord {\textnormal {\textsf {ack}}}(m,\mathord {\textnormal {\textsf {ack}}}(\mathord {\textnormal {\textsf {succ}}}(m),n))\)

Ackermann関数の構成を[002V]に基づいて正当化せよ。ちなみに、Ackermann関数は原始再帰的でないことが知られているので、[002X]の特別な場合としては定義できない。関数型を使えることに注意するとよい。