Hubungan antara Mesin Turing dan kalkulus Lambda?

49

Apakah ada hubungan antara Mesin Turing dan kalkulus Lambda - atau apakah mereka muncul secara bersamaan?

computability lambda-calculus turing-machines Hawkeye
sumber

7

Bisakah Anda menguraikan pertanyaan Anda? Kedua model memiliki kekuatan komputasi yang sama (keduanya mampu mengekspresikan keluarga fungsi rekursif), yaitu, mereka Turing lengkap. Lihat: en.wikipedia.org/wiki/Turing_completeness

Joel Rybicki

terkait: Teori realisasi: perbedaan kekuatan antara kalkulus Lambda dan Mesin Turing

Kaveh

Ini pertanyaan yang bagus!

Tayfun Bayar

31

Kalkulus lambda lebih tua dari model mesin Turing, yang tampaknya berasal dari periode 1928-1929 (Seldin 2006), dan diciptakan untuk merangkum gagasan tentang fungsi skematis yang diperlukan Gereja untuk logika dasar yang ia buat. Itu tidak diciptakan untuk menangkap gagasan umum tentang fungsi yang dapat dihitung, dan memang versi yang diketik lebih lemah akan melayani tujuannya dengan lebih baik.

Tampaknya kebetulan untuk tujuan bahwa Gereja kalkulus diciptakan ternyata Turing lengkap, meskipun kemudian Gereja menggunakan kalkulus lambda sebagai fondasinya untuk apa yang ia sebut fungsi efektif dihitung (1936), yang menarik Turing dalam makalahnya .

Teori tipe sederhana Gereja (1940) memberikan teori fungsi yang lebih moderat dan diketik yang cukup untuk mengekspresikan sintaksis logika tingkat tinggi tetapi tidak mengekspresikan semua fungsi rekursif. Teori ini dapat dilihat sebagai lebih selaras dengan motivasi asli Gereja.

Referensi

Gereja (1936). Masalah yang tidak terpecahkan dalam teori bilangan dasar. American Journal of Mathematics 58: 345-363.
Gereja (1940). Rumusan teori tipe sederhana . Jurnal Logika Simbolik 5 (2): 56-68.
Seldin (2006). Logika Curry and Church . Dalam Buku Pegangan Sejarah Logika, vol.5: Logika dari Russell ke Gereja , hal. 819—874. Belanda Utara: Amsterdam.

Catatan Jawaban ini secara substansial direvisi karena keberatan oleh Kaveh dan Sasho. Saya merekomendasikan timeline Wikipedia yang disarankan Kaveh, tesis History of the Church-Turing , yang memiliki beberapa kutipan pilihan dari artikel mani.

Charles Stewart
sumber

2

Gereja membuat klaim bahwa kalkulus lambda menangkap notasi intuitif dari fungsi yang dapat dihitung sebelum makalah Turing, itulah sebabnya itu disebut Tesis Gereja. Gagasan untuk menangkap gagasan umum tentang fungsi-fungsi yang dapat dihitung berjalan lebih jauh ke belakang (misalnya fungsi rekursif umum Godel), dan Gereja berusaha menangkapnya.

Kaveh

5

Saya pikir itu menyesatkan untuk mengatakan bahwa kesetaraan model adalah kecelakaan total. Tampaknya bagi saya bahwa Gereja dan Turing berangkat untuk menangkap gagasan terkait, bahkan jika tidak segera jelas bahwa gagasan itu sebenarnya terkait. Apakah Anda akan mengatakan bahwa itu "kecelakaan total" bahwa integrasi Riemann dan anti-diferensiasi sangat terkait?

Sasho Nikolov

@ Kaveh: Menurut Seldin (2006) Logika Gereja dan Kari , tujuan dan sintaksis kalkulus lambda dikembangkan pada periode 1928 hingga 1929, jauh sebelum Gereja menyadari gagasan umum fungsi rekursif. Jawaban saya akan mendapat manfaat dari garis waktu, tetapi saya tidak punya waktu untuk menyusunnya sekarang.

Charles Stewart

1

@ Charles: Gereja ada di Göttingen 1927-1928. Dia pasti menyadari apa yang sedang terjadi tentang teori fungsi rekursif dan program Hilbert. Hasil Ackermann tentang fungsi rekursif non-primitif berasal dari tahun yang sama. Gereja sedang berusaha membangun fondasi untuk matematika. Semua ini terjadi sebelum makalah Turing. Lihat ini . Kleene membuktikan kesetaraan fungsi rekursif umum dan fungsi -definable sebelum karya Turing. Paragraf terakhir Anda menyesatkan karena memberi kesan bahwa mereka

λ

$\lambda$

Kaveh

1

@ Charles, ketika saya menulis, saya setuju bahwa motivasi asli Gereja adalah membangun fondasi (seperti sistem Frege) (AFAIK), tetapi dia juga menganggapnya sebagai model perhitungan sebelum karya Turing. Saya tidak berpikir jawabannya perlu dihapus, merevisi paragraf kedua harus baik-baik saja. (Alasan saya berkomentar adalah bahwa saya merasa bahwa belakangan ini orang-orang meremehkan kemampuan kerja Gereja.)

Kaveh

26

Saya hanya ingin menunjukkan bahwa sementara kalkulus lambda dan mesin Turing keduanya menghitung kelas yang sama fungsi bilangan-teoretik, mereka tidak persis sama dalam segala hal yang dapat dibayangkan. Sebagai contoh, dalam teori realisasi ada pernyataan yang dapat direalisasikan oleh mesin Turing tetapi tidak oleh kalkulus lambda. Salah satu pernyataan tersebut adalah tesis resmi Gereja, yang menyatakan:

\forall f : n a t \to n a t \exists e \forall n \exists k (T (e, n, k) \land U (k, f (n)))

$\forall f : \mathbf{nat} \to \mathbf{nat} \ \exists e \ \forall n \ \exists k \ \big( \mathbf{T}(e, n, k) \land \mathbf{U}(k,f(n)) \big)$

Di sini adalah predikat T Kleene . Realizer untuk pernyataan ini adalah program yang menerima (representasi) peta dan output (representasi) dengan properti yang diinginkan. Dalam model mesin Turing, peta diwakili oleh kode mesin Turing yang menghitung , sehingga program hanya (kode komputasi mesin Turing) fungsi identitas. Namun, jika kita menggunakan kalkulus lambda, maka seharusnya menghitung angka yang mewakili mesin Turing dari istilah lambda mewakili fungsi $\mathbf{T}$ $c$ $f$ $e$ $f$ $f$ $c$ $c$ $f$ . Ini tidak dapat dilakukan (saya dapat menjelaskan mengapa, jika Anda mengajukannya sebagai pertanyaan terpisah).

Andrej Bauer
sumber

4

Kami memiliki markup sekarang.

T_{E} X

$T_EX$

András Salamon

Andrej, artikel Wikipedia menggunakan urutan parameter yang Anda gunakan berbeda, argumen kedua adalah input dan yang ketiga adalah kode penghentian perhitungan, argumen pertama adalah kode mesin. Saya kira Anda menyatakan CT, saya mengeditnya berdasarkan vDT88.

Kaveh

Satu hal lagi, tampaknya untuk realisasi Anda memberikan sebagai kode TM dan mengharapkan -term, tetapi bukankah lebih alami untuk memberikan juga sebagai -term dan kemudian fungsi identitas akan berfungsi ? (Saya dapat mengajukannya sebagai pertanyaan terpisah jika Anda mau.)

f

$f$

λ

$\lambda$

f

$f$

λ

$\lambda$

Kaveh

@ Kaveh: Saya pikir itu sebaliknya, tapi saya juga bertanya-tanya mengapa tidak alami juga memiliki output dari jenis yang sama dengan input dalam kasus kalkulus lambda.

Abel Molina

1

Apakah sesuatu seperti realizer untuk pernyataan "setiap kontinu" lakukan? Atau bagaimana dengan realizer untuk "ruang Penyedia dan ruang Baire bersifat homeomorfik"?

f : R \to R

$f : \mathbb{R} \to \mathbb{R}$

2^{N}

$2^\mathbb{N}$

N^{N}

$\mathbb{N}^\mathbb{N}$

Andrej Bauer

11

Mereka terkait baik secara matematis dan historis.

Kalkulus lambda dikembangkan pada tahun 1928 - 1929 oleh Gereja Alonzo (diterbitkan pada tahun 1932).

Mesin Turing dikembangkan pada tahun 1935 - 1937 oleh Alan Turing (diterbitkan pada tahun 1937).

Alan Turing adalah Ph.D. Gereja Alonzo pelajar di Princeton dari tahun 1936 - 1938.

Mesin Turing dan kalkulus lambda setara dalam kekuatan komputasi: masing-masing dapat secara efisien mensimulasikan yang lain.

Matt Might
sumber

6

Entscheidungsproblem adalah salah satu dari 23 masalah terkenal yang dikemukakan oleh ahli matematika David Hilbert.

Pada tahun 1936 dan 1937, Gereja Alonzo dan Alan Turing, menerbitkan makalah independen yang menunjukkan bahwa mustahil untuk memutuskan secara algoritmik apakah pernyataan dalam aritmatika itu benar atau salah, dan dengan demikian solusi umum untuk Entscheidungsproblem tidak mungkin.

Ini dilakukan oleh Gereja Alonzo pada tahun 1936 dengan konsep "kalkulasi efektif" berdasarkan kalkulus λ dan oleh Alan Turing pada tahun yang sama dengan konsep mesin Turing. Kemudian diakui bahwa ini adalah model komputasi yang setara. - Wikipedia

Jadi kalkulus lambda dan mesin Turing tidak hanya terkait erat tetapi mereka adalah model komputasi yang setara .

Anda juga mungkin suka membaca The Annotated Turing: Tur Dipandu Melalui Kertas Bersejarah Alan Turing tentang Kompabilitas dan Mesin Turing oleh Charles Petzold . Buku ini menangkap beberapa informasi menarik tentang topik tersebut.

Pratik Deoghare
sumber

4

Mesin Turing dan Lambda Calculus adalah dua model yang menangkap gagasan algoritma (perhitungan mekanis). Kalkulus Lambda ditemukan oleh Gereja untuk melakukan perhitungan dengan fungsi. Ini adalah dasar dari bahasa pemrograman fungsional. Pada dasarnya, setiap masalah yang dapat dihitung (decidable) oleh mesin Turing juga dapat dihitung menggunakan Lambda calculus. Jadi, mereka adalah dua model komputasi yang setara (hingga faktor polinomial) dan keduanya mencoba menangkap kekuatan komputasi mekanis apa pun.

Mohammad Al-Turkistany
sumber

Hubungan antara Mesin Turing dan kalkulus Lambda?

Jawaban:

Referensi