Telah diketahui secara umum bahwa kombinator S dan K membentuk dasar yang ditetapkan untuk kalkulus kombinator, dalam arti bahwa semua kombinator lainnya dapat diekspresikan sesuai dengan kombinasinya. Ada juga B Curry's B, C, K, W, yang memiliki properti yang sama. Pasti ada jumlah pangkalan yang...
Hukum De Morgan sering diperkenalkan dalam matematika pengantar untuk kursus ilmu komputer, dan saya sering melihatnya sebagai cara untuk mengubah pernyataan dari DAN ke ATAU dengan meniadakan istilah. Apakah ada penjelasan yang lebih intuitif mengapa hal ini berhasil daripada hanya mengingat...
Saya tahu sedikit teori tipe dependen. Dari wikipedia: Tipe dependen adalah tipe yang definisinya tergantung pada suatu nilai. Dan dari mata kuliah teori Type saya, saya ingat bahwa tipe dependen adalah: Keluarga jenis diindeks oleh suatu tipe. Tetapi saya memiliki kebingungan tentang...
Kami memiliki logika Hoare. Mengapa masih mungkin bahwa suatu algoritma itu benar tetapi tidak ada bukti bahwa itu benar? Misalkan algoritma dinyatakan dalam C. Kemudian kita dapat berdebat langkah demi langkah bahwa itu melakukan apa yang seharusnya dilakukan. Jadi pertanyaan saya adalah:...
Saya mulai membaca semakin banyak makalah penelitian bahasa. Saya merasa sangat menarik dan cara yang baik untuk mempelajari lebih lanjut tentang pemrograman secara umum. Namun, biasanya ada bagian di mana saya selalu berjuang dengan (ambil misalnya bagian ketiga dari ini ) karena saya tidak...
Apakah masalah "kehadiran pesta" dapat dipecahkan dalam Prolog? Sebagai contoh: Burdock Muldoon dan Carlotta Pinkstone berkata bahwa mereka akan datang jika Albus Dumbledore datang. Albus Dumbledore dan Daisy Dodderidge keduanya mengatakan mereka akan datang jika Carlotta Pinkstone datang. Albus...
xorgate, sekarang saya perlu membuat gate ini hanya menggunakan 4 nandgate a b out 0 0 0 0 1 1 1 0 1 1 1 0 yang xor = (a and not b) or (not a and b), yang merupakan A¯¯¯¯B+AB¯¯¯¯A¯B+AB¯\begin{split}\overline{A}{B}+{A}\overline{B}\end{split} Saya tahu jawabannya tetapi bagaimana cara...
Saya belajar Pembuktian Teorema Otomatis / Pemecah SMT / Asisten Bukti sendiri dan memposting serangkaian pertanyaan tentang prosesnya, mulai dari sini . Saya terus membaca tentang Algoritma Unifikasi . Apa itu dan mengapa begitu penting untuk Inference Engine ? Mengapa begitu penting bagi Ilmu...
Adakah yang pernah benar-benar menulis sebuah sistem (perangkat lunak atau penjelasan terperinci di atas kertas dengan contoh sederhana) yang menghasilkan program komputer? Saya memasukkan dan ia menciptakan sebuah program yang mencantumkan bilangan prima kurang dari 10. secara sederhana...
Saya mencoba untuk datang dengan sebuah sistem yang akan mengevaluasi peraturan bagi suatu organisasi untuk menentukan logika yang mendasari mereka. Saya pikir sistem predikat orde pertama akan berfungsi untuk mewakili aturan, yang dapat diterjemahkan dari teks melalui penandaan bagian-of-speech...
Combinator Y memiliki tipe . Oleh Korespondensi Curry-Howard, karena jenis ( a → a ) → a dihuni, maka harus sesuai dengan teorema yang benar. Namun a → a selalu benar, jadi sepertinya tipe kombinator Y sesuai dengan teorema a , yang tidak selalu benar. Bagaimana ini bisa terjadi?( a → a ) →...
Saya belajar Automated Teorema Membuktikan / SMT pemecah / Asisten Bukti sendiri dan posting serangkaian pertanyaan tentang proses, mulai di sini . Mengapa bahwa provers teorema otomatis, yaitu ACL2 , dan SMT pemecah tidak perlu bantuan manusia sementara bukti asisten, yaitu Isabelle dan Coq ,...
Saya mencoba untuk membungkus kepala saya di sekitar bukti NP-kelengkapan yang tampaknya berputar di sekitar SAT / 3CNF-SAT. Mungkin ini sudah larut tetapi saya khawatir saya tidak dapat memikirkan formula 3CNF yang tidak dapat dipenuhi (saya mungkin kehilangan sesuatu yang jelas). Bisakah Anda...
Saya sedang mengerjakan kompiler untuk bahasa concatenative dan ingin menambahkan dukungan jenis inferensi. Saya mengerti Hindley-Milner, tetapi saya telah mempelajari teori jenis ketika saya pergi, jadi saya tidak yakin bagaimana mengadaptasinya. Apakah sistem berikut ini masuk akal dan dapat...
Saya adalah asisten bukti belajar mandiri dan memutuskan untuk memulai pada beberapa bukti dasar dan terus maju. Karena bukti didasarkan pada bukti lain dan karenanya membentuk hierarki, adakah repositori dari hierarki bukti? Saya tahu saya dapat memilih asisten bukti dan menganalisis...
Urutan yang berlaku: Selalu sepenuhnya mengevaluasi argumen dari suatu fungsi sebelum mengevaluasi fungsi itu sendiri, seperti - (λx.x2(λx.(x+1) 2)))→(λx.x2(2+1))→ (λx.x2(3))→ 32 → 9(λx.x2(λx.(x+1) 2)))→(λx.x2(2+1))→ (λx.x2(3))→ 32 → 9(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow...
Saya dapat memahami pentingnya bahwa ilmuwan komputer atau insinyur terkait pengembangan perangkat lunak harus memahami studi tentang logika dasar sebagai dasar. Tetapi apakah ada tugas / pekerjaan yang secara eksplisit membutuhkan pengetahuan tentang hal ini, selain tugas yang membutuhkan...
Asumsikan kita memiliki bahasa sederhana yang terdiri dari istilah: truetrue\mathtt{true} falsefalse\mathtt{false} jika adalah suku maka demikian juga saya ft1,t2,t3t1,t2,t3t_1,t_2,t_3ift1thent2elset3ift1thent2elset3\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 Sekarang...
Berikut ini konteksnya ( Struktur dan Interpretasi Program Komputer , bagian 1.1.8, di bawah judul "Nama lokal"): Parameter formal dari suatu prosedur memiliki peran yang sangat khusus dalam definisi prosedur, karena tidak peduli apa nama parameter formal tersebut. Nama seperti itu disebut...
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...