ภาษารูปนัย

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

ในตรรกศาสตร์, คณิตศาสตร์, ภาษาศาสตร์ และวิทยาการคอมพิวเตอร์ **ภาษารูปนัย** () บ้างก็ว่า **ภาษาแบบแผน** ประกอบด้วยคำซึ่งสะกดด้วยตัวอักษร (symbol (formal)) จากชุดตัวอักษรชุดหนึ่ง และจัดดีแล้ว (well-formedness) ตามกฎชุดหนึ่ง

ชุดตัวอักษรของภาษารูปนัยภาษาหนึ่งประกอบด้วยสัญลักษณ์, ตัวอักษร หรือโทเค็น ซึ่งต่อกัน (concatenate) เป็นสายอักขระในภาษานั้น สายอักขระแต่ละสายซึ่งต่อกันขึ้นจากสัญลักษณ์ในชุดตัวอักษรนั้นเรียกว่าคำ และบางครั้งคำในภาษารูปนัยภาษาหนึ่งก็เรียกว่า*คำที่จัดดีแล้ว* หรือ *[[สูตรที่จัดดีแล้ว]]* (well-formed formula) ภาษารูปนัยถูกกำหนดโดยไวยากรณ์รูปนัย (formal grammar) เช่นไวยากรณ์ปรกติ (regular grammar) หรือไวยากรณ์ไม่พึ่งบริบท (context-free grammar) ซึ่งประกอบด้วยกฎการจัดรูป (formation rule) ของตัวเอง

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

## ประวัติ
คำว่าภาษารูปนัย (formal language) อาจถูกใช้เป็นครั้งแรกใน *[[Begriffsschrift]]* (แปลว่า การเขียนแนวคิด, concept writing) โดย ก็อทโลพ เฟรเกอ (Gottlob Frege) ในปี ค.ศ. 1879 ซึ่งอธิบายถึง "ภาษารูปนัยของภาษาบริสุทธิ์"

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

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

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

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

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

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

## ตัวอย่าง

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

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

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

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

การดำเนินการบนสายอักขระ (string operations) เหล่านี้ถูกใช้เพื่อสำรวจหาสมบัติการปิดของภาษาหมวดหมู่หนึ่ง ภาษาหมวดหมู่หนึ่งมีสมบัติการปิดหรือ "ปิด" ภายใต้การดำเนินการอย่างหนึ่ง เมื่อกระทำกับภาษาในหมวดหมู่นั้นแล้วได้ผลลัพธ์เป็นภาษาในหมวดหมู่เดิม ตัวอย่างเช่น ภาษาไม่พึ่งบริบทซึ่งปิดภายใต้การดำเนินการยูเนียน ต่อกัน และส่วนร่วมกับภาษาปรกติ แต่ไม่ปิดภายใต้การดำเนินการส่วนร่วมหรือส่วนเติมเต็ม ทฤษฎีของทริโอ (cone (formal languages)) และตระกูลนามธรรมของภาษา (abstract family of languages) ศึกษาเกี่ยวกับสมบัติการปิดของภาษา

:

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

### ภาษาโปรแกรม

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

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

### ทฤษฎี ระบบ และการพิสูจน์เชิงรูปนัย

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

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

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

#### การตีความและตัวแบบ

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

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

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

## หมายเหตุ

## อ้างอิง
### อ้างอิง

### แหล่งข้อมูล
; งานที่อ้างอิง

* 

; อ้างอิงทั่วไป

* A. G. Hamilton, *Logic for Mathematicians*, Cambridge University Press, 1978, .
* Seymour Ginsburg, *Algebraic and automata theoretic properties of formal languages*, North-Holland, 1975, .
* Michael A. Harrison, *Introduction to Formal Language Theory*, Addison-Wesley, 1978.
* .
* Grzegorz Rozenberg, Arto Salomaa, *Handbook of Formal Languages: Volume I-III*, Springer, 1997, .
* Patrick Suppes, *Introduction to Logic*, D. Van Nostrand, 1957, .

## แหล่งข้อมูลอื่น

*
*University of Maryland, นิยามภาษารูปนัย 
* James Power, "Notes on Formal Language Theory and Parsing" , 29 พฤศจิกายน ค.ศ. 2002.
* ฉบับร่างของบทบางบทใน "Handbook of Formal Language Theory", Vol. 1–3, G. Rozenberg and A. Salomaa (eds.), Springer Verlag, (ค.ศ. 1997):
** Alexandru Mateescu และ Arto Salomaa, "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, "Regular Languages", Chapter 2 in Vol. 1 
** Jean-Michel Autebert, Jean Berstel, Luc Boasson, "Context-Free Languages and Push-Down Automata", Chapter 3 in Vol. 1
** Christian Choffrut และ Juhani Karhumäki, "Combinatorics of Words", Chapter 6 in Vol. 1
** Tero Harju และ Juhani Karhumäki, "Morphisms", Chapter 7 in Vol. 1, pp. 439–510
** Jean-Eric Pin, "Syntactic semigroups", Chapter 10 in Vol. 1, pp. 679–746
** M. Crochemore และ C. Hancart, "Automata for matching patterns", Chapter 9 in Vol. 2
** Dora Giammarresi, Antonio Restivo, "Two-dimensional Languages", Chapter 4 in Vol. 3, pp. 215–267

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