Gramática formal
Ua gramática formal (alguas bezes simplesmente chamada de gramática) ye un oubjeto matemático que permite specificar ua lenguaige ó léngua, ó seia, ye un cunjunto de regras de formaçon de cadeias nua lenguaige formal. Las regras çcriben cumo formar las cadeias de l alfabeto de la lenguaige que son bálidos d'acuordo cula sintaxe de la lenguaige. Ua gramática nun çcribe ls seneficados de las cadeias ó l que puode ser feito culhas an qualquiera cuntesto.

La spresson "gramática formal" por tener ls sentidos:
 gramática dun lenguaige formal;
 çcriçon formal de parte de la gramática dua lenguaige natural.

Teorie de la lenguaige formal, la deciplina que studa gramáticas i lenguaiges formales, ye un galho de matemática aplicada. Sues aplicaçones puoden ser ancontradas na ciéncia de la cumputaçon teórica, lenguísticas teóricas, semánticas formales, matemática lógica, antre outras árias.

Análeze sintática ye l porcesso de recoincer ua eilocuçon (cadeia an lenguaige natural) quebrando-la nun cunjunto de simblos i analisando cada un cula gramática de la lenguaige. La maiorie de las lenguaiges ténen ls seneficados de sues eilocuçones struturados d'acuordo cula sintaxe — ua prática coincida cumo semántica cumposicional. Cumo resultado, l purmeiro passo para çcrebir l seneficado dua eilocuçon an ema lenguaige ye quebrá-la parte por parte, i mirar la sue forma analisada (coincida cumo arble d'análeze an ciéncia de la cumputaçon, i cumo strutura perfunda an gramática geratiba).

Eisemplo antrodutório
Ua gramática cunsiste percipalmente dun cunjunto de regras para cadeias de trasformaçon. (Se el solo cunsiste dessas regras, el serie un sistema semi-Thue). Para gerar ua cadeia na lenguaige, ampeça-se cun ua cadeia que cunsiste an solo un simblo simblo enicial. Las regras de porduçon son, anton, aplicadas an qualquiera orde, até qu'ua cadeia que nun cuntenie nin l simblo enicial, nin ls zeignados simblos nó-treminales, seia porduzida. La lenguaige formada pula gramática cunsiste de todas las cadeias çtintas que puoden ser geradas dessa forma. Qualquiera sequéncia particular de regras de porduçon subre l simblo enicial porduç ua cadeia çtinta na léngua. Se eisisten bárias maneiras de gerar la mesma sequéncia única, la gramática ye chamada de ambígua.
Por eisemplo, assumimos que l'alfabeto cunsiste dun la i un b, l simblo enicial ye S, i tenemos las seguintes regras de porduçon:
 1. 
 2. 
anton ampeçamos cun S, i podemos scolher ua regra pra aplicar a el. Se nós scolhéssemos la regra 1, oubteríamos la cadeia aSb. Se nós scolhermos la regra 1 outra beç, nuolo sustituímos S por aSb, i oubtemos la cadeia aaSbb. Se agora nós scolhermos la regra 2, nós sustituímos S por ba i oubtemos la cadeia aababb, i treminamos. Nós podemos screbir essa série de scolhas mais sucintamente, usando simblos: . La lenguaige de la gramática ye anton l cunjunto anfenito , an que lak ye la repetido k bezes (i m, an particular, repersenta l númaro de bezes que la regra de porduçon 1 fui aplicada).

Defeniçon formal

La sintaxe de las gramáticas
Na formalizaçon clássica de las gramáticas geratriç fui purmeiro proposto por Noan Chomsky por buolta de 1956, ua gramática G cunsiste de ls seguintes cumponentes:
 un cunjunto fenito N de simblos nun treminales, an que nanhun aparece an cadeias formadas a partir de G;
 un cunjunto fenito  de simblos treminales que ye çjunto de N;
 un cunjunto fenito P de regras de porduçon, cun cada regra de la forma
  
an que  ye l'ouperador streilha de Klene i  denota ounion de cunjuntos. Ó seia, cada regra de porduçon mapeia dua cadeia de simblos para outro, an que la purmeira cadeia (la "cabeça" ó "heiad") cuntén un númaro arbitrairo de simblos fornecidos, an que pul menos un deilhes ye un nó-treminal. Ne l causo de la segunda cadeia (l "cuorpo" ó "body") cunsistir solo de la cadeia bazie – i.i., qu'eilha nun cuntenha simblos – eilha puode ser denotada por ua notaçon special (frequentemente , i ó ) cul antuito d'eibitar cunfuson;
 un simblo çtinto  que ye l simblo enicial.

Eilhas son muitas bezes chamadas de sistemas de cadeias reescritos ó de gramática de strutura de frases na literatura.

La semántica de las gramáticas
L'ouparaçon dua gramática puode ser defenida an tenermos de relaçones an cadeias:
 dada ua gramática , la relaçon binária  (pronunciada cumo  "G deriba nun passo") nas cadeias an  ye defenida por:

 la relaçao  (pronunciada cumo G deriba an zero ó mais passos in zero or more steps) ye defenida cumo l feixo reflexibo trasitibo de 
 ua formula sentencial ye un nembro de  que puode ser deribado nun númaro fenito de passos a partir de l simblo enicial ; ó seia, ua formula sentencial ye un nembro de . Ua formula sentencial que nun cuntén nanhun de ls simblos nó treminales (i.i. ye un nembro de ) ye chamada de sentença.
 la lenguaige de , denotada cumo , ye defenida cumo todas las sentenças que puoden ser deribadas nun númaro fenito de passos a partir de l simblo enicial ; esto ye, l cunjunto .

Note que la gramática  ye efetibamente un sistema semi-Thue , rescrebendo cadeias satamente de l mesmo modo; la única defrença ye que çtinguimos simblos nó-treminales specíficos que percisan ser rescritos an regras, i son ls únicos qu'antressan an rescritas a partir de l simblo enicial  para cadeias sin simblos nó-treminales.

Eisemplo 
Para esses eisemplos, lenguaiges formales son specificadas usando notaçon de custruçon de cunjuntos.

Cunsidre la gramática  an que , ,  ye l simblo enicial, i  cunsiste de las seguintes regras porduçon:

 1. 
 2. 
 3. 
 4. 

Essa gramática define la lenguaige  an que  denota la cadeia de m cunsecutibos 's. Inda assi, la lenguaige ye l cunjunto de cadeias que cunsisten de 1 ó mais 's, seguidos pul mesmo númaro de 's, seguidos pul mesmo númaro de 's.

Alguns eisemplos de deribaçon de cadeias an  son: 

 
 
 

(Note la notaçon:  lé-se "cadeia P gera cadeia Q por meio de la porduçon i", i la parte gerada ye cada beç andicada an negrito)

Gramáticas analíticas
Bisto qu'eisisten ua basto belume de algoritmos de análeze sintática, la maiorie desses algoritmos assumen que la lenguaige a ser analisada ye einicialmente çcrita an meios dua gramática formal geratiba, i l'oubjetibo ye trasformar essa gramática geratiba nun berificador que funcione. Falando mais stritamente, ua gramática geratiba, de modo algun, corresponde al algoritmo ousado para analisar la lenguaige, i bários algoritmos ténen defrentes restriçones na forma an que las regras de porduçon son cunsidradas bien formadas.

Ua abordaige altarnatiba ye formalizar la lenguaige an tenermos dua gramática analítica an purmeiro lugar, que corresponde mais specificamente a l'estrutura i semántica dun berificador para ua lenguaige. Eisemplos de formalismos de gramáticas analíticas ancluen ls seguintes:
 la Lenguaige de Máquina amplementa diretamente gramáticas analíticas eirrestritas; sustituiçones de regras son ousadas para trasformar ua antrada para porduzir salidas i cumportamientos; l sistema puode porduzir tamien   l diagrama de Ein que mostra l qu'acuntece quando las regras dua gramática analítica eirrestrita stan sendo aplicadas;
 Lenguaige d'análeze Top-Down (LATD): un formalismo de gramática analítica altamente menimalista zambolbido recentemente ne ls anhos 70 para studar l cumportamiento de ls berificadores top-down;
 Gramática Eilo: ua forma de gramática analítica zambolbida pa las lenguísticas, que deriban la strutura sintática eisaminando ls relacionamientos posicionales antre dous pares de palabras;
 Gramáticas d'análeze de spressones (GAEs): son ua generalizaçon mais recente de las LATD zambolbidas an buolta de la prática de la spressebidade percisando de las lenguaiges de porgramaçon i scritores de cumpiladors.

Ber tamien 
 Arble sintática abstrata
 Gramática ambígua
 Formalismo de Backus-Naur
 Arble sintática cuncreta
 Framework de gramática
 Lojban
 Fórmula bien-formada
 Hierarquia de Chomsky

Ligaçones sternas 
 Yearly Formal Grammar cunference

Teorie de la cumputaçon