در منطق، ریاضیات، علوم رایانه و زبانشناسی، زبان صوری مجموعهای از رشتهها (strings) است که نمادهای آنها از مجموعهای به نام الفبا (alphabet) گرفته میشوند.
الفبای یک زبان صوری از نمادهایی تشکیل شده است که با الحاق (concatenation) به یکدیگر، رشتهها (که «واژه» نیز نامیده میشوند) را پدید میآورند. واژههایی که به یک زبان صوری خاص تعلق دارند، گاه واژههای خوشساخت (well-formed words) نامیده میشوند. یک زبان صوری معمولاً بهوسیلهٔ یک دستور زبان صوری (formal grammar)، مانند دستور زبان منظم (regular grammar) یا دستور زبان مستقل از متن (context-free grammar)، تعریف میشود.
در علوم رایانه، زبانهای صوری از جمله مبنای تعریف دستور زبانهای زبانهای برنامهنویسی و نیز زبانهای طبیعی کنترلشده (controlled natural languages) هستند؛ یعنی نسخههای صورتبندیشدهای از زیرمجموعههایی از زبانهای طبیعی. در نظریهٔ پیچیدگی محاسباتی، مسائل تصمیم (decision problems) معمولاً بهصورت زبانهای صوری تعریف میشوند و ردههای پیچیدگی (complexity classes) نیز بهصورت مجموعهٔ زبانهای صوریای تعریف میشوند که ماشینهایی با توان محاسباتی محدود قادر به تجزیه و تحلیل (parse) آنها هستند. در منطق و مبانی ریاضیات، زبانهای صوری برای بازنمایی نحو (syntax) دستگاههای اصل موضوعی (axiomatic systems) به کار میروند و صورتگرایی ریاضی (mathematical formalism) دیدگاهی فلسفی است که بر اساس آن، تمام ریاضیات را میتوان به دستکاری نحوی زبانهای صوری فروکاست.
نظریهٔ زبانهای صوری (formal language theory) عمدتاً به مطالعهٔ جنبههای صرفاً نحوی این زبانها میپردازد؛ یعنی الگوهای ساختاری درونی آنها. این شاخه از دل زبانشناسی پدید آمد و هدف آن، فهم نظمها و قاعدهمندیهای نحوی زبانهای طبیعی بود.
تاریخچه
در قرن هفدهم، گوتفرید لایبنیتس، زبان جهانی (characteristica universalis) را تصور و توصیف کرد؛ یک زبان جهانی و صوری که از تصویرنگاشتها (pictographs) استفاده میکرد. بعدها، کارل فریدریش گاوس مسئلهٔ کدهای گاوسی (Gauss codes) را بررسی کرد.
در اواسط قرن نوزدهم، جورج بول حوزهٔ جبر بولی (Boolean algebra) را بنیان گذاشت؛ جبر بولی روشی صوری برای توصیف اعمال منطقی با استفاده از ارزشهای صدق (truth values) و عملگرهای مجموعهای (set operators) است. او در اثر خود با عنوان پژوهشی دربارهٔ قوانین اندیشه (An Investigation of The Laws of Thought) نشان داد که استدلال منطقی را میتوان از طریق معادلات نمادین بیان و دستکاری کرد.
گوتلوب فرگه تلاش کرد ایدههای لایبنیتس را از طریق یک نظام نمادگذاری تحقق بخشد؛ نظامی که نخست در اثر مفهومنگاشت (Begriffsschrift) در سال ۱۸۷۹ طرح شد و سپس در اثر دو جلدی او با عنوان قوانین بنیادین حساب (Grundgesetze der Arithmetik) در سالهای ۱۸۹۳ و ۱۹۰۳ بهطور کاملتر توسعه یافت. این اثر یک «زبان صوریِ زبان ناب» را توصیف میکرد.
در نیمهٔ نخست قرن بیستم، چندین تحول مرتبط با زبانهای صوری رخ داد. آکسل توئه بین سالهای ۱۹۰۶ تا ۱۹۱۴ چهار مقاله دربارهٔ واژهها و زبان منتشر کرد. آخرین مقالهٔ او چیزی را معرفی کرد که امیل پست بعدها آن را نظامهای توئه (Thue Systems) نامید و نمونهای اولیه از یک مسئلهٔ حلناپذیر (undecidable problem) ارائه داد.
پست بعدها از این مقاله بهعنوان مبنای اثباتی در سال ۱۹۴۷ استفاده کرد که نشان میداد «مسئلهٔ واژه برای نیمگروهها بهصورت بازگشتی حلناپذیر است»؛ و سپس نظام متعارف پست (Post canonical system) را برای ایجاد زبانهای صوری ابداع کرد.
در سال ۱۹۰۷، لئوناردو تورس ای کوئهبدو یک زبان صوری برای توصیف نقشههای مکانیکی (دستگاههای مکانیکی) در وین معرفی کرد. او مقالهای با عنوان «دربارهٔ نظامی از نمادگذاریها و نشانهها که برای آسانسازی توصیف ماشینها طراحی شده است» (Sobre un sistema de notaciones y símbolos destinados a facilitar la descripción de las máquinas) منتشر کرد.
هاینتس زمانک این نظام را معادل یک زبان برنامهنویسی برای کنترل عددی ماشینهای ابزار دانست.
نوآم چامسکی یک بازنمایی انتزاعی از زبانهای صوری و طبیعی ارائه کرد که با عنوان سلسلهمراتب چامسکی (Chomsky hierarchy) شناخته میشود.
در سال ۱۹۵۹، جان بکوس صورت بکوس–نائور (Backus–Naur form) را برای توصیف نحو یک زبان برنامهنویسی سطح بالا توسعه داد. این کار پس از فعالیت او در ایجاد زبان برنامهنویسی فورترن (FORTRAN) انجام شد.
پیتر نائور دبیر و ویراستار گزارش ALGOL60 بود؛ گزارشی که در آن از صورت بکوس–نائور برای توصیف بخش صوری زبان ALGOL60 استفاده کرد.
واژهها بر روی یک الفبا
در زمینهٔ زبانهای صوری، الفبا (alphabet) میتواند هر مجموعهای باشد و عناصر آن را حروف (letters) مینامند. یک الفبا ممکن است شامل تعداد نامتناهی عنصر نیز باشد.(برای مثال، منطق محمولات مرتبهٔ اول معمولاً با الفبایی بیان میشود که علاوه بر نمادهایی مانند ∧، ¬، ∀ و پرانتزها، شامل بینهایت نماد از قبیل x₀، x₁، x₂، … نیز هست که نقش متغیرها را ایفا میکنند.) با این حال، بیشتر تعریفهای نظریهٔ زبانهای صوری، الفباهایی را در نظر میگیرند که متناهیاند و بسیاری از نتایج این نظریه نیز تنها دربارهٔ چنین الفباهایی برقرار است. در بسیاری از موارد، مناسب است که از یک الفبا به معنای متعارف کلمه، یا بهطور کلی از هر سامانهٔ کدگذاری نویسه (character encoding) متناهی، مانند ASCII یا Unicode، استفاده شود.
واژه (word) بر روی یک الفبا، هر دنبالهٔ متناهی (یعنی رشته (string)) از حروف آن الفبا است. مجموعهٔ همهٔ واژههای ساختهشده بر روی یک الفبا با نماد Σ معمولاً با Σ* نمایش داده میشود (که در آن از ستارهٔ کلینی (Kleene star) استفاده شده است). طول یک واژه برابر است با تعداد حروفی که آن واژه از آنها تشکیل شده است. برای هر الفبا، تنها یک واژه با طول صفر وجود دارد که آن را واژهٔ تهی (empty word) مینامند و معمولاً با نمادهای e، ε، λ یا Λ نمایش میدهند. با عمل الحاق (concatenation) میتوان دو واژه را به یکدیگر متصل کرد و واژهٔ جدیدی ساخت که طول آن برابر با مجموع طول دو واژهٔ اولیه است. همچنین، حاصل الحاق هر واژه با واژهٔ تهی، همان واژهٔ اولیه خواهد بود.
در برخی کاربردها، بهویژه در منطق، به جای واژهٔ «الفبا» از اصطلاح واژگان (vocabulary) استفاده میشود و به جای «واژه» نیز از اصطلاحات فرمول (formula) یا جمله (sentence) بهره میگیرند. در این صورت، استعارهٔ «حرف/واژه» جای خود را به استعارهٔ «واژه/جمله» میدهد.
تعریف
با فرض اینکه $\Sigma$ یک مجموعهٔ ناتهی باشد، یک زبان صوری $L$ بر روی $\Sigma$، زیرمجموعهای از $\Sigma^*$ است؛ که در آن $\Sigma^*$ مجموعهٔ تمام واژههای متناهیِ ممکن بر روی $\Sigma$ است. مجموعهٔ $\Sigma$ را الفبای $L$ مینامیم.
از سوی دیگر، اگر یک زبان صوری $L$ بر روی $\Sigma$ داشته باشیم، یک واژهٔ $w \in \Sigma^{*}$ زمانی خوشساخت (well-formed) است که:
\[ w \in L \]باشد. به همین ترتیب، یک عبارت$ E \subseteq \Sigma^{*} $ نیز خوشساخت است اگر:
\[ E \subseteq L \]باشد. گاهی یک زبان صوری $L$ بر روی $\Sigma$، دارای مجموعهای از قواعد و محدودیتهای روشن برای ایجاد همهٔ واژههای خوشساخت ممکن از میان $\Sigma^*$ است.
در علوم رایانه و ریاضیات، که معمولاً با زبانهای طبیعی سروکار ندارند، صفت «صوری» (formal) اغلب به دلیل زائد بودن حذف میشود. از سوی دیگر، هنگامی که الفبای $\Sigma$ از زمینهٔ بحث روشن باشد، میتوان صرفاً گفت «زبان صوری $L$».
اگرچه نظریهٔ زبانهای صوری معمولاً به زبانهای صوریای میپردازد که با برخی قواعد نحوی توصیف میشوند، تعریف واقعی مفهوم «زبان صوری» تنها همان چیزی است که در بالا بیان شد: مجموعهای (که ممکن است نامتناهی باشد) از رشتههای با طول متناهی که از یک الفبای معین ساخته شدهاند؛ نه بیشتر و نه کمتر.
در عمل، زبانهای بسیاری وجود دارند که میتوان آنها را با قواعد توصیف کرد؛ مانند زبانهای منظم (regular languages) یا زبانهای مستقل از متن (context-free languages). مفهوم دستور زبان صوری (formal grammar) ممکن است به مفهوم شهودی «زبان» نزدیکتر باشد؛ یعنی زبانی که با قواعد نحوی توصیف شده است. با نوعی تسامح در تعریف، معمولاً یک زبان صوری خاص را همراه با یک دستور زبان صوری در نظر میگیرند که آن را توصیف میکند.
مثالها
قواعد زیر یک زبان صوری $L$ را بر روی الفبای $\Sigma = {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$ قرار ندارد. این زبان صوری، اعداد طبیعی، جمعهای خوشساخت و تساویهای حاصل از جمعِ خوشساخت را بیان میکند؛ اما فقط آنچه را که این عبارات به لحاظ ظاهری دارند (یعنی نحو (syntax) آنها) بیان میکند، نه آنچه را که معنا میدهند (معناشناسی (semantics) آنها).
برای مثال، در هیچکدام از این قواعد اشارهای نشده است که «0» به معنای عدد صفر است، «+» به معنای عمل جمع است، یا اینکه «23+4=555» گزارهای نادرست است و مانند آن.
ساختها
برای زبانهای متناهی، میتوان همهٔ واژههای خوشساخت را بهصورت صریح فهرست کرد. برای مثال، میتوان زبانی مانند $L$ را به شکل زیر توصیف کرد:
$$ L = \{a, b, ab, cba\} $$حالت تباهیدهٔ (degenerate) این ساخت، زبان تهی (empty language) است که هیچ واژهای ندارد:
$$ L = \varnothing $$با این حال، حتی بر روی یک الفبای متناهی (و ناتهی) مانند $\Sigma = {a, b}$، تعداد نامتناهیای از واژههای با طول متناهی وجود دارند که میتوانند ساخته شوند؛ مانند:
«a»، «abb»، «ababba»، «aaababbbbaab»، …
بنابراین، زبانهای صوری معمولاً نامتناهی هستند و توصیف یک زبان صوری نامتناهی به سادگی نوشتن
$$ L = \{a, b, ab, cba\} $$نیست.
در ادامه چند نمونه از زبانهای صوری آمده است:
- $L = \Sigma^{*}$، یعنی مجموعهٔ تمام واژهها بر روی $\Sigma$.
- $L = {a}^{*} = {a^{n}}$، که در آن $n$ بر مجموعهٔ اعداد طبیعی تغییر میکند و «$a^{n}$» به معنای تکرار نماد «a» به تعداد $n$ بار است (این مجموعه شامل واژههایی است که فقط از نماد «a» تشکیل شدهاند).
- مجموعهٔ برنامههای دارای نحو صحیح در یک زبان برنامهنویسی معین (که نحو آن معمولاً بهوسیلهٔ یک دستور زبان مستقل از متن (context-free grammar) تعریف میشود).
- مجموعهٔ ورودیهایی که یک ماشین تورینگ معین بر روی آنها متوقف میشود.
- مجموعهٔ رشتههای بیشینه از نویسههای حرفی–عددی (alphanumeric) در قالب ASCII در این خط؛ یعنی مجموعهٔ:
صورتگراییهای مشخصسازی زبان
زبانهای صوری بهعنوان ابزارهایی در رشتههای مختلف مورد استفاده قرار میگیرند. با این حال، نظریهٔ زبانهای صوری بهندرت به زبانهای خاص میپردازد (مگر بهعنوان مثال)، بلکه عمدتاً به مطالعهٔ انواع مختلف صورتگراییها (formalisms) برای توصیف زبانها میپردازد.
برای مثال، یک زبان را میتوان به یکی از شیوههای زیر تعریف کرد:
- مجموعهٔ رشتههایی که توسط یک دستور زبان صوری (formal grammar) تولید میشوند؛
- مجموعهٔ رشتههایی که توسط یک عبارت منظم (regular expression) خاص توصیف یا با آن تطبیق داده میشوند؛
- مجموعهٔ رشتههایی که توسط یک ماشین (automaton)، مانند یک ماشین تورینگ (Turing machine) یا ماشین متناهیحالت (finite-state automaton)، پذیرفته میشوند؛
- مجموعهٔ رشتههایی که برای آنها یک رویهٔ تصمیم (decision procedure) ــ یعنی یک الگوریتم که مجموعهای از پرسشهای مرتبط با پاسخ «بله/خیر» را مطرح میکند ــ پاسخ «بله» تولید میکند.
پرسشهای معمول دربارهٔ چنین صورتگراییهایی عبارتاند از:
توان بیانی آنها چیست؟
(آیا صورتگرایی $X$ میتواند هر زبانی را که صورتگرایی $Y$ توصیف میکند، توصیف کند؟ آیا میتواند زبانهای دیگری را نیز توصیف کند؟)قابلیت تشخیصپذیری آنها چگونه است؟
(تصمیمگیری دربارهٔ اینکه آیا یک واژهٔ مشخص به زبانی تعلق دارد که توسط صورتگرایی $X$ توصیف شده است، چقدر دشوار است؟)قابلیت مقایسهٔ آنها چگونه است؟
(تصمیمگیری دربارهٔ اینکه آیا دو زبان ــ یکی توصیفشده با صورتگرایی $X$ و دیگری توصیفشده با صورتگرایی $Y$، یا دوباره با $X$ ــ در واقع یک زبان واحد هستند، چقدر دشوار است؟)
با کمال شگفتی، در بسیاری از موارد پاسخ این مسائل تصمیم چنین است: «اصلاً امکان انجام آن وجود ندارد» یا «هزینهٔ آن بسیار زیاد است» (همراه با توصیفی از میزان این هزینه). ازاینرو، نظریهٔ زبانهای صوری یکی از حوزههای کاربرد مهم نظریهٔ محاسبهپذیری (computability theory) و نظریهٔ پیچیدگی محاسباتی (computational complexity theory) به شمار میآید.
زبانهای صوری را میتوان بر اساس سلسلهمراتب چامسکی (Chomsky hierarchy) طبقهبندی کرد؛ این طبقهبندی بر پایهٔ توان بیانی دستور زبان مولد آنها و همچنین پیچیدگی ماشین تشخیصدهنده (recognizing automaton) آنها انجام میشود.
دستور زبانهای مستقل از متن (context-free grammars) و دستور زبانهای منظم (regular grammars) تعادلی مناسب میان توان بیانی و سهولت تجزیه و تحلیل نحوی (parsing) فراهم میکنند و در کاربردهای عملی بهطور گسترده مورد استفاده قرار میگیرند.
فرانحو
فرانحو (metasyntax) نحوی است که برای تعریف نحو یک زبان برنامهنویسی یا یک زبان صوری به کار میرود. فرانحو، ساختار و ترکیب مجاز عبارتها و جملههای یک فرازبان (metalanguage) را توصیف میکند؛ فرازبانی که برای توصیف یک زبان طبیعی یا یک زبان برنامهنویسی رایانهای مورد استفاده قرار میگیرد.
برخی از فرازبانهای صوری پرکاربرد برای زبانهای رایانهای عبارتاند از:
- صورت بکوس–نائور (Backus–Naur Form یا BNF)
- صورت بسطیافتهٔ بکوس–نائور (Extended Backus–Naur Form یا EBNF)
- نمادگذاری نحوی ویرث (Wirth Syntax Notation یا WSN)
- صورت افزودهٔ بکوس–نائور (Augmented Backus–Naur Form یا ABNF)
فرازبانها نیز هرکدام فرانحوی مخصوص به خود دارند که از نمادهای پایانهای (terminal symbols)، نمادهای ناپایانهای (nonterminal symbols) و فرانمادها (metasymbols) تشکیل شده است.
یک نماد پایانهای، مانند یک واژه یا یک توکن، ساختاری مستقل در زبانی است که در حال تعریف شدن است. یک نماد ناپایانهای نشاندهندهٔ یک مقولهٔ نحوی (syntactic category) است؛ مقولهای که یک یا چند ساختار معتبر عبارتی یا جملهای را تعریف میکند که از یک زیرمجموعهٔ $n$ عنصری تشکیل شدهاند.
فرانمادها اطلاعات نحوی لازم را برای اهداف دلالتگذاری (denotational purposes) در یک فرانحو مشخص فراهم میکنند. البته پایانهها، ناپایانهها و فرانمادها در همهٔ فرازبانها کاربرد ندارند.
معمولاً فرازبان مربوط به زبانهای در سطح توکن (که بهصورت رسمی زبانهای منظم (regular languages) نامیده میشوند) دارای نمادهای ناپایانه نیست؛ زیرا در این زبانهای منظم، مسئلهٔ تودرتویی (nesting) مطرح نیست.
زبان انگلیسی، هنگامی که بهعنوان فرازبانی برای توصیف برخی زبانها به کار میرود، دارای فرانماد نیست؛ زیرا تمام توضیحات را میتوان با استفاده از عبارتهای انگلیسی بیان کرد.
تنها برخی فرازبانهای صوری که برای توصیف زبانهای بازگشتی (که بهصورت رسمی زبانهای مستقل از متن (context-free languages) نامیده میشوند) به کار میروند، در فرانحو خود دارای هر سه دستهٔ نمادهای پایانهای، نمادهای ناپایانهای و فرانمادها هستند.
عملگرها بر روی زبانها
برخی عملگرها بر روی زبانها کاربرد گستردهای دارند. این عملگرها شامل عملگرهای استاندارد مجموعهای، مانند اجتماع (union)، اشتراک (intersection) و متمم (complement) هستند. دستهٔ دیگری از عملگرها، شامل اعمالِ جزءبهجزءِ عملگرهای مربوط به رشتهها است.
مثال: فرض کنید $L_1$ و $L_2$ زبانهایی بر روی یک الفبای مشترک $\Sigma$ باشند.
الحاق (concatenation) زبانهای $L_1$ و $L_2$، یعنی $L_1 \cdot L_2$، شامل تمام رشتههایی به شکل $vw$ است؛ بهگونهای که $v$ رشتهای از $L_1$ و $w$ رشتهای از $L_2$ باشد.
اشتراک $L_1 \cap L_2$ از زبانهای $L_1$ و $L_2$ شامل تمام رشتههایی است که در هر دو زبان وجود دارند.
متمم $\neg L_1$ از $L_1$ نسبت به $\Sigma$ شامل تمام رشتههای ساختهشده از $\Sigma$ است که در $L_1$ قرار ندارند.
ستارهٔ کلینی (Kleene star): زبانی شامل تمام واژههایی که از الحاق صفر یا تعداد بیشتری از واژههای موجود در زبان اصلی ساخته شدهاند.
وارونسازی (Reversal):
- اگر $\varepsilon$ واژهٔ تهی باشد، آنگاه:
- برای هر واژهٔ ناتهی $w = \sigma_1 \cdots \sigma_n$ (که در آن $\sigma_1, \ldots, \sigma_n$ عناصر یک الفبای مشخص هستند)، داریم:
- بنابراین، برای یک زبان صوری $L$:
همریختی رشتهای (String homomorphism)
اینگونه عملگرهای رشتهای برای بررسی ویژگیهای بستاری (closure properties) ردههای مختلف زبانها به کار میروند. یک ردهٔ زبانی نسبت به یک عملگر خاص بسته است، اگر اعمال آن عملگر بر زبانهای موجود در آن رده، همواره زبانی از همان رده تولید کند.
برای مثال، زبانهای مستقل از متن (context-free languages) نسبت به اجتماع، الحاق و اشتراک با زبانهای منظم بسته هستند؛ اما نسبت به اشتراک یا متمم بهطور کلی بسته نیستند.
نظریهٔ تریوها (trios) و خانوادههای انتزاعی زبانها (abstract families of languages) به مطالعهٔ عمومیترین ویژگیهای بستاری خانوادههای زبانها میپردازند.
ویژگیهای بستاری خانوادههای زبانها
در جدول زیر، $L_1$ Op $L_2$ نشاندهندهٔ اعمال یک عملگر بر دو زبان $L_1$ و $L_2$ است، که هر دو متعلق به خانوادهٔ زبانی مشخصشده در ستون مربوطه هستند.
| عملگر | تعریف | منظم (Regular) | DCFL | مستقل از متن (CFL) | نمایهای (IND) | حساس به متن (CSL) | بازگشتی (Recursive) | شمارشپذیر بازگشتی (RE) |
|---|---|---|---|---|---|---|---|---|
| اجتماع | $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 \notin L_1}$ | بله | بله | خیر | خیر | بله | بله | خیر |
| الحاق | $L_1 \cdot L_2 = {wz \mid w \in L_1 \land z \in L_2}$ | بله | خیر | بله | بله | بله | بله | بله |
| ستارهٔ کلینی (Kleene star) | $ L_1^* = {\varepsilon} \cup {wz \mid w \in L_1 \land z \in L_1^*} $ | بله | خیر | بله | بله | بله | بله | بله |
| همریختی رشتهای $h$ | $h(L_1) = {h(w) \mid w \in L_1}$ | بله | خیر | بله | بله | خیر | خیر | بله |
| همریختی رشتهای بدون $\varepsilon$، یعنی $h$ | $h(L_1) = {h(w) \mid w \in L_1}$ | بله | خیر | بله | بله | بله | بله | بله |
| جانشینی $\varphi$ | $\varphi(L_1)=\bigcup_{\sigma_1\cdots\sigma_n\in L_1}\varphi(\sigma_1)\cdot…\cdot\varphi(\sigma_n)$ | بله | خیر | بله | بله | بله | خیر | بله |
| همریختی معکوس $h^{-1}$ | $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}$ | بله | بله | بله | بله | بله | بله | بله |
کاربردها
زبانهای برنامهنویسی
یک کامپایلر (compiler) معمولاً دارای دو مؤلفهٔ متمایز است. یک تحلیلگر واژگانی (lexical analyzer) که گاهی با استفاده از ابزاری مانند lex تولید میشود، توکنهای دستور زبان زبان برنامهنویسی را شناسایی میکند؛ برای مثال:
- شناسهها (identifiers)
- کلیدواژهها (keywords)
- مقادیر عددی و رشتهای (numeric and string literals)
- علائم نقطهگذاری و نمادهای عملگرها
که خود این عناصر نیز بهوسیلهٔ یک زبان صوری سادهتر، معمولاً از طریق عبارتهای منظم (regular expressions)، مشخص میشوند.
در ابتداییترین سطح مفهومی، یک تجزیهگر (parser) ــ که گاهی با استفاده از مولدی مانند yacc تولید میشود ــ تلاش میکند مشخص کند که آیا برنامهٔ مبدأ از نظر نحوی معتبر است یا نه؛ یعنی آیا با توجه به دستور زبان زبان برنامهنویسیای که کامپایلر برای آن ساخته شده است، خوشساخت (well-formed) هست یا خیر.
البته کامپایلرها صرفاً کد مبدأ را تجزیه نمیکنند؛ بلکه معمولاً آن را به قالبی اجرایی ترجمه میکنند. به همین دلیل، یک تجزیهگر معمولاً بیش از یک پاسخ بله/خیر تولید میکند و اغلب یک درخت نحو انتزاعی (abstract syntax tree) ایجاد میکند.
این درخت در مراحل بعدی کامپایلر مورد استفاده قرار میگیرد تا در نهایت یک فایل اجرایی (executable) شامل کد ماشین (machine code) که مستقیماً روی سختافزار اجرا میشود، یا نوعی کد میانی (intermediate code) که برای اجرا به یک ماشین مجازی (virtual machine) نیاز دارد، تولید شود.
نظریهها، نظامها و برهانهای صوری
در منطق ریاضی، یک نظریهٔ صوری (formal theory) مجموعهای از جملات (sentences) است که در یک زبان صوری بیان شدهاند.
یک نظام صوری (formal system) (که حساب منطقی (logical calculus) یا نظام منطقی (logical system) نیز نامیده میشود) از یک زبان صوری به همراه یک دستگاه استنتاجی (deductive apparatus) (که نظام استنتاجی (deductive system) نیز نامیده میشود) تشکیل شده است.
دستگاه استنتاجی ممکن است شامل مجموعهای از قواعد تبدیل (transformation rules) باشد که میتوان آنها را بهعنوان قواعد معتبر استنتاج تفسیر کرد، یا شامل مجموعهای از اصول موضوعه (axioms) باشد، یا هر دو را دربرگیرد.
یک نظام صوری برای استخراج (derive) یک عبارت از یک یا چند عبارت دیگر به کار میرود.
اگرچه یک زبان صوری را میتوان با مجموعهٔ فرمولهای آن شناسایی کرد، یک نظام صوری را نمیتوان به همین شکل با قضایای آن یکی دانست. برای مثال، دو نظام صوری $\mathcal{FS}$ و $\mathcal{FS’}$ ممکن است تمام قضایای یکسانی داشته باشند، اما از نظر مهمی در جنبههای نظریهٔ برهان (proof theory) با یکدیگر تفاوت داشته باشند؛ برای نمونه، ممکن است فرمول $A$ در یک نظام پیامد نحوی (syntactic consequence) فرمول $B$ باشد، اما در نظام دیگر چنین نباشد.
یک برهان صوری (formal proof) یا اشتقاق (derivation)، یک دنبالهٔ متناهی از فرمولهای خوشساخت است (که ممکن است بهعنوان جملهها یا گزارهها تفسیر شوند) که هر یک از آنها یا یک اصل موضوعه است یا از فرمولهای پیشین در این دنباله، بهوسیلهٔ یک قاعدهٔ استنتاج (rule of inference) نتیجه میشود.
آخرین جمله در این دنباله، یک قضیه (theorem) از نظام صوری است. برهانهای صوری اهمیت دارند، زیرا قضایای آنها میتوانند بهعنوان گزارههای صادق تفسیر شوند.
تفسیرها و مدلها
زبانهای صوری از نظر ماهیت کاملاً نحوی (syntactic) هستند، اما میتوان برای آنها معناشناسی (semantics) تعریف کرد که به عناصر زبان معنا میبخشد.
برای مثال، در منطق ریاضی، مجموعهٔ فرمولهای ممکن یک منطق خاص، یک زبان صوری است و یک تفسیر (interpretation) به هر یک از فرمولها معنا اختصاص میدهد؛ معمولاً این معنا به شکل یک ارزش صدق (truth value) است.
مطالعهٔ تفسیرهای زبانهای صوری، معناشناسی صوری (formal semantics) نامیده میشود. در منطق ریاضی، این کار اغلب در قالب نظریهٔ مدل (model theory) انجام میشود.
در نظریهٔ مدل، اصطلاحاتی که در یک فرمول ظاهر میشوند، بهعنوان اشیایی درون ساختارهای ریاضی (mathematical structures) تفسیر میشوند و قواعد ثابتِ تفسیر ترکیبی تعیین میکنند که چگونه ارزش صدق یک فرمول از تفسیر اصطلاحات آن به دست آید.
یک مدل (model) برای یک فرمول، تفسیری از اصطلاحات است که در آن فرمول صادق میشود.