อรรถศาสตร์เชิงการกำหนด (Denotational Semantics)

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

Definition

อรรถศาสตร์เชิงการกำหนดกำหนดวัตถุทางคณิตศาสตร์ (การกำหนดความหมาย) ให้กับแต่ละโปรแกรม ซึ่งถูกนิยามแบบองค์ประกอบจากความหมายของส่วนประกอบต่างๆ โดยมีการตีความการเรียกซ้ำผ่านจุดตรึงน้อยที่สุดในโดเมน

Scope

หัวข้อนี้ครอบคลุมแนวทางของ Scott-Strachey ซึ่งแต่ละส่วนของโปรแกรมจะแสดงถึงองค์ประกอบของโดเมนทางคณิตศาสตร์ โดยรวมถึงทฤษฎีโดเมน, อันดับบางส่วนสมบูรณ์ (complete partial orders), ฟังก์ชันต่อเนื่อง (continuous functions), และการตีความการเรียกซ้ำแบบจุดตรึงน้อยที่สุด (least-fixed-point interpretations of recursion) ตลอดจนภาวะนามธรรมสมบูรณ์ (full abstraction) ซึ่งเกี่ยวข้องกับความสอดคล้องกันระหว่างความหมายเชิงการกำหนดกับพฤติกรรมที่สังเกตได้

Core questions

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

Key theories

ทฤษฎีโดเมนและอรรถศาสตร์จุดตรึง

ทฤษฎีโดเมนของ Scott จัดหาโครงสร้างอันดับและฟังก์ชันต่อเนื่อง ซึ่งนิยามแบบเรียกซ้ำถูกตีความว่าเป็นจุดตรึงน้อยที่สุด เพื่อแก้ปัญหาการให้ความหมายแก่โปรแกรมที่อ้างอิงถึงตัวเอง

ภาวะนามธรรมสมบูรณ์

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

Clinical relevance

แบบจำลองเชิงการกำหนดให้การอ้างอิงที่แม่นยำและเป็นองค์ประกอบสำหรับความหมายของภาษา สนับสนุนการให้เหตุผลเกี่ยวกับการเทียบเท่าและการปรับปรุงประสิทธิภาพของโปรแกรม และให้ข้อมูลในการออกแบบคุณสมบัติเช่น การเรียกซ้ำและฟังก์ชันลำดับสูง (higher-order functions) ทฤษฎีโดเมนยังเชื่อมโยงภาษาโปรแกรมเข้ากับคณิตศาสตร์และตรรกะที่กว้างขึ้นด้วย

History

งานของ Strachey เกี่ยวกับคำอธิบายทางคณิตศาสตร์ของภาษาและการสร้างแบบจำลองโดเมนของ Scott ในปี 1969 ได้ริเริ่มอรรถศาสตร์เชิงการกำหนด ซึ่งได้รับการจัดรูปแบบในเอกสารของพวกเขาในปี 1971 ทฤษฎีโดเมนของ Scott พัฒนาขึ้นตลอดทศวรรษ 1970 และการวิเคราะห์ LCF ของ Plotkin ได้ทำให้ปัญหาภาวะนามธรรมสมบูรณ์ชัดเจนขึ้น ซึ่งเป็นแรงผลักดันให้เกิดการพัฒนาในภายหลัง เช่น อรรถศาสตร์เชิงเกม (game semantics)

Debates

ปัญหาภาวะนามธรรมสมบูรณ์

คำถามสำคัญคือแบบจำลองเชิงการกำหนดสามารถจับพฤติกรรมที่สังเกตได้ของภาษาได้อย่างแม่นยำหรือไม่ ไม่มากไปกว่าและไม่น้อยไปกว่านั้น แบบจำลองโดเมนแบบคลาสสิกไม่สามารถทำได้สำหรับภาษาลำดับสูงแบบลำดับ (higher-order sequential languages) ซึ่งกระตุ้นให้เกิดแบบจำลองทางเลือก

Key figures

• Dana Scott
• Christopher Strachey
• Gordon Plotkin
• Glynn Winskel

Seminal works

• scott1971
• scott1976
• plotkin1977
• winskel1993

Frequently asked questions

โดเมนในอรรถศาสตร์เชิงการกำหนดคืออะไร?

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

ภาวะนามธรรมสมบูรณ์คืออะไร?

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