- มองกระบวนการสมัครพาสปอร์ตในสหราชอาณาจักรเหมือนเกมปริศนา และเล่าประสบการณ์ในการทำให้กระบวนการสมัครที่ซับซ้อนนี้เป็นกฎด้วยการเขียนโปรแกรมด้วย Haskell
- การสมัครพาสปอร์ตออนไลน์มีความสนุกหลักอยู่ที่การรวบรวมเอกสารหลากหลายชนิด การตีความกฎที่ซับซ้อน และเควสต์ย่อยที่คาดไม่ถึง
- เชื่อมโยงตรรกะของกระบวนการสมัครเข้ากับ 'Constructive Logic' และเน้นย้ำว่าเอกสารต้นฉบับที่รองรับการพิสูจน์แต่ละอย่างเป็นสิ่งจำเป็น
- ใช้โมนาด LogicT และการจัดการสถานะ (State) ของ Haskell เพื่อติดตามรายการเอกสารที่จำเป็นและเส้นทางตรรกะในการพิสูจน์สัญชาติอังกฤษ
- ในความเป็นจริง HMPO มีแนวโน้มจะขอเส้นทางการพิสูจน์ที่ซับซ้อนที่สุดก่อน และเครื่องมืออัตโนมัติก็ยังถูกนำมาใช้อย่างล่าช้าเพราะข้อจำกัดของการตีความกฎหมายที่ซับซ้อน
บทนำ: มองการสมัครพาสปอร์ตเป็นเกม
- ช่วงหลังมานี้มีแนวโน้มเพิ่มขึ้นในการใช้การเขียนโปรแกรมเพื่อแก้เกมออนไลน์หรือเกมปริศนา และ Passport Application ของสหราชอาณาจักรก็ถูกนำมาจัดการด้วยแนวทางแบบนี้เช่นกัน
- Passport Application คือเกมแนว “ผจญภัยไขปริศนาสะสมเอกสาร” ที่ชาวอังกฤษเล่นกันทุก 10 ปี มีค่าใช้จ่ายราว £100 และมีดีไซน์แบบข้อความล้วนที่มินิมอลอย่างเคร่งครัด
- เป้าหมายของเกมนี้คือการรวบรวมเอกสารยืนยัน (artefacts) หลายชนิดผ่านหน่วยงานราชการต่าง ๆ เพื่อพิสูจน์ภายใต้เกณฑ์ทางกฎหมายที่ซับซ้อนว่า “ผู้สมัครคนนี้เป็นชาวอังกฤษ”
- รางวัลของเกมคือสมุดพาสปอร์ตหนึ่งเล่มและ “วันที่สามารถเล่นรอบถัดไปได้”
โครงสร้างและความยากของเกม
- เวอร์ชันออฟไลน์แบบกระดาษดำเนินการผ่านไปรษณีย์ลงทะเบียนและขั้นตอนการรับรอง โดยเอกสารที่ต้องรวบรวมในแต่ละขั้นจะมีคำอธิบายหรือระบุไว้ในรูปแบบตาราง
- ช่วงแรกของกระบวนการค่อนข้างง่าย แต่เมื่อเกมดำเนินไปก็จะมี “ไซด์เควสต์” และอุปสรรคหลายรูปแบบปรากฏขึ้น
- ตัวอย่าง: ขอให้คนรู้จักที่มีอาชีพบางประเภทช่วยยืนยันตัวตน, หาเอกสารแปลรับรองของเอกสารภาษาต่างประเทศ, เล่นแบบร่วมมือกันในครอบครัว, สำรวจขั้นตอนธุรการเฉพาะตัวของแต่ละหน่วยงานราชการ เป็นต้น
ประสบการณ์จริง: ท้าทายระดับ 'บุตรคนแรกที่เกิดในต่างประเทศ'
- ผู้เขียนรับบทแทนตัวเองเพื่อจัดการระดับความยาก 'เด็กคนแรกที่เกิดในต่างประเทศ' ของลูกสาวตัวเล็ก และคาดไว้ล่วงหน้าแล้วว่าน่าจะยากพอสมควรจากประสบการณ์ก่อนหน้า
- ภายหลังพบว่าครึ่งหนึ่งของเอกสารที่ถูกขอในช่วงแรกนั้นไม่จำเป็น และข้อกำหนดกับคำอธิบายเรื่องเอกสารถูกออกแบบมาอย่างคลุมเครือหรือชวนสับสนมาก
- ไม่สามารถสื่อสารกับเจ้าหน้าที่ผู้ตรวจพิจารณา (examiner) ได้โดยตรง และจะได้รับความช่วยเหลือแบบไม่เป็นทางการได้ผ่านทางเอเจนต์ตัวกลางให้คำปรึกษาเท่านั้น
- มีการขอเอกสารเพิ่มซ้ำ ๆ และบางครั้งถึงขั้นขอเอกสารที่ไม่มีอยู่จริง รวมถึงการขอสูติบัตร/ทะเบียนสมรสของบรรพบุรุษในครอบครัวที่พบได้ยาก ทำให้ความยากสูงขึ้นเรื่อย ๆ
ตรรกะของ HMPO: Bureaucratic Logic
- ตรรกะของการสมัครพาสปอร์ตสามารถมองได้ว่าเป็น Bureaucratic Logic (ตรรกะแบบราชการ) ที่ต่อยอดมาจาก Constructive Logic
- แทนที่จะพิสูจน์แบบง่าย ๆ ว่า “จริง/เท็จ” ผู้สมัครจะต้องส่งหลักฐานเอกสารต้นฉบับที่ตรงกับแต่ละกฎโดยตรง
- เนื่องจากไม่ยอมรับกฎ Excluded Middle จึงไม่สามารถพิสูจน์ด้วยเหตุผลว่า “ไม่ว่าสถานการณ์ไหน อย่างน้อยหนึ่งข้อก็ต้องจริง” ได้ และจำเป็นต้องเลือกเพียงเส้นทางเดียวแล้วส่งเอกสารตามทางนั้นเท่านั้น
- โดยเฉพาะอย่างยิ่ง “ความเป็นอังกฤษ” ขึ้นอยู่กับสัญชาติของพ่อแม่ ทำให้การขอเอกสารดำเนินไปแบบเรียกซ้ำตามโครงสร้างต้นไม้ครอบครัว
- กรณีฐาน: เกิดในสหราชอาณาจักรก่อนปี 1983, ได้สัญชาติโดยการแปลงสัญชาติ ฯลฯ ซึ่งเป็นกรณีที่ไม่ต้องใช้หลักฐานของพ่อแม่
สร้างโมเดลกฎด้วยโค้ด Haskell
- เพื่อวัตถุประสงค์ในการแยกโมดูลของกฎและทำให้การอนุมานเป็นอัตโนมัติ ผู้เขียนจึงสร้างต้นแบบตรรกะการสมัครด้วย Haskell (โดยเฉพาะการใช้โมนาด LogicT)
- มีการประกาศชนิดข้อมูลอย่าง Person/Document/Proof เพื่อสร้างโมเดลเส้นทางเอกสารพิสูจน์ที่หลากหลายตามแต่ละเงื่อนไข
- ฟังก์ชันพิสูจน์ความเป็น British จะสำรวจเส้นทางการพิสูจน์หลายแบบ (Set of Proofs) ที่เป็นไปได้ โดยอิงจาก input (ข้อมูลของแต่ละ person)
- จากต้นไม้ของ Proof จะคำนวณชุดเอกสารขั้นต่ำที่จำเป็น (Set of Set Document)
- ใช้การผสานกันของ StateT และ LogicT IO เพื่อทำคำถามตอบแบบอินเทอร์แอกทีฟและแชร์สถานะ โดยแตกแขนงและทำ backtracking ตาม “ข้อมูลที่รู้อยู่”
- ตรรกะการวิเคราะห์โครงสร้างสัญชาติอังกฤษ:
- เส้นทางเดียวสำหรับหลักฐานการแปลงสัญชาติ
- เส้นทางแบบมีเงื่อนไข (กรณีฐาน) สำหรับผู้ที่เกิดในสหราชอาณาจักรก่อนปี 1983
- การพิสูจน์แบบเรียกซ้ำผ่านพ่อแม่ (รวมถึงเงื่อนไขเพิ่มเติมอย่างการสมรสที่ชอบด้วยกฎหมาย)
- เพิ่มเส้นทางข้อยกเว้นสำหรับกรณีที่พ่อแม่เป็น BOTBD (British Otherwise Than By Descent)
- รองรับข้อยกเว้นอย่าง Crown Service ในโค้ดด้วย
ตัวอย่างการรันและเส้นทางการพิสูจน์
- ผ่าน ghci ระบบสามารถหาเส้นทางการพิสูจน์ (Proof) ได้ทั้งหมด 3 แบบโดยอัตโนมัติ ตาม input จริง เช่น สถานที่เกิดของผู้สมัครและสัญชาติของพ่อแม่
- สำหรับแต่ละเส้นทางการพิสูจน์ จะมีการสร้างรายการเอกสารที่ต้องใช้ (เช่น combination of certificates, marriage certificates เป็นต้น)
- พบว่าเส้นทางที่ซับซ้อนที่สุดจำเป็นต้องมีการพิสูจน์แบบเรียกซ้ำและการพิสูจน์ความสัมพันธ์ทางการสมรสที่ย้อนกลับไปถึงบรรพบุรุษ
อภิปรายและสรุป
- ในโลกความเป็นจริง HMPO ดูเหมือนจะจงใจขอเส้นทางการพิสูจน์ที่ซับซ้อนที่สุดก่อน และในกรณีที่มีความขัดแย้งทางกฎหมายจริงหรือข้อกำหนดยิบย่อย ก็จะอ้างอิงแนวทางแยกต่างหากหรือหลักการ "balance of probabilities"
- หากมีการใช้งานเครื่องมืออัตโนมัติอย่างแพร่หลาย ผู้สมัครก็น่าจะเข้าใจเส้นทางการพิสูจน์ของตัวเองและเอกสารที่จำเป็นได้ง่ายขึ้นมาก
- อย่างไรก็ตาม กฎหมายมีความละเอียดอ่อนและเปลี่ยนแปลงได้มาก จึงมีความเสี่ยงหากทำระบบอัตโนมัติแบบง่าย ๆ ที่ให้คอมพิวเตอร์ตัดสินเป็น yes/no verdict
- ขณะนี้ผู้เขียนกำลังพยายามพิสูจน์ผ่านเส้นทางที่สองและสามอยู่
สรุปโค้ดอ้างอิงและโครงสร้างเอกสาร
- โค้ด Haskell ฉบับเต็มดูได้ที่ GitHub
- สามารถดูรายละเอียดการเขียนตรรกะ Haskell เช่น ชนิดข้อมูลต่าง ๆ เส้นทางการพิสูจน์ โครงสร้างโมดูล และฟังก์ชันสำหรับตั้งคำถามได้
1 ความคิดเห็น
ความเห็นจาก Hacker News