Our definition of a language as a propositional function captures the intuition that to know a language is to know the criteria for saying when a sentence is in it. To say is in the language is to know how to prove . This agrees with Hopcroft and Ullman; they are concerned with certain special ways of knowing .
One especially simple kind of representation of arises when the proposition is decidable, that is when there is a function : list such that
Such a language is called decidable or recursive.
Another way to represent a language with a function is to provide an enumeration of , that is a function such that
The function can also be said to represent .
Given the function an interesting procedure arises for
specifying a language, the procedure is called a (real) recognizer. To specify , we write a function
Hopcroft and Ullman go on to show that given a real recognizer, we can also define an enumerator. Basically we enumerate . We do this uniformly only if the type is non-empty. Then given , there is an operation which produces a function from onto . Since we are interested mainly in automata and the Myhill-Nerode theorem of Chapter 3, we skip over Chapter 2 on Grammars although it would not be difficult to formalize all of the results there. (The only interesting result is Theorem 2.2-a context sensitive grammar is recursive.)