索引式語法是無語境語法的一種泛化，它的非端點都配有標志列表，或索引符號。由索引式語法產生的語言被稱為索引式語言。Hopcroft和Ullman的現代定義在Hopcroft和Ullman（1979）之后的當代出版物中。索引語法的正式定義是一個5元組G=?N,T,F,P,S?其中N是一組變量或非終端符號，T是一組終端符號（字母表），F是一組所謂的索引符號，或索引，S∈N是起始符號，P是一個有限的生成集。在生成和索引語法的推導中，每一個非終端符號A∈N都有一串（棧）σ∈F*的索引符號，用A[σ]表示。終端符號后面不能有索引堆棧。對于索引棧σ∈F*和非終端和終端符號的字符串α∈（N∪T）*，α[σ]表示將[σ]附加到α中每個非終端的結果。例如，如果α等于aBCdE，a,d∈T終端，B,C,E∈N個非終端符號，那么α[σ]表示aB[σ]C[σ]dE[σ]。使用這個符號，P中的每個生產都必須是這樣的形式A[σ]→α[σ]，A[σ]→B[fσ]，或者A[fσ]→α[σ]，其中A、B∈N是非終端符號，f∈F是索引，σ∈F*是一串索引符號，而α∈（N∪T）*是一串非終端和終端符號。有些作者在生產規則中用......代替σ來表示索引棧；那么類型1、2、3的規則分別為A[...]→α[...]，A[...]→B[f...]，以及A[f...]→α[...]。除了附加在每個非終端符號上的索引棧之外，派生與無語境語法中的派生相似。當應用像A[σ]→B[σ]C[σ]這樣的生產時，A的索引棧被復制到B和C。此外，一個規則可以將索引符號推到棧上，或彈出其最上面（即最左邊）的索引符號。形式上，關系?（直接派生）在句法形式的集合（N[F*]∪T）*上定義如下。如果A[σ]→α[σ]是類型1的生產，那么βA[φ]γ?βα[φ]γ，使用上述定義。如果A[σ]→B[fσ]是一個類型2的生產，那么βA[φ]γ?βB[fφ]γ。也就是說，右邊的索引棧是通過將f推到左邊的棧φ上而得到的。如果A[fσ]→α[σ]是一個類型3的生產，那么βA[fφ]γ?βα[φ]γ，再次使用α[σ]的定義。也就是說，xxx個索引f從左手邊的堆棧中彈出，然后分配給右手邊的每個非終端。像往常一樣，派生關系??被定義為直接派生?的反身轉義閉合。語言L（G）={w∈T*:S??w}是可從起始符號派生的所有終端符號串的集合。

歷史上，索引語法的概念是由AlfredAho（1968）用不同的形式主義首次提出的。Aho將索引語法定義為一個5元組（N,T,F,P,S），其中N是變量或非終端符號的有限字母表T是終端符號的有限字母表F?2N×(N∪T)*是所謂旗子的有限集合（每個旗子本身是所謂索引生產的集合）P?N×(NF*∪T)*是生產的有限集合S∈N是起始符號直接衍生如下。一個來自P的生產p=(A→X1η1...Xkηk)與一個非術語A∈N及其（可能是空的）標志串ζ∈F*匹配。在上下文中，γAζδ，通過p，派生為γX1θ1...Xkθkδ，其中θi=ηiζ，如果Xi是一個非終端，否則就是空字。

因此，A的舊標志被復制到由p產生的每個新的非終端。每個這樣的生產都可以由霍普克羅夫特/烏爾曼形式主義中的適當的1和2型生產來模擬。一個索引生產p=(A→X1...Xk)∈f匹配Afζ（它來自的標志f必須匹配非終端A后面的xxx個符號），并將剩余的索引字符串ζ復制到每個新的非終端：γAfζδ派生到γX1θ1...Xkθkδ，其中當Xi是終端時，θi是空字，當它是非終端時ζ。每個這樣的生產都對應于Hopcroft/Ullman形式主義中的第3類生產。