ดูต้นฉบับสำหรับ ภาษารูปนัย

[[ไฟล์:Syntax tree.svg|thumb|โครงสร้างของประโยคในภาษาอังกฤษที่แม้ไม่มีความหมายแต่จัดดีแล้วทางวากยสัมพันธ์ ''"Colorless green ideas sleep furiously"'' ([[Colorless green ideas sleep furiously|ตัวอย่าง]]จาก[[โนม ชอมสกี]] ค.ศ. 1957).]]

ใน[[ตรรกศาสตร์]], [[คณิตศาสตร์]], [[ภาษาศาสตร์]] และ[[วิทยาการคอมพิวเตอร์]] '''ภาษารูปนัย''' ({{langx|en|Formal language}}) บ้างก็ว่า '''ภาษาแบบแผน''' ประกอบด้วย[[สายอักขระ|คำ]]ซึ่งสะกดด้วย[[สัญลักษณ์ (รูปนัย)|ตัวอักษร]] (symbol (formal)) จาก[[ชุดตัวอักษร (ภาษารูปนัย)|ชุดตัวอักษร]]ชุดหนึ่ง และ[[ความจัดดีแล้ว|จัดดีแล้ว]] (well-formedness) ตามกฎชุดหนึ่ง

[[ชุดตัวอักษร (ภาษารูปนัย)|ชุดตัวอักษร]]ของภาษารูปนัยภาษาหนึ่งประกอบด้วยสัญลักษณ์, ตัวอักษร หรือโทเค็น ซึ่งต่อกัน (concatenate) เป็นสายอักขระในภาษานั้น<ref>ดูที่ อาทิ {{citation|title=Formal Languages and Compilation|series=Texts in Computer Science|first=Stefano Crespi|last=Reghizzi|publisher=Springer|year=2009|isbn=9781848820500|page=8|quote=An alphabet is a finite set}}.</ref> สายอักขระแต่ละสายซึ่งต่อกันขึ้นจากสัญลักษณ์ในชุดตัวอักษรนั้นเรียกว่าคำ และบางครั้งคำในภาษารูปนัยภาษาหนึ่งก็เรียกว่า''คำที่จัดดีแล้ว'' หรือ ''[[สูตรที่จัดดีแล้ว]]'' (well-formed formula) ภาษารูปนัยถูกกำหนดโดย[[ไวยากรณ์รูปนัย]] (formal grammar) เช่น[[ไวยากรณ์ปรกติ]] (regular grammar) หรือ[[ไวยากรณ์ไม่พึ่งบริบท]] (context-free grammar) ซึ่งประกอบด้วย[[กฎการจัดรูป]] (formation rule) ของตัวเอง

สาขา'''ทฤษฎีภาษารูปนัย''' ({{langx|en|Formal language theory}}) ศึกษาด้าน[[วากยสัมพันธ์]] หรือรูปแบบโครงสร้างภายในของภาษารูปนัยเป็นหลัก ทฤษฎีภาษารูปนัยแยกออกมาจากภาษาศาสตร์ เพื่อทำความเข้าใจถึงระเบียบทางวากยสัมพันธ์ของ[[ภาษาธรรมชาติ]] ภาษารูปนัยถูกใช้ในวิทยาการคอมพิวเตอร์เป็นรากฐานของนิยามของไวยากรณ์ของ[[ภาษาโปรแกรม]] และของภาษาธรรมชาติรูปแบบรูปนัยซึ่งคำในภาษานั้นแทนแนวคิดที่สัมพันธ์กับ[[อรรถศาสตร์|ความหมาย]]อันหนึ่ง ตามปกติใน[[ทฤษฎีความซับซ้อนในการคำนวณ]] [[ปัญหาการตัดสินใจ]]ถูกนิยามเป็นภาษารูปนัย และ[[กลุ่มความซับซ้อน]]ถูกนิยามเป็นเซตของภาษารูปนัยที่เครื่องซึ่งมีพลังในการคำนวณจำกัดสามารถ[[การแจงส่วน|แจงส่วน]] (parsing) ได้ ใน[[ตรรกศาสตร์]]และ[[รากฐานของคณิตศาสตร์]] ภาษารูปนัยถูกนำมาใช้เพื่อแทนวากยสัมพันธ์ของ[[ระบบสัจพจน์]] (axiomatic system) และ[[รูปนัยนิยม (ปรัชญาคณิตศาสตร์)|รูปนัยนิยม]] (formalism (philosophy of mathematics) เป็นปรัชญาที่กล่าวว่าคณิตศาสตร์ทั้งหมดล้วนสามารถถูกลดรูปให้กลายเป็นเพียงกระบวนการดัดแปลงทางวากยสัมพันธ์ของภาษารูปนัยได้

== ประวัติ ==
คำว่าภาษารูปนัย (formal language) อาจถูกใช้เป็นครั้งแรกใน ''[[Begriffsschrift]]'' (แปลว่า การเขียนแนวคิด, concept writing) โดย [[ก็อทโลพ เฟรเกอ]] (Gottlob Frege) ในปี ค.ศ. 1879 ซึ่งอธิบายถึง "ภาษารูปนัยของภาษาบริสุทธิ์" {{NoteTag|แปลจาก "formal language of pure language."}}<ref name="Herken1279">{{cite book|editor=Rolf Herken|title=The universal Turing machine: a half-century survey|chapter-url=https://books.google.com/books?id=YafIDVd1Z68C&pg=PA290|year=1995|publisher=Springer|isbn=978-3-211-82637-9|page=290|chapter=Influences of Mathematical Logic on Computer Science|author=Martin Davis}}</ref>

== คำจากชุดตัวอักษร ==
ในบริบทของภาษารูปนัย '''ชุดตัวอักษร'''เป็น[[เซต]]ของสิ่งใดก็ได้ อย่างไรก็ตามการใช้คำว่า[[อักษร|ชุดตัวอักษร]]ในความหมายทั่วไปทำให้เข้าใจได้ง่ายกว่า เช่น[[รหัสอักขระ|ชุดอักขระ]]อาทิ [[แอสกี|ASCII]] หรือ[[ยูนิโคด]] สมาชิกในชุดตัวอักษรเรียกว่า'''ตัวอักษร''' ชุดตัวอักษรชุดหนึ่งสามารถมีตัวอักษรได้เยอะ[[เซตนับได้|นับไม่ถ้วน]]{{NoteTag|ตัวอย่างเช่น ชุดตัวอักษรที่ใช้แสดง[[ตรรกศาสตร์อันดับหนึ่ง]] (first-order logic) นั้นนอกจากสัญลักษณ์อย่าง ∧, ¬, ∀ และวงเล็บแล้ว ก็ยังมีสมาชิกตัวอักษรอื่น ๆ อีกมากมาย ''x''<sub>0</sub>,&nbsp;''x''<sub>1</sub>,&nbsp;''x''<sub>2</sub>,&nbsp;…  จำนวนนับไม่ถ้วนที่ทำหน้าที่เป็นตัวแปร}} อย่างไรก็ตาม นิยามในทฤษฎีภาษารูปนัยส่วนใหญ่ระบุให้ชุดตัวอักษรมีสมาชิกจำนวนจำกัด และผลลัพธ์ส่วนใหญ่จะใช้ได้กับชุดตัวอักษรแบบนี้เท่านั้น

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

ในการประยุกต์ใช้ในสาขาอื่น โดยเฉพาะ[[ตรรกศาสตร์]] ชุดตัวอักษรมีชื่อเรียกอีกชื่อว่า ''[[วงศัพท์]]'' และคำมีชื่อเรียกอีกชื่อว่า ''สูตร'' (formula) หรือ ''ประโยค'' (sentence) ซึ่งเป็นการเปลี่ยนการเปรียบเทียบ จากการเทียบกับความสัมพันธ์ระหว่างตัวอักษรกับคำ เป็นการเทียบกับความสัมพันธ์ระหว่างคำและประโยค

==บทนิยาม==
''ภาษารูปนัย'' ''L'' ที่ใช้ชุดตัวอักษร Σ เป็น[[เซตย่อย]]ของเซตของ[[#คำบนชุดตัวอักษร|คำ]]ทุกคำ Σ<sup>*</sup> ในชุดตัวอักษรนั้น บางครั้งคำแต่ละคำก็จะถูกจัดกลุ่มเป็นนิพจน์ และกฎเกณฑ์บางอย่างจะถูกกำหนดขึ้นมาเพื่อสร้าง 'นิพจน์ที่จัดดีแล้ว'

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

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

==ตัวอย่าง==

ข้อความดังต่อไปนี้เป็นกฎที่บรรยายถึงภาษารูปนัย&nbsp;{{mvar|L}} ภาษาหนึ่งซึ่งประกอบขึ้นจากชุดตัวอักษร Σ&nbsp;=&nbsp;{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, +, =}:
* สายอักขระที่ไม่ว่างทุกสาย ที่ไม่มีตัว "+" หรือ "=" และไม่ได้เริ่มต้นด้วยตัว "0" เป็นสายอักขระที่มีอยู่ในภาษา &nbsp;{{mvar|L}}
* สายอักขระ "0" มีอยู่ในภาษา&nbsp;{{mvar|L}}
* สายอักขระที่มีตัว "=" นั้นจะมีอยู่ในภาษา&nbsp;{{mvar|L}} ก็ต่อเมื่อมีตัว "=" เพียงตัวเดียวเท่านั้น และจะต้องอยู่ระหว่างสายอักขระสองสายที่ถูกต้องตามกฎของภาษา&nbsp;{{mvar|L}}
* สายอักขระที่มีตัว "+" แต่ไม่มีตัว "=" นั้นจะมีอยู่ในภาษา&nbsp;{{mvar|L}} ก็ต่อเมื่อตัว "+" ทุกตัวในสายอักขระนั้นอยู่ระหว่างสายอักขระสองสายที่ถูกต้องตามกฎของภาษา&nbsp;{{mvar|L}}
* ไม่มีสายอักขระอื่นใดอยู่ในภาษา&nbsp;{{mvar|L}} นอกเหนือจากที่กฎที่ระบุไว้ก่อนหน้านี้สื่อถึง
ภายใต้กฎเหล่านี้ สายอักขระ "23+4=555" มีอยู่ในภาษา&nbsp;{{mvar|L}} แต่ไม่มีสายอักขระ "=234=+" อยู่ในภาษา&nbsp;{{mvar|L}} ภาษารูปนัยภาษานี้แสดงถึง[[จำนวนธรรมชาติ]], [[การบวก]]ที่จัดดีแล้ว และสมการของการบวกที่จัดดีแล้ว แต่แสดงเพียงลักษณะว่าเป็นอย่างไร ([[วากยสัมพันธ์]]) แต่ไม่ได้แสดงว่ามี[[อรรถศาสตร์|ความหมาย]]อย่างไร ตัวอย่างเช่น กฎเหล่านี้ไม่ได้ระบุว่า "0" หมายถึงเลขศูนย์, "+" หมายถึงการบวก, "23+4=555" เป็นเท็จ, ฯลฯ

=== การสร้าง ===
เราสามารถแจกแจงคำที่จัดดีแล้วทุกคำในภาษาจำกัดภาษาหนึ่งได้ เช่น เราสามารถบรรยายภาษา&nbsp;{{mvar|L}} ได้ว่า {{mvar|L}}&nbsp;=&nbsp;{a, b, ab, cba} กรณี[[ภาวะลดรูป|ลดรูป]]ของการสร้างแบบนี้คือ'''ภาษาว่าง'''ซึ่งไม่มีคำอยู่เลย (<span class="nounderlines">{{mvar|L}}&nbsp;=&nbsp;[[∅]]</span>)

ทว่าแม้แต่ชุดตัวอักษรที่จำกัด (ไม่ว่าง) เช่น Σ&nbsp;=&nbsp;{a,&nbsp;b} ก็มีคำที่มีความยาวจำกัดที่ประกอบขึ้นจากชุดตัวอักษรนั้นอยู่มากเป็นจำนวนไม่จำกัด (อนันต์): "a", "abb", "ababba", "aaababbbbaab",&nbsp;.... ดังนั้นภาษารูปนัยโดยปกติเป็นภาษาอนันต์ และการบรรยายภาษารูปนัยอนันต์นั้นไม่สามารถทำได้ด้วยเพียงการเขียนว่า ''L''&nbsp;=&nbsp;{a, b, ab, cba} ข้อความต่อไปนี้เป็นตัวอย่างของภาษารูปนัย:
* {{mvar|L}} = Σ<sup>*</sup> เซตของคำทุกคำในชุดตัวอักษร Σ
* {{mvar|L}} = {a}<sup>*</sup> = {a<sup>''n''</sup>} โดย ''n'' คือจำนวนธรรมชาติ และ "a<sup>''n''</sup>" หมายถึง "a" ซ้ำกัน ''n'' ครั้ง (เซตของคำทุกคำที่ประกอบขึ้นจากสัญลักษณ์ "a" เท่านั้น)
* เซตของโปรแกรมที่ถูกต้องทางวากยสัมพันธ์ทุกโปรแกรมในภาษาโปรแกรมภาษาหนึ่ง (ซึ่งปกติวากยสัมพันธ์ของภาษานั้นถูกให้นิยามด้วย[[ไวยากรณ์ไม่พึ่งบริบท]] (context-free grammar))
* เซตของอินพุตที่ทำให้[[เครื่องทัวริง]]เครื่องหนึ่งหยุด
* เซตของสายอักขระใหญ่ (maximal string) สุดของอักขระ[[แอสกี]]อักษรเลขในบรรทัดต่อไป<br> the set of maximal strings of [[alphanumeric]] [[ASCII]] characters on this line, i.e.,<br>คือเซต {the, set, of, maximal, strings, alphanumeric, ASCII, characters, on, this, line, i, e}

== รูปแบบการกำหนดคุณสมบัติของภาษา ==

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

คำถามทั่วไปเกี่ยวกับการกำหนดภาษาแต่ละรูปแบบมีดังเช่น

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

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

== การดำเนินการบนภาษา ==
การดำเนินการบนภาษาประกอบด้วยการดำเนินการของเซตชุดมาตรฐาน เช่น[[ยูเนียน]] [[อินเตอร์เซกชัน]] และ[[ส่วนเติมเต็ม]] กับการดำเนินการอีกชุดหนึ่งซึ่งเป็นการดำเนินการบนสายอักขระที่ประยุกต์ใช้แบบสมาชิกต่อสมาชิก (element-wise)

ตัวอย่าง: สมมุติให้ <math>L_1</math> และ <math>L_2</math> เป็นภาษาที่มีชุดตัวอักษร <math>\Sigma</math> ร่วมกัน
* ''[[การต่อกัน]]''ของทั้งสอง <math>L_1 \cdot L_2</math> ประกอบด้วยสายอักขระทั้งหมดในรูป <math>vw</math> โดย <math>v</math> เป็นสายอักขระจาก <math>L_1</math> และ <math>w</math> เป็นสายอักขระจาก <math>L_2</math>
* ''อินเตอร์เซกชัน''หรือ''ส่วนร่วม''ของทั้งสอง <math>L_1 \cap L_2</math> ประกอบด้วยสายอักขระทั้งหมดที่มีอยู่ในทั้งสองภาษา
* ''ส่วนเติมเต็ม''ของ <math>L_1</math>: <math>\neg L_1</math> เทียบกับ <math>\Sigma</math> ประกอบด้วยสายอักขระทั้งหมดจาก <math>\Sigma</math> ที่ไม่มีอยู่ใน <math>L_1</math>
* [[คลีนสตาร์]]: ภาษาที่ประกอบด้วยคำทุกคำที่เกิดจากการต่อกันของคำจากภาษาต้นฉบับจำนวนศูนย์คำขึ้นไป
* ''การย้อนกลับ'':
** ให้ ''ε'' เป็นคำว่าง แล้ว <math>\varepsilon^R = \varepsilon</math> และ
** สำหรับคำไม่ว่างแต่ละคำ <math>w = \sigma_1 \cdots \sigma_n</math> (โดย <math>\sigma_1, \ldots, \sigma_n</math> เป็นสมาชิกของชุดตัวอักษรชุดหนึ่ง) ให้ <math>w^R = \sigma_n \cdots \sigma_1</math>
** ฉะนั้นแล้วสำหรับภาษา <math>L</math>, <math>L^R = \{ w^R \mid w \in L \}</math>
* [[การดำเนินการของสายอักขระ|สาทิสสัญฐานของสายอักขระ]] (String homomorphism)

[[การดำเนินการบนสายอักขระ]] (string operations) เหล่านี้ถูกใช้เพื่อสำรวจหา[[สมบัติการปิด]]ของภาษาหมวดหมู่หนึ่ง ภาษาหมวดหมู่หนึ่งมีสมบัติการปิดหรือ "ปิด" ภายใต้การดำเนินการอย่างหนึ่ง เมื่อกระทำกับภาษาในหมวดหมู่นั้นแล้วได้ผลลัพธ์เป็นภาษาในหมวดหมู่เดิม ตัวอย่างเช่น [[ภาษาไม่พึ่งบริบท]]ซึ่งปิดภายใต้การดำเนินการยูเนียน ต่อกัน และส่วนร่วมกับ[[ภาษาปรกติ]] แต่ไม่ปิดภายใต้การดำเนินการส่วนร่วมหรือส่วนเติมเต็ม ทฤษฎีของ[[โคน (ภาษารูปนัย)|ทริโอ]] (cone (formal languages)) และ[[ตระกูลนามธรรมของภาษา]] (abstract family of languages) ศึกษาเกี่ยวกับสมบัติการปิดของภาษา<ref>{{harvtxt|Hopcroft|Ullman|1979}}, Chapter 11: Closure properties of families of languages.</ref>

:{| class="wikitable"
|+ align="top"|สมบัติการปิดของตระกูลภาษาต่าง ๆ ตามฮอปครอฟท์และอูลมันน์<br>(<math>L_1</math> ดำเนินการ <math>L_2</math> ซึ่งทั้ง <math>L_1</math> และ <math>L_2</math> อยู่ในตระกูลภาษาเดียวกันตามแต่ละสดมภ์) 
|-
! การดำเนินการ
!
! [[ภาษาปรกติ|ปรกติ]]
! [[ภาษาไม่พึ่งบริบทเชิงกำหนด|DCFL]]
! [[ภาษาไม่พึ่งบริบท|CFL]]
! [[ภาษาดรรชนี|IND]]
! [[ภาษาไวต่อบริบท|CSL]]
! [[ภาษาเรียกซ้ำ|เรียกซ้ำ]]
! [[ภาษานับได้แบบเรียกซ้ำ|RE]]
|-
|[[ยูเนียน]]
|<math>L_1 \cup L_2 = \{w \mid w \in L_1 \lor w \in L_2\} </math>
| {{Yes}}
| {{No}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
|-
|[[อินเตอร์เซกชัน]]
|<math>L_1 \cap L_2 = \{w \mid w \in L_1 \land w \in L_2\}</math>
| {{Yes}}
| {{No}}
| {{No}}
| {{No}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
|-
|[[ส่วนเติมเต็ม]]
|<math>\neg L_1 = \{w \mid w \not\in L_1\}</math>
| {{Yes}}
| {{Yes}}
| {{No}}
| {{No}}
| {{Yes}}
| {{Yes}}
| {{No}}
|-
|[[การต่อกัน]]
|<math>L_1\cdot L_2 = \{wz \mid w \in L_1 \land z \in L_2\}</math>
| {{Yes}}
| {{No}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
|-
|คลีนสตาร์
|<math>L_1^{*} = \{\varepsilon\} \cup \{wz \mid w \in L_1 \land z \in L_1^{*}\}</math>
| {{Yes}}
| {{No}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
|-
|สาทิสสัญฐาน (ของสายอักขระ), <math>h(L)</math>
|<math>h(L_1) = \{h(w) \mid w \in L_1\}</math>
| {{Yes}}
| {{No}}
| {{Yes}}
| {{Yes}}
| {{No}}
| {{No}}
| {{Yes}}
|-
|สาทิสสัญฐาน (ของสายอักขระ) ไร้ ε, <math>h(L)</math>
|<math>h(L_1) = \{h(w) \mid w \in L_1\}</math>
| {{Yes}}
| {{No}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
|-
|การแทนที่, <math>\varphi(L)</math>
|<math>\varphi(L_1) = \bigcup_{\sigma_1 \cdots \sigma_n \in L_1} \varphi(\sigma_1) \cdot \ldots \cdot \varphi(\sigma_n)</math>
| {{Yes}}
| {{No}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{No}}
| {{Yes}}
|-
|สาทิสสัญฐานผกผัน, <math>h^{-1}(L)</math>
|<math>h^{-1}(L_1) = \bigcup_{w \in L_1} h^{-1}(w)</math>
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
|-
|การย้อนกลับ
|<math>L^R = \{w^R \mid w \in L\} </math>
| {{Yes}}
| {{No}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
|-
|อินเตอร์เซกชันกับ[[ภาษาปรกติ]] <math>R</math>
|<math>L \cap R = \{w \mid w \in L \land w \in R\}</math>
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
<!--
|-
|Min
|
| {{Yes}}
| {{Yes}}
| {{No}}
| {{?}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
|-
|Max
|
| {{Yes}}
| {{Yes}}
| {{No}}
| {{?}}
| {{No}}
| {{No}}
| {{No}}
|-
|Init
|
| {{Yes}}
| {{No}}
| {{Yes}}
| {{?}}
| {{No}}
| {{No}}
| {{Yes}}
|-
|Cycle
|
| {{Yes}}
| {{No}}
| {{Yes}}
| {{?}}
| {{Yes}}
| {{Yes}}
| {{Yes}}
|-
|Shuffle
|
| {{Yes}}
| {{?}}
| {{Yes}}
| {{?}}
| {{?}}
| {{?}}
| {{Yes}}
|-
|Perfect Shuffle
|
| {{Yes}}
| {{?}}
| {{?}}
| {{?}}
| {{?}}
| {{?}}
| {{Yes}}
-->
|}

== การประยุกต์ใช้ ==

=== ภาษาโปรแกรม ===
{{Main|วากยสัมพันธ์ (ภาษาโปรแกรม)|คอมไพเลอร์คอมไพเลอร์}}

''คอมไพเลอร์'' หรือโปรแกรมแปลโปรแกรมมีส่วนประกอบที่ชัดเจนอยู่สองส่วน คือ[[การวิเคราะห์ศัพท์|ตัววิเคราะห์ศัพท์]] (Lexical analysis) ที่จะระบุโทเค็นของไวยากรณ์ของภาษาโปรแกรมเช่น [[ตัวระบุ]] (identifier) หรือ[[คำสงวน]] [[ค่าคงตัว (การเขียนโปรแกรมคอมพิวเตอร์)|ค่าคงตัว]] (Literal) ตัวเลขและสายอักขระ เครื่องหมายวรรคตอนและสัญลักษณ์ตัวดำเนินการ ซึ่งก็ถูกกำหนดอีกทีโดยภาษารูปนัยที่เรียบง่ายกว่าซึ่งโดยทั่วไปก็ทำขึ้นด้วย[[นิพจน์ปรกติ]] ส่วนนี้ถูกสร้างขึ้นด้วยเครื่องมือแบบ [[Lex (ซอฟท์แวร์)|<code>lex</code>]] (Lex (software)) และส่วนที่สองคือ[[การแจงส่วน|ตัวแจงส่วน]]ที่จะทดลองตัดสินว่าโปรแกรมต้นฉบับนั้นสมเหตุสมผลทางวากยสัมพันธ์หรือไม่ หมายความว่าโปรแกรมต้นฉบับนั้นจัดดีแล้วตามไวยากรณ์ของภาษาโปรแกรมที่คอมไพเลอร์ถูกสร้างขึ้นมาหรือไม่ ส่วนนี้ถูกสร้างขึ้นด้วย[[คอมไพเลอร์คอมไพเลอร์|ตัวสร้างตัวแจงส่วน]] (compiler-compiler) เช่น<code>[[yacc]]</code> 

คอมไพเลอร์ทำหน้าที่มากกว่าการแจงส่วน[[รหัสต้นฉบับ]] แต่ยังแปลรหัสให้อยู่ในรูปแบบสั่งทำการรูปแบบหนึ่งด้วย ดังนั้นตัวแจงส่วนจึงให้คำตอบเป็นใช่-ไม่ใช่มากกว่าหนึ่งคำตอบ ซึ่งปกติเป็น[[ต้นไม้วากยสัมพันธ์แบบนามธรรม]] (abstract syntax tree) ที่คอมไพเลอร์นำมาใช้ในขั้นต่อ ๆ มาเพื่อสุดท้ายผลิต[[ไฟล์สั่งทำการ]]ขึ้นจาก[[รหัสเครื่อง]]ที่จะทำการบน[[ฮาร์ดแวร์คอมพิวเตอร์|ฮาร์ดแวร์]]โดยตรง หรือจาก[[รหัสไบต์]]ที่ต้องใช้[[เครื่องเสมือน]] (virtual machine) เพื่อทำการ

=== ทฤษฎี ระบบ และการพิสูจน์เชิงรูปนัย ===
[[File:Formal languages.svg|thumb|300px|right|แผนภาพนี้แสดงถึงการแบ่งหมวดหมู่เชิง[[วากยสัมพันธ์ (ตรรกศาสตร์)|วากยสัมพันธ์]]ภายใน[[ระบบรูปนัย]] [[สายอักขระ|สายอักขระ]] (Strings of symbols) สามารถถูกแบ่งออกได้อย่างกว้าง ๆ เป็นสายอักขระที่ไม่ได้ความกับ[[สูตรที่จัดดีแล้ว]] (well-formed formula) และเซตของสูตรที่จัดดีแล้วสามารถถูกแบ่งออกเป็นอันที่เป็น[[ทฤษฎีบท]] (theorem) กับที่ไม่เป็นทฤษฎีบท]]

{{Main|ทฤษฎี (คณิตตรรกศาสตร์)|ระบบรูปนัย}}

ใน[[คณิตตรรกศาสตร์]] ''ทฤษฎีรูปนัย'' (formal theory) คือชุดของ[[ประโยค (คณิตตรรกศาสตร์)|ประโยค]]ในภาษารูปนัยภาษาหนึ่ง

''ระบบรูปนัย'' (เรียกอีกอย่างว่า ''แคลคูลัสเชิงตรรกะ'' หรือ ''ระบบเชิงตรรกะ'') ประกอบด้วยภาษารูปนัยพร้อมกับ[[ระบบรูปนัย|ระบบนิรนัย]] (deductive system) ซึ่งอาจประกอบด้วย[[การเขียนใหม่|กฎการปริวรรต]] (rewriting) ชุดหนึ่งซึ่งสามารถถูกตีความเป็นกฎการอนุมานที่สมเหตุสมผลได้ หรือ[[สัจพจน์]]ชุดหนึ่ง หรือทั้งสองอย่าง ระบบรูปนัยถูกใช้เพื่อ[[ทฤษฎีการพิสูจน์|สืบ]] (proof theory) นิพจน์หนึ่งมาจากนิพจน์อื่น ๆ เราสามารถระบุภาษารูปนัยภาษาหนึ่งได้ผ่านสูตรของมัน แต่เราไม่สามารถทำได้อย่างเดียวกันกับระบบรูปนัยผ่านทฤษฎีบทของมัน ระบบรูปนัยสองระบบ <math>\mathcal{FS}</math> และ <math>\mathcal{FS'}</math> สามารถมีทฤษฎีบทที่เหมือนกันทั้งหมดได้ ถึงอย่างนั้นแล้วก็ยังต่างกันในแง่ทฤษฎีการพิสูจน์แง่ใดแง่หนึ่งอย่างมีนัยสำคัญ (เช่นสูตร A อาจเป็นผลพวงทางวากยสัมพันธ์ของสูตร B ในระบบหนึ่ง แต่ไม่ได้เป็นในอีกระบบหนึ่ง)

''การพิสูจน์เชิงรูปนัย'' ({{langx|en|Formal proof}}) หรือ ''การสืบสมุฏฐาน'' ({{langx|en|Derivation}}) เป็นลำดับจำกัดของสูตรที่จัดดีแล้ว (ซึ่งก็อาจตีความได้เป็นประโยค หรือ[[ประพจน์]]) ซึ่งแต่ละสูตรเป็นสัจพจน์ข้อหนึ่ง หรือตามจากสูตรที่มาก่อนในลำดับนั้นตาม[[กฎการอนุมาน]] (rule of inference) ประโยคสุดท้ายในลำดับนั้นเป็นทฤษฎีบทของระบบรูปนัยระบบหนึ่ง การพิสูจน์เชิงรูปนัยนั้นมีประโยชน์เพราะทฤษฎีบทที่ได้มาสามารถตีความได้เป็นประพจน์จริง

==== การตีความและตัวแบบ ====
{{main|อรรถศาสตร์ของตรรกศาสตร์||การตีความ (ตรรกศาสตร์)|ทฤษฎีตัวแบบ}}

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

[[อรรถศาสตร์ของตรรกศาสตร์|อรรถศาสตร์รูปนัย]] (semantics of logic) เป็นการศึกษาเกี่ยวกับการตีความภาษารูปนัย ซึ่งมักถูกทำในแง่ของทฤษฎีตัวแบบในคณิตตรรกศาสตร์ พจน์ต่าง ๆ ที่มีอยู่ในสูตร ๆ หนึ่งนั้นถูกตีความเป็นวัตถุที่อยู่ภายใน[[โครงสร้าง (คณิตตรรกศาสตร์)|โครงสร้างทางคณิตศาสตร์]] (Structure (mathematical logic)) และกฎการตีความเชิงประกอบแบบถาวร (fixed compositional interpretation rule) จะตัดสินวิธีการที่จะสืบมาซึ่งค่าความจริงของสูตรหนึ่งจากการตีความพจน์ต่าง ๆ ของมัน ''ตัวแบบ'' ของสูตร ๆ หนึ่งหมายถึงรูปแบบของการตีความพจน์ต่าง ๆ ในสูตรที่จะทำให้สูตรนั้นเป็นจริง

== ดูเพิ่ม ==
* [[คณิตศาสตร์เชิงการจัดคำ]] (Combinatorics on words)
* [[โมนอยด์อิสระ]] (Free monoid)
* [[วิธีรูปนัย]] (Formal method)
* [[ไวยากรณ์|กรอบความคิดเชิงทฤษฏีด้านไวยากรณ์]] (Grammar framework)
* [[สัญกรณ์คณิตศาสตร์]]
* [[แถวลำดับแบบจับคู่]]
* [[สายอักขระ]]

== หมายเหตุ ==
{{NoteFoot}}

== อ้างอิง ==
=== อ้างอิง ===
{{รายการอ้างอิง}}

=== แหล่งข้อมูล ===
; งานที่อ้างอิง
{{เริ่มอ้างอิง}}
* {{wikicite |reference=[[John Hopcroft|John E. Hopcroft]] และ [[Jeffrey Ullman|Jeffrey D. Ullman]], ''[[Introduction to Automata Theory, Languages, and Computation]]'', Addison-Wesley Publishing, Reading Massachusetts, 1979. {{ISBN|81-7808-347-7}}.}}
{{จบอ้างอิง}}

; อ้างอิงทั่วไป
{{เริ่มอ้างอิง}}
* A. G. Hamilton, ''Logic for Mathematicians'', [[Cambridge University Press]], 1978, {{ISBN|0-521-21838-1}}.
* [[Seymour Ginsburg]], ''Algebraic and automata theoretic properties of formal languages'', North-Holland, 1975, {{ISBN|0-7204-2506-9}}.
* [[Michael A. Harrison]], ''Introduction to Formal Language Theory'', Addison-Wesley, 1978.
* {{cite book |last=Rautenberg |first=Wolfgang |author-link = Wolfgang Rautenberg |doi = 10.1007/978-1-4419-1221-3 |title = A Concise Introduction to Mathematical Logic |publisher=[[Springer Science+Business Media]] |location=[[New York City|New York]], NY |edition=3rd |isbn = 978-1-4419-1220-6 |year=2010 }}.
* [[Grzegorz Rozenberg]], [[Arto Salomaa]], ''Handbook of Formal Languages: Volume I-III'', Springer, 1997, {{ISBN|3-540-61486-9}}.
* Patrick Suppes, ''Introduction to Logic'', D. Van Nostrand, 1957, {{ISBN|0-442-08072-7}}.
{{จบอ้างอิง}}

==แหล่งข้อมูลอื่น==
{{Commonscat|Formal languages|ภาษารูปนัย}}
*{{springer|title=Formal language|id=p/f040830}}
*[[University of Maryland, Baltimore|University of Maryland]], [http://www.csee.umbc.edu/help/theory/lang_def.shtml นิยามภาษารูปนัย] {{Webarchive|url=https://web.archive.org/web/20080216230918/http://www.csee.umbc.edu/help/theory/lang_def.shtml |date=2008-02-16 }}
* James Power, [http://www.cs.nuim.ie/~jpower/Courses/parsing/ "Notes on Formal Language Theory and Parsing"] {{Webarchive|url=https://web.archive.org/web/20071121142736/http://www.cs.nuim.ie/~jpower/Courses/parsing/ |date=2007-11-21 }}, 29 พฤศจิกายน ค.ศ. 2002.
* ฉบับร่างของบทบางบทใน "Handbook of Formal Language Theory", Vol. 1–3, G. Rozenberg and A. Salomaa (eds.), [[Springer Verlag]], (ค.ศ. 1997):
** Alexandru Mateescu และ Arto Salomaa, [https://www.cs.cmu.edu/~lkontor/noam/Mateescu-Salomaa.pdf "Preface" in Vol.1, pp. v–viii, and "Formal Languages: An Introduction and a Synopsis", Chapter 1 in Vol. 1, pp.1–39]
** Sheng Yu, [http://www.csd.uwo.ca/~syu/public/draft.ps "Regular Languages", Chapter 2 in Vol. 1] {{Webarchive|url=https://web.archive.org/web/20060519210749/http://www.csd.uwo.ca/~syu/public/draft.ps |date=2006-05-19 }}
** Jean-Michel Autebert, Jean Berstel, Luc Boasson, [http://citeseer.ist.psu.edu/248295.html "Context-Free Languages and Push-Down Automata", Chapter 3 in Vol. 1]
** Christian Choffrut และ Juhani Karhumäki, [http://www.liafa.jussieu.fr/~cc/PUBLICATIONS/CKTUCS.PS.gz "Combinatorics of Words", Chapter 6 in Vol. 1]
** Tero Harju และ Juhani Karhumäki, [http://users.utu.fi/harju/articles/morph.pdf "Morphisms", Chapter 7 in Vol. 1, pp. 439–510]
** Jean-Eric Pin, [http://www.liafa.jussieu.fr/~jep/PDF/HandBook.pdf "Syntactic semigroups", Chapter 10 in Vol. 1, pp. 679–746]
** M. Crochemore และ C. Hancart, [http://www-igm.univ-mlv.fr/~mac/REC/DOC/B4.ps "Automata for matching patterns", Chapter 9 in Vol. 2]
** Dora Giammarresi, Antonio Restivo, [https://web.archive.org/web/20071008170115/http://bruno.maitresdumonde.com/optinfo/Spe-MP/dmds1998/2dlang/giammaresi-restivo-paper.ps "Two-dimensional Languages", Chapter 4 in Vol. 3, pp. 215–267]

{{ไวยากรณ์และภาษารูปนัย}}
{{คณิตตรรกศาสตร์}}
{{Authority control}}

{{DEFAULTSORT:ภาษารูปนัย}}
[[หมวดหมู่:ภาษารูปนัย]]
[[หมวดหมู่:วิทยาการคอมพิวเตอร์เชิงทฤษฎี]]
[[หมวดหมู่:คณิตศาสตร์เชิงการจัดคำ]]