Logika Orde Kedua Monadik untuk Dummies

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 memahami automata dan orang-orang (dalam makalah) telah mencoba menjelaskan hubungannya dengan MSO kepada saya, mereka selalu menganggap latar belakang yang kuat dalam logika dan pemahaman tentang MSO.

Ketika saya melihat buku dan kursus tentang logika, mereka kebanyakan hanya menangani logika urutan pertama, yang tampaknya cukup sederhana dan hanya terdiri dari beberapa konsep: variabel, atau, dan, bukan, menyiratkan, untuk semua, ada, dll.

Dapatkah seseorang menjelaskan atau mengarahkan saya ke sumber yang dapat menjelaskan:

Apa logika urutan kedua berbeda dengan logika urutan pertama?
Apa itu logika monadik vs non monadik?
Mengapa logika urutan kedua harus monadik untuk diperhitungkan ATAU mengapa ini pertanyaan yang salah?
Mengapa logika urutan kedua monadik dapat dipilih?
Hubungannya dengan setidaknya DFA?

Jika ini adalah sumber daya, akan lebih baik jika mengasumsikan bahwa saya seorang programmer dan bukan seorang ahli logika. Ini berarti bahwa saya ingin memahami bagaimana saya akan mengimplementasikannya sebagai kode, karena sampai saat itu matematika terasa ajaib bagi saya;)

Terima kasih untuk bantuan yang Anda dapat berikan kepada saya. Aku akan sangat menghargainya.

automata finite-automata logic coq automated-theorem-proving Walter Schulze
sumber

"Mengapa logika urutan kedua harus monadik untuk diperhitungkan ATAU mengapa ini pertanyaan yang salah?" jika Anda mengizinkan kuantifikasi atas predikat biner, misalnya

maka Anda segera meraih kekuatan Log Urutan Pertama dengan satu predikat biner yang sudah diputuskan (bahkan tanpa fungsi arity> 0, dan tanpa persamaan) [Kalmar, Suranyi, 1950]

\exists M [. . . M (x, y) . . .]

$\exists M[...M(x,y)...]$

Vor

Apa logika urutan kedua berbeda dengan logika urutan pertama?

Apa itu logika monadik vs non monadik?

Logika orde kedua monadik adalah logika orde pertama ditambah kuantifikasi atas set. Jadi, selain bisa mengatakan bahwa ada elemen domain dengan beberapa properti ( ), Anda juga bisa mengatakan bahwa ada set elemen domain dengan beberapa properti. Jadi, misalnya, kita dapat mendefinisikan 3-colourability grafik dengan mengatakan $\exists x\dots$

\begin{aligned} \exists R \exists G \exists B [ & \forall x (x \in R \lor x \in G \lor x \in B) \\ \land \neg \exists x ((x \in R \land x \in G) \lor (x \in G \land x \in B) \lor (x \in B \land x \in R)) \\ \land \forall x \forall y (E (x, y) \to \neg ((x \in R \land y \in R) \lor (x \in G \land y \in G) \\ \lor (x \in B \land y \in B)))] . \end{aligned}

$\begin{align*} \exists R\,\exists G\,\exists B\, \big[&\forall x\,\big(x\in R\lor x\in G\lor x\in B\big)\\ &\land \neg\exists x\,\big((x\in R\land x\in G) \lor (x\in G\land x\in B) \lor (x\in B\land x\in R)\big)\\ &\land \forall x\,\forall y\,\big(E(x,y)\rightarrow \neg \big((x\in R\land y\in R)\lor (x\in G\land y\in G)\\ &\qquad\qquad\qquad\qquad\qquad\quad\lor (x\in B\land y\in B)\big)\big)\big]\,. \end{align*}$

Dengan kata lain, ada warna merah, hijau dan biru sedemikian rupa

setiap simpul memiliki warna
dan tidak ada simpul yang memiliki dua warna
dan, jika ada tepi antara dua simpul, kedua simpul itu tidak memiliki warna yang sama.

$k$ $k$ $k=1$ $1$

Mengapa logika urutan kedua harus monadik untuk diperhitungkan ATAU mengapa ini pertanyaan yang salah?

Mengapa logika urutan kedua monadik dapat dipilih?

Jujur, saya tidak ingat masalah decidability. Poin kuncinya adalah bahwa logika urutan kedua penuh memungkinkan Anda mengukur urutan linear dari domain

\begin{aligned} \exists R \forall x \forall y \forall z [ & (R (x, y) \lor R (y, x)) \\ ((R (x, y) \land R (y, x)) \to x = y) \\ ((R (x, y) \land R (y, z)) \to R (x, z))] . \end{aligned}

$\begin{align*} \exists R\,\forall x\,\forall y\,\forall z\,\big[&(R(x,y)\lor R(y,x)\big)\\ &\big((R(x,y)\land R(y,x))\rightarrow x=y\big)\\ &\big((R(x,y)\land R(y,z))\rightarrow R(x,z)\big)\big]\,. \end{align*}$

$D$ $D^n$ $n$ $D^n$ $n$

(Saya rasa, jika domain Anda tidak terbatas, Anda mungkin perlu menentukan selain bahwa tatanan linier diskrit dan memiliki elemen minimal; maka Anda tahu bahwa ia memiliki segmen awal yang isomorfik dengan bilangan asli, dan itu seharusnya cukup.)

$\exists R_1\dots \exists R_k\,\varphi$ $R_i$ $\varphi$

Hubungannya dengan setidaknya DFA?

$\Sigma$ $\leq$ $R_a$ $a\in\Sigma$ $R_a$

$k$ $Q_1, \dots, Q_k$ $Q_i$ $i$

$j$ $Q_1, \dots, Q_k$
$Q_1$
$j$ $Q_i$ $(j+1)$
posisi akhir dalam keadaan menerima.

$j$ $j$ $j'>j$ $j'$

Saat ini, saya tidak ingat bukti sebaliknya (bahwa semua yang dapat didefinisikan dalam MSO dapat dikenali oleh robot yang sesuai). Jika saya punya waktu, saya akan mencari dan memposting sketsa.

$i$ $X$ $1$ $i$ $X$

$R_a(i)$ $i$ $a$ $i\in X$ $i$ $X$ $i<j$ $i$ $j$

$\lor, \lnot$ $\exists i, \exists X$ $\cup$ ${}^c$

David Richerby
sumber

Menambahkan saran saya untuk yang sebaliknya. Menunggu persetujuan oleh @DavidRicherby

Hendrik

Terima kasih atas tanggapan yang bagus. Saya masih memproses semua ini dan bekerja melalui itu, mencari istilah, berpikir bagaimana saya akan mengimplementasikan ini, dll. Sementara itu saya pikir nomor 3 adalah pertanyaan yang salah. Mungkin lebih baik mengapa hubungan antara automata dan logika begitu penting, sehingga disebutkan dalam banyak artikel?

Walter Schulze

Terima kasih atas jawaban yang bagus!

Klas.

Logika Orde Kedua Monadik untuk Dummies

Jawaban: