ตรรกศาสตร์: วรรคฮอร์น และ ภาษา PROLOG

เราจะเรียกวรรควรรคนึงว่าเป็น วรรคฮอร์น (Horn Clause) ก็ต่อเมื่อ มีเพียง predicate เดียวในวรรคนั้น ที่ไม่มีเครื่องหมายนิเสธกำกับ เช่น

¬P(x) ∨ Q(y) ∨ ¬R(z) เป็นวรรคฮอร์น

P(x) ∨ ¬Q(y) ∨ R(z) ไม่เป็นวรรคฮอร์น

ลองสังเกตนิดนึง จะเข้าใจว่า วรรคฮอร์นพิเศษยังไง ...

¬A ∨ ¬B ∨ ¬C ∨ Z
≡ (A ∧ B ∧ C) → Z

ความหมายมันก็คือ การพิสูจน์ว่า Z เป็นจริง สามารถทำได้โดยการ พิสูจน์ว่า A B C เป็นจริงพร้อมกัน

สมมติว่าเรามีวรรคฮอร์นเพิ่มอีกวรรค กลายเป็นสองวรรค ดังนี้

¬A ∨ ¬B ∨ ¬C ∨ Z
¬ D ∨ ¬ E ∨ ¬ F ∨ Z

ถ้าเราต้องการจะพิสูจน์ว่า Z เป็นจริง จะมีทางเลือกให้ 2 ทาง คือ

1. พิสูจน์ว่า A B C เป็นจริงพร้อมกัน
2. พิสูจน์ว่า D E F เป็นจริงพร้อมกัน

ถ้าทำได้ซักทาง ก็แปลว่า Z เป็นจริง แต่ถ้าทำไม่ได้ ก็แปลว่า Z "ไม่จำเป็นต้องจริง" (ไม่ได้แปลว่า ไม่จริง นะ)

วรรคเป้าหมาย (Goal Clause) คือ วรรคที่ predicate ทุกตัว มีเครื่องหมายนิเสธกำกับ เช่น

¬P(x) ∨ ¬Q(y) ∨ ¬R(z)

สมมติว่า เรามีระบบของภาษาอันดับหนึ่ง ซึ่งเมื่อแปลงเป็นรูปแบบวรรคแล้ว ทุกวรรคเป็นวรรคฮอร์น แล้วเราต้องการจะพิสูจน์ว่า วรรคเป้าหมายซักอันนึง เป็นจริงรึเปล่า ... เราต้องพยายามหา วรรคที่รวมกับวรรคเป้าหมายได้

ดูตัวอย่างดีกว่า ถ้าอ่านแล้วงง ... ถ้าเราต้องการจะนิยามประพจน์ Even(x) กับ Odd(x) เมื่อ x เป็นจำนวนเต็มไม่ติดลบ ดังนี้

• Even(x) ≡ x เป็นเลขคู่
• Odd(x) ≡ x เป็นเลขคี่

เราจะรู้ว่า "กฎ" ต่อไปนี้ เป็นจริง

1. Even(0)
2. Even(x) → Odd(NextOf(x))
3. Odd(x) → Even(NextOf(x))

เราก็ แปลงให้เป็นรูปแบบวรรค ได้แบบนี้

1. Even(0)
2. ¬Even(x) ∨ Odd(NextOf(x))
3. ¬Odd(x) ∨ Even(NextOf(x))

วรรคทั้งสามวรรคนี้ เป็นวรรคฮอร์นหมดเลย

สมมติ เราอยากรู้ว่า Odd(NextOf(NextOf(NextOf(0)))) เป็นจริงรึเปล่า (คือ "3 เป็นเลขคี่รึเปล่า" อะนะ) เราก็ต้องตั้งวรรคเป้าหมาย เป็นนิเสธของสิ่งที่ต้องการพิสูจน์ ว่า

Goal: ¬Odd(NextOf(NextOf(NextOf(0))))

เราก็ต้อง พยายามหา predicate ที่รวมกับกฎได้ ... จะเห็นว่า วรรคที่ 2 สามารถรวมกับ วรรคเป้าหมาย ได้ด้วยตัวรวมทั่วไปที่สุด { NextOf(NextOf(0)) / x } ผลลัพธ์ก็จะเป็นวรรคใหม่ อันนี้...

Goal: ¬Even(NextOf(NextOf(0)))

มันก็เป็นวรรคเป้าหมายเหมือนกัน ตามนิยาม ... จะคิดซะว่า เป็นเป้าหมายใหม่ ก็ใช่แหละ ... คราวนี้ วรรคเป้าหมายนี้ ก็สามารถรวมได้กับ วรรคที่ 3 เท่านั้น ตัวรวมทั่วไปที่สุดคือ { Next(0) / x } ผลลัพธ์เป็น วรรคเป้าหมายใหม่อีกวรรค คือ

Goal: ¬Odd(NextOf(0))

หาวรรคมารวมอีกที จะเห็นว่า วรรคที่ 2 เป็นวรรคเดียวที่ใช้ได้ โดยมีตัวรวมทั่วไปที่สุดเป็น { 0 / x } ผลลัพธ์คือ

Goal: ¬Even(0)

คราวนี้ เห็นชัดเลยว่า วรรคที่ 1 จะรวมกับวรรคนี้ได้ และให้ผลลัพธ์เป็นวรรคว่าง ... สรุปว่า 3 เป็นเลขคี่นะ :D

เห็นแล้วใช่มั้ยหละ ว่าวรรคฮอร์น กับวรรคเป้าหมาย มีคุณสมบัติพิเศษคือ

"ผลลัพธ์ของการรวมวรรคฮอร์นกับวรรคเป้าหมาย (เก่า) คือวรรคเป้าหมาย (ใหม่)"

สาเหตุที่วรรคฮอร์น ก่อกำเนิดขึ้น และได้รับความนิยม เป็นเพราะว่า

• ในวรรคเป้าหมาย ทุก predicate ติดนิเสธ
• ในวรรคฮอร์น มี predicate เดียวที่ไม่ติดนิเสธ
• ผลลัพธ์ของการรวม เป็นวรรคเป้าหมาย (ซึ่งทุก predicate ติดนิเสธ)
  

ดังนั้น การค้นหา predicate ที่สามารถรวมกันได้ จะรวดเร็วกว่ากรณีทั่วไป (ที่มีกฎที่ไม่อยู่ในรูปแบบ วรรคฮอร์น)

นอกจากนั้น การเพิ่มข้อกำหนดที่ว่า กฎทุกข้อ ต้องเป็นวรรคฮอร์น ลงไป ทำให้การสร้างโปรแกรมสำหรับช่วยพิสูจน์ ง่ายขึ้นมาก ... มันก็เร็วขึ้นด้วยแหละ อย่างที่บอกไปแล้ว

ภาษา PROLOG

โปรแกรมคอมพิวเตอร์ที่พูดถึงเมื่อกี๊ ก็คือ ภาษา PROLOG น่ะแหละ หน้าตามันจะประมาณนี้

Z :- A, B, C.
Z :- D, E, F.

ความหมายก็คือ ถ้าฝั่งขวาทุกตัวเป็นจริง ฝั่งซ้ายจะเป็นจริง แต่ถ้าจะเขียนว่า ฝั่งซ้ายเป็นจริงเสมอ ก็เขียนได้ โดยไม่ต้องมีเครื่องหมาย ":-" (แต่อย่าลืม "." ลงท้ายนะ) เช่น

Even(0).

ส่วน วรรคเป้าหมาย เค้ามักจะเขียนกันแบบนี้

:- P, Q, R.

ใครสนใจ ลองไปหาตัวแปลภาษา PROLOG เล่นได้ ที่นี่: SWI-Prolog

อ้อ ... สำหรับใครที่เอา SWI-Prolog ไปเล่น ... ชื่อตัวแปรที่ใช้ จะต้องขึ้นต้นด้วยตัวใหญ่นะ นอกนั้น ให้ขึ้นด้วยตัวเล็ก (ทั้งชื่อ predicate ชื่อฟังก์ชัน แล้วก็ชื่อค่าคงที่ด้วย) ... เอาตัวอย่างให้ดูนิดนึง

even(0).
odd(nextof(X)) :- even(X).
even(nextof(X)) :- odd(X).

แล้วก็ ... เค้ามีฟังก์ชันพื้นฐานให้ใช้ เยอะเหมือนกัน จริง ๆ ไม่ต้องเขียน nextof อะไรแบบนี้หรอก ใช้คำสั่ง add เลยก็ได้