Tampaknya saya telah menemukan cara umum untuk mengubah prosedur rekursif apa pun menjadi rekursi ekor: Tentukan sub-prosedur pembantu dengan parameter "hasil" tambahan. Terapkan apa yang akan diterapkan pada nilai pengembalian prosedur ke parameter itu. Hubungi prosedur bantuan ini untuk...
Ekspresi kombinator (misalkan dalam basis SK) dapat dianggap sebagai fungsi yang memetakan ekspresi kalkulus kombinator ke ekspresi kalkulus kombinator. Artinya, seseorang dapat menganggap ekspresi XXX sebagai fungsi , di mana adalah himpunan semua ekspresi kombinator yang valid secara sintaksis...
Saya seorang programmer dengan pegangan pada automata, tetapi tidak pada logika. Saya membaca di surat kabar bahwa keduanya berhubungan sangat erat. Deterministic Finite Automata (DFA), Tree Automata dan Visible Pushdown Automata semuanya terkait dengan Monadic Second Order Logic (MSO). Meskipun,...
Saya sedang memikirkan bukti dan berlari ke pengamatan yang menarik. Jadi bukti setara dengan program melalui Curry-Howard Isomorphism, dan bukti melingkar sesuai dengan rekursi tak terbatas. Tapi kita tahu dari masalah penghentian bahwa dalam pengujian umum apakah program sewenang-wenang berulang...
Dalam Yayasan Praktis untuk Bahasa Pemrograman , kata Robert Harper Jika proposisi itu benar berarti memiliki buktinya, apa artinya proposisi itu salah? Itu berarti bahwa kita memiliki penolakan terhadapnya, menunjukkan bahwa itu tidak dapat dibuktikan. Yaitu, proposisi salah jika kita dapat...
Untuk mengetahui perbedaannya, saya baru saja menemukan pernyataan di bawah tentang logika temporal di Wikipedia : varian lain dari logika modal yang berbagi banyak fitur umum dengan logika dinamis, berbeda dari semua logika yang disebutkan di atas dengan menjadi apa yang telah ditandai oleh...
Saya sedang membaca pertanyaan Konsistensi dan kelengkapan menyiratkan kesehatan? dan pernyataan pertama di dalamnya mengatakan: Saya mengerti bahwa kesehatan menyiratkan konsistensi. Yang saya cukup bingung karena saya pikir kesehatan adalah pernyataan yang lebih lemah daripada konsistensi...
Saat ini saya harus belajar Coq dan tidak tahu bagaimana menghadapi or: Sebagai contoh, sesederhana itu, saya tidak melihat cara membuktikan: Theorem T0: x \/ ~x. Saya akan sangat menghargainya, jika seseorang dapat membantu saya. Untuk referensi saya menggunakan lembar contekan ini . Juga...
Bisakah Anda memberi saya beberapa saran tentang buku pengantar (tapi komprehensif) yang bagus tentang Logika dan Komputasi? Beberapa topik kabur yang ada dalam pikiran saya adalah: Artihm Presburger, PA, ZF, ZFC, HOL Teori set, teori tipe Modeling Computation (Turing Machines) dalam berbagai...
Saat ini saya sedang mempelajari kalkulus lambda dan bertanya-tanya tentang dua jenis penulisan istilah lambda berikut. λ x y. x yλxy.xy\lambda xy.xy λ x . λ y. x yλx.λy.xy\lambda x.\lambda y.xy Apakah ada perbedaan makna atau cara Anda menerapkan pengurangan beta, atau hanya dua cara untuk...
Di tempat kerja saya ditugaskan untuk menyimpulkan beberapa jenis informasi tentang bahasa yang dinamis. Saya menulis ulang urutan pernyataan menjadi letekspresi bersarang , seperti: return x; Z => x var x; Z => let x = undefined in Z x = y; Z => let x = y in Z if x then T else F; Z =>...
Dispenser minuman mengharuskan pengguna untuk memasukkan koin ( ), lalu tekan salah satu dari tiga tombol: meminta secangkir teh , selain kopi , dan meminta pengembalian uang (yaitu mesin mengembalikan koin: ). Dispenser ini dapat dimodelkan dengan proses CCS berikut :ˉ d teheteh ˉ r ˉ bc¯c¯\bar...
Apakah contoh berikut ini benar tentang apakah algoritma inferensi suara dan lengkap ? Misalkan kita memiliki jarum a, b, c di tumpukan jerami, dan juga memiliki algoritma inferensi yang dirancang untuk menemukan jarum. sound - Hanya jarum a, b dan c yang diperoleh. complete - Jarum a, b dan c...
Dalam diskusi seputar pertanyaan ini , Gilles menyebutkan dengan benar bahwa bukti kebenaran suatu algoritma yang menggunakan array harus membuktikan bahwa tidak ada akses array di luar batas; tergantung pada model runtime, ini akan menyebabkan kesalahan runtime atau akses ke elemen...
Dalam Chaitin Meta Math! The Quest For Omega , ia secara singkat berbicara tentang Masalah ke-10 Hilbert. Dia kemudian mengatakan bahwa Persamaan Diophantine dapat diubah menjadi dua polinomial yang sama dengan koefisien bilangan bulat positif: .p = 0p = 0p=0p=0p = 0⟺hal1= p2p=0⟺p1=p2p=0 \iff p_1 =...
Menurut Peter Selinger , The Lambda Calculus adalah Aljabar (PDF). Di awal artikel ini dia berkata: Interpretasi combinatory dari kalkulus lambda diketahui tidak sempurna, karena tidak memenuhi ξξξ -rule: di bawah interpretasi, M=NM=NM = N tidak berarti λx.M=λx.Nλx.M=λx.N\lambda x.M = \lambda...
Sehubungan dengan utas Membuktikan bahwa konversi dari CNF ke DNF adalah NP-Hard (dan utas Matematika terkait ): Bagaimana dengan arah lain, dari DNF ke CNF? Apakah itu mudah atau sulit? Pada halaman 2 makalah ini , mereka tampaknya mengisyaratkan bahwa kedua arah sama-sama sulit ketika mereka...
Dua model komputasi dapat ditunjukkan saling melengkapi jika masing-masing dapat menyandikan simulator universal untuk yang lain. Dua logika dapat ditunjukkan untuk melengkapi jika suatu pengkodean aturan inferensi (dan mungkin aksioma jika ada) dari masing-masing ditunjukkan sebagai teorema dari...
Saya telah mencoba untuk menyelesaikan latihan berikut tetapi saya macet ketika mencoba menemukan semua pasangan yang kritis . Saya punya pertanyaan berikut: Bagaimana saya tahu pasangan kritis mana yang menghasilkan aturan baru? Bagaimana saya tahu saya menemukan semua pasangan kritis?...
Saya penasaran. Saya telah mengerjakan tipe data ini di OCaml : type 'a exptree = | Epsilon | Delta of 'a exptree * 'a exptree | Omicron of 'a | Iota of 'a exptree exptree Yang dapat dimanipulasi menggunakan fungsi rekursif yang diketik secara eksplisit (fitur yang telah ditambahkan...