<p>I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding:</p>

<pre><code>{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ImpredicativeTypes #-}

type Nat = forall a . (a -&gt; a) -&gt; (a -&gt; a)

succ :: Nat -&gt; Nat
succ n = \s z -&gt; n s (s z)

c0 :: Nat
c1 :: Nat

c0 = \_s z -&gt; z
c1 = succ c0


exp :: Nat -&gt; Nat -&gt; Nat
exp = \n m -&gt; n m

tetr :: Nat -&gt; Nat -&gt; Nat
tetr k n = n @Nat (\x -&gt; x k) c1

iter :: (Nat -&gt; Nat) -&gt; (Nat -&gt; Nat)
iter f n = (n @Nat) f c1

ack :: Nat -&gt; Nat -&gt; Nat
ack = \m -&gt; (m @(Nat -&gt; Nat)) iter succ
</code></pre>

<p>You can notice a variant of <a href="https://en.wikipedia.org/wiki/Tetration" rel="nofollow noreferrer">tetration</a> on the way.</p>

<p>Can Ackermann function (and tetration) be defined as a pure lambda term without inductive types in a predicative system?</p>

<p>For instance in Agda with level polymorphism?</p>

<p>If not, what other type-theory tools apart from inductive types, can help us define non-primitive-recursive functions?</p>

CC BY-SA 4.0
2018-06-10T15:19:15.343Z
For a part of the latter question it seems to me that type level (smallest) fixed point would allow to encode Scott numerals and with that encode easily Ackermann function and more. Fixed point feels very powerful.
Łukasz Lew
CC BY-SA 4.0
2018-06-12T14:32:57.057Z
As a first step, I would recommend trying to transcribe your implementation in Agda itself! You might have to define several versions of `Nat`, say `Nat₁`, `Nat₂`, etc. Long story short, I *think* you can define the Ackermann function with just 3 "stacks" of universes, but haven't tried myself.
cody
CC BY-SA 4.0
2018-06-13T15:03:27.320Z
I learned Agda to try it :). I got exponentiation to work, even tetration, but pentation seems impossible, not even getting close to Ackermann's function.
I'll post a separate question.
Łukasz Lew
CC BY-SA 4.0
2018-06-13T15:15:58.657Z
[Follow-up question](https://cstheory.stackexchange.com/questions/40987/is-church-pentation-implementable-in-agda).
Łukasz Lew
<lo.logic><type-theory><coq><hierarchy-theorems><agda>
Is it possible to type Ackermann function with (stratified variant of) System F?
Łukasz Lew
# Is it possible to type Ackermann function with (stratified variant of) System F?

(Asked by: username_0 on 2018-06-10)

I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ImpredicativeTypes #-}

type Nat = forall a . (a -> a) -> (a -> a)

succ :: Nat -> Nat
succ n = \s z -> n s (s z)

c0 :: Nat
c1 :: Nat

c0 = \_s z -> z
c1 = succ c0


exp :: Nat -> Nat -> Nat
exp = \n m -> n m

tetr :: Nat -> Nat -> Nat
tetr k n = n @Nat (\x -> x k) c1

iter :: (Nat -> Nat) -> (Nat -> Nat)
iter f n = (n @Nat) f c1

ack :: Nat -> Nat -> Nat
ack = \m -> (m @(Nat -> Nat)) iter succ

You can notice a variant of tetration on the way.
Can Ackermann function (and tetration) be defined as a pure lambda term without inductive types in a predicative system?
For instance in Agda with level polymorphism?
If not, what other type-theory tools apart from inductive types, can help us define non-primitive-recursive functions?

**Tags:** lo.logic, type-theory, coq, hierarchy-theorems, agda

> **Comments:**
> **username_0**: For a part of the latter question it seems to me that type level (smallest) fixed point would allow to encode Scott numerals and with that encode easily Ackermann function and more. Fixed point feels very powerful.  
> **username_1**: As a first step, I would recommend trying to transcribe your implementation in Agda itself! You might have to define several versions of `Nat`, say `Nat₁`, `Nat₂`, etc. Long story short, I *think* you can define the Ackermann function with just 3 "stacks" of universes, but haven't tried myself.  
> **username_0**: I learned Agda to try it :). I got exponentiation to work, even tetration, but pentation seems impossible, not even getting close to Ackermann's function. I'll post a separate question.  
> **username_0**: [Follow-up question](https://cstheory.stackexchange.com/questions/40987/is-church-pentation-implementable-in-agda).  

---

## 0 answers

