שפה פורמלית

במתמטיקה, לוגיקה ומדעי המחשב, שפה פורמלית היא קבוצה כלשהי של רצפים סופיים של סימנים (או אותיות) מקבוצה סופית .
קבוצת הסימנים  מכונה "האלפבית של השפה". את הרצפים של השפה נהוג לכנות "מילים".

מושגים יסודיים בשפות פורמליות

א. אלפבית (פורמלי): קבוצה של סימנים, או אותיות, שמהם מייצרים את המילים בשפה. קבוצה זו היא סופית. 
ב. מילה (פורמלית): רצף סופי של אותיות מהאלפבית (ובאופן פורמלי - סדרת אותיות סופית מהאלפבית). מקובל לומר שמילה המכילה רק אותיות מאלפבית מסוים היא מעל האלפבית המסוים. 
ג. המילה הריקה: רצף אותיות באורך 0. למילה הריקה, המסומנת בדרך-כלל באות , יש מעמד זהה לכל מילה אחרת מעל האלפבית, והיא יכולה להיות שייכת או לא שייכת לשפה. 
ד. שפה (פורמלית): קבוצה של מילים. למרות שהאלפבית הוא סופי ואורך כל מילה הוא סופי, השפה יכולה להיות אינסופית; זאת משום שמספר המילים בשפה אינו חסום. 
כאשר מייצגים שפה טבעית על ידי שפה פורמלית, נוהגים לעיתים לראות במילים של השפה הטבעית אותיות של השפה הפורמלית, כך שהאלפבית הפורמלי מכונה "לקסיקון" או "אוצר מילים". בהתאם לייצוג זה, המילים הפורמליות הן משפטים של השפה הטבעית, דבר שעלול לגרום לבלבול.

תת-קבוצה של שפה פורמלית

קיימות דרכים שונות לאפיין שפה פורמלית עבור אלפבית  מסוים, כלומר דרכים להגדיר אילו רצפים של אותיות מהאלפבית שייכים לשפה ואילו הן שגיאות כתיב בשפה הפורמלית. 
הדרך הישירה להגדיר שפה פורמלית היא באמצעות "מילון", רשימה מפורשת של רצפי אותיות, אשר הן (ורק הן) יהוו את המילים השייכות לשפה. למשל, את השפה הפורמלית "המילים התקניות של השפה העברית" מעל האלפבית העברי, אין ברירה אלא לאפיין בדרך זו (כל זאת מנקודת מבט פורמלית. מבחינה בלשנית, המילים בשפה טבעית אינן מאופיינת באמצעות מילון). בדרך כלל שיטה זו אינה טובה, ואף אינה אפשרית (כך למשל, בכל מקרה בה השפה מכילה מספר אינסופי של מילים).
דרך נוספת לאפיין שפה פורמלית, היא באמצעות דקדוק פורמלי. כאשר נתונות כמה שפות אשר כולן מוגדרות מעל אותו האלפבית (ואותן אנו יודעים לאפיין, למשל בעזרת מילון), הדקדוק הפורמלי מאפשר לאפיין באמצעותן שפה חדשה, אף היא מעל אותו אלפבית. כך למשל ניתן להגדיר (באופן עקרוני ומקורב, לפחות) "דקדוק פורמלי" של השפה העברית, שיאפשר להרכיב את כל המשפטים בשפה העברית (אשר מספרם אינסופי) באמצעות "שפת השורשים בעברית" (קבוצה סופית ובת-אפיון באמצעות מילון). 
דרך דומה לאפיון שפה פורמלית, המקובלת מאוד במתמטיקה, היא באמצעות מבני-יצירה. בדרך זו נעזרים בתת-קבוצה של מילות השפה אותה רוצים לאפיין (תת-קבוצה סופית, בדרך כלל), ומגדירים אוסף של יחסים על תת-קבוצה הזו, אשר באמצעותו ניתן לאפיין את כל המילים בשפה. דרך זו מקובלת בלוגיקה המתמטית, בשל האפשרות לאפיין את השפה באמצעות אלגברת יצירה חופשית, המאפשרת להגדיר היטב פונקציות ברקורסיה על הפעולות של מבנה-היצירה, ולהוכיח טענות הנוגעות למילים ברקורסיה על עץ הבנייה שלהם. דוגמאות רלוונטיות אפשר למצוא, למשל, בערכים תחשיב הפסוקים ו-תחשיב היחסים.

כריעות וכריעות למחצה

שפה אשר ניתן לאפיינה באופן "מועיל" מכונה "שפה כריעה". כלומר, על שפה A נאמר שהיא "כריעה" אם ורק אם קיים אלגוריתם המקבל כל צירוף סופי של סימנים מעל האלפבית של השפה, ועוצר כעבור מספר סופי של צעדים עבור כל מילה השייכת ל-A בהכרזה "המילה שייכת ל-A", ועבור כל מילה שאינה שייכת ל-A בהכרזה "המילה אינה שייכת ל-A".
על שפה A נאמר שהיא "כריעה למחצה", אם ורק אם קיים אלגוריתם, שעוצר עבור מספר סופי של צעדים בהכרזה "המילה שייכת ל-A", אם המילה שייכת ל-A (אך עבור מילת קלט שאינה שייכת ל-A, ייתכן שלא יעצור כלל).
כל שפה שהיא כריעה, היא גם כריעה למחצה. 
עבור משפחת שפות תחשיב היחסים, משפט צ'רץ' קובע ששפה מסדר ראשון המכילה, בנוסף לקבוע השוויון, קבוע יחס או קבוע פעולה בעל שני מקומות לפחות, אז קבוצת הנוסחאות של השפה שהן אמיתיות לוגיות, אינה כריעה.