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

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

บางทีการจุติอย่างเป็นทางการครั้งแรกของความหมายเชิงปฏิบัติการอาจเป็นการใช้แคลคูลัสแลมบ์ดาเพื่อกำหนดความหมายของLisp [ ^{1 ]}เครื่องจักรนามธรรมในแบบฉบับของเครื่องจักร SECDก็มีความเกี่ยวข้องอย่างใกล้ชิดเช่น ^กัน

แนวคิดเรื่องความหมายเชิงปฏิบัติการ (operational semantics) ถูกนำมาใช้เป็นครั้งแรกในการกำหนดความหมายของAlgol 68ข้อความต่อไปนี้เป็นข้อความที่ยกมาจากรายงาน ALGOL 68 ฉบับปรับปรุง:

ความหมายของโปรแกรมในภาษาที่เข้มงวดนั้นอธิบายได้โดยใช้คอมพิวเตอร์สมมติซึ่งดำเนินการชุดการกระทำที่ประกอบขึ้นเป็นการประมวลผลของโปรแกรมนั้น ( Algol68 , ส่วนที่ 2)

การใช้คำว่า "ความหมายเชิงปฏิบัติการ" ในความหมายปัจจุบันเป็นครั้งแรกนั้น มีที่มาจาก Dana Scott ( Plotkin04 ) ต่อไปนี้เป็นข้อความที่ยกมาจากบทความสำคัญของ Scott เกี่ยวกับความหมายเชิงรูปธรรม ซึ่งเขากล่าวถึงแง่มุม "เชิงปฏิบัติการ" ของความหมาย

การมุ่งเป้าไปที่แนวทางที่ 'เป็นนามธรรม' และ 'ชัดเจน' มากขึ้นในด้านความหมายนั้นเป็นเรื่องที่ดี แต่ถ้าแผนนั้นจะได้ผลดี ก็ต้องไม่ละเลยแง่มุมการดำเนินงานโดยสิ้นเชิง ( Scott70 )

Gordon Plotkinได้นำเสนอความหมายเชิงปฏิบัติการเชิงโครงสร้างMatthias Felleisenและ Robert Hieb ได้นำเสนอความหมายเชิงการลดทอน^{[ 2 ]}และGilles Kahnได้นำเสนอความหมายเชิงธรรมชาติ

ความหมายเชิงปฏิบัติการเชิงโครงสร้าง (SOS หรือเรียกอีกอย่างว่าความหมายเชิงปฏิบัติการแบบมีโครงสร้างหรือความหมายแบบขั้นตอนเล็ก ) ได้รับการแนะนำโดยGordon Plotkinใน ( Plotkin81 ) ในฐานะวิธีการเชิงตรรกะในการกำหนดความหมายเชิงปฏิบัติการ แนวคิดพื้นฐานเบื้องหลัง SOS คือการกำหนดพฤติกรรมของโปรแกรมในแง่ของพฤติกรรมของส่วนประกอบต่างๆ จึงให้มุมมองเชิงโครงสร้าง กล่าวคือ เน้นไวยากรณ์และอุปนัยเกี่ยวกับความหมายเชิงปฏิบัติการ ข้อกำหนด SOS กำหนดพฤติกรรมของโปรแกรมในแง่ของความสัมพันธ์การเปลี่ยนสถานะ (ชุดของความสัมพันธ์ ) ข้อกำหนด SOS อยู่ในรูปแบบของชุดกฎการอนุมานที่กำหนดการเปลี่ยนสถานะที่ถูกต้องของส่วนไวยากรณ์แบบผสมในแง่ของการเปลี่ยนสถานะของส่วนประกอบต่างๆ

เพื่อเป็นตัวอย่างง่ายๆ เราจะพิจารณาส่วนหนึ่งของความหมายของภาษาโปรแกรมอย่างง่ายๆ ตัวอย่างที่เหมาะสมมีอยู่ในPlotkin81และHennessy90และตำราอื่นๆ ให้ครอบคลุมโปรแกรมของภาษา และให้ครอบคลุมสถานะ (เช่น ฟังก์ชันจากตำแหน่งหน่วยความจำไปยังค่า) ถ้าเรามีนิพจน์ (ครอบคลุมโดย) ค่า( )และตำแหน่ง ( ) แล้วคำสั่งอัปเดตหน่วยความจำจะมีอรรถความหมายดังนี้: ${\displaystyle C_{1},C_{2}}$${\displaystyle s}$${\displaystyle E}$${\displaystyle V}$${\displaystyle L}$

${\displaystyle {\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}}$

โดยคร่าวๆ แล้ว กฎนี้กล่าวว่า " ถ้าค่าในสถานะลดลงเหลือค่าที่กำหนดโปรแกรมจะอัปเดตสถานะด้วยค่าที่กำหนดให้" ${\displaystyle E}$${\displaystyle s}$${\displaystyle V}$${\displaystyle L:=E}$${\displaystyle s}$${\displaystyle L=V}$

ความหมายของการเรียงลำดับสามารถกำหนดได้ด้วยกฎสามข้อต่อไปนี้:

1.${\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}}$

2.${\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}}$

3.${\displaystyle {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}}$

โดยไม่เป็นทางการ กฎข้อแรกกล่าวว่า หากโปรแกรมในสถานะจบลงในสถานะแล้วโปรแกรมในสถานะจะลดลงเหลือโปรแกรมในสถานะ(คุณอาจคิดว่านี่เป็นการทำให้เป็นทางการของ "คุณสามารถเรียกใช้แล้วเรียกใช้ โดยใช้หน่วยความจำที่ได้มา") กฎข้อที่สองกล่าวว่า หากโปรแกรมในสถานะสามารถลดเหลือโปรแกรมที่มีสถานะ ได้แล้วโปรแกรมในสถานะจะลดลงเหลือโปรแกรมในสถานะ(คุณอาจคิดว่านี่เป็นการทำให้เป็นทางการของหลักการสำหรับคอมไพเลอร์ที่ปรับแต่งประสิทธิภาพ: "คุณได้รับอนุญาตให้แปลงราวกับว่ามันเป็นโปรแกรมแบบสแตนด์อะโลน แม้ว่ามันจะเป็นเพียงส่วนแรกของโปรแกรมก็ตาม") ความหมายเป็นแบบโครงสร้าง เนื่องจากความหมายของโปรแกรมแบบลำดับถูกกำหนดโดยความหมายของและความหมายของ ${\displaystyle C_{1}}$${\displaystyle s}$${\displaystyle s'}$${\displaystyle C_{1};C_{2}}$${\displaystyle s}$${\displaystyle C_{2}}$${\displaystyle s'}$${\displaystyle C_{1}}$${\displaystyle C_{2}}$${\displaystyle C_{1}}$${\displaystyle s}$${\displaystyle C_{1}'}$${\displaystyle s'}$${\displaystyle C_{1};C_{2}}$${\displaystyle s}$${\displaystyle C_{1}';C_{2}}$${\displaystyle s'}$${\displaystyle C_{1}}$${\displaystyle C_{1};C_{2}}$${\displaystyle C_{1}}$${\displaystyle C_{2}}$

ถ้าเรามีนิพจน์บูลีนเกี่ยวกับสถานะ โดยกำหนดช่วงด้วย เราก็สามารถกำหนดความหมายของ คำสั่ง whileได้: ${\displaystyle B}$${\displaystyle {\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}}$

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

ด้วยรูปลักษณ์ที่ใช้งานง่ายและโครงสร้างที่เข้าใจง่าย SOS จึงได้รับความนิยมอย่างมากและกลายเป็นมาตรฐานโดยพฤตินัยในการกำหนดความหมายเชิงปฏิบัติการ เพื่อแสดงให้เห็นถึงความสำเร็จ รายงานฉบับดั้งเดิม (ที่เรียกว่ารายงาน Aarhus) เกี่ยวกับ SOS ( Plotkin81 ) ได้รับการอ้างอิงมากกว่า 1,000 ครั้ง ตามข้อมูลจาก CiteSeer [1]ทำให้รายงานฉบับนี้เป็นหนึ่งในรายงานทางเทคนิคที่มีการอ้างอิงมากที่สุดในสาขาวิทยาการคอมพิวเตอร์

ความหมายเชิงลดทอน (Reduction semantics)เป็นการนำเสนอทางเลือกของความหมายเชิงปฏิบัติการ (operational semantics) แนวคิดหลักของมันถูกนำไปใช้กับฟังก์ชันบริสุทธิ์แบบเรียกตามชื่อ (call by name)และเรียกตามค่า (call by value)ของ แคลคูลัสแลมบ์ดา (lambda calculus)โดยGordon Plotkinในปี 1975 ^{[ 3 ]}และถูกขยายไปสู่ภาษาฟังก์ชันลำดับสูงที่มีคุณสมบัติเชิงคำสั่งโดยMatthias Felleisenในวิทยานิพนธ์ของเขาในปี 1987 ^{[ 4 ]}วิธีการนี้ได้รับการพัฒนาเพิ่มเติมโดย Matthias Felleisen และ Robert Hieb ในปี 1992 ให้เป็นทฤษฎีสมการ อย่างสมบูรณ์ สำหรับการควบคุมและสถานะ^{[ 2 ]}วลี “ความหมายเชิงลดทอน” (reduction semantics) เองนั้นถูกบัญญัติขึ้นครั้งแรกโดย Felleisen และDaniel P. Friedmanในบทความ PARLE ปี 1987 ^{[ 5 ]}

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

${\displaystyle \mathbf {let\ rec} \ x=v_{1}\ \mathbf {in} \ x\leftarrow v_{2};\ e\ \ \longrightarrow \ \ \mathbf {let\ rec} \ x=v_{2}\ \mathbf {in} \ e}$

เพื่อให้คำสั่งกำหนดค่าอยู่ในตำแหน่งดังกล่าว จะต้อง "ส่งต่อ" ผ่านการเรียกใช้ฟังก์ชันและด้านขวามือของคำสั่งกำหนดค่า จนกว่าจะถึงจุดที่เหมาะสม เนื่องจากนิพจน์ที่อยู่ระหว่างกลางอาจประกาศตัวแปรที่แตกต่างกัน แคลคูลัสจึงต้องการกฎการขยายสำหรับนิพจน์ด้วย การใช้งานความหมายเชิงลดรูปส่วนใหญ่ที่ตีพิมพ์เผยแพร่จะกำหนด "กฎการส่งต่อ" ดังกล่าวโดยสะดวกด้วยบริบทการประเมิน ตัวอย่างเช่น ไวยากรณ์ของบริบทการประเมินใน ภาษา เรียกค่าแบบ ง่าย สามารถแสดงได้ดังนี้ ${\displaystyle \mathbf {let} }$${\displaystyle \mathbf {let} }$

${\displaystyle E::=[\,]\ {\big |}\ v\ E\ {\big |}\ E\ e\ {\big |}\ x\leftarrow E\ {\big |}\ \mathbf {let\ rec} \ x=v\ \mathbf {in} \ E\ {\big |}\ E;\ e}$

โดยที่หมายถึงนิพจน์ใดๆ และหมายถึงค่าที่ลดรูปอย่างสมบูรณ์ บริบทการประเมินแต่ละครั้งจะมีช่องว่างเพียงช่องเดียวซึ่งจะเสียบเทอมเข้าไปในลักษณะการจับภาพ รูปร่างของบริบทจะระบุว่าการลดรูปจะเกิดขึ้นที่ใด ในการอธิบาย "การเกิดฟอง" โดยใช้บริบทการประเมิน สัจพจน์เพียงข้อเดียวก็เพียงพอแล้ว: ${\displaystyle e}$${\displaystyle v}$${\displaystyle [\,]}$

${\displaystyle E[\,x\leftarrow v;\ e\,]\ \ \longrightarrow \ \ x\leftarrow v;\ E[\,e\,]\qquad {\text{(lift assignments)}}}$

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

ตามแนวคิดของ Plotkin การแสดงให้เห็นถึงประโยชน์ของแคลคูลัสที่ได้มาจากชุดของกฎการลดรูปนั้นต้องการ (1) เลมมา Church-Rosser สำหรับความสัมพันธ์แบบขั้นตอนเดียว ซึ่งเหนี่ยวนำให้เกิดฟังก์ชันการประเมิน และ (2) เลมมาการกำหนดมาตรฐาน Curry-Feys สำหรับการปิดแบบถ่ายทอด-สะท้อนของความสัมพันธ์แบบขั้นตอนเดียว ซึ่งแทนที่การค้นหาแบบไม่กำหนดในฟังก์ชันการประเมินด้วยการค้นหาแบบกำหนดจากซ้ายสุด/นอกสุด Felleisen แสดงให้เห็นว่าส่วนขยายเชิงคำสั่งของแคลคูลัสนี้เป็นไปตามทฤษฎีบทเหล่านี้ ผลที่ตามมาของทฤษฎีบทเหล่านี้คือทฤษฎีสมการ—การปิดแบบสมมาตร-ถ่ายทอด-สะท้อน—เป็นหลักการให้เหตุผลที่ถูกต้องสำหรับภาษาเหล่านี้ อย่างไรก็ตาม ในทางปฏิบัติ การประยุกต์ใช้ความหมายการลดรูปส่วนใหญ่จะละเว้นแคลคูลัสและใช้การลดรูปมาตรฐานเท่านั้น (และตัวประเมินที่สามารถได้มาจากมัน)

ความหมายเชิงลดทอนมีประโยชน์อย่างยิ่งเนื่องจากบริบทการประเมินสามารถจำลองสถานะหรือโครงสร้างการควบคุมที่ผิดปกติได้อย่างง่ายดาย (เช่นการต่อเนื่องระดับเฟิร์สคลาส ) นอกจากนี้ ความหมายเชิงลดทอนยังถูกนำมาใช้เพื่อจำลองภาษาเชิงวัตถุ^{[ 6 ]}ระบบสัญญาข้อยกเว้น อนาคต การเรียกตามความจำเป็น และคุณลักษณะภาษาอื่นๆ อีกมากมาย การวิเคราะห์ความหมายเชิงลดทอนที่ทันสมัยและครอบคลุมซึ่งกล่าวถึงการใช้งานดังกล่าวหลายอย่างโดยละเอียดนั้นได้มาจาก Matthias Felleisen, Robert Bruce Findler และ Matthew Flatt ในSemantics Engineering with PLT Redex ^{[ 7 ]}

ความหมายเชิงปฏิบัติการเชิงโครงสร้างแบบก้าวใหญ่ยังเป็นที่รู้จักในชื่อความหมายธรรมชาติความหมายเชิงสัมพันธ์และ ความหมาย เชิงการประเมิน^{[ 8 ]}ความหมายเชิงปฏิบัติการแบบก้าวใหญ่ได้รับการแนะนำภายใต้ชื่อความหมายธรรมชาติโดยGilles Kahn เมื่อนำ เสนอ Mini-ML ซึ่งเป็นภาษาถิ่นบริสุทธิ์ของML

เราสามารถมองคำจำกัดความขั้นตอนใหญ่เป็นคำจำกัดความของฟังก์ชัน หรือโดยทั่วไปแล้วเป็นคำจำกัดความของความสัมพันธ์ โดยตีความโครงสร้างภาษาแต่ละอย่างในโดเมนที่เหมาะสม ความเข้าใจง่ายทำให้เป็นตัวเลือกยอดนิยมสำหรับการกำหนดความหมายในภาษาโปรแกรม แต่ก็มีข้อเสียบางประการที่ทำให้ไม่สะดวกหรือเป็นไปไม่ได้ที่จะใช้ในหลายสถานการณ์ เช่น ภาษาที่มีคุณสมบัติที่เน้นการควบคุมหรือการทำงานพร้อมกัน^{[ 9 ]}

ความหมายเชิงขั้นตอนใหญ่ (Big-step semantics) อธิบายในลักษณะแบ่งและพิชิต (divide-and-conquer) ว่าผลการประเมินขั้นสุดท้ายของโครงสร้างทางภาษา สามารถได้มาอย่างไร โดยการรวมผลการประเมินของส่วนประกอบทางไวยากรณ์ (เช่น นิพจน์ย่อย ประโยคย่อย เป็นต้น) เข้าด้วยกัน

มีความแตกต่างหลายประการระหว่างความหมายเชิงขั้นตอนเล็กและความหมายเชิงขั้นตอนใหญ่ ซึ่งส่งผลต่อว่าความหมายแบบใดเหมาะสมกว่ากันในการกำหนดความหมายของภาษาโปรแกรม

ความหมายแบบขั้นตอนใหญ่มีข้อดีคือมักจะเรียบง่ายกว่า (ต้องการกฎการอนุมานน้อยกว่า) และมักจะสอดคล้องกับการใช้งานตัวแปลภาษาที่มีประสิทธิภาพโดยตรง (ดังนั้น Kahn จึงเรียกสิ่งเหล่านี้ว่า "เป็นธรรมชาติ") ทั้งสองอย่างสามารถนำไปสู่การพิสูจน์ที่ง่ายขึ้น ตัวอย่างเช่น เมื่อพิสูจน์การรักษาความถูกต้องภายใต้การแปลงโปรแกรม บางอย่าง ^{[ 10 ]}

ข้อเสียหลักของความหมายแบบขั้นตอนใหญ่คือการคำนวณที่ไม่สิ้นสุด ( แยกออก ) ไม่มีต้นไม้การอนุมาน ทำให้ไม่สามารถระบุและพิสูจน์คุณสมบัติเกี่ยวกับการคำนวณดังกล่าวได้^{[ 10 ]}

ความหมายแบบขั้นตอนเล็กช่วยให้ควบคุมรายละเอียดและลำดับการประเมินได้มากขึ้น ในกรณีของความหมายเชิงปฏิบัติการที่มีเครื่องมือ ความหมายเชิงปฏิบัติการนี้ช่วยให้สามารถติดตามความหมายเชิงปฏิบัติการได้ และนักความหมายสามารถระบุและพิสูจน์ทฤษฎีบทที่แม่นยำยิ่งขึ้นเกี่ยวกับพฤติกรรมการทำงานของภาษาได้ คุณสมบัติเหล่านี้ทำให้ความหมายแบบขั้นตอนเล็กสะดวกยิ่งขึ้นเมื่อพิสูจน์ความถูกต้องของประเภทของระบบประเภทเทียบกับความหมายเชิงปฏิบัติการ^{[ 10 ]}

• ความหมายเชิงพีชคณิต
• ความหมายเชิงสัจพจน์
• ความหมายเชิงความหมาย
• ความหมายเชิงรูปธรรมของภาษาโปรแกรม

• กิลส์ คาห์น . "ความหมายเชิงธรรมชาติ". รายงานการประชุมสัมมนาประจำปีครั้งที่ 4 ว่าด้วยแง่มุมทางทฤษฎีของวิทยาการคอมพิวเตอร์ . สปริงเกอร์-เวอร์แลก. ลอนดอน. 1987.
• Gordon D. Plotkin. แนวทางเชิงโครงสร้างสำหรับความหมายเชิงปฏิบัติการ (1981) รายงานทางเทคนิค DAIMI FN-19 ภาควิชาวิทยาการคอมพิวเตอร์ มหาวิทยาลัยอาร์ฮุส อาร์ฮุส เดนมาร์ก (พิมพ์ซ้ำพร้อมการแก้ไขใน J. Log. Algebr. Program. 60-61: 17-139 (2004), ( ฉบับก่อนตีพิมพ์ ))
• Gordon D. Plotkin.ที่มาของความหมายเชิงปฏิบัติการเชิงโครงสร้าง. J. Log. Algebr. Program. 60-61:3-15, 2004. ( ฉบับก่อนตีพิมพ์ ).
• Dana S. Scott.โครงร่างทฤษฎีทางคณิตศาสตร์ของการคำนวณ, กลุ่มวิจัยการเขียนโปรแกรม, เอกสารทางเทคนิค PRG–2, มหาวิทยาลัยออกซ์ฟอร์ด, 1970.
• เอเดรียน ฟาน ไวจ์นการ์เดนและคณะ รายงานฉบับแก้ไขเกี่ยวกับภาษาอัลกอริทึมALGOL 68 ไอไอพีพี. 2511 [2]
• Matthew Hennessy . ความหมายของภาษาโปรแกรม. Wiley, 1990. มีให้ดาวน์โหลดออนไลน์ .

• สื่อที่เกี่ยวข้องกับความหมายเชิงปฏิบัติการในวิกิมีเดียคอมมอนส์