ภาพประกอบทฤษฎีหมวดหมู่: ตรรกะ (2021)

 (abuseofnotation.github.io)
2 คะแนน โดย GN⁺ 2024-10-27 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • ตรรกะเริ่มจาก ประพจน์อะตอม ที่ยอมรับว่าเป็นจริง แล้วใช้ตัวดำเนินการอย่าง and, or, implies เพื่อสร้างประพจน์ที่ใหญ่ขึ้น และเช่นเดียวกับทฤษฎีหมวดหมู่ แก่นสำคัญคือ การประกอบ
  • ตรรกะแบบคลาสสิกตีความประพจน์เป็นค่า Boolean จริง/เท็จ และตีความตัวดำเนินการเชิงตรรกะเป็นฟังก์ชัน Boolean โดยใช้ตารางค่าความจริงเพื่อจัดการกับการปฏิเสธ การเชื่อมแบบและ การเชื่อมแบบหรือ การอิมพลาย และความสมมูล
  • การตีความแบบ BHK ของตรรกะแบบสัญชาตญาณนิยมมองประพจน์เป็นสิ่งที่มีบทพิสูจน์ โดยตีความ A ∧ B เป็นคู่ของบทพิสูจน์ และ A → B เป็นฟังก์ชันที่แปลงบทพิสูจน์ของ A ให้เป็นบทพิสูจน์ของ B
  • ในบางหมวดหมู่ วัตถุสอดคล้องกับ ประพจน์ และมอร์ฟิซึมสอดคล้องกับ บทพิสูจน์; ในเชิงลำดับ A ≤ B แทน A → B ในรูปของ preorder หรือ partial order
  • ตรรกะแบบสัญชาตญาณนิยมสอดคล้องในเชิงทฤษฎีลำดับกับ Heyting algebra และในเชิงทฤษฎีหมวดหมู่ทั่วไปกับ bicartesian closed category โดยการเชื่อมแบบและ การเชื่อมแบบหรือ จริง เท็จ และการอิมพลาย สอดคล้องกับ meet/join, terminal/initial และ exponential object ตามลำดับ

ตรรกะที่เริ่มจากประพจน์

  • ตรรกะว่าด้วยกฎเชิงรูปแบบที่สอดคล้องในตัวเองโดยไม่ขึ้นกับการสังเกต และเป็นระบบสำหรับสรุปหรือพิสูจน์ว่าเมื่อรู้อะไรบางอย่างแล้ว สิ่งอื่นใดเป็นจริง
  • ทฤษฎีทางคณิตศาสตร์อาจมองได้ว่าเป็นสิ่งที่เพิ่มนิยามเข้าไปบนตรรกะ
    • ทฤษฎีเซตสามารถนิยามได้โดยเพิ่มแนวคิดปฐมฐานเรื่อง ความเป็นสมาชิกของเซต ลงบนสัจพจน์ตรรกะมาตรฐาน
  • การเริ่มต้นตรรกะต้องมีเซตเริ่มต้นของประพจน์ที่ยอมรับว่าเป็นจริงหรือเท็จ
    • สิ่งนี้เรียกว่า premises, ประพจน์อะตอม, หรือ primary proposition
  • ประพจน์ตั้งแต่สองข้อขึ้นไปสามารถรวมเป็นประพจน์ประกอบหนึ่งข้อได้ด้วย ตัวดำเนินการเชิงตรรกะ อย่าง and, or, implies/entails
    • ∧ คือ and
    • ∨ คือ or
    • → หมายถึง follows หรือการอิมพลาย
  • ประพจน์ประกอบก็สามารถกลับไปประกอบกับประพจน์อื่นได้อีกเช่นเดียวกับประพจน์อะตอม

Modus ponens และสัจนิรันดร์

  • Modus ponens เป็นรูปแบบตรรกะโบราณที่ว่า ถ้า A เป็นจริง และ A → B เป็นจริง ก็ย่อมได้ว่า B เป็นจริง
    • รูปแบบคือ (A ∧ (A ⇒ B)) → B
    • อาจเขียนเป็นตัวอย่างได้เช่น “Socrates เป็นมนุษย์ และถ้ามนุษย์ย่อมต้องตาย ดังนั้น Socrates ต้องตาย”
  • ตรรกะไม่ได้สนใจแค่ตัวดำเนินการเดี่ยว ๆ แต่ยังสนใจการผสมและความสัมพันธ์ระหว่างตัวดำเนินการเชิงตรรกะหลายตัว
    • ความสัมพันธ์ระหว่าง and กับ implies ปรากฏชัดใน modus ponens
    • กฎแจกแจงของ and และ or ก็เป็นหัวข้อสำคัญเช่นกัน
  • สัจนิรันดร์ คือประพจน์ที่เป็นจริงเสมอไม่ว่าค่าจริง/เท็จของประพจน์องค์ประกอบจะเป็นอย่างไร
    • Modus ponens เป็นจริงเสมอไม่ว่า A และ B จะจริงหรือเท็จก็ตาม
    • ประพจน์ที่เป็นเท็จเสมอเรียกว่า contradiction
    • เมื่อติด not ให้สัจนิรันดร์จะได้ contradiction และเมื่อติด not ให้ contradiction จะได้สัจนิรันดร์
  • ประพจน์ที่ค่าจริงหรือเท็จเปลี่ยนไปตามค่าเรียกว่า contingent statement ซึ่งอยู่นอกความสนใจหลักของตรรกะ
  • สัจนิรันดร์ที่ง่ายที่สุดคือ กฎเอกลักษณ์ ที่ว่าประพจน์แต่ละข้ออิมพลายตัวมันเอง

Axiom schema และระบบตรรกะ

  • สัจนิรันดร์เป็นฐานของ axiom schema และกฎการอนุมาน
  • axiom schema คือสูตรที่มีตัวแทนตำแหน่ง ซึ่งสามารถแทนที่ด้วยประพจน์เพื่อสร้างประพจน์เฉพาะได้
    • หากลบสีหรือประพจน์เฉพาะออกจาก modus ponens ก็จะเหลือโครงสร้างทั่วไป
    • สามารถใส่ประพจน์อะตอมหรือประพจน์ประกอบลงในโครงสร้างนั้นเพื่อสร้างประพจน์ modus ponens แบบเฉพาะได้
  • กฎการอนุมานสามารถเขียนใช้งานได้เกือบแบบเดียวกับ axiom schema และ axiom schema ก็ใช้ได้คล้ายกฎการอนุมาน
  • สัจนิรันดร์ทุกข้อสามารถใช้เป็น axiom schema ได้
  • ระบบตรรกะหรือระบบเชิงรูปแบบคือชุดของ axiom schema และกฎการอนุมาน ซึ่งเมื่อนำไปใช้แล้วจะสร้างประพจน์ที่เป็นไปได้ทั้งหมด
    • มีการยกตัวอย่างระบบที่ประกอบด้วย axiom schema ห้าข้อและกฎการอนุมาน modus ponens
    • ข้อเท็จจริงที่ว่าระบบตรรกะแบบนี้สมบูรณ์เชื่อมโยงกับ ทฤษฎีบทความสมบูรณ์ของ Gödel

การตีความแบบฟังก์ชันค่าความจริงของตรรกะแบบคลาสสิก

  • ตรรกะแบบคลาสสิก ตั้งอยู่บนทวิลักษณ์ที่ว่าประพจน์ต้องเป็นจริงหรือเท็จอย่างใดอย่างหนึ่ง
  • ในการตีความแบบคลาสสิก ประพจน์และตัวดำเนินการถูกนิยามดังนี้
    • ประพจน์คือสิ่งที่เป็นจริงหรือเท็จได้เหมือนค่า Boolean
    • ตัวดำเนินการเชิงตรรกะคือฟังก์ชันที่รับค่า Boolean หนึ่งค่าหรือมากกว่าแล้วคืนค่า Boolean
  • การปฏิเสธ ¬p เป็นตัวดำเนินการหนึ่งหน่วย เปลี่ยนค่าจริงเป็นเท็จ และเปลี่ยนค่าเท็จเป็นจริง
    • เรื่องเดียวกันนี้สามารถแสดงด้วย ตารางค่าความจริง
    • การตัดการปฏิเสธซ้อนสองชั้นพิสูจน์ได้จากการที่เมื่อติดปฏิเสธสองครั้งจะกลับไปได้ค่าเดิม
  • and รับค่า Boolean สองค่าและให้จริงก็ต่อเมื่อทั้งคู่จริง
    • p ∧ q → p
    • p ∧ q → q
  • or ให้จริงเมื่อค่า Boolean อย่างน้อยหนึ่งค่าจริง
    • p → p ∨ q
    • q → p ∨ q
  • implies หรือ material condition เขียนเป็น p → q และจะเป็นเท็จเฉพาะเมื่อ p จริงแต่ q เท็จ
    • ในตรรกะแบบคลาสสิก p → q เทียบเท่ากับกรณีที่ ¬p ∨ q เป็นจริง
  • if and only if หรือ iff จะเป็นจริงเมื่อประพจน์ทั้งสองมีค่าเดียวกัน
    • P ↔ Q สมมูลกับ P → Q ∧ Q → P
  • นอกจากตารางค่าความจริงแล้ว ยังสามารถพิสูจน์ความสมมูลของ p → q และ ¬p ∨ q ได้ด้วยสัจพจน์และกฎการอนุมาน
    • การพิสูจน์ความสมมูลอย่างสมบูรณ์ต้องมีการพิสูจน์ทั้งสองทิศทาง

ตรรกะแบบสัญชาตญาณนิยมและการตีความแบบ BHK

  • ตรรกะแบบสัญชาตญาณนิยม มองบทพิสูจน์ไม่ใช่การค้นพบความจริงสากล แต่เป็นการสร้างประกอบขึ้น
  • ในมุมมองนี้ ไม่อาจใช้ทวิลักษณ์ที่ว่าทุกประพจน์ต้องจริงหรือเท็จเสมอไปได้
    • บางประพจน์อาจพิสูจน์ไม่ได้ ไม่ใช่เพราะมันเป็นเท็จ แต่เพราะอยู่นอกขอบเขตของระบบตรรกะที่กำหนด
    • ข้อคาดการณ์จำนวนเฉพาะแฝดมักถูกยกเป็นตัวอย่างของกรณีนี้
  • ใน การตีความแบบ Brouwer–Heyting–Kolmogorov(BHK) จุดศูนย์กลางอยู่ที่บทพิสูจน์มากกว่าตัวประพจน์
    • ประพจน์คือสิ่งที่มีบทพิสูจน์
    • ตัวดำเนินการเชิงตรรกะคือการประกอบที่สร้างบทพิสูจน์จากบทพิสูจน์อื่น
  • บทพิสูจน์ของ A ∧ B คือ คู่ ที่ประกอบด้วยบทพิสูจน์ของ A และบทพิสูจน์ของ B หรือก็คือ product
  • A → B หมายถึงมีฟังก์ชันที่แปลงบทพิสูจน์ของ A ให้เป็นบทพิสูจน์ของ B
    • เซตของบทพิสูจน์ของ A → B แทนได้ด้วยเซตของฟังก์ชันจาก A ไป B หรือก็คือ hom-set
    • ถ้าเซตนี้ว่าง ก็ไม่มีวิธีแปลงบทพิสูจน์ของ A ให้เป็นบทพิสูจน์ของ B
  • ในการตีความแบบ BHK ไม่มีตัวดำเนินการ iff แยกต่างหาก แต่มีลูกศร
    • เมื่อมีฟังก์ชันจาก A ไป B และจาก B ไป A ประพจน์ทั้งสองจะถูกมองว่าเทียบเท่ากัน
    • ในมุมมองแบบเซต นั่นคือสถานการณ์ที่เซตของบทพิสูจน์ของสองประพจน์เป็น isomorphic กัน
  • การปฏิเสธไม่ได้หมายถึงแค่ไม่มีบทพิสูจน์ แต่ต้องแสดงให้เห็นว่าถ้าสมมติว่า A เป็นจริงแล้วจะนำไปสู่ contradiction
    • ⊥ ทำหน้าที่เป็นบทพิสูจน์ของสูตรที่ไม่มีบทพิสูจน์ หรือก็คือ False หรือ bottom value
    • ใน BHK, ¬A อ่านว่า A → ⊥
    • ในทฤษฎีเซต ⊥ แทนด้วยเซตว่าง

มองตรรกะเป็นหมวดหมู่

  • การตีความแบบ BHK ให้มุมมองระดับสูงสำหรับตีความตรรกะด้วยทฤษฎีหมวดหมู่
  • บางหมวดหมู่สามารถมองได้เหมือนระบบตรรกะ
    • วัตถุคือ ประพจน์
    • มอร์ฟิซึมคือ บทพิสูจน์
  • ไม่ใช่ทุกหมวดหมู่จะเป็นระบบตรรกะได้ และต้องมีเงื่อนไขที่ทำให้มีวัตถุที่สอดคล้องกับประพจน์ตรรกะที่ใช้ได้ และไม่มีวัตถุที่สอดคล้องกับประพจน์ที่ใช้ไม่ได้
  • หมวดหมู่ที่ตรงตามเงื่อนไขนั้นเรียกว่า bicartesian closed category
  • ในกรณีอย่างง่าย อาจเริ่มดูจากลำดับ(order)ก่อน ซึ่งระบบตรรกะกับเซตของประพจน์อะตอมจะก่อเป็นหมวดหมู่หนึ่ง
    • ถ้าวิธีจาก A ไป B มีได้เพียงหนึ่งวิธี หรือไม่นับความแตกต่างระหว่างวิธีเหล่านั้น ก็จะได้ preorder
    • ถ้ามองประพจน์ที่ตามกันและกันว่าเทียบเท่ากัน ก็จะได้ partial order
    • A ≤ B หมายถึง A → B
  • ใน Hasse diagram ถ้า A อยู่ใต้ B ก็หมายความว่า A → B เป็นจริง

ความสอดคล้องเชิงทฤษฎีลำดับของตัวดำเนินการเชิงตรรกะ

  • and และ or ในตรรกะปรากฏเป็น product และ sum ในการตีความแบบ BHK และในเชิงทฤษฎีลำดับจะสอดคล้องกับ meet และ join
  • หากจะเป็นระบบตรรกะได้ ลำดับนั้นต้องสามารถรวมประพจน์คู่ใด ๆ ด้วย and หรือ or ได้ ดังนั้นลำดับต้องมี meet และ join สำหรับทุกองค์ประกอบ
    • ลำดับแบบนี้เรียกว่า lattice
  • กฎสำคัญระหว่าง and และ or คือการแจกแจง
    • ถ้าสำหรับทุก A, B, C มี A ∧ (B ∨ C) ≅ (A ∧ B) ∨ (A ∧ C) ก็จะเป็น distributive lattice
  • เพื่อแทนตรรกะแบบสัญชาตญาณนิยม lattice ต้องมีองค์ประกอบที่สอดคล้องกับ True และ False ด้วย
    • False เขียนเป็น ⊥ และเชื่อมโยงกับ หลักการระเบิด ที่ว่าถ้ามีบทพิสูจน์ของ False ก็สามารถพิสูจน์ประพจน์ใดก็ได้
    • True เขียนเป็น ⊤ และเป็นสิ่งที่ตามมาจากทุกประพจน์ แต่ในตัวมันเองไม่ได้ให้สาระสำคัญเพิ่มเติม
  • ในลำดับ True และ False คือ greatest object และ least object ตามลำดับ
    • ในศัพท์ของทฤษฎีหมวดหมู่จะสอดคล้องกับ terminal object และ initial object
    • lattice ที่มีทั้ง least และ greatest เรียกว่า bounded lattice

วัตถุอิมพลายและวัตถุเอ็กซ์โปเนนเชียล

  • lattice ที่ใช้แทนระบบตรรกะต้องมี วัตถุอิมพลาย สำหรับแต่ละคู่ A, B เพื่อแทนประพจน์ที่ว่า A อิมพลาย B
  • วัตถุนี้นิยามผ่านโครงสร้างของ modus ponens
    • ต้องมี A ∧ (A ⇒ B) → B
  • แค่เงื่อนไขนี้อย่างเดียวยังไม่พอ
    • วัตถุอื่นอย่าง A ⇒ B ∧ C หรือ A ⇒ B ∧ C ∧ D ก็อาจใส่แทนที่ตรงนี้ได้เช่นกัน
    • A ⇒ B ที่แท้จริงคือวัตถุที่ใหญ่ที่สุดในบรรดาวัตถุ X ที่ทำให้ A ∧ X → B เป็นจริง
  • ในเชิงทฤษฎีลำดับ A ⇒ B เรียกว่า exponential element หรือ relative pseudo-complement
    • คือ X ที่ใหญ่ที่สุดซึ่งทำให้ A ∧ X ≤ B
  • ในเชิงตรรกะ X ที่ไม่สาระเกินจำเป็นและทำให้ A ∧ X → B เป็นจริง ก็คือ ประพจน์อิมพลาย A ⇒ B
  • ในเชิงทฤษฎีหมวดหมู่ นิยามเป็น exponential object หรือ internal homomorphism object
    • ต้องมีมอร์ฟิซึม A × X → B
    • และต้องมีมอร์ฟิซึมเอกลักษณ์เพียงหนึ่งเดียวจากวัตถุผู้สมัครอื่นที่มีสมบัติเดียวกันไปสู่วัตถุเอ็กซ์โปเนนเชียลจริง
  • นิยามของวัตถุอิมพลายนี้สอดคล้องกับตรรกะแบบสัญชาตญาณนิยม
    • ในตรรกะแบบคลาสสิก A ⇒ B ยุบรูปได้เป็น ¬A ∨ B เพราะกฎ excluded middle
  • เช่นเดียวกับ meet, join และวัตถุอิมพลาย A ⇒ B ก็ถูกนิยามได้เอกลักษณ์ถึงระดับ isomorphism

Heyting algebra และ bicartesian closed category

  • ตรรกะแบบสัญชาตญาณนิยมประกอบด้วย True, False, and, or, implies
  • เมื่อเขียนในรูปของลำดับ จะได้ Heyting algebra
    • มี join และ meet
    • มี greatest และ least object
    • มีวัตถุอิมพลาย
  • ระบบตรรกะแบบสัญชาตญาณนิยมสามารถมองเป็น Heyting algebra ได้
    • and และ or คือ meet และ join
    • True และ False คือ greatest และ least object
    • implies คือ exponential object
  • เมื่อนำคำนิยามเดียวกันไปปรับให้เข้ากับหมวดหมู่ทั่วไป ก็จะได้ bicartesian closed category
    • มี product และ coproduct
    • มี initial object และ terminal object
    • มี exponential object
  • ระบบตรรกะแบบสัญชาตญาณนิยมสามารถมองเป็น bicartesian closed category ได้เช่นกัน
    • and และ or คือ product และ coproduct
    • True และ False คือ terminal object และ initial object
    • implies คือ exponential object
  • lattice ที่เป็นไปตามตรรกะแบบคลาสสิกต้องเป็น complemented เพิ่มจากการเป็น bounded และ distributive
    • สำหรับแต่ละประพจน์ A จะมี ¬A เฉพาะตัวที่ทำให้ A ∨ ¬A = 1, A ∧ ¬A = 0
    • lattice แบบนี้เรียกว่า Boolean algebra

บทพิสูจน์อย่างง่ายในมุมมองตรรกะเชิงหมวดหมู่

  • A ∨ ⊤ ≅ ⊤ ตามมาทันทีจากนิยามของ join
    • join คือ upper bound ต่ำสุดที่มากกว่าหรือเท่ากับวัตถุทั้งสอง
    • วัตถุที่มากกว่าหรือเท่ากับ ⊤ มีเพียง ⊤ เองเท่านั้น ดังนั้น join ของ A กับ ⊤ จึงเป็น ⊤
    • ในเชิงตรรกะ นี่คือสัจนิรันดร์ “A ใด ๆ หรือ True ย่อมเป็น True”
  • ถ้ามี A → B ก็จะได้ A ∨ B = B
    • เมื่อวัตถุหนึ่งอยู่สูงกว่าอีกวัตถุหนึ่ง join จะเป็นวัตถุที่อยู่สูงกว่า
    • มองได้ว่าเป็นการทำให้ A ∨ ⊤ = ⊤ เป็นกรณีทั่วไป
    • เพราะสำหรับทุกวัตถุ A จะมี A → ⊤ เป็นจริงเสมอ
  • กฎเอกลักษณ์พิสูจน์ได้ผ่านวัตถุอิมพลายเช่นกัน
    • A ⇒ A คือวัตถุที่ใหญ่ที่สุดซึ่งทำให้ A ∧ X → A เป็นจริง
    • เงื่อนไขนี้เป็นจริงสำหรับทุก X ดังนั้นจึงได้วัตถุที่ใหญ่ที่สุดคือ ⊤
    • เพราะฉะนั้น A → A จึงเป็นจริงเสมอ
  • ถ้า A เป็น semantic consequence ของ B ในทุกโมเดล หรือ A ⊨ B ก็จะได้ว่า A ⇒ B สอดคล้องกับ ⊤ ด้วย
    • เพราะ A เองก็อิมพลาย B อยู่แล้ว จึงทำให้ A ∧ X → B เป็นจริงสำหรับทุก X
    • สิ่งนี้เรียกอีกอย่างว่า deduction theorem

สร้างตรรกะด้วย Free Heyting algebra

  • หากต้องการทำตรรกะ ต้องเริ่มจากเลือก ประพจน์อะตอม ที่จะใช้ตามขอบเขตของปัญหาก่อน
  • ถ้าตรรกะที่เลือกเป็นตรรกะแบบสัญชาตญาณนิยม ก็ต้องวาดกราฟของประพจน์ประกอบอย่าง A ∧ B, A ∨ B สำหรับทุก A, B
  • เนื่องจากต้องรวมการประกอบของประพจน์ประกอบเหล่านั้นเข้าไปอีก รายการทั้งหมดจึงไม่มีที่สิ้นสุด
  • การตรวจว่าประพจน์หนึ่งอิมพลายอีกประพจน์หนึ่งหรือไม่ ทำได้โดยตามเส้นทางของลูกศรที่ออกจากประพจน์ต้นทาง
  • การทำตรรกะคือกระบวนการหาเส้นทางจากสิ่งที่รู้อยู่แล้วไปยังสิ่งที่ต้องการพิสูจน์ หรือจัดการบทพิสูจน์ที่มีอยู่เพื่อประกอบบทพิสูจน์ใหม่
  • ในตรรกะแบบสัญชาตญาณนิยม โดยทั่วไปการพิสูจน์ว่าข้อเท็จจริงบางอย่างเข้าถึงไม่ได้จากสัจพจน์ หรือก็คือพิสูจน์ไม่ได้ มักทำได้ยาก

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2024-10-27
ความคิดเห็นบน Hacker News

  • หน้านี้ยอดเยี่ยมจริง ๆ และผมเคยเจอมันหลายครั้งตอนศึกษาหัวข้อที่เกี่ยวข้อง
    ถึงอย่างนั้น ผมยังอยากโหวตให้เรียนจาก Milewski มากกว่า การเรียนเรื่องนี้เป็นเส้นทางหนึ่ง และผู้เขียน ct-illustrated ดูเหมือนยังอยู่ระหว่างทาง
    Milewski เป็นคนที่เดินเส้นทางนั้นมาแล้วหลายรอบ หนังสือและบล็อกของเขาจึงเป็นจุดเริ่มต้นที่ดี
    https://github.com/hmemcpy/milewski-ctfp-pdf Book
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • ผมอ่านสิบกว่าบทแรกของ Milewski แล้ว ช่วงไม่กี่บทแรกดีมากจริง ๆ แต่สไตล์การเขียนที่ไม่ให้ นิยามและสัญกรณ์ที่แม่นยำ ทำให้ยิ่งอ่านยิ่งหงุดหงิด
      ดูเหมือนเขามองว่าถ้าเขียนเป็นร้อยแก้วเบา ๆ และไม่แม่นยำ อะไรก็จะเข้าใจง่ายขึ้น แต่ผลคือแทบใช้เป็นหนังสืออ้างอิงไม่ได้เลย
      ไม่ใช่อย่างนั้นเลย¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • ผมไม่เข้าใจว่า bartoszmilewski กำลังพูดอะไร หนังสือเล่มนั้นเลยดูไม่มีประโยชน์สำหรับผม
      แต่ที่ทำงาน ผมใช้ทฤษฎีหมวดหมู่กับ domain model ทั้งหมดของผมอยู่

  • เคยมีการคุยกันแล้วที่ URL อื่นก่อนหน้านี้
    https://news.ycombinator.com/item?id=28660131 (2 ความคิดเห็น)
    https://news.ycombinator.com/item?id=28660157 (112 ความคิดเห็น)

  • ช่วงต้นของหนังสือ ผมเจอประโยคเท่ ๆ ตอนเปรียบเทียบคณิตศาสตร์กับวิทยาศาสตร์หรือวิศวกรรม
    “ด้วยเหตุนี้ นักคณิตศาสตร์จึงอยู่ในสถานะที่แปลก และอาจเรียกได้ว่าเป็นเอกลักษณ์ คือพวกเขาต้องคอยปกป้องสิ่งที่ทำอยู่เสมอในแง่คุณค่าต่อสาขาวิชาอื่น ๆ ขอเน้นอีกครั้งว่า หากเป็นสาขาวิชาอื่นใด เรื่องแบบนี้คงถูกมองว่าเหลวไหล”
    นี่เป็นแนวคิดที่ใครก็ตามที่เคยเรียนสาขาซึ่งไม่ได้นำไปสู่ผลลัพธ์ที่ทำเงินได้โดยตรงย่อมเข้าใจ และก็ดีใจที่ได้ยินว่าคนที่มีพรสวรรค์ด้านตัวเลขก็ต้องสู้กับ มีดโกนของ Milton Friedman เช่นกัน

    • ถ้าอย่างนั้น ก็นับว่าโชคดีที่โปรเจกต์จำนวนมากใน “cultural studies” ได้รับเงินทุนโดยตรงจาก กระทรวงกลาโหมและกระทรวงการต่างประเทศของสหรัฐฯ จริง ๆ
      ทุกวันนี้ งานวิจัย “หลังอาณานิคมนิยม” ทั้งหมดก็เป็นแค่แบ็กเอนด์ของซอฟต์พาวเวอร์สหรัฐฯ และถ้าเกิดสงครามขึ้น ก็คงเป็นแบ็กเอนด์ของฮาร์ดพาวเวอร์ด้วย

  • ถ้าวงกลมด้านในถูกจัดให้อยู่กึ่งกลางแนวตั้งเสมอ แผนภาพแบบ วงกลมซ้อนวงกลม จะไม่ทนเมื่อขนาดขยายขึ้น

  • มีเรื่องราวความสำเร็จไหมที่ใช้ทฤษฎีหมวดหมู่แก้ปัญหา CS/SWE ได้อย่างมีประโยชน์ โดยเป็นปัญหาที่แก้ไม่ได้หากไม่มีทฤษฎีหมวดหมู่? Monad ไม่นับ เพราะถ้าสถานการณ์ต้องการก็จะถูกคิดขึ้นเองตามธรรมชาติ
    ผมเรียนมันอยู่ 1 ปีในบัณฑิตวิทยาลัย แต่สุดท้ายก็ยอมแพ้

    • ไม่มีปัญหาใดที่ไม่สามารถโมเดลได้หากไม่มีทฤษฎีหมวดหมู่
      หนึ่งในทฤษฎีบทพื้นฐานที่สุดของทฤษฎีหมวดหมู่คือ บทช่วยของ Yoneda ซึ่งบอกโดยตรงว่าปัญหาใด ๆ ที่แสดงในภาษาของหมวดหมู่สามารถแปลเป็นภาษาของเซตและฟังก์ชันได้ เช่นเดียวกับวัตถุทางคณิตศาสตร์ใด ๆ ที่นิยามด้วยเซต ดังนั้นชื่อสามารถถูกแทนด้วยนิยามได้เสมอ
      สิ่งที่ภาษาทฤษฎีหมวดหมู่มีส่วนช่วยต่อกรอบโดยนัยของทฤษฎีหนึ่ง ๆ ไม่อาจมากไปกว่านิยามของ “หมวดหมู่” เอง และนิยามนั้นก็เล็กมาก คล้ายกับถามว่าทำไมต้องใช้กรุ๊ป ในเมื่อ “การดำเนินการบนเซตที่มีสมบัติการเปลี่ยนหมู่ การปิด เอกลักษณ์ และอินเวอร์ส” เข้าถึงง่ายกว่า
      พีชคณิตนามธรรมตั้งอยู่บนไลบรารีของนิยามที่ชี้ไปยังชนิดของการดำเนินการบนเซตซึ่งเรียบง่ายพอจะพบได้ทั่วไป เครื่องมือหรือเทคนิคไม่ใช่สิ่งที่คุณจะหาเจอได้ภายในนิยาม
      ริง เวกเตอร์สเปซ และมอดูลมักถูกยอมรับได้ทันทีในตัวมันเอง แต่พอเป็นหมวดหมู่กลับแบ่งคนออกเป็นฝ่ายเชื่อกับไม่เชื่อ ผมสงสัยว่าทำไมถึงเป็นแบบนั้น
    • ตัวอย่างที่ใกล้ที่สุดเท่าที่ผมรู้คือผลงาน UMAP
      ตอนสัมภาษณ์ Leland McInnes เขาอธิบายอย่างละเอียดว่าทฤษฎีหมวดหมู่มีบทบาทมากในการเชื่อมหลายจุดเข้าด้วยกัน แม้ว่าจะไม่ได้จำเป็นต่อโค้ดจริงของผลลัพธ์สุดท้ายก็ตาม
      เมื่อดูระดับการปรับปรุงเมื่อเทียบกับเทคนิคล้ำสมัยก่อนหน้าอย่าง t-SNE นี่เป็นตัวอย่างเดียวที่ทำให้ผมต้องคิดใหม่กับคำวิจารณ์ของตัวเองต่อวิธีที่เราพูดถึงทฤษฎีหมวดหมู่ในซอฟต์แวร์
      https://arxiv.org/abs/1802.03426
    • คล้ายกับถามว่า “มีเรื่องราวความสำเร็จที่ใช้รถยนต์ไปยังที่ที่เดินไปไม่ได้ไหม?”
      ทฤษฎีหมวดหมู่ เป็นทั้งภาษาและเครื่องมือ ดังนั้นสิ่งที่พูดได้ด้วยภาษาของทฤษฎีหมวดหมู่ก็พูดได้ด้วยภาษาอื่นเช่นกัน
      เหมือนรถยนต์ ถ้าคุณเรียนรู้วิธีขับ และสิ่งนี้มีเส้นโค้งการเรียนรู้ที่ชันมาก คุณก็ไปได้เร็วขึ้น โดยหลักการแล้ว ไม่มีอะไรที่เดินไปไม่ได้โดยไม่เอ่ยถึงแนวคิดทฤษฎีหมวดหมู่อย่างชัดเจน
    • เมื่อปรับสิ่งที่เข้าใจอยู่แล้วให้อยู่ในกรอบที่ทั่วไปกว่า คุณจะเห็นชัดขึ้นว่ามันหมายถึงอะไรจริง ๆ และแยกสาระสำคัญออกจากรายละเอียดรก ๆ ได้
      เท่าที่ผมเข้าใจอย่างจำกัดมาก ๆ การระบุลักษณะของวัตถุด้วย สมบัติสากล เป็นส่วนสำคัญของทฤษฎีหมวดหมู่
      ประโยชน์เชิงปฏิบัติอีกอย่างของทฤษฎีหมวดหมู่คือมันให้ ภาษากลาง สำหรับให้นักวิทยาการคอมพิวเตอร์ นักคณิตศาสตร์ และนักฟิสิกส์คุยกัน หากทุกคนเรียกแพตเทิร์นเดียวกันด้วยชื่อต่างกันและนิยามที่เข้ากันไม่ได้เล็กน้อย การทำงานร่วมกันก็ไม่ง่าย
    • Topos Institute กำลังสร้างซอฟต์แวร์ใหม่ที่หวังว่าจะดูโปร่งใสขึ้นมากสำหรับคนที่ยังไม่ได้ดื่ม Kool-Aid ของทฤษฎีหมวดหมู่
      พรีอัลฟาปัจจุบันใช้หลัก ๆ สำหรับ การทำโมเดลพลวัตของระบบ แต่ผมมองว่ารากฐานเชิงทฤษฎีหมวดหมู่เป็นสิ่งจำเป็นต่อขอบเขตงานที่ตั้งเป้าไว้ ยินดีมากที่จะได้ฟังความคิดของทุกคน
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • ผมคิดว่าทฤษฎีหมวดหมู่มีประโยชน์ แต่ยังไม่น่าจะใช่ใน computing
    ถ้าไม่มีเรื่องที่จำเป็นต้องใช้จริง ๆ มันก็ย่อมรู้สึกยาก คุณจำเป็นต้องเข้าใจสมบัติสากล ฟังก์เตอร์ adjoint และบทช่วยของ Yoneda จริง ๆ หรือไม่? ถ้าไม่จำเป็น คุณก็จะลำบากในการเรียนว่ามันคืออะไร
    ที่น่าสนใจคือประสบการณ์ด้าน functional programming ช่วยให้เข้าใจทฤษฎีหมวดหมู่ แต่ในทางกลับกันไม่ค่อยเท่าไร ตัวอย่างเช่น parametric polymorphism ให้สัญชาตญาณเกี่ยวกับ natural transformation และ natural transformation ก็เป็นหัวใจของทุกการประยุกต์ใช้ทฤษฎีหมวดหมู่
    การประยุกต์ใช้ทฤษฎีหมวดหมู่ที่น่าเชื่อถือนั้นเป็นเชิงคณิตศาสตร์มาก พบได้ใน algebraic topology, representation theory, algebraic geometry และตรรกะแบบไม่คลาสสิก

  • มีข้อผิดพลาด
    “modus ponens เป็นประพจน์ที่ประกอบด้วยอีกสองประพจน์ ซึ่งในที่นี้ระบุเป็น A และ B และบอกว่า หากประพจน์ A เป็นจริง และ A --> B ก็เป็นจริงด้วย กล่าวคือ A อิมพลาย B แล้ว B ก็เป็นจริงด้วย ตัวอย่างเช่น ถ้าเรารู้ว่า ‘โสเครตีสเป็นมนุษย์’ และ ‘มนุษย์ตายได้’ เราก็รู้ด้วยว่า ‘โสเครตีสตายได้’”
    ตัวอย่างนี้ไม่ใช่กรณีของ modus ponens ซึ่งเป็นกฎของ ตรรกะเชิงประพจน์ แต่เป็น categorical syllogism ที่ต้องใช้ตรรกะภาคแสดง

  • ที่นี่บอกว่า “ตรรกะคือวิทยาศาสตร์ของสิ่งที่เป็นไปได้” แต่ตรรกะควรเป็น วิทยาศาสตร์ของสิ่งที่แน่นอน ไม่ใช่หรือ?
    ผมคิดว่าแก่นของมันคือการทำให้เราบอกได้อย่างแน่นอนว่าอะไร valid หรือไม่ valid

  • สัญกรณ์แบบแผนภาพน่าสนใจ
    ผู้เขียนเสนอ rules of inference สำหรับ การแปลงแผนภาพที่รักษาความจริง ด้วยไหม?