ตรรกศาสตร์: Unification

โทษทีนะที่ไม่ได้ update วันต่อวัน ... คือว่า ช่วงนี้ไม่ค่อยมีเวลาอยู่กับเครื่องคอมพิวเตอร์หละ โดนพี่แย่ง :P ขอชดเชย เขียนย้อนหลังไปอีก 2 วันนะ

มาต่อกันเรื่องตรรกศาสตร์อีกนิด จะจบแล้ว ตอนนี้เราทำภาษาอันดับหนึ่ง ให้อยู่ รูปแบบวรรค (Clause Form)

ตัวอย่างที่ 1 สมมติว่าเรามีวรรคต่อไปนี้

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

Q(x) และ ¬Q(y) ในทั้งสองวรรค มันจะรวมกัน (ด้วย Resolution) ได้ถ้า x = y

เนื่องจาก x และ y เป็นตัวแปรที่บ่งปริมาณด้วย ∀ เราจะใช้คุณสมบัติที่ว่า

∀x[P(x)] ∧ ∀y[Q(y)] ≡ ∀x[P(x) ∧ Q(x)]

เพื่อรวมตัวแปรทั้งสองให้เป็นตัวแปรใหม่ตัวเดียว ผลลัพธ์ก็คือ เราจะได้วรรคใหม่ 2 วรรคเป็น

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

คราวนี้ เราจะใช้ Resolution ได้แล้ว ผลลัพธ์ก็คือวรรคใหม่ที่หน้าตาเป็นหยั่งงี้

¬P(x) ∨ R(x)

ข้อสังเกต: วรรค 2 วรรคแรก สามารถแปลงกลับเป็น ∀x[P(x) → Q(x)] กับ ∀x[Q(x) → R(x)] ได้ ส่วนวรรคสุดท้าย ก็สามารถแปลงกลับได้เป็น ∀x[P(x) → R(x)]

ตัวอย่างที่ 2 มาดูเรื่องการเปลี่ยนตัวแปรกัน

สมมติว่ามีวรรคแบบนี้

1. P(x) ∨ ¬Q(x, y) ∨ S(x)
2. R(x, y) ∨ ¬P(y) ∨ S(x)

เราเห็นว่า ตัว P(x) กับ ¬P(y) เนี่ย น่าจะรวมกันได้ เราจะทำแบบเมื่อกี๊ได้มั้ย? ... ถ้าเราเปลี่ยนตัวแปร y ในวรรคที่ 2 ให้เป็น x มันจะกลายเป็น

R(x, x) ∨ ¬P(x) ∨ S(x)

ตัวแปรมันหายไปตัวนึง ... วรรคนี้มันไม่เท่ากับวรรคต้นฉบับแล้ว ... แต่ก็แก้ง่าย ๆ นะ แค่เปลี่ยนเป็นตัวแปรอื่นที่มันไม่ซ้ำกัน ก็ใช้ได้แล้ว (จริง ๆ อันนี้มันก็ใช้ได้แหละ แต่มันไม่ทั่วไปที่สุด ซึ่งเดี๋ยวจะพูดถึง) เอาหละ ลองแทนแบบนี้นะ

• วรรค 1 แทนด้วย { a/x, b/y }
• วรรค 2 แทนด้วย { a/y, c/x } (จริง ๆ เป็น { a/y, b/x } ก็ได้ แต่ผลมันจะไม่เหมือนกัน เดี๋ยวจะทำให้ดูอีกที)

นี่เป็นสัญลักษณ์ที่เค้านิยมใช้กัน หมายถึง การแทนค่า (Substitution) ตัว a/x หมายถึง เอา a ไปแทนที่ x ... ผลลัพธ์ของการแทนค่าก็คือ

3. P(a) ∨ ¬Q(a, b) ∨ S(a)
4. R(c, a) ∨ ¬P(a) ∨ S(c)

มันรวมกันได้แล้ว ผลลัพธ์เป็น

5. ¬Q(a, b) ∨ S(a) ∨ R(c, a) ∨ S(c)

ซึ่งเราจะเปลี่ยนตัวแปรกลับเป็น x y z ก็ได้ เช่น

5. ¬Q(x, y) ∨ S(x) ∨ R(z, x) ∨ S(z)

ตรงนี้เป็นผลลัพธ์ที่ถูกต้องแล้ว แต่เมื่อกี๊บอกไว้นิดนึงว่า จะลองใช้ { a/y, b/x } แทนใน 2 ตอนนี้ทำให้ดูเลยละกัน ว่ามันจะได้อะไร

6. R(b, a) ∨ ¬P(a) ∨ S(b)

แล้วลองดูวรรคที่ 3 อีกที

3. P(a) ∨ ¬Q(a, b) ∨ S(a)

วรรคที่ 6 กับ 3 ก็รวมกันได้ ผลลัพธ์จะเป็น

7. ¬Q(a, b) ∨ S(a) ∨ R(b, a) ∨ S(b)

เอา 5 มามองดู เทียบกับ 7 ดูว่ามันต่างกันยังไง

5. ¬Q(a, b) ∨ S(a) ∨ R(c, a) ∨ S(c)

จะเห็นว่า ถ้าเราแทนค่าด้วย { b/c } ในวรรคที่ 5 เราก็จะได้วรรทึ่ 7 ซึ่งก็แปลว่า 5 เป็น กรณีทั่วไป มากกว่า 7 ดังนั้น ผลลัพธ์การรวมในวรรคที่ 5 จึง น่าจะ ใช้ประโยชน์ได้มากกว่า 7 (เดี๋ยวพูดถึงอีกที)

ตรงนี้ เราได้หลักการหา ตัวรวมทั่วไปที่สุด (Most General Unifier) คร่าว ๆ แล้ว ดังนี้

• มองพจน์ที่ต้องการจะรวม แทนค่าตัวแปรของพจน์นั้นในทั้งสองวรรค ให้พจน์หน้าตาเหมือนกัน
• ตัวแปรอื่น ๆ ที่ยังไม่ถูกแทนค่า (เพราะว่า ไม่ได้อยู่ในพจน์ที่ต้องการจะรวม) ในทั้งสองวรรค ให้แทนค่าเป็น ตัวแปรใหม่ที่หน้าตาไม่เหมือนกัน (ตัวอย่างนี้ คือ a/x ในวรรคที่ 1 และ c/x ในวรรคที่ 2)
  

ตัวอย่างที่ 3 ลองดูอีกอันนึง แบบมีัฟังก์ชันมายุ่งด้วย

1. P(x, f(x)) ∨ R(x)
2. ¬Q(x, f(x), z) ∨ R(x)
3. ¬P(x, y) ∨ Q(x, y, g(x, y)) ∨ ¬R(x)

สมมติว่า เราอยากรวมวรรค 2 กับ 3 ที่ตัว R(x) ด้วยตัวรวมทั่วไปที่สุด ... จะได้

4. ¬Q(x, f(x), z) ∨ ¬P(x, y) ∨ Q(x, y, g(x, y))

แล้วถ้าเพิ่ม { g(x, y)/z, f(x)/y } เข้าไปหละ (y กับ z มันบ่งปริมาณด้วย ∀ เราจะให้มันเป็นอะไรก็ได้) ... เราจะได้อะไรอีกอย่าง

5. ¬Q(x, f(x), g(x, f(x))) ∨ ¬P(x, f(x)) ∨ Q(x, f(x), g(x, f(x)))

ซึ่งมันเท่ากับ

5. ¬P(x, f(x))

รู้สึกว่า วรรคที่ 5 มันจะดูดีกว่า 4 นะ ... หยั่งงี้มันแปลว่า ตัวรวมทั่วไปที่สุดอาจจะไม่ได้ดีที่สุดน่ะสิ ??? (วรรคที่ 4 เกิดจากตัวรวมทั่วไปที่สุด แต่วรรคที่ 5 มันไม่ใช่หนิ)

มันไม่ใช่หยั่งงั้นหรอก :P ลองเอาวรรคที่ 4 รวมกับตัวเองสิ

4. ¬Q(x, f(x), z) ∨ ¬P(x, y) ∨ Q(x, y, g(x, y))

4. ¬Q(x, f(x), z) ∨ ¬P(x, y) ∨ Q(x, y, g(x, y))

คู่เดียวที่จับได้คือ Q(x, y, g(x, y)) กับ ¬Q(x, f(x), z) ดังนั้น ตัวรวมทั่วไปที่สุดก็จะเป็น { g(x, y)/z, f(x)/y } ซึ่งก็คือ ตัวเดียวกับที่เราใช้เพื่อสร้างวรรคที่ 5 ผลลัพธ์ที่ได้ ก็คือวรรคที่ 5 น่ะแหละ

5. ¬P(x, f(x))

คราวนี้ ลองเอาวรรคที่ 1 กับ 5 รวมกัน (ขอเปลี่ยนตัวแปรให้ไม่ซ้ำกันนะ)

1. P(x, f(x)) ∨ R(x)
5. ¬P(y, f(y))

ตัวรวมทั่วไปที่สุดคือ { x/y } (หรือ { y/x }) ได้ผลลัพธ์เป็น

6. R(x)

ข้อสังเกต: เมื่อเราได้วรรคที่ 6 แล้ว วรรคที่ 1 กับ 2 ก็จะไม่มีประโยชน์แล้ว

อีกนิดนึง เรื่องการแทนค่า

เอาตัวอย่างเมื่อกี๊แหละ ตอนที่รวม 2 กับ 3 เข้าด้วยกัน สมมติว่า คราวนี้เราเลือกที่จะรวม Q แทนที่จะรวม R

2. ¬Q(x, f(x), z) ∨ R(x)
3. ¬P(x, y) ∨ Q(x, y, g(x, y)) ∨ ¬R(x)

เราบอกว่า ตัวรวมทั่วไปที่สุดคือ { g(x, y)/z, f(x)/y } ... ลองเอาไปแทนค่า จากซ้ายไปขวา

Q(x, f(x), z) ⋅ { g(x, y)/z } = Q(x, f(x), g(x, y))
Q(x, f(x), g(x, y)) ⋅ { f(x)/y } = Q(x, f(x), g(x, f(x)))

แล้วถ้าเราแทนจากขวาไปซ้ายหละ?

Q(x, f(x), z) ⋅ { f(x)/y } = Q(x, f(x), z)
Q(x, f(x), z) ⋅ { g(x, y)/z } = Q(x, f(x), g(x, y))

มันไม่เหมือนกัน!!! ถ้าแทนจากซ้ายไปขวา จะไม่มีตัว y เหลือ แต่พอแทนจากขวาไปซ้าย มันดันมีตัว y เหลืออยู่...

มันก็แปลว่า ตอนที่เราหาตัวรวมทั่วไปที่สุด เราต้องหาลำดับที่ถูกต้องเลยรึเปล่า?

จริง ๆ แล้วไม่ต้องหรอก แต่ตอนหาต้องระวังนิดนึง ... มันมี algorithm อยู่ ดูนี่นะ

Q(x, f(x), z)
Q(x, y, g(x, y))

เริ่มต้น เราก็ดูว่า parameter แรก มันรวมกันได้รึเปล่า ... มันเป็น x กับ x อยู่แล้ว ไม่ต้องสน ดูตัวต่อไปเลย

Q(x, f(x), z)
Q(x, y, g(x, y))

คราวนี้ f(x) กับ y มันจะรวมได้ถ้าเราใช้ { f(x)/y } (ตัวที่ถูกแทนที่ ต้องเป็นตัวแปรเสมอนะ) คราวนี้ เราจะดูตัวต่อไป

Q(x, f(x), z)
Q(x, y, g(x, y))

ตรงนี้แหละที่มันแปลก ๆ เพราะว่าเมื่อกี๊เรากำจัดตัว y ไปแล้ว ทำไมมันยังมีอยู่? ... จริง ๆ แล้วเราต้องเอา { f(x)/y } เมื่อกี๊ ไปแทนในโจทย์เลยต่างหาก มันจะเป็น

Q(x, f(x), z)
Q(x, y, g(x, f(x)))

นี่สิ ถึงจะถูก!! ... ทำต่อนะ ตัวรวม z กับ g(x, f(x)) ก็คือ { g(x, f(x))/z }

ตัวรวมทั่วไป ก็คือ { f(x)/y, g(x, f(x))/z } นั่นเอง ... แต่มันไม่ตรงกับ คราวที่แล้วนะ คราวที่แล้วมันเป็น { g(x, y)/z, f(x)/y } ?

มันก็ไม่ตรงแหละ แต่เวลาเอาไปแทนค่า มันจะได้ผลลัพธ์เหมือนกัน (ไม่เชื่อก็ลองสิ :P)

หมายเหตุ: algorithm การหาตัวรวมทั่วไปที่บอกเนี่ย มันมอง parameter จากซ้ายไปขวา ผลลัพธ์ก็เป็น { f(x)/y, g(x, f(x))/z } แต่ลำดับการมอง parameter จริง ๆ แล้ว มันจะเป็นยังไงก็ได้ ถ้ามองจากขวาไปซ้าย ก็จะได้ตัวรวมทั่วไปที่บอกไว้ตอนแรก คือ { g(x, y)/z, f(x)/y } ตัวรวมที่ได้ อาจจะไม่เหมือนกัน แต่พอเอาไปแทนค่า มันจะเหมือนกัน

การพิสูจน์แบบ Resolution-Refutation สำหรับภาษาอันดับหนึ่ง

เมื่อกี๊เรารู้แล้ว ว่า Resolution สามารถทำกับวรรคได้ยังไง เราก็ใช้หลักการเดียวกับที่เคยบอกไว้ใน ตรรกศาสตร์: รูปแบบปกติประพจน์รวม ได้ ซึ่งก็คือ

1. ใส่นิเสธที่ประพจน์ที่ต้องการพิสูจน์
2. แปลงประพจน์ทั้งหมด (ทั้งที่กำหนดให้ และที่ต้องการพิสูจน์) ให้อยู่ในรูปแบบวรรค
3. ทำ Resolution จนกว่าจะได้ประพจน์ว่าง

แต่กรณีของภาษาอันดับหนึ่งเนี่ย มันต่างไปตรงที่ ... มันสามารถทำ resolution ได้เรื่อย ๆ ไม่สิ้นสุดน่ะสิ

ดังนั้น ถ้าประพจน์ที่ต้องการพิสูจน์เป็นจริง เมื่อได้ประพจน์ว่างเราก็จะรู้ แต่ถ้ามันไม่จริง เราก็อาจจะต้องทำไปเรื่อย ๆ เรื่อย ๆ ... เหมือนกับ ไม่มีทางรู้เลย ว่ามันเป็นจริงรึเปล่า

จะว่าไป มันก็เทียบได้กับ halting problem น่ะแหละ (เทียบได้จริง ๆ นะ เหมือนกัันเด๊ะเลย)

เฮ่อ ... จบแล้ว เรื่อง algorithm ของภาษาอันดับหนึ่ง คราวหน้าเรื่อง วรรคฮอร์น (Horn Clause) และ ภาษา PROLOG นะ