ในตรรกศาสตร คณ ตศาสตร ภาษาศาสตร และว ทยาการคอมพ วเตอร ภาษาร ปน ย อ งกฤษ Formal language บ างก ว า ภาษาแบบแผน ประกอบด วยค

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

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

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

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

ประวัติ

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

คำจากชุดตัวอักษร

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

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

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

บทนิยาม

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

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

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

ตัวอย่าง

ข้อความดังต่อไปนี้เป็นกฎที่บรรยายถึงภาษารูปนัย $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" เท่านั้น)
เซตของโปรแกรมที่ถูกต้องทางวากยสัมพันธ์ทุกโปรแกรมในภาษาโปรแกรมภาษาหนึ่ง (ซึ่งปกติวากยสัมพันธ์ของภาษานั้นถูกให้นิยามด้วย (context-free grammar))
เซตของอินพุตที่ทำให้เครื่องทัวริงเครื่องหนึ่งหยุด
เซตของสายอักขระใหญ่ (maximal string) สุดของอักขระแอสกีอักษรเลขในบรรทัดต่อไป
the set of maximal strings of 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) ศึกษาเกี่ยวกับสมบัติการปิดของภาษา

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

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

ภาษาโปรแกรม

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

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

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

แผนภาพนี้แสดงถึงการแบ่งหมวดหมู่เชิงภายใน สายอักขระ (Strings of symbols) สามารถถูกแบ่งออกได้อย่างกว้าง ๆ เป็นสายอักขระที่ไม่ได้ความกับ (well-formed formula) และเซตของสูตรที่จัดดีแล้วสามารถถูกแบ่งออกเป็นอันที่เป็นทฤษฎีบท (theorem) กับที่ไม่เป็นทฤษฎีบท

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

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

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

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

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

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

ดูเพิ่ม

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

หมายเหตุ

แปลจาก "formal language of pure language."
ตัวอย่างเช่น ชุดตัวอักษรที่ใช้แสดง (first-order logic) นั้นนอกจากสัญลักษณ์อย่าง ∧, ¬, ∀ และวงเล็บแล้ว ก็ยังมีสมาชิกตัวอักษรอื่น ๆ อีกมากมาย x₀, x₁, x₂, … จำนวนนับไม่ถ้วนที่ทำหน้าที่เป็นตัวแปร

อ้างอิง

ดูที่ อาทิ Reghizzi, Stefano Crespi (2009), Formal Languages and Compilation, Texts in Computer Science, Springer, p. 8, ISBN , An alphabet is a finite set.
Martin Davis (1995). "Influences of Mathematical Logic on Computer Science". ใน Rolf Herken (บ.ก.). The universal Turing machine: a half-century survey. Springer. p. 290. ISBN .
Hopcroft & Ullman (1979), Chapter 11: Closure properties of families of languages.

แหล่งข้อมูล

งานที่อ้างอิง

และ , , Addison-Wesley Publishing, Reading Massachusetts, 1979. ISBN .

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

A. G. Hamilton, Logic for Mathematicians, , 1978, ISBN .
, Algebraic and automata theoretic properties of formal languages, North-Holland, 1975, ISBN .
, Introduction to Formal Language Theory, Addison-Wesley, 1978.
(2010). A Concise Introduction to Mathematical Logic (3rd ed.). New York, NY: . doi:10.1007/978-1-4419-1221-3. ISBN ..
, , Handbook of Formal Languages: Volume I-III, Springer, 1997, ISBN .
Patrick Suppes, Introduction to Logic, D. Van Nostrand, 1957, ISBN .

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

Hazewinkel, Michiel, บ.ก. (2001), "Formal language", , , ISBN
, นิยามภาษารูปนัย
James Power, "Notes on Formal Language Theory and Parsing" 2007-11-21 ที่ เวย์แบ็กแมชชีน, 29 พฤศจิกายน ค.ศ. 2002.
ฉบับร่างของบทบางบทใน "Handbook of Formal Language Theory", Vol. 1–3, G. Rozenberg and A. Salomaa (eds.), , (ค.ศ. 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 2006-05-19 ที่ เวย์แบ็กแมชชีน
- 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,

[2] แปลจาก "formal language of pure language."

[4] ตัวอย่างเช่น ชุดตัวอักษรที่ใช้แสดง (first-order logic) นั้นนอกจากสัญลักษณ์อย่าง ∧, ¬, ∀ และวงเล็บแล้ว ก็ยังมีสมาชิกตัวอักษรอื่น ๆ อีกมากมาย x₀, x₁, x₂, … จำนวนนับไม่ถ้วนที่ทำหน้าที่เป็นตัวแปร

[1] ดูที่ อาทิ Reghizzi, Stefano Crespi (2009), Formal Languages and Compilation, Texts in Computer Science, Springer, p. 8, ISBN , An alphabet is a finite set.

[Herken1279-3] Martin Davis (1995). "Influences of Mathematical Logic on Computer Science". ใน Rolf Herken (บ.ก.). The universal Turing machine: a half-century survey. Springer. p. 290. ISBN .

[5] Hopcroft & Ullman (1979), Chapter 11: Closure properties of families of languages.