Inspired by suggestion in this question, I've implemented predicative Church encoding of Peano arithmetic. Exponentiation works fine, unfortunately tetration requires the level of one of the arguments to he higher, rendering pentation's type unclear.

This is the code:

module Church where
open import Agda.Primitive

Church : {l : Level} -> Set l -> Set l 
Church A = (A -> A) -> (A -> A)

Nat = {A : Set} -> Church A  
Nat₁ = {A : Set₁} -> Church A
Nat₂ = {A : Set₂} -> Church A

c0 : Nat
c0 = \s z -> z

c1 : Nat
c1 = \s z -> s z

c2 : Nat
c2 = \s z -> s (s z)

add : Nat -> Nat -> Nat
add a b s z = b s (a s z)

mul : Nat -> Nat -> Nat
mul a b s z = b (a s) z

-- First signs of the type growing:
-- exp : {A : Set} -> Church A -> Church (A -> A) -> Church A
exp : Nat -> Nat -> Nat
exp a b = b a 

tetr : Nat -> Nat₁ -> Nat
tetr k n = n (exp k) c1

-- does not type-check
-- pent : Nat -> Nat₁ -> Nat
-- pent k n = n (tetr k) c1 

Is Church-pentation implementable in Agda?

This paper: Finitely stratified polymorphism might be relevant.

I learned Agda for this task, so perhaps I don't know how to exploit its power.


According to the paper you linked, I think the answer to the question you want to ask is, "no." Pentation is not definable in a stratified version of system F.

The paper says that their system can define every super-elementary function, and all definable functions are super-elementary. The super-elementary functions are level $\mathcal{E}^4$ in the Grzegorczyk hierarchy, and according to wikipedia, moving to the next hyper-operation requires one additional step in that hierarchy. So, $\mathcal{E}^4$ contains tetration, products and sums of tetration, and finite compositions of tetration, but pentation isn't included until $\mathcal{E}^5$. So it is beyond the capabilities of the stratified system F.

This also answers your other question (of course), because the union of all levels in the Grzegorczyk hierarchy is exactly the primitive recursive functions, and the Ackermann function is not primitive recursive. So it cannot be defined.

Now, Agda of course is capable of defining pentation (and the Ackermann function), because any Church numeral can be used to get an equivalent value of the inductively defined natural numbers, and then those can be used to compute the function and converted back to a Church numeral. But presumably that's not what you're interested in.

However, there is also another possibility. Agda's predefined universes are closed under induction-recursion. This means that (in a way) they contain universes of their own, and far, far more universes than exist in the predicative system presented in the paper (which only has $\omega$ many universes, I believe). You can of course define Church numerals for each of these universes. But, I do not know what effect adding quantity of universes (and ignoring structure besides Pi types) has on the ability to define functions on the Church numerals.


I did some additional investigation to expand on my last idea, and was able to define pentation of Church numerals. Here is some code, with explanations.

module Pent where

open import Function
open import Level hiding (suc)
open import Data.Unit

import Data.Product
import Data.Nat as N
open N using (ℕ)

Most of this is just for convenience. I won't be cheating with the natural numbers, but they're easier to visualize at the end.

The following exhibits Set as a Mahlo universe. This means that for any A : Set and B : A → Set, there is a universe U : Set that is itself closed under A and B

module Mahlo (A : Set) (B : A → Set) where
  data U : Set
  T : U → Set

  data U where
    A' : U
    B' : A → U
    Π : (s : U) (f : T s → U) → U

  syntax Π s (λ x → t) = Π[ x ∈ s ] t

  T A' = A
  T (B' a) = B a
  T (Π s f) = (x : T s) → T (f x)

  infixr 4 _⇒_
  _⇒_ : U → U → U
  a ⇒ b = Π[ _ ∈ a ] b

I haven't included any universe structure in U besides Pi types. But this means that we can define the type of Church numerals over U, and easily build up to exponentiation of such numerals:

  CH : Set
  CH = (r : U) → (T r → T r) → T r → T r

  zro : CH
  zro r s z = z

  suc : CH → CH
  suc m r s = s ∘ m r s

  one : CH
  one = suc zro

  infixl 10 _+_
  _+_ : CH → CH → CH
  (m + n) r s = m r s ∘ n r s

  infixl 20 _×_
  _×_ : CH → CH → CH
  (m × n) r = m r ∘ n r

  infixr 30 _^_
  _^_ : CH → CH → CH
  (m ^ n) r = n (r ⇒ r) (m r)

However, that is where we get stuck for 'generic' universes about which we know nothing but that they have Pi types (i.e. we don't really know anything about A and B).

Next we define Church numerals valued in arbitrary Set levels:

CHURCH : (α : Level) → Set (Level.suc α)
CHURCH α = ∀(R : Set α) → (R → R) → (R → R)

It is possible to define tetration of CHURCH zero as follows:

_↑_ : CHURCH zero → CHURCH zero → CHURCH zero
(m ↑ n) R s z = n CH (_^_ m') one R' s z
  open Mahlo R (const ⊤) renaming (A' to R')

  m' : CH
  m' = m CH suc zro

So, this might not look like anything special is going on, but it's actually a bit crazier than it first appears. We have two Church numerals over Set, and R : Set that is our result type. So, we use the fact that Set is Mahlo to find a universe U inside Set that contains R. This means that Church numerals over U also live inside Set, which means we can 1) lower our big church numeral m into them, and 2) repeatedly exponentiate the lowered numeral by itself n times. And since U contains R, the numeral we construct is able to iterate the R → R function on the R value to give our answer.

Now, since tetration is defined with a uniform type, it's easy to define pentation as you defined tetration:

_⇈_ : CHURCH zero → CHURCH (Level.suc zero) → CHURCH zero
(m ⇈ n) = n (CHURCH zero) (_↑_ m) (λ R s z → s z)

If you want to visualize the results, you can use the following:

module Visualize where
  open Data.Product

  toCH : ∀{α} → ℕ → CHURCH α
  toCH 0 R s z = z
  toCH (N.suc n) R s z = s (toCH n R s z)

  fromCH : ∀{α} → CHURCH α → ℕ
  fromCH m = lower $ m (Lift _ ℕ) (lift ∘ N.suc ∘ lower) (lift N.zero)

  lift₀ : (CHURCH zero → CHURCH zero → CHURCH zero) → ℕ → ℕ → ℕ
  lift₀ op m n = fromCH (op (toCH m) (toCH n))

  lift₁ : (CHURCH zero → CHURCH (Level.suc zero) → CHURCH zero) → ℕ → ℕ → ℕ
  lift₁ op m n = fromCH (op (toCH m) (toCH n))

  2↑2 2↑3 2↑4 3↑2 3↑3 : ℕ
  2↑2 = lift₀ _↑_ 2 2
  2↑3 = lift₀ _↑_ 2 3
  2↑4 = lift₀ _↑_ 2 4
  3↑2 = lift₀ _↑_ 3 2
  3↑3 = lift₀ _↑_ 3 3

  2⇈2 2⇈3 : ℕ
  2⇈2 = lift₁ _⇈_ 2 2
  2⇈3 = lift₁ _⇈_ 2 3

  tetr : ℕ
  tetr = 3↑3

  pent : ℕ
  pent = 2⇈3

Note, I got tired of waiting for 3↑3 to finish.

So, just to go back a bit, the universe creation principle I used was basically: for every set $R$ there exists a universe $U$ with $R \in U$, which is basically the Grothendieck universe axiom, except all of these universes are themselves inside the universe Set (and the universes are much weaker than set theoretic universes). But this is actually just scratching the surface of how powerful Mahlo is, because you'll notice I essentially did nothing with the B family. So I'm confident you can go beyond pentation with this. This is just the easiest one step further.

(To expand slightly on the last paragraph, the axiom "there exists a universe $V$ such that for every set $S \in V$ there exists a universe $U \in V$ such that $S \in U$" means (if I understand correctly) that $V$ is related to a 1-inaccessible cardinal/ordinal. But Mahlo cardinals/ordinals are hyper-hyper-hyper-...-inaccessible, which is well beyond that.)

Edit 2:

Here is a simpler development showing how you can define uniform tetration with $\omega+1$ universe levels. It uses the latest Agda to be able to talk about Setω, but you might be able to do it in older Agda versions if you inline CHURCH.

module PentPoly where

open import Level
open import Function
open import Agda.Primitive

module Gen (α : Level) where
  Church : Set (suc α)
  Church = ∀(R : Set α) → (R → R) → (R → R)

  one : Church
  one R s z = s z

  _+_  : Church → Church → Church
  (m + n) R s = n R s ∘ m R s

  _×_  : Church → Church → Church
  (m × n) R = n R ∘ m R

  _^_ : Church → Church → Church
  (m ^ n) R = n (R → R) (m R)

CHURCH = ∀(α : Level) (R : Set α) → (R → R) → (R → R)

(m ↑ n) α R s z = n (suc α) Church (_^_ m') one R s z
  open Gen α
  m' : Church
  m' = m α

I think the way to think about this is that we're taking advantage of Setω being a limit of the universes below it. So any iteration we are asked to do occurs at some particular level below it, and we can iterate exponentiation one level above that. I think this means that we can get all hyper-operations with 'only' $\omega \cdot \omega$ universes.

I also realized my Mahlo above is wrong. It says that for every family on Set there is a universe (U,T) that contains that family. But Mahlo is actually the property that for every mapping between families of sets, there is a universe such that the mapping restricts to that universe. This looks like:

module Mahlo
    (f₁ : (X : Set) → (X → Set) → Set)
    (f₂ : (X : Set) → (Y : X → Set) → f₁ X Y → Set)

  data U : Set
  T : U → Set

  data U where
    Π : (x : U) → (y : T x → U) → U
    reflect₁ : (x : U) → (y : T x → U) → U
    reflect₂ : (x : U) → (y : T x → U) → f₁ (T x) (T ∘ y) → U

  T (Π x y) = (v : T x) → T (y v)
  T (reflect₁ x y) = f₁ (T x) (T ∘ y)
  T (reflect₂ x y z) = f₂ (T x) (T ∘ y) z

  res : Σ[ x ∈ U ] (T x → U) → Σ[ x ∈ U ] (T x → U)
  res (x , y) = (reflect₁ x y , reflect₂ x y)

But this is even further unnecessary power from the perspective of the original question.

  • 1
    $\begingroup$ One way of thinking about a Mahlo universe is as a universe which contains so many (names of) universes that they are "plentiful". In set theory "plentiful" is expressed as "the (names of the) universes are stationary". Speaking informally, this means that they are "dense" or "have measure 1". The type-theoretic way of saying the same thing is that the universes cannot be exhausted by any type family, as in your answer. It's an open problem how to go beyond Mahlo in type theory. $\endgroup$ – Andrej Bauer Aug 31 '18 at 6:48
  • $\begingroup$ If you didn't do anything with the type family, could you pull off the same development with a weaker universe axiom? A la Grothendieck? $\endgroup$ – Andrej Bauer Aug 31 '18 at 6:49
  • $\begingroup$ So, yes, it definitely seems like my argument 'merely' requires a universe that itself models (if that's the right word) the Grothendieck universe axiom. Then you can define pentation with another universe above that. It's possible that some other idea could let you define things with even weaker universe axioms. $\endgroup$ – Dan Doel Aug 31 '18 at 12:13
  • $\begingroup$ Oh, also... Anton Setzer has a paper on a type theoretic principle stronger than Mahlo, the Π₃ reflecting universe, which is so named due to related stuff in proof theory. If I understand correctly (which I might not), this is a type/proof theoretic analogue of weakly compact cardinals, where now the Mahlo cardinals are stationary (instead of just the inaccessibles). However, I don't think there's anywhere you can try it out, because it's a more complicated definition principle than Agda's induction-recursion allows (I think). $\endgroup$ – Dan Doel Aug 31 '18 at 12:40
  • $\begingroup$ I messed around a little, and I think the only requirement for defining tetration with a uniform type is that you have unbounded universes below you. So, if you build the latest Agda, you can tetrate Church numerals in Set_omega. I think this means the Grothendieck axiom can go way beyond tetration. Probably the whole hierarchy at least. I also realized my characterization of Mahlo in the code is too weak. I'll amend the post later. $\endgroup$ – Dan Doel Aug 31 '18 at 17:01

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.