Apakah kelas rekursi primitif fungsional setara dengan kelas fungsi yang dibuktikan oleh janin?

Janin, jika Anda belum pernah mendengarnya, dapat dibaca di sini . Ia menggunakan sistem 'matriks panggilan' dan 'grafik panggilan' untuk menemukan semua 'perilaku rekursi' dari panggilan rekursif dalam suatu fungsi. Untuk menunjukkan bahwa suatu fungsi berakhir, itu menunjukkan bahwa semua perilaku rekursi dari panggilan rekursif yang dilakukan pada suatu fungsi mematuhi 'pemesanan leksikografis' tertentu. Pengecek terminasi ini memungkinkan semua fungsi rekursif primitif dan fungsi seperti fungsi Ackermann. Pada dasarnya itu memungkinkan rekursi primitif multi-argumen. Ini pada dasarnya juga merupakan pemeriksa penghentian Agda; Saya percaya bahwa Coq memiliki beberapa fasilitas serupa walaupun mungkin lebih umum.

Dari membaca kertas "Total Functional Programming" oleh DA Turner . Dia menjelaskan bahwa bahasa yang diusulkannya akan mampu mengekspresikan semua "fungsi rekursif primitif" seperti yang terlihat dalam Sistem T yang dipelajari oleh Godel. Dia melanjutkan dengan mengatakan bahwa sistem ini "diketahui mencakup setiap fungsi rekursif yang totalitasnya dapat dibuktikan dalam logika urutan pertama".

Dosis Janin memungkinkan semua fungsi rekursif primitif? Jika demikian, apakah itu memungkinkan fungsi yang bukan fungsional rekursif primitif? Bisakah kutipan diberikan untuk jawaban ini? (Ini sebenarnya tidak perlu karena saya hanya tertarik; Hanya saja beberapa membaca perkawinan tentang masalah ini akan menyenangkan)

Pertanyaan bonus: Fungsional rekursif primitif memiliki definisi yang sangat ringkas dalam hal combinator: diketik S dan K (yang tidak dapat mengekspresikan combinator titik tetap), nol, fungsi penerus, dan fungsi iterasi; itu dia. Apakah ada bahasa lain yang lebih umum yang memiliki definisi ringkas dan di mana semua ekspresi berakhir?

lo.logic computability functional-programming Jake
sumber

Pada Agda vs Coq: Saya selalu membaca pemeriksa penghentian Agda menjadi lebih maju dan menerima lebih banyak fungsi, milik Anda adalah klaim pertama yang bertentangan (ini adalah aturan praktis yang baik ketika membandingkan Agda dengan Coq, kecuali untuk kurangnya taktik Agda: Agda lebih penelitian dan terbuka untuk ekstensi yang stabilitasnya kurang mapan). Andreas Abel telah bekerja pada checker terminasi bahkan lebih maju berdasarkan jenis ukuran, lihat karyanya di MiniAgda dan juga tulisan ini .

Blaisorblade

Ada "menerima lebih banyak definisi fungsi" dan "memiliki kelas fungsi komputasi yang lebih besar". Keduanya tak tertandingi. Agda menang pada hitungan pertama, tetapi Coq jelas menang pada yang kedua.

cody

Saya harus mengklarifikasi bahwa saya belum pernah menggunakan Coq sama sekali dan Agda hanya sedikit. Tampaknya dari apa yang saya baca sedikit Coq mampu mendefinisikan kelas yang lebih luas dari fungsi yang dapat dihitung tetapi saya tidak tahu jadi saya berkata, "Saya percaya bahwa Coq memiliki beberapa fasilitas serupa juga meskipun mungkin lebih umum"; "Belive" dan "mungkin" digunakan untuk menyampaikan bahwa saya tidak tahu.

Jake

Jawaban:

Ya, pemeriksa janin dapat memeriksa semua yang ada di Goedel's T. Anda dapat menunjukkan ini dengan menggunakan pemeriksa untuk menunjukkan bahwa operator iterasi di T sedang mengakhiri. Misalnya, definisi berikut akan berfungsi:

\begin{array}{lcl} i t e r & : & A \to (A \to A) \to N \to A \\ i t e r i f 0 & = & i \\ i t e r i f (n + 1) & = & f (i t e r i f n) \end{array}

$\begin{array}{lcl} \mathit{iter} & : & A \to (A \to A) \to \mathbb{N} \to A \\ \mathit{iter} \;i \;f \;0 & = & i \\ \mathit{iter} \;i \;f \;(n+1) & = & f\;(\mathit{iter} \;i \;f \;n) \end{array}$

Ini sangat mudah bagi pemeriksa janin (atau sebagian besar pemeriksa penghentian lainnya) untuk memeriksanya, karena ini merupakan definisi rekursif struktural yang jelas.

Agda dan Coq keduanya membuktikan pembatalan fungsi yang jauh melebihi apa yang terbukti total dalam aritmatika orde pertama. Fitur yang memungkinkan ini adalah bahwa mereka mengizinkan mendefinisikan jenis dengan rekursi pada data, yang disebut "eliminasi besar". (Dalam teori himpunan ZF, skema aksioma penggantian kira-kira memiliki tujuan yang sama.)

Contoh mudah dari sesuatu yang melampaui T adalah konsistensi dari Goedel's T itu sendiri! Kami dapat memberikan sintaks sebagai tipe data:

data T : Set where 
   N : T 
   _⇒_ : T → T → T

data Term : T → Set where 
   zero : Term N
   succ : Term (N ⇒ N)
   k    : {A B : T} → Term (A ⇒ B ⇒ A)
   s    : {A B C : T} → Term ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)
   r    : {A : T} → Term (A ⇒ (A ⇒ A) ⇒ N ⇒ A)
   _·_  : {A B : T} → Term (A ⇒ B) → Term A → Term B

Perhatikan bahwa dependensi jenis memungkinkan kita untuk menentukan tipe data dari istilah yang hanya mengandung istilah T. yang diketik dengan baik. Kemudian kita dapat memberikan fungsi interpretasi untuk jenis-jenis:

interp-T : T → Set 
interp-T N       = Nat 
interp-T (A ⇒ B) = (interp-T A) → (interp-T B)

Ini mengatakan bahwa itu Nharus bilangan asli Agda, dan panah T harus ditafsirkan sebagai ruang fungsi Agda. Ini adalah eliminasi "besar", karena kita mendefinisikan satu set oleh rekursi pada struktur tipe data T.

Kami kemudian dapat mendefinisikan fungsi interpretasi, menunjukkan bahwa setiap istilah Goedel's T dapat ditafsirkan oleh istilah Agda:

interp-term : {A : T} → Term A → interp-T A
interp-term zero    = 0 
interp-term succ    = \n → n + 1
interp-term k       = \x y → x
interp-term s       = \x y z → x z (y z)
interp-term r       = Data.Nat.fold 
interp-term (f · t) = (interp-term f) (interp-term t)

(Saya tidak memiliki Agda di mesin ini, jadi pasti ada beberapa impor yang hilang, deklarasi fixity, dan kesalahan ketik. Memperbaiki itu adalah latihan untuk pembaca, yang juga bisa menjadi editor, jika mereka mau.)

Saya tidak tahu apa kekuatan konsistensi Agda, tetapi Benjamin Werner telah menunjukkan bahwa Kalkulus Konstruksi Induktif (kalkulus kernel Coq) sama dengan ZFC plus banyak kardinal yang tidak dapat diakses.

Neel Krishnaswami
sumber

Perhatikan bahwa Anda belum menggunakan eliminasi besar dalam contoh Anda. Penghapusan besar sebenarnya tidak menambah daya komputasi. Impredikatifitas memang: sistem F tidak memiliki yang pertama, tetapi dapat mengekspresikan fungsi yang tidak dapat diungkapkan dalam sistem T.

cody

@cody: Fungsi interp-T menghitung set dari suatu term, yang tampak seperti eliminasi besar bagi saya! Jelaslah bahwa eliminasi besar menambah kekuatan: teori tipe Martin-Loef bahkan tidak bisa mendapatkan inkonsistensi dari 0 = 1 tanpa eliminasi besar. (Untuk melihat ini, perhatikan bahwa tanpa alam semesta / eliminasi besar Anda dapat menghapus semua dependensi dan mendapatkan istilah yang diketik sederhana: inilah yang Harper dan Pfenning lakukan dalam bukti kecukupan mereka untuk LF.)

Neel Krishnaswami

Maaf: ya fungsi interp-T memang menggunakan eliminasi besar. Saya juga setuju bahwa membuktikan 0! = 1 memang membutuhkannya. Namun, mendefinisikan fungsi yang dapat dihitung tidak sama dengan membuktikan pernyataan matematika . Jawaban saya mengklarifikasi ini sedikit. Kalkulus Konstruksi murni, misalnya, tidak dapat membuktikan 0! = 1. Namun, ia dapat mendefinisikan fungsi Ackermann dengan relatif mudah.

cody

Ini menunjukkan bahwa Agda adalah pengertian yang lebih umum ia dapat menulis juru bahasa untuk sistem T tetapi apakah ia tidak menunjukkan cuaca atau tidak, Janin, bahasa yang tidak diketik secara tergantung, lebih umum. Bisakah Janin melakukan ini? Apakah Agda masih bisa melakukan ini jika bukan karena "eliminasi besar"?

Jake

Dokumentasi Agda mengatakan bahwa termination checker-nya menggunakan algoritma Fetus. Jika Anda mengambil T, dan memperpanjangnya dengan pencocokan pola dan definisi rekursif diperiksa oleh Fetus, Anda tidak akan dapat menulis penerjemah untuk T di dalamnya. Faktanya, Anda tidak akan mengubah fungsi yang dapat dihitung oleh T sama sekali - semua perintah penghentian yang dihitung Fetus terbukti sangat beralasan dalam aritmetika Peano. (Lihat jawaban cody.) Algoritma Fetus memungkinkan Anda menulis lebih banyak definisi , tanpa mengubah serangkaian fungsi yang dapat Anda hitung. Eliminasi besar Agda sebenarnya meningkatkan set fungsi.

Neel Krishnaswami

Sebagai sarana klarifikasi, saya harus mencatat bahwa Fetus dikembangkan oleh Andreas Abel , yang juga mengembangkan pemeriksa terminasi asli untuk Agda , dan bekerja pada teknik terminasi yang lebih maju sejak itu.

$\mathbb{N}$ $\mathbb{N}$ $\mathrm{F}$ $\mathrm{PA}^2$ $\mathrm F$ $\mathrm{PA}$ $\mathrm{T}$

$\mathrm{PA}$

$\mathrm{T}$

cody
sumber

bagaimana kelas fungsi yang terbukti mengakhiri (PA ^ 2) dapat setara dengan kelas fungsi dalam sistem F yang tidak dapat dibuktikan untuk berakhir sejauh yang saya tahu? Saya juga tidak mengerti bagaimana Anda menjawab pertanyaan saya. Apakah Anda mengatakan sistem T memiliki kelas fungsi komputasi yang lebih besar atau apakah Anda mengatakan bahwa janin itu? Saya pikir ada lompatan dalam logika Anda yang diharapkan saya memiliki lebih banyak latar belakang daripada yang sebenarnya saya lakukan. Juga tautan yang Anda berikan tampaknya mengarah ke halaman yang buruk yang tidak dirender dengan benar.

Jake

Fungsi dalam sistem F semuanya berakhir. Fetus menangkap kelas fungsi komputasi yang lebih besar daripada sistem T, tetapi "secara tidak sengaja", jika Anda menghapus polimorfisme, maka Fetus hanya menangkap persis sistem T. Bisakah Anda memberi tahu saya tautan mana yang tidak berfungsi untuk Anda? (dan browser mana yang Anda gunakan :)

cody

Jika dengan fungsi rekursif primitif yang Anda maksud adalah fungsi rekursif primitif dan Anda tahu bahwa Janin mengandung fungsi Ackermann maka Fetus tidak bertepatan dengan kelas fungsi pr karena fungsi Ackermann bukan rekursif primitif. Ini ditunjukkan oleh Ackermann dan kemudian sebuah bukti yang disederhanakan diberikan oleh Rosza Peter dalam " Konstruktion nichtrekursiver Funktionen " 1935 (sayangnya hanya di Jerman sejauh yang saya tahu).

Jika Anda mencari kelas yang lebih besar dari fungsi rekursif yang dijamin akan berakhir yang mungkin bertepatan dengan kelas fungsi yang ditangkap oleh Fetus maka beberapa karya lain dari Rosza Peter mungkin menarik bagi Anda.

$f(a,b)$ $f(a,b-1)$ $f(a-1,b)$

$<$

(a, b) < (c, d) ⟺ (a < c \land b \leq d) \lor (a \leq c \land b < d)

$(a,b) < (c,d) \iff ( a < c \wedge b \leq d ) \vee ( a \leq c \wedge b < d )$

ω^{2}, ω^{3}

$\omega^2, \omega^3$

p_{i}

$p_i$

i

$i$

z = p_{1}^{n} \cdot p_{2}^{x_{1}} \cdot p_{3}^{x_{2}} \cdot \dots

$z = p_1^{n} \cdot p_2^{x_1} \cdot p_3^{x_2} \cdot \dots$

n

$n$

z

$z$

x_{i}

$x_i$

ω^{ω}

$\omega^\omega$

[sunting] Fungsi rekursif primitif tidak sama dengan fungsi rekursif primitif seperti yang disebutkan dalam komentar di bawah ini. Namun saya pikir seseorang dapat mentransfer konsep rekursi transfinite ke fungsional. Namun, tidak jelas apakah itu masih lebih kuat dan pengaturan fungsional.

John D.
sumber

kelas fungsional rekursif primitif tipe terbatas lebih umum daripada kelas fungsi rekursif primitif. Ini dapat mengekspresikan fungsi Ackermann misalnya dan dapat dilihat di sistem Godel T.

Jake