En informatique théorique, et notamment en théorie des langages formels, une grammaire algébrique est en forme normale de Greibach (en anglais, Greibach normal form ou GNF) si les membres droits de ses règles commencent tous par un symbole terminal, suivi éventuellement d'une ou plusieurs variables. Une variante permet une règle additionnelle pour engendrer le mot vide s'il fait partie du langage. Cette forme normale porte le nom de Sheila Greibach qui l'a introduite et a prouvé son existence. D'autres formes normales de grammaire existent, comme la forme normale de Chomsky, ou les grammaires sans récursivité gauche. La forme normale de Greibach est la plus élaborée de ces formes normales, et elle a été raffinée par la suite. Une grammaire algébrique est en forme normale de Greibach si toutes ses règles sont de la forme : ou où est une variable, est une lettre, et est une suite éventuellement vide de variables ; est l'axiome et ε est le mot vide. Une grammaire en forme normale de Greibach est notamment sans récursivité gauche. La propriété principale est que toute grammaire algébrique peut être transformée en une grammaire équivalent en forme normale de Greibach, théorème établi en 1965 par Sheila Greibach. Il existe plusieurs constructions. Lorsqu'il n'y a pas de epsilon-règle , l'algorithme est plus simple ; il existe des transformations complexité en temps dans le cas général et en temps si la grammaire n'a pas de règle unité (de la forme pour une variable ). En forme normale de Greibach, une dérivation engendre, à chaque pas de dérivation, une lettre d'un mot du langage donnée : la longueur de la dérivation est donc égale à la longueur du mot. La forme normale peut être utilisée, de manière équivalente, pour construire une automate à pile qui accepte les mots du langage en temps réel, c'est-à-dire qui lit une lettre du mot d'entrée à chaque pas de calcul. La construction d'une grammaire en forme normale de Greibach à partir d'une grammaire algébrique donnée par partie des sujets traités dans de nombreux manuels d'informatique théorique sur les langages formels, les automates et leur complexité.