ในตรรกศาสตร์คณิตศาสตร์วิทยาการคอมพิวเตอร์และภาษาศาสตร์ภาษาเชิงรูปธรรมคือ เซตของสตริง ที่ มีสัญลักษณ์ซึ่งนำมาจากเซตที่เรียกว่า " ตัวอักษร "

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

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

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

ในศตวรรษที่ 17 ก็อตฟรีด ไลบ์นิซ ได้จินตนาการและอธิบายcharacteristica universalisซึ่งเป็นภาษาสากลและเป็นทางการที่ใช้ภาพสัญลักษณ์ต่อมาคาร์ล ฟรีดริช เกาส์ได้ศึกษาปัญหาของรหัสเกาส์^{[ 3 ]}

ในช่วงกลางศตวรรษที่ 19 จอร์จ บูลได้ก่อตั้งสาขาพีชคณิตบูลีนซึ่งเป็นวิธีการอย่างเป็นทางการในการอธิบายการดำเนินการทางตรรกะโดยใช้ค่าความจริงและตัวดำเนินการเซต ในงานของเขาเรื่อง An Investigation of The Laws of Thoughtเขาได้แสดงให้เห็นว่าการให้เหตุผลเชิงตรรกะสามารถแสดงออกและจัดการได้ผ่านสมการเชิงสัญลักษณ์^{[ 4 ]}

Gottlob Fregeพยายามทำให้แนวคิดของ Leibniz เป็นจริงผ่านระบบสัญลักษณ์ ซึ่งร่างไว้ครั้งแรกในBegriffsschrift (1879) และพัฒนาให้สมบูรณ์ยิ่งขึ้นใน Grundgesetze der Arithmetik (1893/1903) ซึ่งเป็นหนังสือ 2 เล่ม^{[ 5 ]}ระบบนี้อธิบายถึง "ภาษาที่เป็นทางการของภาษาบริสุทธิ์" ^{[ 6 ]}

ในช่วงครึ่งแรกของศตวรรษที่ 20 มีการพัฒนาหลายอย่างที่เกี่ยวข้องกับภาษาทางการAxel Thueได้ตีพิมพ์บทความสี่ฉบับที่เกี่ยวข้องกับคำและภาษาระหว่างปี 1906 ถึง 1914 บทความสุดท้ายนี้ได้แนะนำสิ่งที่Emil Postเรียกในภายหลังว่า 'ระบบ Thue' และให้ตัวอย่างแรกๆ ของปัญหาที่ไม่สามารถตัดสินได้ [ ^{7 ] ต่อ}มา Post จะใช้บทความนี้เป็นพื้นฐานสำหรับการพิสูจน์ในปี 1947 ว่า "ปัญหาคำสำหรับเซมิกรุปไม่สามารถแก้ได้แบบเรียกซ้ำ" ^{[ 8 ]}และต่อมาได้คิดค้นระบบมาตรฐานสำหรับการสร้างภาษาทางการ

ในปี พ.ศ. 2450 Leonardo Torres Quevedoได้นำเสนอภาษาที่เป็นทางการสำหรับการอธิบายภาพวาดทางกล (อุปกรณ์ทางกล) ในเวียนนาเขาได้ตีพิมพ์ "Sobre un sistema de notaciones y símbolos destinados a facilitar la descripción de las máquinas" ("เกี่ยวกับระบบของสัญกรณ์และสัญลักษณ์ที่มุ่งอำนวยความสะดวกในการอธิบายเครื่องจักร") ^{[ 9 ]} Heinz Zemanekประเมินว่ามันเทียบเท่ากับภาษาโปรแกรมสำหรับการควบคุมเชิงตัวเลขของเครื่องมือกล^{[ 10 ]}

โนอัม ชอมสกีได้คิดค้นการแสดงแทนเชิงนามธรรมของภาษาทางการและภาษาธรรมชาติ ซึ่งรู้จักกันในชื่อลำดับชั้นของชอมสกี [ ^{11 ] ใน}ปี พ.ศ. 2492 จอห์น แบคคัสได้พัฒนารูปแบบแบคคัส-เนาเออร์ เพื่ออธิบายไวยากรณ์ของภาษาโปรแกรมระดับสูง โดยต่อยอดจากงานของเขาในการสร้างFORTRAN ^{[ 12 ]}ปีเตอร์ เนาเออร์ เป็นเลขานุการ/บรรณาธิการของรายงาน ALGOL60 ซึ่งเขาใช้รูปแบบแบคคัส-เนาเออร์เพื่ออธิบายส่วนที่เป็นทางการของ ALGOL60

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

คำ บน ชุดตัวอักษรใดๆ ก็ได้ สามารถเป็นลำดับจำกัด (เช่นสตริง ) ของตัวอักษรได้ เซตของคำทั้งหมดบนชุดตัวอักษร Σ มักจะใช้สัญลักษณ์ Σ ^* (โดยใช้สัญลักษณ์ดาวคลีน ) ความยาวของคำคือจำนวนตัวอักษรที่ประกอบเป็นคำนั้น สำหรับชุดตัวอักษรใดๆ จะมีคำที่มีความยาวเป็น 0 เพียงคำเดียว คือคำว่างซึ่งมักจะใช้สัญลักษณ์ e, ε, λ หรือแม้แต่ Λ โดยการเชื่อมต่อคำสองคำเข้าด้วยกัน เราสามารถรวมคำใหม่ได้ ซึ่งความยาวของคำใหม่จะเท่ากับผลรวมของความยาวของคำเดิม ผลลัพธ์ของการเชื่อมต่อคำกับคำว่างคือคำเดิม

ในบางการประยุกต์ใช้ โดยเฉพาะในตรรกศาสตร์ตัวอักษรยังถูกเรียกว่าคำศัพท์และคำต่างๆ ถูกเรียกว่าสูตรหรือประโยคซึ่งเป็นการทำลายอุปมาอุปไมยระหว่างตัวอักษรกับคำ และแทนที่ด้วยอุปมาอุปไมยระหว่างคำกับประโยค

กำหนดให้เซตที่ไม่ว่างเปล่าภาษาเชิงรูปธรรมบนคือเซตย่อยของโดยที่คือเซตของคำที่มีความยาวจำกัดที่เป็นไปได้ทั้งหมดบนเราเรียกเซต ว่าตัวอักษรของในทางกลับกัน กำหนดให้ภาษาเชิงรูปธรรมบน คำหนึ่งจะเรียก ว่าคำที่มีรูปแบบดี (well-formed ) ถ้า ในทำนอง เดียวกัน นิพจน์ หนึ่งจะเรียกว่าคำ ที่มีรูปแบบดี (well-formed)ถ้าบางครั้ง ภาษาเชิงรูปธรรมบนมีชุดของกฎและข้อจำกัดที่ชัดเจนสำหรับการสร้างคำที่มีรูปแบบดีที่เป็นไปได้ทั้งหมดจาก ${\displaystyle \Sigma }$${\displaystyle L}$${\displaystyle \Sigma }$${\displaystyle \Sigma ^{*}}$${\displaystyle \Sigma ^{*}}$${\displaystyle \Sigma }$${\displaystyle \Sigma }$${\displaystyle L}$${\displaystyle L}$${\displaystyle \Sigma }$${\displaystyle w\in \Sigma ^{*}}$${\displaystyle w\in L}$${\displaystyle E\subseteq \Sigma ^{*}}$${\displaystyle E\subseteq L}$${\displaystyle L}$${\displaystyle \Sigma }$${\displaystyle \Sigma ^{*}}$

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

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

กฎต่อไปนี้อธิบายภาษาเชิงรูปธรรม  Lบนตัวอักษร Σ = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, +, =}:

• สตริงที่ไม่ว่าง เปล่าทุกสตริงที่ไม่ประกอบด้วย "+" หรือ "=" และไม่ขึ้นต้นด้วย "0" จะอยู่ใน  L
• สตริง "0" อยู่  ในL
• สตริงที่มี "=" จะอยู่ใน  L ก็ต่อเมื่อมี "=" เพียงตัวเดียว และ "=" นั้นคั่นระหว่างสตริงที่ถูกต้องสองสตริงของ  L
• สตริงที่มีเครื่องหมาย "+" แต่ไม่มีเครื่องหมาย "=" จะอยู่ใน  Lก็ต่อเมื่อเครื่องหมาย "+" ทุกตัวในสตริงนั้นคั่นระหว่างสตริงที่ถูกต้องสองสตริง  ของL
• ไม่มีสตริงใดอยู่ใน  Lนอกเหนือจากสตริงที่กำหนดโดยกฎก่อนหน้านี้

ภายใต้กฎเหล่านี้ สตริง "23+4=555" อยู่ใน  Lแต่สตริง "=234=+" ไม่อยู่ใน L ภาษาเชิงรูปธรรมนี้แสดงถึงจำนวนธรรมชาติการบวกที่ถูกต้อง และความเท่าเทียมกันของการบวกที่ถูกต้อง แต่แสดงเฉพาะสิ่งที่พวกมันดูเหมือน ( ไวยากรณ์ ) เท่านั้น ไม่ใช่สิ่งที่พวกมันหมายถึง ( ความหมาย ) ตัวอย่างเช่น ไม่มีที่ใดในกฎเหล่านี้ที่บ่งชี้ว่า "0" หมายถึงเลขศูนย์ "+" หมายถึงการบวก "23+4=555" เป็นเท็จ เป็นต้น

สำหรับภาษาจำกัด เราสามารถแจกแจงคำที่ถูกต้องทั้งหมดได้อย่างชัดเจน ตัวอย่างเช่น เราสามารถอธิบายภาษา  L ได้ ว่าL  = {a, b, ab, cba} กรณี ที่เสื่อมสภาพของการสร้างนี้คือภาษาว่างเปล่าซึ่งไม่มีคำใด ๆ เลย ( L  =  ∅ )

อย่างไรก็ตาม แม้แต่ในตัวอักษรที่มีจำนวนจำกัด (ไม่ว่างเปล่า) เช่น Σ = {a, b} ก็ยังมีคำที่มีความยาวจำกัดจำนวนอนันต์ที่สามารถแสดงออกมาได้ เช่น "a", "abb", "ababba", "aaababbbbaab", .... ดังนั้น ภาษาทางการจึงมักเป็นอนันต์ และการอธิบายภาษาทางการที่เป็นอนันต์นั้นไม่ใช่เรื่องง่ายเหมือนกับการเขียนL  = {a, b, ab, cba} ต่อไปนี้เป็นตัวอย่างของภาษาทางการบางส่วน:

• L = Σ ^* , เซตของ คำ ทั้งหมดเหนือ Σ;
• L = {a} ^* = {a ⁿ } โดยที่nเป็นจำนวนธรรมชาติ และ "a ⁿ " หมายถึง "a" ซ้ำกันnครั้ง (นี่คือเซตของคำที่ประกอบด้วยสัญลักษณ์ "a" เท่านั้น)
• ชุดของโปรแกรมที่ถูกต้องตามหลักไวยากรณ์ในภาษาโปรแกรมที่กำหนด (ซึ่งโดยปกติแล้วไวยากรณ์ของภาษานั้นจะถูกกำหนดโดยไวยากรณ์แบบไม่ขึ้นกับบริบท )
• ชุดข้อมูลป้อนเข้าที่ทำให้เครื่องจักรทัวริง เครื่องหนึ่ง หยุดทำงาน หรือ
• เซตของสตริง ตัว อักษร และตัวเลข ASCII ที่ยาวที่สุด ในบรรทัดนี้ กล่าวคือเซต {the, set, of, maximal, strings, alphanumeric, ASCII, characters, on, this, line, i, e}

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

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

คำถามทั่วไปที่มักถามเกี่ยวกับรูปแบบที่เป็นทางการเหล่านี้ ได้แก่:

• พลังในการแสดงออกของพวกมันคืออะไร? (รูปแบบทางภาษาX สามารถ อธิบายทุกภาษาที่รูปแบบทางภาษาYสามารถอธิบายได้หรือไม่? มันสามารถอธิบายภาษาอื่นๆ ได้หรือไม่?)
• คำเหล่านั้นสามารถจดจำได้ง่ายแค่ไหน? (การตัดสินใจว่าคำใดคำหนึ่งอยู่ในภาษาที่อธิบายโดยรูปแบบทางภาษาX นั้นยากแค่ไหน ?)
• ความสามารถในการเปรียบเทียบของทั้งสองภาษาเป็นอย่างไร? (การตัดสินใจว่าภาษาสองภาษา ภาษาหนึ่งอธิบายด้วยรูปแบบXและอีกภาษาหนึ่งอธิบายด้วยรูปแบบYหรือใน รูปแบบ Xอีกครั้ง เป็นภาษาเดียวกันหรือไม่นั้น ยากเพียงใด?)

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

การดำเนินการบางอย่างกับภาษาเป็นเรื่องปกติ ซึ่งรวมถึงการดำเนินการเซตมาตรฐาน เช่น ยูเนียน อินเตอร์เซกชัน และคอมพลีเมนต์ การดำเนินการอีกประเภทหนึ่งคือการประยุกต์ใช้การดำเนินการกับสตริงทีละองค์ประกอบ

ตัวอย่าง: สมมติว่าและเป็นภาษาที่ใช้อักษรพื้นฐานร่วมกัน ${\displaystyle L_{1}}$${\displaystyle L_{2}}$${\displaystyle \Sigma }$

• การต่อสตริง ประกอบด้วยสตริงทั้งหมดที่มีรูปแบบโดยที่เป็นสตริงจากและเป็นสตริงจาก${\displaystyle L_{1}\cdot L_{2}}$${\displaystyle vw}$${\displaystyle v}$${\displaystyle L_{1}}$${\displaystyle w}$${\displaystyle L_{2}}$
• จุดตัด ของและประกอบด้วยสตริงทั้งหมดที่มีอยู่ในทั้งสองภาษา${\displaystyle L_{1}\หมวก L_{2}}$${\displaystyle L_{1}}$${\displaystyle L_{2}}$
• ส่วนเติมเต็ม ของเมื่อเทียบกับประกอบด้วยสตริงทั้งหมดบนที่ไม่ได้อยู่ใน${\displaystyle \neg L_{1}}$${\displaystyle L_{1}}$${\displaystyle \Sigma }$${\displaystyle \Sigma }$${\displaystyle L_{1}}$
• ภาษาKleene star : ภาษาที่ประกอบด้วยคำทุกคำที่เกิดจากการต่อกันของคำตั้งแต่ศูนย์คำขึ้นไปในภาษาต้นฉบับ
• การกลับทิศทาง :
  • ให้εเป็นคำว่างเปล่า ดังนั้นและ${\displaystyle \varepsilon ^{R}=\varepsilon }$
  • สำหรับแต่ละคำที่ไม่ว่างเปล่า(โดยที่เป็นองค์ประกอบของตัวอักษรบางตัว) ให้กำหนด,${\displaystyle w=\sigma _{1}\cdots \sigma _{n}}$${\displaystyle \sigma _{1},\ldots ,\sigma _{n}}$${\displaystyle w^{R}=\sigma _{n}\cdots \sigma _{1}}$
  • จากนั้น สำหรับภาษาที่เป็นทางการ.${\displaystyle L}$${\displaystyle L^{R}=\{w^{R}\mid w\in L\}}$
• โฮโมมอร์ฟิซึมของสตริง

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

คุณสมบัติการปิดของตระกูลภาษา ( Op โดยที่ทั้งและอยู่ในตระกูลภาษาที่กำหนดโดยคอลัมน์) อ้างอิงจาก Hopcroft และ Ullman ${\displaystyle L_{1}}$${\displaystyle L_{2}}$${\displaystyle L_{1}}$${\displaystyle L_{2}}$

การดำเนินการ		ปกติ	ดีซีเอฟแอล	ซีเอฟแอล	อินเดีย	ซีเอสแอล	เรียกซ้ำ	อีกครั้ง
สหภาพ	${\displaystyle L_{1}\cup L_{2}=\{w\mid w\in L_{1}\lor w\in L_{2}\}}$	ใช่	เลขที่	ใช่	ใช่	ใช่	ใช่	ใช่
จุดตัด	${\displaystyle L_{1}\cap L_{2}=\{w\mid w\in L_{1}\land w\in L_{2}\}}$	ใช่	เลขที่	เลขที่	เลขที่	ใช่	ใช่	ใช่
คอมพลีเมนต์	${\displaystyle \neg L_{1}=\{w\mid w\not \in L_{1}\}}$	ใช่	ใช่	เลขที่	เลขที่	ใช่	ใช่	เลขที่
การต่อกัน	${\displaystyle L_{1}\cdot L_{2}=\{wz\mid w\in L_{1}\land z\in L_{2}\}}$	ใช่	เลขที่	ใช่	ใช่	ใช่	ใช่	ใช่
คลีน สตาร์	${\displaystyle L_{1}^{*}=\{\varepsilon \}\cup \{wz\mid w\in L_{1}\land z\in L_{1}^{*}\}}$	ใช่	เลขที่	ใช่	ใช่	ใช่	ใช่	ใช่
โฮโมมอร์ฟิซึม (สตริง)${\displaystyle h}$	${\displaystyle h(L_{1})=\{h(w)\mid w\in L_{1}\}}$	ใช่	เลขที่	ใช่	ใช่	เลขที่	เลขที่	ใช่
โฮโมมอร์ฟิซึมแบบ ε-free (สตริง)${\displaystyle h}$	${\displaystyle h(L_{1})=\{h(w)\mid w\in L_{1}\}}$	ใช่	เลขที่	ใช่	ใช่	ใช่	ใช่	ใช่
การทดแทน${\displaystyle \varphi }$	${\displaystyle \varphi (L_{1})=\bigcup _{\sigma _{1}\cdots \sigma _{n}\in L_{1}}\varphi (\sigma _{1})\cdot \ldots \cdot \varphi (\sigma _{n})}$	ใช่	เลขที่	ใช่	ใช่	ใช่	เลขที่	ใช่
โฮโมมอร์ฟิซึมผกผัน${\displaystyle h^{-1}}$	${\displaystyle h^{-1}(L_{1})=\bigcup _{w\in L_{1}}h^{-1}(w)}$	ใช่	ใช่	ใช่	ใช่	ใช่	ใช่	ใช่
ย้อนกลับ	${\displaystyle L^{R}=\{w^{R}\mid w\in L\}}$	ใช่	เลขที่	ใช่	ใช่	ใช่	ใช่	ใช่
จุดตัดกับภาษาปกติ${\displaystyle R}$	${\displaystyle L\cap R=\{w\mid w\in L\land w\in R\}}$	ใช่	ใช่	ใช่	ใช่	ใช่	ใช่	ใช่

โดยทั่วไปแล้ว คอมไพเลอร์จะมีส่วนประกอบที่แตกต่างกันสองส่วน ส่วนแรกคือตัววิเคราะห์คำศัพท์ (lexical analyzer ) ซึ่งบางครั้งสร้างขึ้นโดยเครื่องมืออย่างเช่น ` compiler` ทำ lexหน้าที่ระบุโทเค็นของไวยากรณ์ภาษาโปรแกรม เช่นตัวระบุหรือคำหลักตัวเลขและสตริง เครื่องหมายวรรคตอน และสัญลักษณ์ตัวดำเนินการ ซึ่งระบุโดยภาษาที่เป็นทางการที่ง่ายกว่า โดยปกติแล้วจะใช้การแสดงออกปกติ (regular expressions ) ส่วนที่สองคือ ตัวแยก วิเคราะห์ (parser)ซึ่งบางครั้งสร้างขึ้นโดยตัวสร้างตัวแยกวิเคราะห์ (parser generator)ในระดับแนวคิดพื้นฐานที่สุดyaccจะพยายามตัดสินว่าโปรแกรมต้นฉบับนั้นถูกต้องตามหลักไวยากรณ์หรือไม่ กล่าวคือ ถูกต้องตามหลักไวยากรณ์ภาษาโปรแกรมที่คอมไพเลอร์สร้างขึ้นหรือไม่

แน่นอนว่า คอมไพเลอร์ไม่ได้แค่ทำการวิเคราะห์โค้ดต้นฉบับเท่านั้น แต่โดยทั่วไปแล้วมันจะแปลงโค้ดนั้นให้เป็นรูปแบบที่สามารถเรียกใช้งานได้ ด้วยเหตุนี้ ตัววิเคราะห์โค้ดจึงมักให้ผลลัพธ์มากกว่าแค่คำตอบใช่/ไม่ใช่ โดยทั่วไปแล้ว จะเป็นโครงสร้าง ต้นไม้ไวยากรณ์นามธรรม (Abstract Syntax Tree ) ซึ่งจะถูกใช้ในขั้นตอนต่อๆ ไปของคอมไพเลอร์เพื่อสร้างไฟล์ที่สามารถเรียกใช้งานได้ ซึ่งประกอบด้วย โค้ดเครื่อง ที่ ทำงานโดยตรงบนฮาร์ดแวร์ หรือโค้ดระดับกลางที่ต้องใช้เครื่องเสมือน (Virtual Machine)ในการเรียกใช้งาน

ในตรรกศาสตร์ทางคณิตศาสตร์ทฤษฎีเชิงรูปธรรมคือ เซตของประโยคที่แสดงออกมาในภาษาเชิงรูปธรรม

ระบบเชิงรูปธรรม (เรียกอีกอย่างว่าแคลคูลัสเชิงตรรกะหรือระบบตรรกะ ) ประกอบด้วยภาษาเชิงรูปธรรมร่วมกับเครื่องมืออนุมาน (เรียกอีกอย่างว่าระบบอนุมาน ) เครื่องมืออนุมานอาจประกอบด้วยชุดของกฎการแปลงซึ่งอาจตีความได้ว่าเป็นกฎการอนุมานที่ถูกต้อง หรือชุดของสัจพจน์หรืออาจมีทั้งสองอย่าง ระบบเชิงรูปธรรมใช้ในการอนุมานนิพจน์หนึ่งจากนิพจน์อื่นตั้งแต่หนึ่งนิพจน์ขึ้นไป แม้ว่าภาษาเชิงรูปธรรมจะสามารถระบุได้ด้วยสูตรของมัน แต่ระบบเชิงรูปธรรมไม่สามารถระบุได้ด้วยทฤษฎีบทของมัน ระบบเชิงรูปธรรมสองระบบอาจมีทฤษฎีบทเหมือนกันทั้งหมด แต่แตกต่างกันในเชิงทฤษฎีการพิสูจน์อย่างมีนัยสำคัญ (เช่น สูตร A อาจเป็นผลสืบเนื่องทางไวยากรณ์ของสูตร B ในระบบหนึ่ง แต่ไม่ใช่ในอีกระบบหนึ่ง) ${\displaystyle {\mathcal {FS}}}$${\displaystyle {\mathcal {FS'}}}$

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

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

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

• คณิตศาสตร์เชิงการจัดเรียงบนคำศัพท์
• วิธีการที่เป็นทางการ
• โมโนอิดอิสระ
• กรอบไวยากรณ์
• สัญกรณ์ทางคณิตศาสตร์
• สตริง (วิทยาการคอมพิวเตอร์)

• "ภาษาเชิงรูปธรรม" , สารานุกรมคณิตศาสตร์ , EMS Press , 2001 [1994]
• มหาวิทยาลัยแมริแลนด์ , คำจำกัดความของภาษาเชิงทางการ(เก็บถาวรเมื่อวันที่ 16 กุมภาพันธ์ 2551 ที่Wayback Machine)
• เจมส์ พาวเวอร์, "บันทึกเกี่ยวกับทฤษฎีภาษาเชิงรูปธรรมและการวิเคราะห์ไวยากรณ์" เก็บถาวรเมื่อวันที่ 21 พฤศจิกายน 2007 ที่Wayback Machine , 29 พฤศจิกายน 2002
• ร่างบทบางส่วนใน "คู่มือทฤษฎีภาษาเชิงรูปธรรม" เล่ม 1-3, จี. โรเซนเบิร์ก และ เอ. ซาโลมา (บรรณาธิการ), สำนักพิมพ์สปริงเกอร์ (1997):
  • Alexandru Mateescu และ Arto Salomaa, "คำนำ" ในเล่ม 1, หน้า v–viii และ "ภาษาทางการ: บทนำและเรื่องย่อ" บทที่ 1 ในเล่ม 1 1, หน้า 1–39
  • Sheng Yu, "ภาษาปกติ", บทที่ 2 ในเล่ม 1
  • Jean-Michel Autebert, Jean Berstel, Luc Boasson, "ภาษาไร้บริบทและออโตมาตาแบบพุชดาวน์", บทที่ 3 ในเล่มที่ 1
  • Christian Choffrut และ Juhani Karhumäki, "Combinatorics of Words", บทที่ 6 ในเล่ม 1 1
  • Tero Harju และ Juhani Karhumäki "Morphisms" บทที่ 7 ในเล่ม 1 1, หน้า 439–510
  • ฌอง-เอริค ปิน, "เซมิกรุปเชิงไวยากรณ์", บทที่ 10 ในเล่ม 1, หน้า 679–746
  • M. Crochemore และ C. Hancart, "Automata for matching patterns", บทที่ 9 ในเล่มที่ 2
  • Dora Giammarresi, Antonio Restivo, "ภาษาสองมิติ", บทที่ 4 ในเล่ม 1 3, หน้า 215–267