Church-pentationはAgdaで実装可能ですか?


で示唆されたこの質問
は、私はピアノ算術の叙述教会符号化を実装しました。指数関数はうまくいきますが、残念なことにtetrationは引数のレベルを高くする必要があり、ペンテレーションの型を不明瞭にします。

これはコードです:

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 

Church-pentationはAgdaで実装可能ですか?

This paper: Finitely stratified polymorphism
might be relevant.

私はこの仕事のためにAgdaを学んだので、おそらく私はその力をいかに活用するか分かりません。

ベストアンサー
申し訳ありませんが、適切な答えはありません

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です