ตรรกะในการคำนวณ

ตรรกะในการคำนวณประยุกต์ใช้เครื่องมือของตรรกะทางคณิตศาสตร์เพื่ออธิบาย ระบุ และให้เหตุผลเกี่ยวกับระบบการคำนวณ และเพื่อจำแนกประเภทความซับซ้อนโดยใช้ทรัพยากรเชิงตรรกะที่จำเป็นในการกำหนดปัญหาของประเภทเหล่านั้น

Definition

ตรรกะในการคำนวณคือการศึกษาเกี่ยวกับระบบตรรกะเชิงรูปนัย (formal logical systems) ในฐานะภาษาสำหรับการระบุและตรวจสอบพฤติกรรมการคำนวณ และในฐานะมาตรวัดสำหรับความซับซ้อนเชิงคำนวณ โดยถือว่าการคำนวณและการนิยามเชิงตรรกะเป็นสองด้านของปรากฏการณ์เดียวกัน

Scope

สาขานี้ครอบคลุมตรรกะเชิงเวลาและตรรกะเชิงโมดอลสำหรับการระบุพฤติกรรมของโปรแกรมและระบบเชิงตอบสนอง (reactive systems) ความซับซ้อนเชิงพรรณนา (descriptive complexity) ที่เทียบเท่าประเภทความซับซ้อนกับการนิยามเชิงตรรกะ และการตีความเชิงคำนวณของทฤษฎีบทความไม่สมบูรณ์ของเกอเดล (Gödel's incompleteness theorems) และความสัมพันธ์กับการตัดสินไม่ได้ (undecidability) โดยอาศัยปฏิสัมพันธ์อันยาวนานระหว่างตรรกะและวิทยาการคอมพิวเตอร์

Sub-topics

• ความซับซ้อนเชิงพรรณนา
• ความไม่สมบูรณ์และการคำนวณของเกอเดล
• ตรรกะเชิงเวลาและเชิงกิริยาในการคำนวณ

Core questions

• สูตรตรรกะสามารถระบุพฤติกรรมที่ถูกต้องของโปรแกรมและระบบได้อย่างไร?
• ประเภทความซับซ้อนสามารถจำแนกได้อย่างบริสุทธิ์ด้วยความสามารถในการแสดงออกเชิงตรรกะหรือไม่?
• เนื้อหาเชิงคำนวณของทฤษฎีบทความไม่สมบูรณ์ของเกอเดลคืออะไร?
• ตรรกะและการคำนวณให้ความกระจ่างแก่ข้อจำกัดของกันและกันได้อย่างไร?

Key theories

ความซับซ้อนเชิงพรรณนา

ประเภทความซับซ้อนที่สำคัญสอดคล้องกับประเภทของปัญหาที่สามารถนิยามได้ในตรรกะเฉพาะ ดังนั้นทรัพยากรของการคำนวณจึงสามารถวัดได้ด้วยพลังการแสดงออกเชิงตรรกะ แทนที่จะเป็นเวลาหรือพื้นที่ของเครื่องจักร

ตรรกะสำหรับพฤติกรรมของโปรแกรม

ตรรกะเชิงเวลา ตรรกะเชิงโมดอล และตรรกะเชิงพลวัต (dynamic logics) เป็นภาษาที่แม่นยำสำหรับการระบุคุณสมบัติ เช่น ความปลอดภัยและการมีชีวิต (liveness) ซึ่งเป็นพื้นฐานของการตรวจสอบเชิงรูปนัยของฮาร์ดแวร์และซอฟต์แวร์

Clinical relevance

การระบุพฤติกรรมของระบบเชิงตรรกะเป็นพื้นฐานของการตรวจสอบเชิงรูปนัย (formal verification) และการตรวจสอบแบบจำลอง (model checking) ที่ใช้ในการรับรองฮาร์ดแวร์และซอฟต์แวร์ที่สำคัญต่อความปลอดภัย ในขณะที่ความซับซ้อนเชิงพรรณนาเสนอแนวคิดเกี่ยวกับความสามารถในการจัดการ (tractability) ที่ไม่ขึ้นกับเครื่องจักร ซึ่งเป็นข้อมูลสำหรับภาษาคิวรีฐานข้อมูลและรากฐานของทฤษฎีความซับซ้อน

History

ความเชื่อมโยงระหว่างตรรกะและการคำนวณมีมาตั้งแต่เกอเดลและทัวริงในช่วงทศวรรษ 1930 จนถึงการเติบโตของวิทยาการคอมพิวเตอร์ ทฤษฎีบทของ Fagin ในปี 1974 ได้ริเริ่มความซับซ้อนเชิงพรรณนา Pnueli ได้นำเสนอ ตรรกะเชิงเวลา (temporal logic) สำหรับโปรแกรมในปี 1977 และการตรวจสอบแบบจำลองได้พัฒนาขึ้นในช่วงทศวรรษ 1980 กลายเป็นเทคโนโลยีการตรวจสอบที่สำคัญ ซึ่งทำให้รากฐานเชิงตรรกะของสาขานี้ลึกซึ้งยิ่งขึ้น

Key figures

• Kurt Gödel
• Amir Pnueli
• Neil Immerman
• Ronald Fagin

Seminal works

• immerman1999
• harel2000

Frequently asked questions

ตรรกะถูกนำมาใช้ในวิทยาการคอมพิวเตอร์นอกเหนือจากคณิตศาสตร์บริสุทธิ์ได้อย่างไร?

ตรรกะเป็นภาษาสำหรับการระบุว่าระบบควรทำอะไรอย่างแม่นยำ และเป็นวิธีการพิสูจน์ว่าระบบทำเช่นนั้น ตรรกะเชิงเวลาระบุพฤติกรรมที่กำลังดำเนินอยู่ ระบบประเภท (type systems) และตรรกะของโปรแกรม (program logics) รับรองรหัส และความซับซ้อนเชิงพรรณนาปรับเปลี่ยนประสิทธิภาพในแง่ของการนิยาม ทำให้ตรรกะเป็นเครื่องมือทางวิศวกรรมที่ใช้งานได้จริงและเป็นรากฐาน

ความซับซ้อนเชิงพรรณนาเผยให้เห็นอะไร?

แสดงให้เห็นว่าประเภทความซับซ้อนสามารถนิยามได้โดยไม่ต้องอ้างอิงถึงเครื่องจักรหรือขอบเขตเวลา โดยอาศัยเพียงตรรกะที่สามารถแสดงปัญหาของประเภทเหล่านั้นได้ ตัวอย่างเช่น ปัญหาที่สามารถแก้ไขได้ในเวลาพหุนามบนโครงสร้างที่มีลำดับคือปัญหาที่สามารถนิยามได้ในส่วนขยายบางอย่างของตรรกะอันดับหนึ่ง ซึ่งเชื่อมโยงการคำนวณเข้ากับความสามารถในการแสดงออกเชิงตรรกะ